Copilot.Library.LTL

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 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 ptLTL library is probaby more useful.

Documentation

next :: Stream Bool -> Stream Bool

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.

eventually :: Integral a => a -> Stream Bool -> Stream Bool

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

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 ...

until :: Integral a => a -> Stream Bool -> Stream Bool -> Stream Bool

until n s0 s1 means that eventually n s1, and up until at least the period before s1 holds, s0 continuously holds.

release :: Integral a => a -> Stream Bool -> Stream Bool -> Stream Bool

release n s0 s1 means that either always n s1, or s1 holds up to and including the period at which s0 becomes true.