Language.Copilot.Libs.PTLTL

Description

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.

Synopsis

Documentation

previous :: Var -> Spec Bool -> Streams Source

Did s hold in the previous period?

alwaysBeen :: Var -> Spec Bool -> Streams Source

Has s always held?

eventuallyPrev :: Var -> Spec Bool -> Streams Source

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

since :: Var -> (Spec Bool, Spec Bool) -> Streams Source

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