PTLTL Plugin3 Output Syntax

From FSL
Jump to: navigation, search

The PTLTL plugin generates a state machine from the input pattern. The state of the monitor is updated according to the current state and the received event. A trace of events is validated whenever the monitor reaches one of the acceptance states, e.g., state 3 in the below example. The pattern is violated when the monitor gets stuck, i.e., when no transition can be made from the current state upon the received event. The output is an FSM description in the input syntax of the FSM plugin, which can be found here.

Example

For the pattern:

<mop>
<Client>Web</Client>
<Events>next hasnext</Events>
<Property>
<Logic>ptltl</Logic>
<Formula>next -> (*) hasnext</Formula>
</Property>
<Categories>violation</Categories>
</mop>

The output generated by the PTLTL plugin is:

<mop>
<Client>Web</Client>
<Events>hasnext next</Events>
<Property>
<Logic>fsm</Logic>
<Formula>n0[
default n2,
hasnext -> n1,
next -> n0
]
n1[
default n2,
hasnext -> n1,
next -> n2
]
n2[
default n2,
hasnext -> n1,
next -> n0
]
alias violation = n0
alias validation = n1,n2
</Formula>
</Property>
<Categories>violation</Categories>
<CreationEvents></CreationEvents>
<Message>done</Message>
<EnableSets>// fail Enables
{hasnext=[], next=[]}
</EnableSets>
<Statistics>
<TotalMOPCount>1657</TotalMOPCount>
<CurrentClient>Web</CurrentClient>
<ClientCount>60</ClientCount>
<CurrentLogic>ptltl</CurrentLogic>
<LogicCount>52</LogicCount>
<ClientAndLogicCount>6</ClientAndLogicCount>
<TotalExecutionTime>433ms</TotalExecutionTime>
</Statistics>
</mop>


Personal tools
Namespaces

Variants
Actions
Navigation