Copyright | (c) 2011 National Institute of Aerospace / Galois Inc. |
---|---|
Safe Haskell | Safe-Inferred |
Language | Haskell2010 |
Copilot.Library.LTL
Description
Bounded Linear Temporal Logic (LTL) operators. For a bound n
, a property
p
holds if it holds on the next n
transitions (between periods). If
n == 0
, then the trace includes only the current period. For example,
eventually 3 p
holds if p
holds at least once every four periods (3 transitions).
Interface: See Examples/LTLExamples.hs
in the
Copilot repository.
You can embed an LTL specification within a Copilot specification using the form:
operator spec
For some properties, stream dependencies may not allow their specification. In particular, you cannot determine the "future" value of an external variable. In general, the Copilot.Library.PTLTL library is probably more useful.
Documentation
next :: Stream Bool -> Stream Bool Source #
Property s
holds at the next period. For example:
0 1 2 3 4 5 6 7 s => F F F T F F T F ... next s => F F T F F T F ...
Note: s must have sufficient history to drop
a value from it.
Property s
holds at some period in the next n
periods. If n == 0
,
then s
holds in the current period. We require n >= 0
. E.g., if p =
eventually 2 s
, then we have the following relationship between the streams
generated:
s => F F F T F F F T ... p => F T T T F T T T ...
always :: Integral a => a -> Stream Bool -> Stream Bool Source #
Property s
holds for the next n
periods. We require n >= 0
. If n ==
0
, then s
holds in the current period, e.g., if p = always 2 s
, then we
have the following relationship between the streams generated:
0 1 2 3 4 5 6 7 s => T T T F T T T T ... p => T F F F T T ...