PTCaRet Plugin3 Output Syntax

From FSL
Jump to: navigation, search

The PTCaRet plugin generates a monitor from the input formula, which updates its state according to the observed event and the previous state. The state of the monitor is represented as two arrays of bits, namely, one for standard temporal operators and one for abstract temporal operators.

Example

For the pattern:

<mop>
<Client>Web</Client>
<Events>a b c</Events>
<Property>
<Logic>ptcaret</Logic>
<Formula>a implies (not c Sa b)</Formula>
</Property>
<Categories>validation</Categories>
</mop>

The output generated by the PTCaRet plugin is:

<mop>
<Client>Web</Client>
<Events>a b c</Events>
<Property>
<Logic>ptcaret pseudo-code</Logic>
<Formula>
$beta$[0] := (b || !c && $beta$[0]);
output((!a || $beta$[0]))
</Formula>
</Property>
<Categories>validation</Categories>
<Message>done</Message>
<Message>versioned stack</Message>
<Statistics>
<TotalMOPCount>2015</TotalMOPCount>
<CurrentClient>Web</CurrentClient>
<ClientCount>192</ClientCount>
<CurrentLogic>ptcaret</CurrentLogic>
<LogicCount>8</LogicCount>
<ClientAndLogicCount>1</ClientAndLogicCount>
<TotalExecutionTime>437ms</TotalExecutionTime>
</Statistics>
</mop>
Personal tools
Namespaces

Variants
Actions
Navigation