Locations are connected by edges. Edges are annotated with selections, guards, synchronisations and updates. Edges may also have branches of possible destinations with their own updates and probabilistic weights.
SelectList ::= ID ':' Type
| SelectList ',' ID ':' Type
For each ID in SelectList, bind ID non-deterministically to a value of type Type domain.
The identifiers are available as variables within the other labels of this edge (guard, synchronization, or update). The supported types are bounded integers and scalar sets.
Note: The identifiers will shadow any variables with the same name.
Select: i : int[0,3]
Synchronization: a[i]?
Update: receive_a(i)
This edge will non-deterministically bind i to an integer in the range 0 to 3, inclusive. The value i is then used both as an array index when deciding what channel to synchronize on, and as an argument in the subsequent call to the function receive_a.
Guards follow the abstract syntax of expressions. However, the type checker restricts the set of possible expressions allowed in guards: A guard must be a conjunction of simple conditions on clocks, differences between clocks, and boolean expressions not involving clocks. The bound must be given by an integer expression.
x >= 1 && x <= 2x is in the interval [1,2].x < yx is (strictly) less than y.(i[0]+1) != (i[1]*10)0 in an integer array i plus one is not equal to value at position 1 times 10 (i must be an integer array since we use arithmetic operations on its elements).Channels are used to synchronise processes. This is done by annotating edges in the model with synchronisation labels. Synchronisation labels are syntactically very simple. They are of the form e? or e!, where e is a side effect free expression evaluating to a channel.
The intuition is that two processes can synchronise on enabled edges annotated with complementary synchronisation labels, i.e. two edges in different processes can synchronise if the guards of both edges are satisfied, and they have synchronisation labels e1? and e2! respectively, where e1 and e2 evaluate to the same channel.
When two processes synchronise, both edges are fired at the same time, i.e. the current location of both processes is changed. The update expression on an edge synchronizing on e1! is executed before the update expression on an edge synchronizing on e2?. This is similar to the kind of synchronisation used in CCS or to rendezvous synchronisation in SPIN.
Urgent channels are similar to regular channels, except that it is not possible to delay in the source state if it is possible to trigger a synchronisation over an urgent channel. Notice that clock guards are not allowed on edges synchronising over urgent channels.
Broadcast channels allow 1-to-many synchronisations. The intuition is that an edge with synchronisation label e! emits a broadcast on the channel e and that any enabled edge with synchronisation label e? will synchronise with the emitting process. I.e. an edge with an emit-synchronisation on a broadcast channel can always fire (provided that the guard is satisfied), no matter if any receiving edges are enabled. But those receiving edges, which are enabled will synchronise. Notice that clock guards are not allowed on edges receiving on a broadcast channel. The update on the emitting edge is executed first. The update on the receiving edges are executed left-to-right in the order the processes are given in the system definition.
Notice that for both urgent and broadcast channels it is important to understand when an edge is enabled. An edge is enabled if the guard is satisfied. Depending on the invariants, the target state might be undefined. This does not change the fact that the edges are enabled! E.g. when two edges in two different processes synchronise via a broadcast channel, and the invariant of the target location of the receiving edge is violated, then this state is not defined. It is not the case that the emitting edge can be fired by itself since the receiving edge is enabled and thus must synchronise. Please see the section about the semantics for further details.
An update is a comma separated list of expressions. These expressions will typically have side effects. Assignments to clocks are limited to the regular = assignment operator and only integer expressions are allowed on the right hand side of such assignments. The syntax of updates is defined by the grammar for Update:
Update ::= [Expression (',' Expression)*]
Note: Assignments are evaluated sequentially (not concurrently). On synchronizing edges, the assignments on the !-side (the emitting side) are evaluated before the ?-side (the receiving side).
The regular assignment operator, =, can be used for assigning values to integer, boolean, record and clock variables. The other assignment operators are limitted to integer and boolean variables and work as in C, e.g. i += 2 is equivalent to i = i + 2 except that any side effect of evaluating i is only executed once in the first case whereas it is executed twice in the latter case.
Please remember that any integers are bounded. Any attempt to assign a value outside the declared range to an integer, will cause an error and the verification will be aborted.
x = 0x is reset.j = ( i[1]>i[2] ? i[1] : i[2] )j is assigned the maximum value of array elements i[1] and i[2]. This is equivalent to j = i[1] >? i[2], except that one of the sub-expressions is evaluated twice in the example (once in the condition, and again in either the true case or the false case).x = 1, y = 2 * xx is set to 1 and y to 2 (as assignments are interpreted sequentially).The weight over branch is a constant non-negative integer expressions denoting the probabilistic likely-hood of the branch being executed. The probability of a particular branch is determined as a ratio of its weight over the sum of weights of all branches emanating from the same branch node.
The weights are used in probabilistic and statistical model checking.
Select: i : int[0,3]
Update: gen_data(i)
Weight: w[i]