content: module LTLExamples where
  
  import qualified Prelude as P
  import Language.Copilot
  
  ----------------
  -- LTL tests ---
  ----------------
  
  testAlways :: Int -> Int -> Stream Bool
  testAlways i1 i2 = let input = replicate i1 P.True P.++ [ False ] ++ true
                     in  always i2 input
  
  testNext :: Stream Bool
  testNext = let input = [ False, False, True ] ++ input
             in  next input
  
  testFuture :: Int -> Int -> Stream Bool
  testFuture i1 i2 = let input = replicate i1 False P.++ [ True ] ++ false
                     in  eventually i2 input
  
  testUntil :: Int -> Int -> Int -> Stream Bool
  testUntil i1 i2 i3 =
      let t0 = replicate i1 True  ++ false
          t1 = replicate ( i2 - 1 ) False P.++ [ True ] ++ false
      in until i3 t0 t1
  
  testRelease :: Int -> Int -> Int -> Stream Bool
  testRelease i1 i2 i3 =
      let t0 = replicate i1 True ++ false
          t1 = replicate ( i2 - 1 ) False P.++ [ True ] ++ false
      in release i3 t1 t0
  
  ltlTest :: Spec
  ltlTest = do
    trigger "testAlways1" true [ arg $ testAlways  0  0    ]
    trigger "testAlways2" true [ arg $ testAlways  5  1    ]
    trigger "testNext"    true [ arg $ testNext            ]
    trigger "testFuture"  true [ arg $ testFuture  12  10   ]
    trigger "testUntil"   true [ arg $ testUntil   5  6  4 ]
    trigger "testRelease" true [ arg $ testRelease 5  5  4 ]
  
  ltlExamples :: IO ()
  ltlExamples = do
    prettyPrint ltlTest
    putStrLn ""
    putStrLn ""
    interpret 20 ltlTest
  