Provides past-time linear-temporal logic (ptLTL operators).
Interface: see Examples/PTLTLExamples.hs, particularly function tSinExt2 in
that file. You can embed a ptLTL specification within a Copilot
specification using the form:
var
where ptltl
(operator spec)
var
is the variable you want to assign to the ptLTL specification
you're writing.
Documentation
since :: Spec Bool -> Spec Bool -> Var -> StreamsSource
Once s2
holds, in the following state (period), does s1
continuously hold?
alwaysBeen :: Spec Bool -> Var -> StreamsSource
Has s
always held (up to and including the current state)?