copilot-libraries-3.7: Libraries for the Copilot language.
Copyright(c) 2011 National Institute of Aerospace / Galois Inc.
Safe HaskellSafe-Inferred
LanguageHaskell2010

Copilot.Library.PTLTL

Description

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

Interface: See Examples/PTLTLExamples.hs in the Copilot repository.

You can embed a ptLTL specification within a Copilot specification using the form:

  operator stream
Synopsis

Documentation

since :: Stream Bool -> Stream Bool -> Stream Bool Source #

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

alwaysBeen :: Stream Bool -> Stream Bool Source #

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

eventuallyPrev :: Stream Bool -> Stream Bool Source #

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

previous :: Stream Bool -> Stream Bool Source #

Did s hold in the previous period?