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