LTL Plugin2.2 Output Syntax

From FSL
Jump to: navigation, search

The LTL 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 violated whenever the monitor reaches one of the violation states. The algorithm we use cannot find validations, but because LTL is an invertible logic we are able to monitor for validation by negating the formula and monitoring for violation. 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>request acquire</Events>
<Property>
<Logic>ltl</Logic>
<Formula>[](acquire => (*) request)</Formula>
</Property>
<Categories>violation</Categories>
</mop>

The output generated by the LTL plugin is:

<mop>
<Client>Web</Client>
<Events>acquire request</Events>
<Property>
<Logic>fsm</Logic>
<Formula>s0_s2_s3_s4[
default s0_s2_s3_s4
acquire -> s1
request -> s0_s2_s3_s4
]
violation[
 
]
s1[
default violation
acquire ->; violation
request ->; s0_s2_s3_s4
]
</Formula>
</Property>
<Categories>violation</Categories>
<CreationEvents> request acquire</CreationEvents>
<Message>done</Message>
<EnableSets>// violation Enables
{request=[[], [request], [acquire], [acquire, request]], acquire=[[], [request], [acquire], [request, acquire]]}
</EnableSets>
</mop>


Personal tools
Namespaces

Variants
Actions
Navigation