module Language.Copilot.Libs.PTLTL(previous, alwaysBeen, eventuallyPrev, since) where
import Prelude ()
import qualified Prelude as P
import Language.Copilot.Core
import Language.Copilot.Language
previous :: Var -> Spec Bool -> Streams
previous v s = do
v .= [False] ++ s
alwaysBeen :: Var -> Spec Bool -> Streams
alwaysBeen v s = do
tmp .= [True] ++ (var tmp) && s
v .= s && varB tmp
where tmp = "alwaysBeenTmp_" P.++ v
eventuallyPrev :: Var -> Spec Bool -> Streams
eventuallyPrev v s = do
tmp .= [False] ++ (var tmp) || s
v .= s || varB tmp
where tmp = "eventuallyPrevTmp_" P.++ v
since :: Var -> (Spec Bool, Spec Bool) -> Streams
since v (s1, s2) = do
tmp .= [False] ++ (s2 || (s1 && varB v))
v .= varB tmp && s1
where tmp = "sinceTmp_" P.++ v