copilot-libraries-0.1: A Haskell-embedded DSL for monitoring hard real-time distributed systems.

Copilot.Library.PTLTL

Description

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

Interface: see Examples/PTLTLExamples.hs. You can embed a ptLTL specification within a Copilot specification using the form: operator stream

Synopsis

Documentation

since :: Stream Bool -> Stream Bool -> Stream BoolSource

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

alwaysBeen :: Stream Bool -> Stream BoolSource

Has s always held (up to and including the current state)?

eventuallyPrev :: Stream Bool -> Stream BoolSource

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

previous :: Stream Bool -> Stream BoolSource

Did s hold in the previous period?