If x and y are actions then (x-> P | y-> Q) describes a process which initially engages in either of the actions x or y. After the first action has occurred, the subsequent behavior is described by P if the first action was x and Q if the first action was y.
DRINKS = (red->coffee->DRINKS |blue->tea->DRINKS).
COIN = (toss->HEADS|toss->TAILS), HEADS= (heads->COIN), TAILS= (tails->COIN).
Indexed Processes and Actions
Imagine you need to define the same set of actions with several processes. For instance, you want to define a clique graph.
CLIQUE = NODE, NODE[i:0..10] = (move[j:0..10] -> NODE[j]).
In the above example we use index i for NODE and index j for move.
Const and Range
Same example using constant named N and ranges.
const N = 10 range I = 0..N range J = 0..N CLIQUE = NODE, NODE[I] = (move[j:J] -> NODE[j]).
You may also use math expressions ( + * / - ), for example:
const N = 5 range T = 0..N-1 range R = 0..2*N SUM = (in[a:T][b:T]->TOTAL[a+b]), TOTAL[s:R] = (out[s]->SUM).
And you can also use math expressions
The choice (when B x -> P | y -> Q) means that when the guard B is true then the actions x and y are both eligible to be chosen, otherwise if B is false then the action x cannot be chosen.
COUNTDOWN (N=3) = (start->COUNTDOWN[N]), COUNTDOWN[i:0..N] = (when(i>0) tick->COUNTDOWN[i-1] |when(i==0)beep->STOP |stop->STOP ).
const False = 0 const True = 1 range Reserved = False..True range Seats = 1..5 TERMINAL = (choose[r:Reserved] -> if (!r) then (seat[s:Seats].reserve -> TERMINAL) else TERMINAL).
Back to End User