Documentation

always :: Int -> Spec Bool -> Spec Bool Source

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 Source

Property s holds at the next period.

eventually :: Int -> Spec Bool -> Spec Bool Source

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 Source

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 Source

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