Safe Haskell | Safe-Infered |
---|
Provides past-time linear-temporal logic (ptLTL operators).
Interface: see Examples/PTLTLExamples.hs.
You can embed a ptLTL specification within a Copilot specification using
the form:
operator stream
Documentation
since :: Stream Bool -> Stream Bool -> Stream BoolSource
Once s2
holds, in the following state (period), does s1
continuously hold?
alwaysBeen :: Stream Bool -> Stream BoolSource
Has s
always held (up to and including the current state)?
eventuallyPrev :: Stream Bool -> Stream BoolSource
Did s
hold at some time in the past (including the current state)?