Depending on the context, the following types of statements and expressions are valid:
abort skip with (skip; skip)
Execute the first statement, but permanently terminate this execution when the other statements execute.
delay 1
Postpone the execution with a number of time units (integer or real).
[true] skip
Block the statement whenever the guard does not evaluate to true. The evaluation of the condition and the execution of the statement together form a single execution step.
if true then skip else skip fi
Depending on whether the condition evaluates to true, execute the first or the second body statement. The evaluation of the condition and the execution of any of the body statements are two separate execution steps.
interrupt skip with (skip; skip)
Execute the first statement, but temporarily suspend this execution when the other statements execute (possibly multiple times).
par skip and skip rap
Execute multiple statements in parallel, in an interleaved way. Communication and synchronization within a process can only be performed through shared variables.
method()()
Invoke a process method with a series of input parameter values and a series of output variables. If the process method call is the last statement of a method, then there is no danger of stack overflow.
sel skip or skip les
Non-deterministic choice between multiple alternative statements. It is blocked when all alternatives are blocked. The choice is finally resolved by the first statement that executes. Fairness of the choice is not guaranteed.
skip
Execute without any observeable effect on variables or messages. If used in the context of a sel statement, a skip statement is never blocked, and can resolve the choice. This can be used to model an internal decision.
port?msg(var1, var2 | true)
Receive a message over a port, and assign the message parameters to variables. The (optional) condition restricts the accepted parameter values.
port!msg(expr1, expr2)
Send a message over a port, and add the expressions as message parameters.
while true do skip od
As long as the condition evaluates to true, execute the statement. The evaluation of the condition and the execution of the statement are two separate execution steps.
v := nil
currentTime
"foo" printString()
if true then nil else nil fi
Depending on whether the condition evaluates to true, return the first or the second body expression.
new(Object)
Create a new instance of a data class.
return nil
self
self^
while true do nil od
As long as the condition evaluates to true, evaluate the body expression. Finally return nil.