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

Copyright | (c) 2011 National Institute of Aerospace / Galois Inc.
Safe Haskell | Safe-Inferred
Language | Haskell2010

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

- since :: Stream Bool -> Stream Bool -> Stream Bool
- alwaysBeen :: Stream Bool -> Stream Bool
- eventuallyPrev :: Stream Bool -> Stream Bool
- previous :: Stream Bool -> Stream Bool

# Documentation

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

Is there a time when `s2` holds and after which `s1` continuously holds?

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?