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