PTCaRet Monitoring Algorithm

From FSL
Jump to: navigation, search

The monitoring algorithm for PTCaRet uses two arrays of bits to keep track of the value of the different temporal operators in the formula. One array is for abstract operators and the other array is for standard temporal operators. Thus, there is one bit per operator. At the beginning of monitoring, all bits are initialized to false, as the monitoring output shows. And a stack is initialized to empty. As each event in a trace is received, the sequential code is run, updating the bits, if any. At each function begin, the array of bits for abstract operators is copied and pushed into the stack. At each function end, an array is popped from the stack and it replaces the current array of bits for abstract operators. When the output statement is reached, the output of the monitor is set by evaluating the expression in the output statement. It is imperative that the output statement be where it is, because the value of bits holding previously operators must be set after the output statement, as they should affect the monitor's output on the next event, not the current.

Personal tools
Namespaces

Variants
Actions
Navigation