module Language.Copilot.Libs.PTLTL
( ptltl, since, alwaysBeen, eventuallyPrev, previous )
where
import Prelude (String, ($), error)
import qualified Prelude as P
import Language.Copilot.Core
import Language.Copilot.Language
tmpName :: Spec Bool -> String -> Spec Bool
tmpName v name =
case v of
Var v' -> varB (v' P.++ "_" P.++ name)
_ -> error "Copilot error in tmpName in PTLTL.hs."
ptltl :: Spec Bool -> (Spec Bool -> Streams) -> Streams
ptltl v f = f v
previous :: Spec Bool -> Spec Bool -> Streams
previous s v = v .= [False] ++ s
alwaysBeen :: Spec Bool -> Spec Bool -> Streams
alwaysBeen s v = do
tmp .= [True] ++ v
v .= tmp && s'
s' .= s
where
tmp = tmpName v "ab_tmp"
s' = tmpName v "ab"
eventuallyPrev :: Spec Bool -> Spec Bool -> Streams
eventuallyPrev s v = do
tmp .= [False] ++ tmp || s'
v .= s' || tmp
s' .= s
where
tmp = tmpName v "ep_tmp"
s' = tmpName v "ep"
since :: Spec Bool -> Spec Bool -> Spec Bool -> Streams
since s1 s2 v = do
tmp `ptltl` (eventuallyPrev $ [False] ++ s2)
v `ptltl` (alwaysBeen $ tmp ==> s1')
s1' .= s1
s2' .= s2
where
tmp = tmpName v "since_tmp"
s1' = tmpName v "since1"
s2' = tmpName v "since2"