View source for PTCaRet Plugin2.3 Output Syntax

__NOTOC__ __NOEDITSECTION__
{{shortcut|[[Special:PTCaRetPlugin2.3|PTCARET Plugin]] <br /> [[PTCaRet_Plugin2.3_Input_Syntax|PTCaRet Plugin Input Syntax]] <br /> [[PTCaRet Monitoring Algorithm]] }}

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:

<code lang=xml>
<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>
</code>

The output generated by the PTCaRet plugin is:

<code lang=xml>

<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>
</code>