module Copilot.Library.PTLTL
( since, alwaysBeen, eventuallyPrev, previous ) where
import Prelude ( ($) )
import Copilot.Language
import Data.Bool hiding ( (&&), (||) )
previous :: Stream Bool -> Stream Bool
previous s = [ False ] ++ s
alwaysBeen :: Stream Bool -> Stream Bool
alwaysBeen s = s && tmp
where tmp = [ True ] ++ s && tmp
eventuallyPrev :: Stream Bool -> Stream Bool
eventuallyPrev s = s || tmp
where tmp = [ False ] ++ s || tmp
since :: Stream Bool -> Stream Bool -> Stream Bool
since s1 s2 = alwaysBeen ( tmp ==> s1 )
where tmp = eventuallyPrev $ [ False ] ++ s2