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:
ptltl (operator spec)
var is the variable you want to assign to the ptLTL specification
s2 holds, in the following state (period), does
s1 continuously hold?
s always held (up to and including the current state)?
s hold at some time in the past (including the current state)?