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 choice

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

Closure keyword

The closure keyword adds new transitions to the LTS resulting from compiling an FSP process according to the transitive closure of the transition relation over tau (silent) events The keyword can be used with sequential and composite processes.

closure A = (a -> b -> A)\{b}.


B = (d -> a -> b -> B | d -> a -> c -> B).
closure ||COMP = (B)\{a}.

Constraint keyword

The constraint keyword builds an LTS from an FLTL formula such that its traces are all traces that satisfy the formula.

The formula must be a safety property. The alphabet of the resulting LTS contains exactly all events that appear in the formula or in fluent definitions used by the formula. This implies that the interpetation of the next operator (X) is like an alphabetised next.

constraint P = [] (p -> X q)

fluent A = <a, c>
fluent B = <b, c>

constraint Q = [](A -> X B)

Deterministic keyword

The deterministic keyword produces a deterministic LTS that preserves that traces of the original one. It can be used with sequential and composite processes.

Note that in composite processes the keyword takes precedence over hiding.

deterministic A = (a -> b -> A | a -> c -> A).

B = (a -> b -> B | a -> c -> B).
deterministic ||COMP = (B)\{a}.

C = (a -> b -> C | a -> c -> C)\{a}.
deterministic ||COMP2 = (C).

Property keyword

The property keyword adds an error state and for every event and every other state it adds a transition to it if the event is not enabled in that state. It requires a deterministic LTS.

property POLITE
  = (knock->enter->POLITE).

Modal Transition Systems

Modal transition systems (MTS) can be modelled by using a question mark (?) on event labels.

A = (a -> b? -> A | a? -> A).

Abstract keyword

The abstract keyword builds an MTS from a FSP process adding to each state maybe transitions on labels that are not enabled in the original process. It can be applied both to sequential and composite processes.

abstract A = (a -> b -> A | a->STOP | b->END).

B = (a -> b -> B | b? -> B).
abstract ||COMP = (B).

End

Back to End User