variables
State variables for this specification.
Nested DSLs
variables.variable
variable name, default \\ nil
Declare a state variable.
Arguments
| Name | Type | Default | Docs |
|---|
name | atom | | Variable name. |
default | any | | Initial value of the variable. |
Options
| Name | Type | Default | Docs |
|---|
type | atom | | Variable type (for documentation; not enforced by TLA+). |
constants
Model constants (bound at model-checking time).
Nested DSLs
constants.constant
constant name
Declare a model constant.
Arguments
| Name | Type | Default | Docs |
|---|
name | atom | | Constant name (bound at model-checking time). |
actions
Guarded state transitions.
Nested DSLs
actions.action
action name
Define a guarded state transition.
Nested DSLs
Arguments
| Name | Type | Default | Docs |
|---|
name | atom | | Action name. |
Options
| Name | Type | Default | Docs |
|---|
guard | any | | A quoted boolean expression that must be true for this action to fire. |
await | any | | Alias for guard. A quoted boolean expression that must be true for this action to fire. |
fairness | :weak | :strong | | Fairness constraint: :weak (WF) or :strong (SF). |
actions.action.next
next variable, expr
Set the next-state value of a variable.
Arguments
| Name | Type | Default | Docs |
|---|
variable | atom | | The variable to update in the next state. |
expr | any | | A quoted expression for the next-state value. |
actions.action.branch
branch name
A non-deterministic branch within an action (either/or).
Nested DSLs
Arguments
| Name | Type | Default | Docs |
|---|
name | atom | | Branch name (for documentation). |
Options
| Name | Type | Default | Docs |
|---|
guard | any | | A quoted boolean expression that must be true for this branch. |
actions.action.branch.next
next variable, expr
Set the next-state value of a variable.
Arguments
| Name | Type | Default | Docs |
|---|
variable | atom | | The variable to update in the next state. |
expr | any | | A quoted expression for the next-state value. |
invariants
Safety invariants checked at every reachable state.
Nested DSLs
invariants.invariant
invariant name, expr
Declare a safety invariant.
Arguments
| Name | Type | Default | Docs |
|---|
name | atom | | Invariant name. |
expr | any | | A quoted boolean expression that must hold in every reachable state. |
processes
Concurrent process declarations.
Nested DSLs
processes.process
process name
Declare a concurrent process (PlusCal process (Name \in Set)).
Nested DSLs
Arguments
| Name | Type | Default | Docs |
|---|
name | atom | | Process name. |
Options
| Name | Type | Default | Docs |
|---|
set | any | | The set of process identifiers (e.g., a constant name or literal set). |
fairness | :weak | :strong | | Default fairness for all actions in this process: :weak (WF) or :strong (SF). |
processes.process.action
action name
Define a guarded state transition.
Nested DSLs
Arguments
| Name | Type | Default | Docs |
|---|
name | atom | | Action name. |
Options
| Name | Type | Default | Docs |
|---|
guard | any | | A quoted boolean expression that must be true for this action to fire. |
await | any | | Alias for guard. A quoted boolean expression that must be true for this action to fire. |
fairness | :weak | :strong | | Fairness constraint: :weak (WF) or :strong (SF). |
processes.process.action.next
next variable, expr
Set the next-state value of a variable.
Arguments
| Name | Type | Default | Docs |
|---|
variable | atom | | The variable to update in the next state. |
expr | any | | A quoted expression for the next-state value. |
processes.process.action.branch
branch name
A non-deterministic branch within an action (either/or).
Nested DSLs
Arguments
| Name | Type | Default | Docs |
|---|
name | atom | | Branch name (for documentation). |
Options
| Name | Type | Default | Docs |
|---|
guard | any | | A quoted boolean expression that must be true for this branch. |
processes.process.action.branch.next
next variable, expr
Set the next-state value of a variable.
Arguments
| Name | Type | Default | Docs |
|---|
variable | atom | | The variable to update in the next state. |
expr | any | | A quoted expression for the next-state value. |
processes.process.variable
variable name, default \\ nil
Declare a state variable.
Arguments
| Name | Type | Default | Docs |
|---|
name | atom | | Variable name. |
default | any | | Initial value of the variable. |
Options
| Name | Type | Default | Docs |
|---|
type | atom | | Variable type (for documentation; not enforced by TLA+). |
properties
Temporal properties checked over infinite traces.
Nested DSLs
properties.property
property name, expr
Declare a temporal property (liveness or safety over traces).
Arguments
| Name | Type | Default | Docs |
|---|
name | atom | | Property name. |
expr | any | | A temporal expression: always(P), eventually(P), leads_to(P, Q). |