copilot-0.25: A stream DSL for writing embedded C monitors.



Provides past-time linear-temporal logic (ptLTL operators).

Interface: see Examples/PTLTLExamples.hs, particularly function tSinExt2 in that file. You can embed a ptLTL specification within a Copilot specification using the form: var ptltl (operator spec) where var is the variable you want to assign to the ptLTL specification you're writing.



since :: Spec Bool -> Spec Bool -> Var -> StreamsSource

Once s2 holds, in the following state (period), does s1 continuously hold?

alwaysBeen :: Spec Bool -> Var -> StreamsSource

Has s always held (up to and including the current state)?

eventuallyPrev :: Spec Bool -> Var -> StreamsSource

Did s hold at some time in the past (including the current state)?

previous :: Spec Bool -> Var -> StreamsSource

Did s hold in the previous period?