Language.Copilot.Libs.PTLTL

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.

Documentation

ptltl :: Spec Bool -> (Spec Bool -> Streams) -> Streams

since :: Spec Bool -> Spec Bool -> Spec Bool -> Streams

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

alwaysBeen :: Spec Bool -> Spec Bool -> Streams

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

eventuallyPrev :: Spec Bool -> Spec Bool -> Streams

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

previous :: Spec Bool -> Spec Bool -> Streams

Did s hold in the previous period?