• Basic FSP syntax
• Deterministic keyword
• Closure keyword
• Property keyword

Basic FSP syntax

MTSA preserves the full syntax of supported by LTSA. Some references for its syntax are FSP-Syntax by Jeff Magee and Notes on FSP, Alan Williams, Donal Fellows, and Howard Barringer

The syntax for sequential and composite processes has remained the same in MTSA. Multiple additions have been made regarding modifiers for composite processes, hence we cover them below.

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

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

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