# Wiki

# mtsa / enduser / fsp_keywords

# Choice

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.

## Deterministic

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.

CLIQUE = NODE[0], 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[0], 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] |when(i==0)beep->STOP |stop->STOP ).

## 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) else TERMINAL).

Back to End User

Updated