-- | 
-- Module: PTLTL
-- Description: Past-Time Linear-Temporal Logic
-- Copyright: (c) 2011 National Institute of Aerospace / Galois, Inc.
--
-- Provides past-time linear-temporal logic (ptLTL operators).
--
-- /Interface:/ See @Examples/PTLTLExamples.hs@ in the
-- <https://github.com/leepike/Copilot/tree/master/Examples Copilot repository>.
--
-- You can embed a ptLTL specification within a Copilot specification using
-- the form:
--
-- @
--   operator stream
-- @

{-# LANGUAGE NoImplicitPrelude #-}

module Copilot.Library.PTLTL
    ( since, alwaysBeen, eventuallyPrev, previous ) where

import Prelude ()
import Copilot.Language

-- | Did @s@ hold in the previous period?
previous :: Stream Bool -> Stream Bool
previous :: Stream Bool -> Stream Bool
previous Stream Bool
s = [ Bool
False ] [Bool] -> Stream Bool -> Stream Bool
forall a. Typed a => [a] -> Stream a -> Stream a
++ Stream Bool
s


-- | Has @s@ always held (up to and including the current state)?
alwaysBeen :: Stream Bool -> Stream Bool
alwaysBeen :: Stream Bool -> Stream Bool
alwaysBeen Stream Bool
s = Stream Bool
s Stream Bool -> Stream Bool -> Stream Bool
&& Stream Bool
tmp
    where tmp :: Stream Bool
tmp = [ Bool
True ] [Bool] -> Stream Bool -> Stream Bool
forall a. Typed a => [a] -> Stream a -> Stream a
++ Stream Bool
s Stream Bool -> Stream Bool -> Stream Bool
&& Stream Bool
tmp


-- | Did @s@ hold at some time in the past (including the current state)?
eventuallyPrev :: Stream Bool -> Stream Bool
eventuallyPrev :: Stream Bool -> Stream Bool
eventuallyPrev Stream Bool
s = Stream Bool
s Stream Bool -> Stream Bool -> Stream Bool
|| Stream Bool
tmp
  where tmp :: Stream Bool
tmp = [ Bool
False ] [Bool] -> Stream Bool -> Stream Bool
forall a. Typed a => [a] -> Stream a -> Stream a
++ Stream Bool
s Stream Bool -> Stream Bool -> Stream Bool
|| Stream Bool
tmp


-- | Once @s2@ holds, in the following state (period), does @s1@ continuously hold?
since ::  Stream Bool -> Stream Bool -> Stream Bool
since :: Stream Bool -> Stream Bool -> Stream Bool
since Stream Bool
s1 Stream Bool
s2 = Stream Bool -> Stream Bool
alwaysBeen ( Stream Bool
tmp Stream Bool -> Stream Bool -> Stream Bool
==> Stream Bool
s1 )
    where tmp :: Stream Bool
tmp = Stream Bool -> Stream Bool
eventuallyPrev (Stream Bool -> Stream Bool) -> Stream Bool -> Stream Bool
forall a b. (a -> b) -> a -> b
$ [ Bool
False ] [Bool] -> Stream Bool -> Stream Bool
forall a. Typed a => [a] -> Stream a -> Stream a
++ Stream Bool
s2