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



Provides past-time linear-temporal logic (ptLTL operators). Currently won't make unique tmp stream names if you use the same operator twice in one stream definition.



previous :: Var -> Spec Bool -> StreamsSource

Did s hold in the previous period?

alwaysBeen :: Var -> Spec Bool -> StreamsSource

Has s always held?

eventuallyPrev :: Var -> Spec Bool -> StreamsSource

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

since :: Var -> (Spec Bool, Spec Bool) -> StreamsSource

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