copilot-2.0.4: Examples/PTLTLExamples.hs

-- | The examples are for testing the ptLTL library

module PTLTLExamples ( ptltlExamples ) where 

import Language.Copilot
import Prelude ()
import qualified Data.List as L


-- | test of previous
previousTestData :: Stream Bool
previousTestData = [ True, False ] ++ previousTestData

previousTest :: Spec
previousTest = do
  observer "previousTest" ( previous previousTestData )


-- | test of alwaysBeen
alwaysBeenTestData ::  Stream Bool
alwaysBeenTestData = [ True, True, True, True, True, True, True, False ]
                     ++ alwaysBeenTestData

alwaysBeenTest :: Spec
alwaysBeenTest = do
  observer "testAlwaysBeen" ( alwaysBeen alwaysBeenTestData )


-- | test of eventuallyPrevious
eventuallyPrevTestData ::  Stream Bool
eventuallyPrevTestData = [ False, False, False, False, False, True, False ]
                         ++ eventuallyPrevTestData

eventuallyPrevTest :: Spec
eventuallyPrevTest = observer "eventuallyPrevTest"
                     ( eventuallyPrev eventuallyPrevTestData )


-- | test of since
sinceTestData1 :: Stream Bool
sinceTestData1 = [ False, False, False ] ++ true

sinceTestData2 :: Stream Bool
sinceTestData2 = [ False, False, True, False, False, False, False ]
                 ++ sinceTestData2

sinceTest :: Spec
sinceTest = observer "sinceTest"
            ( sinceTestData1 `since` sinceTestData2 )


-- | test since with external variables
sinceExtTest :: Spec
sinceExtTest = observer "sinceExtTest"
               ( extern "e1" (Just e1) `since` extern "e2" (Just e2))

-- | external variables
e1, e2 :: [Bool]
e1 = replicate 10 False L.++               repeat True
e2 = replicate 9  False L.++ [ True ] L.++ repeat False

ptltlExamples :: IO ()
ptltlExamples = do
  prettyPrint previousTest
  interpret 20 previousTest

  prettyPrint alwaysBeenTest
  interpret 20 alwaysBeenTest

  prettyPrint eventuallyPrevTest
  interpret 20 eventuallyPrevTest

  prettyPrint sinceTest
  interpret 20 sinceTest

  prettyPrint sinceExtTest
  interpret 20  sinceExtTest