Clone wiki

mtsa / enduser / fsp_keywords


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).

Non Deterministic

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.

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

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

Guarded Actions

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]

Conditional guard

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)

Back to End User