10.4.3.1 on

The on defines which trigger is to be handled:

on        ::= "on" trigger ("," trigger)* ":" statement
trigger   ::= event-name | "inevitable" | "optional"
statement ::= declarative-statement | imperative-statement | illegal
imperative-statement
          ::= action | assign | call | if | reply | return | variable
                | imperative-compound
                | empty-statement
illegal   ::= "illegal"
imperative-compound
          ::= "{" (imperative-statement ";")+ "}"
empty-statement
          ::= ";" | "{" "}"

For example:

on hello: {}
on inevitable: {world; idle = true;}

When two or more observably distinct imperative statements are specified for a certain trigger, the interface is said to behave non-deterministic with respect to the trigger. For example:

on hello: world;
on hello: cruel;

when the trigger hello is sent, the response can either be world or cruel but which one it will be cannot be predicted. Non-determinism in interfaces is allowed as long as it is observable non-determinism, i.e., after the trigger has returned the client should be able to know which state the interface is in. For example, this is not allowed:

on hello: {}
on hello: idle = true;

and will lead to a verification error (See Verification Checks and Errors).

• There must be exactly one imperative statement for every combination of guard and on,
• There can be only one on leading to an imperative statement.