Files
bot-formal-models/tla/models/nodes_pipeline_negative_replay.cfg

26 lines
470 B
INI

SPECIFICATION Spec
INVARIANT Inv_SharedNodesRunSafe
CONSTANTS
Tools = {"nodes.run"}
NodesRunTool = "nodes.run"
RequestIds = {"r1","r2"}
SessionType = "shared"
PolicyAllowShared = {"nodes.run"}
PolicyAllowMain = {"nodes.run"}
NodeCommands = {"system.run"}
NodesRunCommand = "system.run"
PlatformDefaults = {"system.run"}
ExtraAllow = {}
Deny = {}
DeclaredByNode = {"system.run"}
ApprovalRequired = TRUE
MaxQueueLen = 1
MaxExecLen = 1