Keywords and Reserved Words

Core Keywords

action - Defines an action (model checker entry point)
func - Defines a function
role - Defines a role (class-like structure)
symmetric - Modifier for roles or values (enables symmetry reduction)
assertion - Defines a property to check

Flow Modifiers

atomic - Execute without yielding
serial - Execute with yields between statements (default)
parallel - Execute statements concurrently
oneof - Choose one of multiple branches

Fairness Modifiers

fair - Weak fairness (same as fair<weak>)
fair<weak> - Eventually executes if continuously enabled
fair<strong> - Eventually executes if infinitely often enabled

Assertion Modifiers

always - Safety property (holds in all states)
exists - Existential property (holds in at least one state)
eventually always - Liveness property (eventually reaches stable state)
always eventually - Progress property (always makes progress)
transition - Property about state transitions

Control Flow

if, elif, else - Conditional branching
for - Iteration over collections
while - Conditional iteration
break - Exit loop early
continue - Skip to next iteration
return - Return from function/action
pass - No-op (explicitly enables action)
require - Guard clause (disables action if false)
oneof - Nondeterministic choice (preferred; any is deprecated alias)
`checkpoint` - Visualization breakpoint (backtick syntax)

State and Scope

self - Reference to role instance (implicit in role methods)
global - NOT a keyword (state variables are automatically global)
@state - Decorator for role state (durable/ephemeral)

Built-in Types

enum - Enumeration definition
record - Mutable named structure
struct - Immutable named structure (Starlark)
set, dict, list - Standard collections
genericset, genericmap - Collections for non-hashable types
bag - Multiset (collection with duplicates)
symmetric_values - Creates interchangeable values for symmetry reduction