FSM Plugin Output Syntax
The FSM plugin generates a state machine from the input fsm description. The state of the monitor is updated according to the current state and the received event. The output, seen here, is a pictorial representation, generated using dot. The fsm is violated when the monitor gets stuck, i.e., when no transition can be made from the current state upon the received event. As mentioned on the FSM Plugin Input Syntax page, <Property Handler>s (see MOP Syntax) can be associated with any state. Note that each instantiation of MOP must handle FSMs itself; in fact, FSM is not so much a plugin as it is an intermediate representation for all the logic plugins that can be reduced to finite state descriptions (e.g., ERE, PTLTL, FTLTL, etc). We provide this graphical output to help visualize the finite state machines only; it is not used by any instance of MOP.
In the following example, three events, namely, next, hasnext and dummy, and three states, namely, start, safe and unsafe, are defined. Two state aliases are declared: all_states represents all the states in the state machine and safe_states includes the start state and the safe state. Note that the state machine will go into "fail" whenever a dummy event is received, unless the machine is in the first state, in which case it will stay in the first state. Note that in the image default transitions are given the label MOP_default.
event next event hasnext event dummy fsm: start [ default start next -> unsafe hasnext -> safe ] safe [ next -> start hasnext -> safe ] unsafe [ next -> unsafe hasnext -> safe ] all_states : start, safe, unsafe safe_states : start, safe
The output generated by the FSM plugin is:
|all_states||start safe unsafe|