FSM Plugin2.0 Output Syntax

From FSL
Jump to: navigation, search

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 
 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:

safe_states start safe
all_states start safe unsafe

Fsm ex3.jpg

Personal tools