# 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),
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