copilot-0.21: A lazy-list language for generating constant-time and constant-space C programs. Uses Atom as a backend.

Language.Copilot.Libs.PTLTL

Description

Provides past-time linear-temporal logic (ptLTL operators).

Synopsis

Documentation

previous :: Var -> Spec Bool -> Streams Source

Did s hold in the previous period?

alwaysBeen :: Var -> Spec Bool -> Streams Source

Has s always held?

eventuallyPrev :: Var -> Spec Bool -> Streams Source

Did s hold at some time in the past (including the current state)?

since :: Var -> (Spec Bool, Spec Bool) -> Streams Source

Once s2 holds, in the following state (period), does s1 continuously hold?