Copyright | (c) 2011 National Institute of Aerospace / Galois Inc. |
---|---|
Safe Haskell | Safe |
Language | Haskell2010 |
Provides past-time linear-temporal logic (ptLTL operators).
Interface: See Examples/PTLTLExamples.hs
in the
Copilot repository.
You can embed a ptLTL specification within a Copilot specification using the form:
operator stream
Synopsis
- since :: Stream Bool -> Stream Bool -> Stream Bool
- alwaysBeen :: Stream Bool -> Stream Bool
- eventuallyPrev :: Stream Bool -> Stream Bool
- previous :: Stream Bool -> Stream Bool
Documentation
since :: Stream Bool -> Stream Bool -> Stream Bool Source #
Once s2
holds, in the following state (period), does s1
continuously hold?
alwaysBeen :: Stream Bool -> Stream Bool Source #
Has s
always held (up to and including the current state)?
eventuallyPrev :: Stream Bool -> Stream Bool Source #
Did s
hold at some time in the past (including the current state)?