copilot-libraries-2.2.0: Libraries for the Copilot language.

Copyright(c) 2011 National Institute of Aerospace / Galois, Inc.
Safe HaskellSafe
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?