Configuration

---
# Global options
options:
  max_actions: 100              # Max total action executions
  max_concurrent_actions: 2     # Max actions running in parallel
  crash_on_yield: true          # Enable crash fault injection (default: true)

# Deadlock detection
deadlock_detection: true        # Enable deadlock checking (default: true)
                                # Set to false if deadlock is expected/acceptable

# Liveness checking
liveness: "false"               # Disable liveness checking
# liveness: "strict"            # Enable strict liveness checking
# liveness: true                # Enable liveness checking

# Custom seed for reproducibility
seed: 12345                     # Optional: for reproducing specific runs
---

# Fast exploration (no crashes)
---
options:
  crash_on_yield: false
  max_concurrent_actions: 1
---

# Thorough testing
---
options:
  crash_on_yield: true
  max_concurrent_actions: 3
liveness: "strict"
deadlock_detection: true
---

# Debugging specific scenario
---
options:
  max_actions: 50
seed: 12345
---

---
action_options:
  HighFrequency:
    max_actions: 50             # Limit this action

  CriticalPath:
    crash_on_yield: false       # No crashes for this

  BackgroundTask:
    max_concurrent_actions: 1   # Only one at a time
---

---
action_options:
  # Limit across ALL Server instances combined
  "Server.Process":
    max_actions: 10

  # Limit PER Server instance
  "Server#.Process":
    max_concurrent_actions: 1   # Each instance runs at most 1

  # Thread example: disable crashes, limit concurrency per thread
  "Thread.Run":
    crash_on_yield: false
  "Thread#.Run":
    max_concurrent_actions: 1   # Only 1 Run per Thread instance
---

role Worker:
    action Process:
        # Do work
        pass

action Init:
    workers = [Worker(), Worker(), Worker()]

# With "Worker.Process": max_actions: 5
# → Total of 5 Process actions across all 3 workers

# With "Worker#.Process": max_actions: 5
# → Each worker can execute Process 5 times (15 total possible)

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21

---
# Example 0054: YAML Frontmatter Configuration
# Configure model checker behavior
# Demonstrates: options with max_actions, deadlock_detection

options:
  max_actions: 20

deadlock_detection: false
---

# This spec intentionally hits max_actions limit
action Init:
    counter = 0

atomic action Increment:
    # No guard - runs forever (until max_actions)
    counter = counter + 1

# Demonstrates hitting the configured limit
# With max_actions: 20, this will stop at 20 instead of default 100

StateSpaceOptions: options:{max_actions:20 max_concurrent_actions:2} deadlock_detection:false
Nodes: 21, queued: 0
Valid Nodes: 21 Unique states: 21
IsLive: true
PASSED: Model checker completed successfully

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53

---
# Example 0082: Action-Level Configuration
# Per-action limits and crash settings
# Demonstrates: action_options, per-action max_actions, crash_on_yield

# Global options
options:
  max_actions: 100
  crash_on_yield: true

# Per-action overrides
action_options:
  HighFrequency:
    max_actions: 5  # Limit this action to 5 executions

  CriticalPath:
    crash_on_yield: false  # Disable crashes for this action

  BackgroundTask:
    max_concurrent_actions: 1  # Only one instance at a time
---

action Init:
    high_freq_count = 0
    critical_count = 0
    background_count = 0

# Limited to 5 executions by action_options
action HighFrequency:
    require high_freq_count < 10

    high_freq_count = high_freq_count + 1

# No crash injection (crash_on_yield: false)
action CriticalPath:
    require critical_count < 3

    # These steps run without crash injection
    critical_count = critical_count + 1
    # More work here...

# Only runs once at a time (max_concurrent_actions: 1)
action BackgroundTask:
    require background_count < 2

    background_count = background_count + 1

# Safety: high frequency action respects limit
always assertion HighFreqWithinLimit:
    return high_freq_count <= 5

atomic action NoOp:
    pass

StateSpaceOptions: options:{max_actions:100 max_concurrent_actions:2 crash_on_yield:true} action_options:{key:"BackgroundTask" value:{max_concurrent_actions:1}} action_options:{key:"CriticalPath" value:{crash_on_yield:false}} action_options:{key:"HighFrequency" value:{max_actions:5}}
Nodes: 72, queued: 0
Valid Nodes: 72 Unique states: 72
IsLive: true
PASSED: Model checker completed successfully

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54

# Example 0083: Action Coordination
# Using require mid-action with yield points for synchronization
# Demonstrates: require as wait mechanism, action coordination

---
deadlock_detection: false
options:
    crash_on_yield: false
---

action Init:
    stage = 0

# First action: does work in stages, waits for second action
action Step1:
    require stage == 0     # Only start when stage is 0
    stage = 1              # Set to stage 1, then yield

    # After yield, this require acts as a "wait"
    # Step1 continuation disabled until stage becomes 2
    require stage == 2     # Wait for Step2 to advance stage
    stage = 3              # Continue when condition met

# Second action: advances stage when ready
action Step2:
    require stage == 1     # Only enabled when Step1 sets stage to 1
    stage = 2              # Advance to stage 2, unblocking Step1

# Execution flow:
# 1. Step1 starts (stage == 0), sets stage = 1
# 2. Yield point after stage = 1
# 3. Step1 tries to continue, hits require stage == 2, fails
# 4. Step1 continuation disabled
# 5. Step2 becomes enabled (stage == 1), runs, sets stage = 2
# 6. Step1 can be rescheduled, require passes
# 7. Step1 continues, sets stage = 3

# This pattern is equivalent to:
# - Step1 "waits" for Step2
# - Handshake/synchronization between actions
# - Multi-phase coordination without busy-waiting

always assertion StageMonotonic:
    return stage >= 0 and stage <= 3

transition assertion StageIncrementsOneAtATime(before, after):
    # Stutter step allowed (no change)
    if after.stage == before.stage:
        return True
    # When stage changes, must increment by exactly 1
    return after.stage == before.stage + 1

exists assertion ReachesStage3:
    return stage == 3

StateSpaceOptions: options:{max_actions:100 max_concurrent_actions:2 crash_on_yield:false} deadlock_detection:false
Nodes: 4, queued: 0
Valid Nodes: 4 Unique states: 4
IsLive: true
PASSED: Model checker completed successfully

gdoc_arrow_left_alt Fault Injection Symmetry Reduction gdoc_arrow_right_alt