|
| Language.Copilot.Libs.LTL |
|
|
| Description |
| Bounded Linear Temporal Logic (LTL) operators.
|
|
| Synopsis |
|
|
|
| Documentation |
|
| always :: Int -> Spec Bool -> Spec Bool |
| Property s holds for the next n periods. If n == 0, then s holds
in the current period. We require n >= 0.
E.g., if p = always 2 s, then we have the following relationship between the streams generated:
s => T T T T F F F F ...
p => T T F F F F F F ...
|
|
| next :: Spec Bool -> Spec Bool |
| Property s holds at the next period.
|
|
| eventually :: Int -> Spec Bool -> Spec 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 F T F T F ...
p => F F T T T T T T ...
|
|
| until :: Int -> Spec Bool -> Spec Bool -> Spec Bool |
| until n s0 s1 means that eventually n s1, and up until at least the
period before s1 holds, s0 continuously holds.
|
|
| release :: Int -> Spec Bool -> Spec Bool -> Spec 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.
|
|
| Produced by Haddock version 2.6.1 |
