FSM Plugin3 Output Syntax

From FSL
Jump to: navigation, search

The FSM plugin generates a state machine from the input fsm description. 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). One can see in the resulting output the enable sets and creation events for this property, as well as some possible statistics on monitor generation.

Example

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.


<mop>
<Client>Web</Client>
<Events>hasnext next dummy</Events>
<Property>
<Logic>fsm</Logic>
<Formula>
start [
default start
next -> unsafe
hasnext -> safe
]
safe [
next -> start
hasnext -> safe
]
unsafe [
next -> unsafe
hasnext -> safe
]
alias all_states = start, safe, unsafe
alias safe_states = start, safe
</Formula>
</Property>
<Categories>fail safe unsafe all_states safe_states</Categories>
<CreationEvents> hasnext next dummy</CreationEvents>
<Message>done</Message>
<EnableSets>// fail Enables
{hasnext=[[], [hasnext, dummy], [hasnext], [hasnext, next], [hasnext, next, dummy], [next],
[next, dummy], [dummy]],
next=[[], [hasnext, dummy], [hasnext], [hasnext, next], [hasnext, next, dummy], [next],
[next, dummy], [dummy]],
dummy=[[], [hasnext, dummy], [hasnext], [hasnext, next], [hasnext, next, dummy], [next],
[next, dummy], [dummy]]}
// safe Enables
{hasnext=[[], [hasnext, dummy], [hasnext], [hasnext, next], [hasnext, next, dummy], [next],
[next, dummy], [dummy]],
next=[[], [hasnext, dummy], [hasnext], [hasnext, next], [hasnext, next, dummy], [next],
[next, dummy], [dummy]],
dummy=[[], [hasnext, next], [hasnext, next, dummy], [dummy]]}
// unsafe Enables
{hasnext=[[], [hasnext, dummy], [hasnext], [hasnext, next], [hasnext, next, dummy], [next],
[next, dummy], [dummy]],
next=[[], [hasnext, dummy], [hasnext], [hasnext, next], [hasnext, next, dummy], [next],
[next, dummy], [dummy]],
dummy=[[], [hasnext, next], [hasnext, next, dummy], [dummy]]}
// all_states Enables
{hasnext=[[], [hasnext, dummy], [hasnext], [hasnext, next], [hasnext, next, dummy], [next],
[next, dummy], [dummy]],
next=[[], [hasnext, dummy], [hasnext], [hasnext, next], [hasnext, next, dummy], [next],
[next, dummy], [dummy]],
dummy=[[], [hasnext, next], [hasnext, next, dummy], [dummy]]}
// safe_states Enables
{hasnext=[[], [hasnext, dummy], [hasnext], [hasnext, next], [hasnext, next, dummy], [next],
[next, dummy], [dummy]],
next=[[], [hasnext, dummy], [hasnext], [hasnext, next], [hasnext, next, dummy], [next],
[next, dummy], [dummy]],
dummy=[[], [hasnext, next], [hasnext, next, dummy], [dummy]]}
</EnableSets>
<Statistics>
<TotalMOPCount>226</TotalMOPCount>
<CurrentClient>Web</CurrentClient>
<ClientCount>18</ClientCount>
<CurrentLogic>fsm</CurrentLogic>
<LogicCount>38</LogicCount>
<ClientAndLogicCount>15</ClientAndLogicCount>
<TotalExecutionTime>638ms</TotalExecutionTime>
</Statistics>
</mop>


Personal tools
Namespaces

Variants
Actions
Navigation