Sebastian UchitelModal Transition Systems
Modal transition systems (MTS) can be modelled by using a question mark (?) on event labels to indicate may-transitions (transitions that may or may not be present in an implementation).
A = (a -> b? -> A | a? -> A).Abstract keyword
The abstract keyword builds an MTS from an FSP process by 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).