PTLTLPlugin4

PTLTL plugin for MOP allows one to synthesize monitors from from past time linear temporal logic (PTLTL) descriptions. The generated monitors are based on a series of assignments to array elements, one element for each temporal operator in the formula. From these array assignments a static finite state machine is generated for monitoring purposes (the finite state machine is slightly more efficient than array assignments, and it eases the generation of enable sets.