    -- |
    -- 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/Copilot-Language/copilot/blob/v2.2.1/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

    -- | Is there a time when @s2@ holds and after which @s1@ continuously holds?
    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
    eventuallyPrev (Stream Bool
    s2 Stream Bool -> Stream Bool -> Stream Bool
    ==> (Stream Bool -> Stream Bool
    alwaysBeen Stream Bool
    s1))