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

Temporal Formula Keywords

Used in the return of an assertion with no prefix (see Temporal Formulas):

always, eventually - Prefix temporal operators
until, unless - Strong and weak until
leadsto - P leadsto Q is always (P implies eventually Q)
implies - Logical implication
possibly - Some path reaches a state (exists eventually is another spelling)

until, unless, leadsto, implies and possibly are keywords only in an assertion’s return, so they can still be used as names elsewhere.

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