Language.Copilot.Libs.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,
always 3 p
holds if p holds at least once every four periods (3 transitions).
Interface: see Examples/LTLExamples.hs You can embed a LTL specification
within a Copilot specification using the form:
var
where ltl (operator spec)
var is the variable you want to assign to the LTL specification
you're writing.
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.
- ltl :: Spec Bool -> (Spec Bool -> Streams) -> Streams
- eventually :: Int -> Spec Bool -> Spec Bool -> Streams
- next :: Spec Bool -> Spec Bool -> Streams
- always :: Int -> Spec Bool -> Spec Bool -> Streams
- until :: Int -> Spec Bool -> Spec Bool -> Spec Bool -> Streams
- release :: Int -> Spec Bool -> Spec Bool -> Spec Bool -> Streams
Documentation
eventually :: Int -> Spec Bool -> Spec Bool -> StreamsSource
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 ...
next :: Spec Bool -> Spec Bool -> StreamsSource
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.
always :: Int -> Spec Bool -> Spec Bool -> StreamsSource
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 ...