module Language.Copilot.Examples.PTLTLExamples where
import Prelude (($), repeat, replicate, IO())
import qualified Prelude as P
import Data.Map (fromList)
import Language.Copilot hiding (check)
import Language.Copilot.Libs.PTLTL
import Language.Copilot.Libs.Vote
tstdatprv :: Streams
tstdatprv = do
let a = varB "a"
a .= [True, False] ++ a
tprv :: Streams
tprv = do
let c = varB "c"
a = varB "a"
tstdatprv
c `ptltl` previous a
tstdatAB :: Streams
tstdatAB = do
let d = varB "d"
d .= [True, True, True, True, True, True, True, False] ++ d
tAB :: Streams
tAB = do
let f = varB "f"
d = varB "d"
tstdatAB
f `ptltl` alwaysBeen d
tstdatEP :: Streams
tstdatEP = do
let g = varB "g"
g .= [False, False, False, False, False, True, False] ++ g
tEP :: Streams
tEP = do
let h = varB "h"
g = varB "g"
tstdatEP
h `ptltl` eventuallyPrev g
q1, q2, z :: Spec Bool
q1 = varB "q1"
q2 = varB "q2"
z = varB "z"
tstdat1Sin :: Streams
tstdat1Sin = q1 .= [False, False, False, False, True] ++ true
tstdat2Sin :: Streams
tstdat2Sin = q2 .= [False, False, True, False, False, False, False ] ++ q2
tSince :: Streams
tSince = do
tstdat1Sin
tstdat2Sin
z `ptltl` (q1 `since` q2)
tSinExt :: Streams
tSinExt = do
let e1 = extB "e1"
e2 = extB "e2"
z `ptltl` (e1 `since` e2)
tSinExt2 :: Streams
tSinExt2 = do
let e1 = extB "e1"
e2 = extB "e2"
a = varB "a"
s = varB "s"
d = varB "d"
t = varB "t"
e = varB "e"
a .= not e1
s `ptltl` (e2 `since` d)
t `ptltl` (alwaysBeen $ not a)
e .= e1 ==> d
engine :: Streams
engine = do
let t0 = extW8 "temp_probe_0"
t1 = extW8 "temp_probe_1"
t2 = extW8 "temp_probe_2"
cooler = extB "fan_status"
maj = varW8 "maj"
check = varB "maj_check"
overHeat = varB "over_heat"
monitor = varB "monitor"
temps = [t0, t1, t2]
maj .= majority temps
check .= aMajority temps maj
overHeat `ptltl` ( (cooler || (maj <= 250 && check))
`since` (maj > 250))
monitor .= not overHeat
trigger monitor "shutoff_engine" void
engineRun :: Bool -> IO ()
engineRun b = if b then
interpret engine 40 $
setE (emptySM { bMap = fromList [("fan_status", replicate 3 False P.++ repeat False)]
, w8Map = fromList [ ("temp_probe_0", [240,240..])
, ("temp_probe_1", [240,241..])
, ("temp_probe_2", [240,241..])
]
})
baseOpts
else compile engine "engine" $ setSim baseOpts