Known Issues and Limitations
Line numbers in error messages: Line numbers may be incorrect in some error messages (known issue, to be fixed)
Assertions within roles: Assertions within role definitions are not yet fully supported. Use top-level assertions instead.
Interactive commands: Commands requiring interactive input (e.g., git rebase -i, git add -i) are not supported in model checking context
Python features not supported:
delstatementimportstatement — there is no user-level import; a curated set of modules is pre-imported globally. See Standard Library.is/is notoperators (use==/!=instead)- Tuple unpacking in
forloops (for k, v in dict.items()fails; usefor k in dict+dict[k])
Cross-role function return to self.*: self.x = otherRole.fn() crashes. Use a local variable: result = otherRole.fn() then self.x = result.
For a complete list of gotchas and workarounds, see Gotchas and Common Issues.
For role assertions: Define assertions at top level and reference role state:
role Server:
action Init:
self.value = 0
# ✅ Top-level assertion instead of role assertion
always assertion ServerValuePositive:
for s in servers:
if s.value < 0:
return False
return True
For complex expressions with fizz functions: Extract to variables first (see Function Call Syntax Limitations)
For generic collections in state: Use regular collections with hashable types, or restructure to keep generic collections in local scope