Generate Copilot monitors

Author: ivanperez-keera

.github/workflows/repo-ghc-8.6-cabal-2.4-ros.yml

@@ -48,5 +48,7 @@ jobs:
     - name: Generate ROS app
       run: |
         ogma ros --app-target-dir demo --variable-db ogma-cli/examples/ros-copilot/vars-db --variable-file ogma-cli/examples/ros-copilot/variables --handlers-file ogma-cli/examples/ros-copilot/handlers
+        cabal v1-exec -- runhaskell ogma-cli/examples/ros-copilot/ROS.hs
+        find demo/
         cd demo/
         docker build .

ogma-cli/examples/ros-copilot/Monitor.hs

@@ -0,0 +1,48 @@
+import           Copilot.Compile.C99
+import           Copilot.Language          hiding (prop)
+import           Copilot.Language.Prelude
+import           Copilot.Library.LTL       (next)
+import           Copilot.Library.MTL       hiding (since, alwaysBeen, trigger)
+import           Copilot.Library.PTLTL     (since, previous, alwaysBeen)
+import qualified Copilot.Library.PTLTL     as PTLTL
+import qualified Copilot.Library.MTL       as MTL
+import           Language.Copilot          (reify)
+import           Prelude                   hiding ((&&), (||), (++), (<=), (>=), (<), (>), (==), (/=), not)
+
+a :: Stream (Bool)
+a = extern "a" Nothing
+
+-- | testCopilot
+--   @
+--   unimportant
+--   @
+propTestCopilot :: Stream Bool
+propTestCopilot = a
+
+
+-- | Clock that increases in one-unit steps.
+clock :: Stream Int64
+clock = [0] ++ (clock + 1)
+
+
+-- | First Time Point
+ftp :: Stream Bool
+ftp = [True] ++ false
+
+
+pre :: Stream Bool -> Stream Bool
+pre = ([False] ++)
+
+tpre :: Stream Bool -> Stream Bool
+tpre = ([True] ++)
+
+-- | Complete specification. Calls the C function void  handler(); when
+-- the property is violated.
+spec :: Spec
+spec = do
+  trigger "handlerTestCopilot" (not propTestCopilot) []
+
+
+main :: IO ()
+main = reify spec >>= compile "monitor"
+