ogma-core 1.14.0 → 1.15.0

raw patch · 38 files changed

+1306/−634 lines, 38 filesdep +copilot-librariesdep ~copilot-coredep ~copilot-languagedep ~copilot-theoremPVP ok

version bump matches the API change (PVP)

Dependencies added: copilot-libraries

Dependency ranges changed: copilot-core, copilot-language, copilot-theorem, ogma-extra, ogma-language-c, ogma-language-copilot, ogma-language-csv, ogma-language-jsonspec, ogma-language-lustre, ogma-language-smv, ogma-language-xlsx, ogma-language-xmlspec, ogma-spec

API changes (from Hackage documentation)

Files

• CHANGELOG.md +32/−0
• ogma-core.cabal +18/−14
• src/Command/CFSApp.hs +112/−71
• src/Command/Common.hs +0/−1
• src/Command/Diagram.hs +12/−42
• src/Command/FPrimeApp.hs +67/−47
• src/Command/Overview.hs +108/−38
• src/Command/ROSApp.hs +86/−60
• src/Command/Report.hs +92/−50
• src/Command/Search.hs +199/−0
• src/Command/Standalone.hs +54/−45
• src/Command/VariableDB.hs +24/−8
• src/Data/Diagram/Analysis.hs +8/−29
• src/Data/ExprPair.hs +5/−5
• src/Data/Project.hs +55/−0
• src/Data/Spec/Parser.hs +5/−7
• src/Language/Trans/CStructs2MsgHandlers.hs +1/−1
• src/Language/Trans/Diagram2Copilot.hs +1/−1
• src/Language/Trans/Spec2Copilot.hs +2/−3
• src/Language/YAMLSpec/Parser.hs +94/−16
• templates/cfs/copilot/fsw/platform_inc/copilot_cfs_msgids.h +24/−3
• templates/cfs/copilot/fsw/src/Properties.hs +9/−33
• templates/cfs/copilot/fsw/src/copilot_cfs.c +97/−37
• templates/cfs/copilot/fsw/src/copilot_cfs.h +2/−2
• templates/cfs/copilot/fsw/src/copilot_cfs_events.h +2/−0
• templates/cfs/copilot/fsw/src/copilot_cfs_msg.h +6/−6
• templates/diagram/Copilot.hs +13/−29
• templates/fprime/Copilot.hs +49/−0
• templates/report/Report.md +18/−14
• templates/ros/Dockerfile +34/−4
• templates/ros/copilot/CMakeLists.txt +10/−1
• templates/ros/copilot/package.xml +10/−0
• templates/ros/copilot/src/Copilot.hs +9/−33
• templates/ros/copilot/src/copilot_monitor.cpp +8/−0
• templates/ros/test_requirements/CMakeLists.txt +10/−1
• templates/ros/test_requirements/package.xml +10/−0
• templates/ros/test_requirements/src/test_requirements.cpp +11/−0
• templates/standalone/Copilot.hs +9/−33

@@ -1,5 +1,37 @@ # Revision history for ogma-core +## [1.15.0] - 2026-07-21++* Version bump (1.15.0) (#508).+* Remove commented code from `Data.Spec.Parser` (#430).+* Remove redundant `where` block (#432).+* Fix incorrect Haddock comment syntax (#434).+* Remove redundant occurrences of `MultiWayIf` pragma (#440).+* Fix indentation of record fields in multiple backends (#442).+* Move expressions from `let` block into `where` clause (#444).+* Update backends to use state machine module from `copilot-libraries` (#446).+* Leverage `Data.ExprPair.exprPair` in `Command.Diagram.exprPair` (#448).+* Remove empty Haddock section heading from `Command.Diagram` (#450).+* Add missing dependency to Cabal file (#458).+* Adjust overview command to accept multiple input files (#456).+* Add Copilot file from F Prime template to data-files in Cabal file (#462).+* Add module defining Ogma projects (#460).+* Introduce search command (#464).+* Remove unnecessary vertical space (#470).+* Allow using file name as requirement ID in JSON or YAML files (#472).+* Allow controlling when monitors are re-evaluated in cFS apps (#474).+* Extend cFS backend with diagram mode (#476).+* Replace mentions of ICAROUS (#482).+* Adjust report command to accept multiple input files (#486).+* Apply multiple style fixes (#492).+* Adjust cFS app template to allow customizing MIDs (#494).+* Allow variable DB topics to carry extra info available to cFS template (#496).+* Make variable field names available to ROS template when present (#499).+* Adjust ROS template to enable injecting dependencies (#500).+* Bump upper version constraints on Copilot packages (#501).+* Update cFS template for cFS 7.0 (#509).+* Update `Dockerfile` in ROS 2 template for Space ROS `jazzy-2026.04.0` (#512).+ ## [1.14.0] - 2026-05-21  * Version bump (1.14.0) (#425).

@@ -19,7 +19,7 @@ build-type:          Simple  name:                ogma-core-version:             1.14.0+version:             1.15.0 homepage:            https://github.com/nasa/ogma bug-reports:         https://github.com/nasa/ogma/issues license:             Apache-2.0@@ -71,6 +71,7 @@                      templates/fprime/Copilot.cpp                      templates/fprime/Copilot.fpp                      templates/fprime/Copilot.hpp+                     templates/fprime/Copilot.hs                      templates/fprime/Dockerfile                      templates/fprime/instance-copilot                      templates/report/Report.md@@ -109,9 +110,11 @@     Command.Report     Command.Result     Command.ROSApp+    Command.Search     Command.Standalone      Data.Location+    Data.Project      Language.Trans.CStruct2CopilotStruct     Language.Trans.CStructs2Copilot@@ -149,9 +152,10 @@     , aeson                   >= 2.0.0.0  && < 2.3     , bytestring              >= 0.10.8.2 && < 0.13     , containers              >= 0.5      && < 0.8-    , copilot-core            >= 4.6.1    && < 4.8-    , copilot-language        >= 4.6.1    && < 4.8-    , copilot-theorem         >= 4.6.1    && < 4.8+    , copilot-core            >= 4.7.1    && < 4.9+    , copilot-language        >= 4.7.1    && < 4.9+    , copilot-libraries       >= 4.7.1    && < 4.9+    , copilot-theorem         >= 4.7.1    && < 4.9     , directory               >= 1.3.1.5  && < 1.4     , filepath                >= 1.4.2    && < 1.6     , graphviz                >= 2999.20  && < 2999.21@@ -163,16 +167,16 @@     , vector                  >= 0.12.0.1 && < 0.14     , yaml                    >= 0.11.7.0 && < 0.12 -    , ogma-extra              >= 1.14.0 && < 1.15-    , ogma-language-c         >= 1.14.0 && < 1.15-    , ogma-language-copilot   >= 1.14.0 && < 1.15-    , ogma-language-csv       >= 1.14.0 && < 1.15-    , ogma-language-jsonspec  >= 1.14.0 && < 1.15-    , ogma-language-lustre    >= 1.14.0 && < 1.15-    , ogma-language-smv       >= 1.14.0 && < 1.15-    , ogma-language-xlsx      >= 1.14.0 && < 1.15-    , ogma-language-xmlspec   >= 1.14.0 && < 1.15-    , ogma-spec               >= 1.14.0 && < 1.15+    , ogma-extra              >= 1.15.0 && < 1.16+    , ogma-language-c         >= 1.15.0 && < 1.16+    , ogma-language-copilot   >= 1.15.0 && < 1.16+    , ogma-language-csv       >= 1.15.0 && < 1.16+    , ogma-language-jsonspec  >= 1.15.0 && < 1.16+    , ogma-language-lustre    >= 1.15.0 && < 1.16+    , ogma-language-smv       >= 1.15.0 && < 1.16+    , ogma-language-xlsx      >= 1.15.0 && < 1.16+    , ogma-language-xmlspec   >= 1.15.0 && < 1.16+    , ogma-spec               >= 1.15.0 && < 1.16    hs-source-dirs:     src

@@ -1,6 +1,5 @@ {-# LANGUAGE DeriveGeneric             #-} {-# LANGUAGE ExistentialQuantification #-}-{-# LANGUAGE MultiWayIf                #-} {-# LANGUAGE ScopedTypeVariables       #-} -- Copyright 2020 United States Government as represented by the Administrator -- of the National Aeronautics and Space Administration. All Rights Reserved.@@ -39,8 +38,9 @@ -- External imports import           Control.Applicative    ( liftA2, (<|>) ) import qualified Control.Exception      as E-import           Control.Monad.Except   ( ExceptT (..), liftEither )-import           Data.Aeson             ( ToJSON (..) )+import           Control.Monad.Except   ( ExceptT (..), liftEither,+                                          throwError )+import           Data.Aeson             ( ToJSON (..), Value ) import           Data.Maybe             ( fromMaybe, mapMaybe, maybeToList ) import           GHC.Generics           ( Generic ) @@ -54,15 +54,26 @@ import System.Directory.Extra ( copyTemplate )  -- Internal imports-import Command.Common-import Command.Errors     (ErrorCode, ErrorTriplet (..))-import Command.VariableDB (Connection (..), TopicDef (..), TypeDef (..),-                           VariableDB, findConnection, findInput, findTopic,-                           findType, findTypeByType)-import Data.Aeson.Extra   (mergeObjects)-import Data.ExprPair      (ExprPair(..), exprPair)-import Data.Location      (Location (..))-import Data.Spec.Parser   (readInputExpr)+import Command.Common                 (InputFile (..), cannotCopyTemplate,+                                       checkArguments, combineInputFiles,+                                       locateTemplateDir, makeLeftE,+                                       openVarDBFilesWithDefault,+                                       parseInputFile,+                                       parseRequirementsListFile,+                                       parseTemplateVarsFile,+                                       parseVariablesFile, processResult,+                                       specExtractExternalVariables,+                                       specExtractHandlers)+import Command.Errors                 (ErrorCode, ErrorTriplet (..))+import Command.VariableDB             (Connection (..), TopicDef (..),+                                       TypeDef (..), VariableDB, findConnection,+                                       findInput, findTopic, findType,+                                       findTypeByType, inputActive)+import Data.Aeson.Extra               (mergeObjects)+import Data.ExprPair                  (ExprPair (..), exprPair)+import Data.Location                  (Location (..))+import Data.Spec.Parser               (readInputExpr)+import Language.Trans.Diagram2Copilot (DiagramMode (..))  -- | Generate a new CFS application connected to Copilot. command :: CommandOptions@@ -97,22 +108,29 @@     rs    <- parseRequirementsListFile handlersFile     varDB <- openVarDBFilesWithDefault varDBFile -    specT <- maybe (return Nothing) (\e -> Just . InputFileSpec <$> readInputExpr' e) cExpr+    specT <- maybe+               (return Nothing)+               (\e -> Just . InputFileSpec <$> readInputExpr' e)+               cExpr+     specF <- if null fpA-                  then return Nothing-                  else do-                    fpA' <- mapM readInputFile' fpA-                    let fpA'' = combineInputFiles fpA'-                    if length fpA'' > 1-                      then liftEither $ Left commandMultipleInputTypes-                      else pure $ Just $ head fpA''+               then return Nothing+               else do+                 fpA' <- mapM readInputFile' fpA+                 let fpA'' = combineInputFiles fpA'+                 if length fpA'' > 1+                   then liftEither $ Left commandMultipleInputTypes+                   else pure $ Just $ head fpA''      let spec = specT <|> specF      liftEither $ checkArguments spec vs rs -    copilotM <- sequenceA $ (\spec' -> processSpec spec' cExpr fpA) <$> spec+    mode <- parseDiagramMode (commandDiagramMode options) +    copilotM <- sequenceA $+                  (\spec' -> processSpec spec' cExpr fpA mode) <$> spec+     let varNames = fromMaybe (defaultVarNames spec) vs         monitors = maybe (defaultMonitors spec) (map (\x -> (x, Nothing))) rs @@ -138,20 +156,24 @@     readInputFile' f =       parseInputFile f formatName propFormatName propVia exprT -    processSpec spec' expr' fp' =-      Command.Standalone.commandLogic expr' fp' "copilot" [] exprT spec'+    processSpec spec' expr' fp' mode =+      Command.Standalone.commandLogic expr' fp' "copilot" [] exprT spec' mode      defaultVarNames spec = case spec of       Just (InputFileSpec spec') -> specExtractExternalVariables (Just spec')       Just (InputFileDiagram _)  -> []       Nothing                    -> specExtractExternalVariables Nothing -     defaultMonitors spec = case spec of       Just (InputFileSpec spec') -> specExtractHandlers (Just spec')       Just (InputFileDiagram _)  -> [ ("handler", Just "uint8_t" ) ]       Nothing                    -> specExtractHandlers Nothing +    parseDiagramMode :: String -> ExceptT ErrorTriplet IO DiagramMode+    parseDiagramMode "check"     = return CheckState+    parseDiagramMode "calculate" = return ComputeState+    parseDiagramMode mode        = throwError $ commandWrongDiagramMode mode+ -- | Generate a variable substitution map for a cFS application. commandLogic :: VariableDB              -> [String]@@ -177,29 +199,31 @@ -- applications. data CommandOptions = CommandOptions   { commandConditionExpr :: Maybe String   -- ^ Trigger condition.-  , commandInputFiles  :: [FilePath]     -- ^ Input specification files.-  , commandTargetDir   :: FilePath       -- ^ Target directory where the-                                         -- application should be created.-  , commandTemplateDir :: Maybe FilePath -- ^ Directory where the template is-                                         -- to be found.-  , commandVariables   :: Maybe FilePath -- ^ File containing a list of-                                         -- variables to make available to-                                         -- Copilot.-  , commandVariableDB  :: Maybe FilePath -- ^ File containing a list of known-                                         -- variables with their types and the-                                         -- message IDs they can be obtained-                                         -- from.-  , commandHandlers    :: Maybe FilePath -- ^ File containing a list of-                                         -- handlers used in the Copilot-                                         -- specification. The handlers are-                                         -- assumed to receive no arguments.-  , commandFormat      :: String         -- ^ Format of the input file.-  , commandPropFormat  :: String         -- ^ Format used for input properties.-  , commandPropVia     :: Maybe String   -- ^ Use external command to-                                         -- pre-process system properties.-  , commandExtraVars   :: Maybe FilePath -- ^ File containing additional-                                         -- variables to make available to the-                                         -- template.+  , commandInputFiles    :: [FilePath]     -- ^ Input specification files.+  , commandTargetDir     :: FilePath       -- ^ Target directory where the+                                           -- application should be created.+  , commandTemplateDir   :: Maybe FilePath -- ^ Directory where the template is+                                           -- to be found.+  , commandVariables     :: Maybe FilePath -- ^ File containing a list of+                                           -- variables to make available to+                                           -- Copilot.+  , commandVariableDB    :: Maybe FilePath -- ^ File containing a list of known+                                           -- variables with their types and+                                           -- the message IDs they can be+                                           -- obtained from.+  , commandHandlers      :: Maybe FilePath -- ^ File containing a list of+                                           -- handlers used in the Copilot+                                           -- specification. The handlers are+                                           -- assumed to receive no arguments.+  , commandFormat        :: String         -- ^ Format of the input file.+  , commandPropFormat    :: String         -- ^ Format used for input+                                           -- properties.+  , commandPropVia       :: Maybe String   -- ^ Use external command to+                                           -- pre-process system properties.+  , commandDiagramMode   :: String         -- ^ Diagram mode.+  , commandExtraVars     :: Maybe FilePath -- ^ File containing additional+                                           -- variables to make available to+                                           -- the template.   }  -- | Return the variable information needed to generate declarations@@ -208,28 +232,30 @@             -> String             -> Maybe (VarDecl, MsgInfoId, MsgInfo, MsgData) variableMap varDB varName = do-    inputDef  <- findInput varDB varName-    mid       <- connectionTopic <$> findConnection inputDef "cfs"-    topicDef  <- findTopic varDB "cfs" mid+  inputDef  <- findInput varDB varName+  mid       <- connectionTopic <$> findConnection inputDef "cfs"+  topicDef  <- findTopic varDB "cfs" mid -    let typeDef = findType varDB varName "cfs" "C"+  let extra = topicExtra topicDef -    let typeMsgFromType  = typeFromType <$> typeDef-        typeMsgFromField = typeFromField =<< typeDef+  let typeDef = findType varDB varName "cfs" "C" -    let typeVar' = fromMaybe (topicType topicDef) (typeToType <$> typeDef)+  let typeMsgFromType  = typeFromType <$> typeDef+      typeMsgFromField = typeFromField =<< typeDef -    -- Pick name for the function to process a message ID.-    let mn = pascalCase $ stripSuffix "_MID" mid+      active = inputActive inputDef -    return ( VarDecl varName typeVar'-           , mid-           , MsgInfo mid mn-           , MsgData mn typeMsgFromType typeMsgFromField varName typeVar'-           )+  let typeVar' = fromMaybe (topicType topicDef) (typeToType <$> typeDef) -  where+  -- Pick name for the function to process a message ID.+  let mn = pascalCase $ stripSuffix "_MID" mid +  return ( VarDecl varName typeVar'+         , mid+         , MsgInfo mid mn extra+         , MsgData mn typeMsgFromType typeMsgFromField varName typeVar' active+         )+ -- | Return the monitor information needed to generate declarations and -- publishers for the given monitor info, and variable database. monitorMap :: VariableDB@@ -256,8 +282,9 @@ -- | A message ID to subscribe to and the name associated to it. The name is -- used to generate a suitable name for the message handler. data MsgInfo = MsgInfo-    { msgInfoId   :: MsgInfoId-    , msgInfoDesc :: String+    { msgInfoId    :: MsgInfoId+    , msgInfoDesc  :: String+    , msgInfoExtra :: Value     }   deriving (Generic) @@ -271,6 +298,7 @@     , msgDataFromField :: Maybe String     , msgDataVarName   :: String     , msgDataVarType   :: String+    , msgDataActive    :: Bool     }   deriving (Generic) @@ -288,13 +316,13 @@  -- | Data that may be relevant to generate a cFS monitoring application. data AppData = AppData-  { variables   :: [VarDecl]-  , msgIds      :: [MsgInfoId]-  , msgCases    :: [MsgInfo]-  , msgHandlers :: [MsgData]-  , triggers    :: [Trigger]-  , copilot     :: Maybe Command.Standalone.AppData-  }+    { variables   :: [VarDecl]+    , msgIds      :: [MsgInfoId]+    , msgCases    :: [MsgInfo]+    , msgHandlers :: [MsgData]+    , triggers    :: [Trigger]+    , copilot     :: Maybe Command.Standalone.AppData+    }   deriving (Generic)  instance ToJSON AppData@@ -311,3 +339,16 @@ -- | Error: multiple inputs of incompatible types. ecMultipleInputTypes :: ErrorCode ecMultipleInputTypes = 1++-- | Error message associated to providing a diagram mode not supported by the+-- cFS backend.+commandWrongDiagramMode :: String -> ErrorTriplet+commandWrongDiagramMode mode =+    ErrorTriplet ecWrongDiagramMode msg LocationNothing+  where+    msg = "The diagram mode provided " ++ show mode ++ " is not known or is "+       ++ "not supported by this backend."++-- | Error: wrong diagram mode.+ecWrongDiagramMode :: ErrorCode+ecWrongDiagramMode = 1

@@ -1,5 +1,4 @@ {-# LANGUAGE ExistentialQuantification #-}-{-# LANGUAGE MultiWayIf                #-} {-# LANGUAGE OverloadedStrings         #-} {-# LANGUAGE ScopedTypeVariables       #-} -- Copyright 2022 United States Government as represented by the Administrator

@@ -33,6 +33,7 @@ import Control.Exception    as E import Control.Monad.Except (runExceptT) import Data.Aeson           (object, (.=))+import Data.Char            (toLower) import Data.Foldable        (for_) import Data.Text.Lazy       (pack) import System.FilePath      ((</>))@@ -40,28 +41,17 @@ -- External imports: auxiliary import System.Directory.Extra ( copyTemplate ) --- External imports: parsing expressions.-import qualified Language.Lustre.AbsLustre as Lustre-import qualified Language.Lustre.ParLustre as Lustre (myLexer, pBoolSpec)-import qualified Language.SMV.AbsSMV       as SMV-import qualified Language.SMV.ParSMV       as SMV (myLexer, pBoolSpec)- -- Internal imports: auxiliary-import Command.Errors      (ErrorTriplet (..))-import Command.Result      (Result (..))-import Data.Diagram.Parser (DiagramFormat (..), readDiagram)-import Data.ExprPair       (ExprPair (..), ExprPairT (..))-import Data.Location       (Location (..))-import Paths_ogma_core     (getDataDir)+import           Command.Errors      (ErrorTriplet (..))+import           Command.Result      (Result (..))+import           Data.Diagram.Parser (DiagramFormat (..), readDiagram)+import           Data.ExprPair       (ExprPair (..), ExprPairT (..))+import qualified Data.ExprPair+import           Data.Location       (Location (..))+import           Paths_ogma_core     (getDataDir)  -- Internal imports: language ASTs, transformers-import           Language.SMV.Substitution      (substituteBoolExpr)-import           Language.Trans.Diagram2Copilot (DiagramMode (..),-                                                 diagram2CopilotSpec)-import qualified Language.Trans.Lustre2Copilot  as Lustre (boolSpec2Copilot,-                                                           boolSpecNames)-import           Language.Trans.SMV2Copilot     as SMV (boolSpec2Copilot,-                                                        boolSpecNames)+import Language.Trans.Diagram2Copilot (DiagramMode (..), diagram2CopilotSpec)  -- | Generate a new Copilot monitor that implements a state machine described -- in a diagram given as an input file.@@ -194,13 +184,6 @@ -- | Return a handler depending on the format used for edge or transition -- properties. exprPair :: DiagramPropFormat -> ExprPair-exprPair Lustre = ExprPair $-  ExprPairT-    (Lustre.pBoolSpec . Lustre.myLexer)-    (\_ -> id)-    Lustre.boolSpec2Copilot-    Lustre.boolSpecNames-    (Lustre.BoolSpecSignal (Lustre.Ident "undefined")) exprPair Inputs = ExprPair $   ExprPairT     ((Right . read) :: String -> Either String Int)@@ -208,19 +191,6 @@     (\x -> "input == " ++ show x)     (const [])     (-1)-exprPair Literal = ExprPair $-  ExprPairT-    Right-    (\_ -> id)-    id-    (const [])-    "undefined"-exprPair SMV = ExprPair $-  ExprPairT-    (SMV.pBoolSpec . SMV.myLexer)-    substituteBoolExpr-    SMV.boolSpec2Copilot-    SMV.boolSpecNames-    (SMV.BoolSpecSignal (SMV.Ident "undefined"))---- * Backend+exprPair f = Data.ExprPair.exprPair (formatName f)+  where+    formatName = map toLower . show

@@ -1,6 +1,5 @@-{-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE DeriveGeneric             #-}-{-# LANGUAGE MultiWayIf                #-}+{-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE OverloadedStrings         #-} {-# LANGUAGE ScopedTypeVariables       #-} -- Copyright 2022 United States Government as represented by the Administrator@@ -49,14 +48,24 @@ import Command.Result (Result (..))  -- Internal imports-import Command.Common-import Command.Errors     (ErrorCode, ErrorTriplet (..))-import Command.VariableDB (InputDef (..), TypeDef (..), VariableDB, findInput,-                           findType, findTypeByType)-import Data.Aeson.Extra   (mergeObjects)-import Data.ExprPair      (ExprPair(..), exprPair)-import Data.Location      (Location (..))-import Data.Spec.Parser   (readInputExpr)+import Command.Common                 (InputFile (..), cannotCopyTemplate,+                                       checkArguments, combineInputFiles,+                                       locateTemplateDir, makeLeftE,+                                       openVarDBFilesWithDefault,+                                       parseInputFile,+                                       parseRequirementsListFile,+                                       parseTemplateVarsFile,+                                       parseVariablesFile, processResult,+                                       specExtractExternalVariables,+                                       specExtractHandlers)+import Command.Errors                 (ErrorCode, ErrorTriplet (..))+import Command.VariableDB             (InputDef (..), TypeDef (..), VariableDB,+                                       findInput, findType, findTypeByType)+import Data.Aeson.Extra               (mergeObjects)+import Data.ExprPair                  (ExprPair (..), exprPair)+import Data.Location                  (Location (..))+import Data.Spec.Parser               (readInputExpr)+import Language.Trans.Diagram2Copilot (DiagramMode (..))  -- | Generate a new FPrime component connected to Copilot. command :: CommandOptions -- ^ Options to the ROS backend.@@ -91,15 +100,19 @@     rs    <- parseRequirementsListFile handlersFile     varDB <- openVarDBFilesWithDefault varDBFile -    specT <- maybe (return Nothing) (\e -> Just . InputFileSpec <$> readInputExpr' e) cExpr+    specT <- maybe+               (return Nothing)+               (\e -> Just . InputFileSpec <$> readInputExpr' e)+               cExpr+     specF <- if null fpA-                  then return Nothing-                  else do-                    fpA' <- mapM readInputFile' fpA-                    let fpA'' = combineInputFiles fpA'-                    if length fpA'' > 1-                      then liftEither $ Left commandMultipleInputTypes-                      else pure $ Just $ head fpA''+               then return Nothing+               else do+                 fpA' <- mapM readInputFile' fpA+                 let fpA'' = combineInputFiles fpA'+                 if length fpA'' > 1+                   then liftEither $ Left commandMultipleInputTypes+                   else pure $ Just $ head fpA''      let spec = specT <|> specF @@ -134,14 +147,20 @@       parseInputFile f formatName propFormatName propVia exprT      processSpec spec' expr' fp' =-      Command.Standalone.commandLogic expr' fp' "copilot" [] exprT spec'+      Command.Standalone.commandLogic+        expr'+        fp'+        "copilot"+        []+        exprT+        spec'+        ComputeState      defaultVarNames spec = case spec of       Just (InputFileSpec spec') -> specExtractExternalVariables (Just spec')       Just (InputFileDiagram _)  -> []       Nothing                    -> specExtractExternalVariables Nothing -     defaultMonitors spec = case spec of       Just (InputFileSpec spec') -> specExtractHandlers (Just spec')       Just (InputFileDiagram _)  -> [ ("handler", Just "uint8_t" ) ]@@ -153,29 +172,30 @@ -- applications. data CommandOptions = CommandOptions   { commandConditionExpr :: Maybe String   -- ^ Trigger condition.-  , commandInputFiles  :: [FilePath]     -- ^ Input specification files.-  , commandTargetDir   :: FilePath       -- ^ Target directory where the-                                         -- component should be created.-  , commandTemplateDir :: Maybe FilePath -- ^ Directory where the template is-                                         -- to be found.-  , commandVariables   :: Maybe FilePath -- ^ File containing a list of-                                         -- variables to make available to-                                         -- Copilot.-  , commandVariableDB  :: Maybe FilePath -- ^ File containing a list of known-                                         -- variables with their types and the-                                         -- message IDs they can be obtained-                                         -- from.-  , commandHandlers    :: Maybe FilePath -- ^ File containing a list of-                                         -- handlers used in the Copilot-                                         -- specification. The handlers are-                                         -- assumed to receive no arguments.-  , commandFormat      :: String         -- ^ Format of the input file.-  , commandPropFormat  :: String         -- ^ Format used for input properties.-  , commandPropVia     :: Maybe String   -- ^ Use external command to-                                         -- pre-process system properties.-  , commandExtraVars   :: Maybe FilePath -- ^ File containing additional-                                         -- variables to make available to the-                                         -- template.+  , commandInputFiles    :: [FilePath]     -- ^ Input specification files.+  , commandTargetDir     :: FilePath       -- ^ Target directory where the+                                           -- component should be created.+  , commandTemplateDir   :: Maybe FilePath -- ^ Directory where the template is+                                           -- to be found.+  , commandVariables     :: Maybe FilePath -- ^ File containing a list of+                                           -- variables to make available to+                                           -- Copilot.+  , commandVariableDB    :: Maybe FilePath -- ^ File containing a list of known+                                           -- variables with their types and+                                           -- the message IDs they can be+                                           -- obtained from.+  , commandHandlers      :: Maybe FilePath -- ^ File containing a list of+                                           -- handlers used in the Copilot+                                           -- specification. The handlers are+                                           -- assumed to receive no arguments.+  , commandFormat        :: String         -- ^ Format of the input file.+  , commandPropFormat    :: String         -- ^ Format used for input+                                           -- properties.+  , commandPropVia       :: Maybe String   -- ^ Use external command to+                                           -- pre-process system properties.+  , commandExtraVars     :: Maybe FilePath -- ^ File containing additional+                                           -- variables to make available to+                                           -- the template.   }  -- | Return the variable information needed to generate declarations@@ -225,10 +245,10 @@  -- | Data that may be relevant to generate a ROS application. data AppData = AppData-  { variables :: [VarDecl]-  , monitors  :: [Monitor]-  , copilot   :: Maybe Command.Standalone.AppData-  }+    { variables :: [VarDecl]+    , monitors  :: [Monitor]+    , copilot   :: Maybe Command.Standalone.AppData+    }   deriving (Generic)  instance ToJSON AppData

@@ -23,12 +23,16 @@ module Command.Overview     ( command     , CommandOptions(..)+    , OverviewFile(..)     , CommandSummary(..)+    , CommandSummaryRequirements(..)+    , CommandSummaryDiagram(..)     , ErrorCode     )   where  -- External imports+import Control.Monad        (foldM) import Control.Monad.Except (runExceptT) import Data.Aeson           (ToJSON (..)) import GHC.Generics         (Generic)@@ -57,16 +61,30 @@ -- used are valid C99 identifiers. The template, if provided, exists and uses -- the variables needed by the overview application generator. The target -- directory is writable and there's enough disk space to copy the files over.-command :: FilePath        -- ^ Path to a file containing a specification-        -> CommandOptions -- ^ Customization options+command :: CommandOptions -- ^ Customization options         -> IO (Maybe CommandSummary, Result ErrorCode)-command fp options = do-  let functions = exprPair (commandPropFormat options)+command options = do+    fs <- foldM+            processFile+            (Right emptyCommandSummary)+            (commandInputFiles options) -  copilot <- command' fp options functions+    return $ commandResult options fs -  return $ commandResult options fp copilot+  where +    processFile :: Either (FilePath, String) CommandSummary+                -> OverviewFile+                -> IO (Either (FilePath, String) CommandSummary)+    processFile acc file = case acc of+      Left _     -> return acc+      Right acc' -> do+        let functions = exprPair (overviewFilePropFormat file)+        c <- command' (overviewFilePath file) file functions+        case c of+          Left msg -> return $ Left (overviewFilePath file, msg)+          Right s  -> return $ Right $ mergeCommandSummary acc' s+ -- | Generate overview of a spec given in an input file. -- -- PRE: The file given is readable, contains a valid file with recognizable@@ -76,7 +94,7 @@ -- the variables needed by the overview application generator. The target -- directory is writable and there's enough disk space to copy the files over. command' :: FilePath-          -> CommandOptions+          -> OverviewFile           -> ExprPair           -> IO (Either String CommandSummary) command' fp options (ExprPair exprT) = do@@ -87,10 +105,14 @@        Right (InputFileDiagram diagramR) -> do         analysisResult <- analyzeDiagram diagramR-        pure $ Right $-          CommandSummaryDiagram-            (numStates analysisResult)-            (deterministic analysisResult)+        pure $ Right $ emptyCommandSummary+                         { commandSummaryDiagrams =+                             [ CommandSummaryDiagram+                                 fp+                                 (numStates analysisResult)+                                 (deterministic analysisResult)+                             ]+                         }        Right (InputFileSpec spec') -> do         let specCompleted = addMissingIdentifiers ids spec'@@ -107,42 +129,91 @@           numFalses   <- SpecAnalysis.numAlwaysFalse <$> specFormalAnalysis           consistent  <- SpecAnalysis.consistent     <$> specFormalAnalysis -          pure $-            CommandSummaryRequirement-              numExterns numInternal numReqs numTrues numFalses consistent+          pure $ emptyCommandSummary+                   { commandSummaryRequirements =+                       [ CommandSummaryRequirements+                           fp+                           numExterns+                           numInternal+                           numReqs+                           numTrues+                           numFalses+                           consistent+                      ]+                   }    where -    formatName     = commandFormat options-    propFormatName = commandPropFormat options-    propVia        = commandPropVia options+    formatName     = overviewFileFormat options+    propFormatName = overviewFilePropFormat options+    propVia        = overviewFilePropVia options      ExprPairT _parse replace printExpr ids _def = exprT -data CommandSummary-    = CommandSummaryRequirement-        { commandExternalVariables      :: Int-        , commandInternalVariables      :: Int-        , commandRequirements           :: Int-        , commandRequirementsTrue       :: Int-        , commandRequirementsFalse      :: Int-        , commandRequirementsConsistent :: Bool-        }-    | CommandSummaryDiagram-        { commandNumStates     :: Int-        , commandDeterministic :: Bool-        }+data CommandSummary = CommandSummary+    { commandSummaryRequirements :: [CommandSummaryRequirements]+    , commandSummaryDiagrams     :: [CommandSummaryDiagram]+    }   deriving (Generic, Show)  instance ToJSON CommandSummary +-- | Summary with empty data.+emptyCommandSummary :: CommandSummary+emptyCommandSummary = CommandSummary [] []++-- | Merge two summaries.+mergeCommandSummary :: CommandSummary -> CommandSummary -> CommandSummary+mergeCommandSummary c1 c2 = CommandSummary+  { commandSummaryRequirements =+      commandSummaryRequirements c1 ++ commandSummaryRequirements c2+  , commandSummaryDiagrams =+      commandSummaryDiagrams c1 ++ commandSummaryDiagrams c2+  }++instance Semigroup CommandSummary where+  (<>) = mergeCommandSummary++instance Monoid CommandSummary where+  mempty  = emptyCommandSummary++-- | Requirement data for inclusion in the summary.+data CommandSummaryRequirements = CommandSummaryRequirements+    { commandRequirementsFile       :: FilePath+    , commandExternalVariables      :: Int+    , commandInternalVariables      :: Int+    , commandRequirements           :: Int+    , commandRequirementsTrue       :: Int+    , commandRequirementsFalse      :: Int+    , commandRequirementsConsistent :: Bool+    }+  deriving (Generic, Show)++instance ToJSON CommandSummaryRequirements++-- | Diagram Data for inclusion in the summary.+data CommandSummaryDiagram = CommandSummaryDiagram+    { commandDiagramFile          :: FilePath+    , commandDiagramNumStates     :: Int+    , commandDiagramDeterministic :: Bool+    }+  deriving (Generic, Show)++instance ToJSON CommandSummaryDiagram+ -- | Options used to customize the interpretation of input specifications. data CommandOptions = CommandOptions-  { commandFormat     :: String-  , commandPropFormat :: String-  , commandPropVia    :: Maybe String+  { commandInputFiles :: [ OverviewFile ]   } +-- | Information about one file in the command options.+data OverviewFile = OverviewFile+  { overviewFilePath       :: FilePath+  , overviewFileFormat     :: String+  , overviewFilePropFormat :: String+  , overviewFilePropVia    :: Maybe String+  }+ -- * Error codes  -- | Error: the input file cannot be read due to it being unreadable or the@@ -154,9 +225,8 @@  -- | Process the result of the transformation function. commandResult :: CommandOptions-              -> FilePath-              -> Either String a+              -> Either (FilePath, String) a               -> (Maybe a, Result ErrorCode)-commandResult _options fp result = case result of-  Left msg -> (Nothing, Error ecOverviewError msg (LocationFile fp))-  Right t  -> (Just t,  Success)+commandResult _options result = case result of+  Left (fp, msg) -> (Nothing, Error ecOverviewError msg (LocationFile fp))+  Right t        -> (Just t,  Success)

@@ -1,6 +1,5 @@-{-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE DeriveGeneric             #-}-{-# LANGUAGE MultiWayIf                #-}+{-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE OverloadedStrings         #-} {-# LANGUAGE ScopedTypeVariables       #-} -- Copyright 2022 United States Government as represented by the Administrator@@ -53,15 +52,26 @@ import Command.Result (Result (..))  -- Internal imports-import Command.Common-import Command.Errors     (ErrorCode, ErrorTriplet (..))-import Command.VariableDB (Connection (..), InputDef (..), TopicDef (..),-                           TypeDef (..), VariableDB, findConnection, findInput,-                           findTopic, findType, findTypeByType)-import Data.Aeson.Extra   (mergeObjects)-import Data.ExprPair      (ExprPair(..), exprPair)-import Data.Location      (Location (..))-import Data.Spec.Parser   (readInputExpr)+import Command.Common                 (InputFile (..), cannotCopyTemplate,+                                       checkArguments, combineInputFiles,+                                       locateTemplateDir, makeLeftE,+                                       openVarDBFilesWithDefault,+                                       parseInputFile,+                                       parseRequirementsListFile,+                                       parseTemplateVarsFile,+                                       parseVariablesFile, processResult,+                                       specExtractExternalVariables,+                                       specExtractHandlers)+import Command.Errors                 (ErrorCode, ErrorTriplet (..))+import Command.VariableDB             (Connection (..), InputDef (..),+                                       TopicDef (..), TypeDef (..), VariableDB,+                                       findConnection, findInput, findTopic,+                                       findType, findTypeByType)+import Data.Aeson.Extra               (mergeObjects)+import Data.ExprPair                  (ExprPair (..), exprPair)+import Data.Location                  (Location (..))+import Data.Spec.Parser               (readInputExpr)+import Language.Trans.Diagram2Copilot (DiagramMode (..))  -- | Generate a new ROS application connected to Copilot. command :: CommandOptions -- ^ Options to the ROS backend.@@ -96,15 +106,19 @@     rs    <- parseRequirementsListFile handlersFile     varDB <- openVarDBFilesWithDefault varDBFile -    specT <- maybe (return Nothing) (\e -> Just . InputFileSpec <$> readInputExpr' e) cExpr+    specT <- maybe+               (return Nothing)+               (\e -> Just . InputFileSpec <$> readInputExpr' e)+               cExpr+     specF <- if null fpA-                  then return Nothing-                  else do-                    fpA' <- mapM readInputFile' fpA-                    let fpA'' = combineInputFiles fpA'-                    if length fpA'' > 1-                      then liftEither $ Left commandMultipleInputTypes-                      else pure $ Just $ head fpA''+               then return Nothing+               else do+                 fpA' <- mapM readInputFile' fpA+                 let fpA'' = combineInputFiles fpA'+                 if length fpA'' > 1+                   then liftEither $ Left commandMultipleInputTypes+                   else pure $ Just $ head fpA''      let spec = specT <|> specF @@ -147,14 +161,20 @@       parseInputFile f formatName propFormatName propVia exprT      processSpec spec' expr' fp' =-      Command.Standalone.commandLogic expr' fp' "copilot" [] exprT spec'+      Command.Standalone.commandLogic+        expr'+        fp'+        "copilot"+        []+        exprT+        spec'+        ComputeState      defaultVarNames spec = case spec of       Just (InputFileSpec spec') -> specExtractExternalVariables (Just spec')       Just (InputFileDiagram _)  -> []       Nothing                    -> specExtractExternalVariables Nothing -     defaultMonitors spec = case spec of       Just (InputFileSpec spec') -> specExtractHandlers (Just spec')       Just (InputFileDiagram _)  -> [ ("handler", Just "uint8_t" ) ]@@ -169,33 +189,34 @@ -- applications. data CommandOptions = CommandOptions   { commandConditionExpr :: Maybe String   -- ^ Trigger condition.-  , commandInputFiles  :: [FilePath]     -- ^ Input specification files.-  , commandTargetDir   :: FilePath       -- ^ Target directory where the-                                         -- application should be created.-  , commandTemplateDir :: Maybe FilePath -- ^ Directory where the template is-                                         -- to be found.-  , commandVariables   :: Maybe FilePath -- ^ File containing a list of-                                         -- variables to make available to-                                         -- Copilot.-  , commandVariableDB  :: Maybe FilePath -- ^ File containing a list of known-                                         -- variables with their types and the-                                         -- message IDs they can be obtained-                                         -- from.-  , commandHandlers    :: Maybe FilePath -- ^ File containing a list of-                                         -- handlers used in the Copilot-                                         -- specification. The handlers are-                                         -- assumed to receive no arguments.-  , commandFormat      :: String         -- ^ Format of the input file.-  , commandPropFormat  :: String         -- ^ Format used for input properties.-  , commandPropVia     :: Maybe String   -- ^ Use external command to-                                         -- pre-process system properties.-  , commandExtraVars   :: Maybe FilePath -- ^ File containing additional-                                         -- variables to make available to the-                                         -- template.-  , commandTestingApps :: [Node]         -- ^ Additional applications to turn-                                         -- on during testing.-  , commandTestingVars :: [String]       -- ^ Limited list of variables to use-                                         -- for testing.+  , commandInputFiles    :: [FilePath]     -- ^ Input specification files.+  , commandTargetDir     :: FilePath       -- ^ Target directory where the+                                           -- application should be created.+  , commandTemplateDir   :: Maybe FilePath -- ^ Directory where the template is+                                           -- to be found.+  , commandVariables     :: Maybe FilePath -- ^ File containing a list of+                                           -- variables to make available to+                                           -- Copilot.+  , commandVariableDB    :: Maybe FilePath -- ^ File containing a list of known+                                           -- variables with their types and+                                           -- the message IDs they can be+                                           -- obtained from.+  , commandHandlers      :: Maybe FilePath -- ^ File containing a list of+                                           -- handlers used in the Copilot+                                           -- specification. The handlers are+                                           -- assumed to receive no arguments.+  , commandFormat        :: String         -- ^ Format of the input file.+  , commandPropFormat    :: String         -- ^ Format used for input+                                           -- properties.+  , commandPropVia       :: Maybe String   -- ^ Use external command to+                                           -- pre-process system properties.+  , commandExtraVars     :: Maybe FilePath -- ^ File containing additional+                                           -- variables to make available to+                                           -- the template.+  , commandTestingApps   :: [Node]         -- ^ Additional applications to turn+                                           -- on during testing.+  , commandTestingVars   :: [String]       -- ^ Limited list of variables to+                                           -- use for testing.   }  -- | Return the variable information needed to generate declarations@@ -214,8 +235,12 @@   let typeMsg' = fromMaybe                    (topicType topicDef)                    (typeFromType <$> findType varDB varName "ros/message" "C")-  return $ VarDecl varName typeVar' mid typeMsg' (randomBaseType typeVar') +      fieldMsg = typeFromField =<< findType varDB varName "ros/message" "C"++  return $+    VarDecl varName typeVar' mid typeMsg' fieldMsg (randomBaseType typeVar')+ -- | Return the monitor information needed to generate declarations and -- publishers for the given monitor info, and variable database. monitorMap :: VariableDB@@ -230,11 +255,12 @@  -- | The declaration of a variable in C, with a given type and name. data VarDecl = VarDecl-    { varDeclName    :: String-    , varDeclType    :: String-    , varDeclId      :: String-    , varDeclMsgType :: String-    , varDeclRandom  :: String+    { varDeclName     :: String+    , varDeclType     :: String+    , varDeclId       :: String+    , varDeclMsgType  :: String+    , varDeclMsgField :: Maybe String+    , varDeclRandom   :: String     }   deriving Generic @@ -262,12 +288,12 @@  -- | Data that may be relevant to generate a ROS application. data AppData = AppData-  { variables        :: [VarDecl]-  , monitors         :: [Monitor]-  , copilot          :: Maybe Command.Standalone.AppData-  , testingApps      :: [Node]-  , testingVariables :: [VarDecl]-  }+    { variables        :: [VarDecl]+    , monitors         :: [Monitor]+    , copilot          :: Maybe Command.Standalone.AppData+    , testingApps      :: [Node]+    , testingVariables :: [VarDecl]+    }   deriving (Generic)  instance ToJSON AppData

@@ -20,6 +20,7 @@ module Command.Report     ( command     , CommandOptions(..)+    , ReportFile(..)     , CommandSummary(..)     , ErrorCode     )@@ -27,7 +28,9 @@  -- External imports import qualified Control.Exception      as E-import           Control.Monad.Except   (ExceptT (..), liftEither, withExceptT)+import           Control.Monad          (foldM)+import           Control.Monad.Except   (ExceptT (..), liftEither, runExceptT,+                                         withExceptT) import           Control.Monad.IO.Class (liftIO) import           Data.Aeson             (ToJSON (..)) import           GHC.Generics           (Generic)@@ -67,9 +70,10 @@     -- Obtain template dir     templateDir <- locateTemplateDir mTemplateDir "report" -    let functions = exprPair (commandPropFormat options)--    reportData <- command' options functions+    reportData <- foldM+                    processFile+                    emptyCommandSummary+                    (commandInputFiles options)      -- Expand template     ExceptT $ fmap (makeLeftE cannotCopyTemplate) $ E.try $@@ -80,6 +84,14 @@     targetDir    = commandTargetDir options     mTemplateDir = commandTemplateDir options +    processFile :: CommandSummary+                -> ReportFile+                -> ExceptT ErrorTriplet IO CommandSummary+    processFile acc file = do+      let functions = exprPair (reportFilePropFormat file)+      s <- command' options functions file+      return $ mergeCommandSummary acc s+ -- | Generate report of a spec or diagram given in an input file. -- -- PRE: The file given is readable, contains a valid file with recognizable@@ -90,28 +102,23 @@ -- copy the files over. command' :: CommandOptions          -> ExprPair+         -> ReportFile          -> ExceptT ErrorTriplet IO CommandSummary-command' options (ExprPair exprT) = do+command' options (ExprPair exprT) file = do     res <- parseInputFile fp formatName propFormatName propVia exprT     case res of       InputFileDiagram diagramR -> do         analysisResult <- liftIO $ analyzeDiagram diagramR-        let diagramDetails = DiagramDetails+        let diagramDetails = CommandSummaryDiagram+                               fp                                (numStates analysisResult)                                (deterministic analysisResult)          pure $ CommandSummary-                 { commandExternalVariables      = 0-                 , commandInternalVariables      = 0-                 , commandRequirementsAny        = False-                 , commandRequirements           = 0-                 , commandRequirementsTrue       = 0-                 , commandRequirementsFalse      = 0-                 , commandRequirementsConsistent = True-                 , commandRequirementList        = []-                 , commandDiagramsAny            = True-                 , commandDiagrams               = 1-                 , commandDiagramList            = [diagramDetails]+                 { commandRequirementsAny = False+                 , commandRequirementList = []+                 , commandDiagramsList    = [ diagramDetails ]+                 , commandDiagramsAny     = True                  }        InputFileSpec spec -> withExceptT commandCannotAnalyzeF $ do@@ -140,26 +147,30 @@             falseReqs  = SpecAnalysis.alwaysFalseReq specFormalAnalysis             consistent = SpecAnalysis.consistent     specFormalAnalysis +            fileReqs   = CommandSummaryRequirements+                           { summaryRequirementsFile       = fp+                           , summaryExternalVariables      = numExterns+                           , summaryInternalVariables      = numInternal+                           , summaryRequirements           = numReqs+                           , summaryRequirementsTrue       = numTrues+                           , summaryRequirementsFalse      = numFalses+                           , summaryRequirementsConsistent = consistent+                           , summaryRequirementsDetails    = reqListDetails+                           }+         pure $ CommandSummary-                 { commandExternalVariables      = numExterns-                 , commandInternalVariables      = numInternal-                 , commandRequirementsAny        = numReqs > 0-                 , commandRequirements           = numReqs-                 , commandRequirementsTrue       = numTrues-                 , commandRequirementsFalse      = numFalses-                 , commandRequirementsConsistent = consistent-                 , commandRequirementList        = reqListDetails-                 , commandDiagramsAny            = False-                 , commandDiagrams               = 0-                 , commandDiagramList            = []+                 { commandRequirementsAny = length reqListDetails > 0+                 , commandRequirementList = [fileReqs]+                 , commandDiagramsAny     = False+                 , commandDiagramsList    = []                  }    where -    fp             = commandInputFile options-    formatName     = commandFormat options-    propFormatName = commandPropFormat options-    propVia        = commandPropVia options+    fp             = reportFilePath file+    formatName     = reportFileFormat file+    propFormatName = reportFilePropFormat file+    propVia        = reportFilePropVia file      ExprPairT _parse replace printExpr ids _def = exprT @@ -168,30 +179,60 @@ data CommandOptions = CommandOptions   { commandTargetDir   :: String   , commandTemplateDir :: Maybe String-  , commandInputFile   :: String-  , commandFormat      :: String-  , commandPropFormat  :: String-  , commandPropVia     :: Maybe String+  , commandInputFiles  :: [ ReportFile ]   } +-- | Information about one file in the command options.+data ReportFile = ReportFile+  { reportFilePath       :: FilePath+  , reportFileFormat     :: String+  , reportFilePropFormat :: String+  , reportFilePropVia    :: Maybe String+  }+ -- | Summary of the files read. data CommandSummary = CommandSummary-    { commandExternalVariables      :: Int-    , commandInternalVariables      :: Int-    , commandRequirementsAny        :: Bool-    , commandRequirements           :: Int-    , commandRequirementsTrue       :: Int-    , commandRequirementsFalse      :: Int-    , commandRequirementsConsistent :: Bool-    , commandRequirementList        :: [RequirementDetails]-    , commandDiagramsAny            :: Bool-    , commandDiagrams               :: Int-    , commandDiagramList            :: [DiagramDetails]+    { commandRequirementsAny :: Bool+    , commandRequirementList :: [CommandSummaryRequirements]+    , commandDiagramsAny     :: Bool+    , commandDiagramsList    :: [CommandSummaryDiagram]     }   deriving (Generic, Show)  instance ToJSON CommandSummary +-- | Summary with empty data.+emptyCommandSummary :: CommandSummary+emptyCommandSummary = CommandSummary False [] False []++-- | Merge two summaries.+mergeCommandSummary :: CommandSummary -> CommandSummary -> CommandSummary+mergeCommandSummary c1 c2 = CommandSummary+  { commandRequirementsAny =+      commandRequirementsAny c1 || commandRequirementsAny c2+  , commandRequirementList =+      commandRequirementList c1 ++ commandRequirementList c2+  , commandDiagramsAny =+      commandDiagramsAny c1 || commandDiagramsAny c2+  , commandDiagramsList =+      commandDiagramsList c1 ++ commandDiagramsList c2+  }++-- | Requirement data for inclusion in the summary.+data CommandSummaryRequirements = CommandSummaryRequirements+    { summaryRequirementsFile       :: FilePath+    , summaryExternalVariables      :: Int+    , summaryInternalVariables      :: Int+    , summaryRequirements           :: Int+    , summaryRequirementsTrue       :: Int+    , summaryRequirementsFalse      :: Int+    , summaryRequirementsConsistent :: Bool+    , summaryRequirementsDetails    :: [RequirementDetails]+    }+  deriving (Generic, Show)++instance ToJSON CommandSummaryRequirements+ -- | Information to include in a report about a requirement. data RequirementDetails = RequirementDetails     { summaryRequirementName  :: String@@ -204,13 +245,14 @@ instance ToJSON RequirementDetails  -- | Information to include in a report about a diagram.-data DiagramDetails = DiagramDetails-    { summaryDiagramNumStates     :: Int+data CommandSummaryDiagram = CommandSummaryDiagram+    { summaryDiagramFile          :: FilePath+    , summaryDiagramNumStates     :: Int     , summaryDiagramDeterministic :: Bool     }   deriving (Generic, Show) -instance ToJSON DiagramDetails+instance ToJSON CommandSummaryDiagram  -- * Errors 

@@ -0,0 +1,199 @@+{-# LANGUAGE DeriveGeneric #-}+-- Copyright 2025 United States Government as represented by the Administrator+-- of the National Aeronautics and Space Administration. All Rights Reserved.+--+-- Disclaimers+--+-- Licensed under the Apache License, Version 2.0 (the "License"); you may+-- not use this file except in compliance with the License. You may obtain a+-- copy of the License at+--+--      https://www.apache.org/licenses/LICENSE-2.0+--+-- Unless required by applicable law or agreed to in writing, software+-- distributed under the License is distributed on an "AS IS" BASIS, WITHOUT+-- WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the+-- License for the specific language governing permissions and limitations+-- under the License.+--+-- | Find elements in a project that meet a search query.+module Command.Search+    ( command+    , CommandOptions(..)+    , SearchFile(..)+    , CommandSearchResults(..)+    , RequirementInfo(..)+    , DiagramInfo(..)+    , ErrorCode+    )+  where++-- External imports+import Control.Monad        (foldM)+import Control.Monad.Except (runExceptT)+import Data.Aeson           (ToJSON (..))+import Data.List            (isInfixOf)+import GHC.Generics         (Generic)++-- External imports: ogma+import Data.OgmaSpec (Requirement (..), Spec (..))++-- Internal imports+import Command.Common (InputFile (..), parseInputFile)+import Command.Errors (ErrorCode, ErrorTriplet (..))+import Command.Result (Result (..))+import Data.Diagram   (Diagram (..))+import Data.ExprPair  (ExprPair (..), exprPair)+import Data.Location  (Location (..))++-- | Find elements in a project that meet a search query.+command :: CommandOptions -- ^ Customization options+        -> IO (Maybe CommandSearchResults, Result ErrorCode)+command options = do+    fs <- foldM+            processFile+            (Right emptyCommandSearchResults)+            (commandInputFiles options)++    return $ commandResult options fs++  where++    processFile :: Either (FilePath, String) CommandSearchResults+                -> SearchFile+                -> IO (Either (FilePath, String) CommandSearchResults)+    processFile acc file = case acc of+      Left _     -> return acc+      Right acc' -> do+        let functions = exprPair (searchFilePropFormat file)+        c <- command' file functions (commandSearchQuery options)+        case c of+          Left msg -> return $ Left (searchFilePath file, msg)+          Right s  -> return $ Right $ mergeCommandSearchResults acc' s++-- | Find elements in a file that meet a search query.+command' :: SearchFile+         -> ExprPair+         -> String+         -> IO (Either String CommandSearchResults)+command' file (ExprPair exprT) query = do+    res <- runExceptT $+             parseInputFile fp formatName propFormatName propVia exprT++    case res of+      Left (ErrorTriplet _ s _) -> return $ Left s++      Right (InputFileDiagram diagramR) ->+        return $ Right $ diagramResults fp diagramR query++      Right (InputFileSpec spec) ->+        return $ Right $ specResults fp spec query++  where++    fp             = searchFilePath file+    formatName     = searchFileFormat file+    propFormatName = searchFilePropFormat file+    propVia        = searchFilePropVia file++-- | Find elements in a spec that meet a search query.+specResults :: FilePath -> Spec a -> String -> CommandSearchResults+specResults file spec query = CommandSearchResults+  { searchResultRequirements =+      [ RequirementInfo file n d+      | r <- requirements spec+      , let n = requirementName r+      , let d = requirementDescription r+      , query `isInfixOf` n || query `isInfixOf` d+      ]+  , searchResultDiagrams = []+  }++-- | Find elements in a diagram that meet a search query.+diagramResults :: FilePath -> Diagram -> String -> CommandSearchResults+diagramResults file diagramR query = CommandSearchResults+  { searchResultRequirements = []+  , searchResultDiagrams =+      [ DiagramInfo file+      | any (\(f, t, d) -> query `isInfixOf` show f+                        || query `isInfixOf` t+                        || query `isInfixOf` show d)+        (diagramTransitions diagramR)+      ]+  }++-- | Options used to customize the interpretation of input specifications.+data CommandOptions = CommandOptions+  { commandInputFiles  :: [ SearchFile ]+  , commandSearchQuery :: String+  }++-- | Information about one file in the command options.+data SearchFile = SearchFile+  { searchFilePath       :: FilePath+  , searchFileFormat     :: String+  , searchFilePropFormat :: String+  , searchFilePropVia    :: Maybe String+  }++-- | Lists of search results.+data CommandSearchResults = CommandSearchResults+    { searchResultRequirements :: [RequirementInfo]+    , searchResultDiagrams     :: [DiagramInfo]+    }+  deriving (Generic, Show)++instance ToJSON CommandSearchResults++-- | Empty lists of search results.+emptyCommandSearchResults :: CommandSearchResults+emptyCommandSearchResults = CommandSearchResults+  { searchResultRequirements = []+  , searchResultDiagrams     = []+  }++-- | Merge lists of search results.+mergeCommandSearchResults :: CommandSearchResults+                          -> CommandSearchResults+                          -> CommandSearchResults+mergeCommandSearchResults c1 c2 = CommandSearchResults+  { searchResultRequirements =+      searchResultRequirements c1 ++ searchResultRequirements c2+  , searchResultDiagrams =+      searchResultDiagrams c1 ++ searchResultDiagrams c2+  }++-- | Information about a requirement that matches the search query.+data RequirementInfo = RequirementInfo+    { requirementInfoLocation    :: FilePath+    , requirementInfoName        :: String+    , requirementInfoDescription :: String+    }+  deriving (Generic, Show)++instance ToJSON RequirementInfo++-- | Information about a diagram that matches the search query.+data DiagramInfo = DiagramInfo+    { diagramInfoLocation :: FilePath+    }+  deriving (Generic, Show)++instance ToJSON DiagramInfo++-- * Error codes++-- | Error: the input file cannot be read due to it being unreadable or the+-- format being incorrect.+ecSearchError :: ErrorCode+ecSearchError = 1++-- * Result++-- | Process the result of the transformation function.+commandResult :: CommandOptions+              -> Either (FilePath, String) a+              -> (Maybe a, Result ErrorCode)+commandResult _options result = case result of+  Left (fp, msg) -> (Nothing, Error ecSearchError msg (LocationFile fp))+  Right t        -> (Just t,  Success)

@@ -1,6 +1,5 @@-{-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE DeriveGeneric             #-}-{-# LANGUAGE MultiWayIf                #-}+{-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE OverloadedStrings         #-} {-# LANGUAGE ScopedTypeVariables       #-} -- Copyright 2020 United States Government as represented by the Administrator@@ -42,12 +41,15 @@ import System.Directory.Extra (copyTemplate)  -- Internal imports-import Command.Common-import Command.Errors                 (ErrorCode, ErrorTriplet(..))+import Command.Common                 (InputFile (..), cannotCopyTemplate,+                                       combineInputFiles, locateTemplateDir,+                                       makeLeftE, parseInputFile,+                                       parseTemplateVarsFile, processResult)+import Command.Errors                 (ErrorCode, ErrorTriplet (..)) import Command.Result                 (Result (..)) import Data.Aeson.Extra               (mergeObjects) import Data.Either.Extra              (mapLeft)-import Data.ExprPair                  (ExprPair(..), ExprPairT(..), exprPair)+import Data.ExprPair                  (ExprPair (..), ExprPairT (..), exprPair) import Data.Location                  (Location (..)) import Data.Spec.Extra                (addMissingIdentifiers) import Data.Spec.Parser               (readInputExpr)@@ -102,21 +104,26 @@      -- Read spec and complement the specification with any missing/implicit     -- definitions.-    specT <- maybe (return Nothing) (\e -> Just . InputFileSpec <$> readInputExpr' e) triggerExprM+    specT <- maybe+               (return Nothing)+               (\e -> Just . InputFileSpec <$> readInputExpr' e)+               triggerExprM+     specF <- if null fpA-                  then return Nothing-                  else do-                    fpA' <- mapM readInputFile' fpA-                    let fpA'' = combineInputFiles fpA'-                    if length fpA'' > 1-                      then liftEither $ Left commandMultipleInputTypes-                      else pure $ Just $ head fpA''+               then return Nothing+               else do+                 fpA' <- mapM readInputFile' fpA+                 let fpA'' = combineInputFiles fpA'+                 if length fpA'' > 1+                   then liftEither $ Left commandMultipleInputTypes+                   else pure $ Just $ head fpA''      let spec = specT <|> specF      case spec of       Nothing    -> liftEither $ Left $ commandMissingSpec-      Just spec' -> commandLogic triggerExprM fpA name typeMaps exprT spec'+      Just spec' ->+        commandLogic triggerExprM fpA name typeMaps exprT spec' ComputeState    where     triggerExprM   = commandConditionExpr options@@ -133,7 +140,6 @@     readInputFile' f =       parseInputFile f formatName propFormatName propVia exprT - -- | Generate the data of a new standalone Copilot monitor that implements the -- spec, using a subexpression handler. commandLogic :: Maybe String@@ -142,34 +148,37 @@              -> [(String, String)]              -> ExprPairT a              -> InputFile a+             -> DiagramMode              -> ExceptT ErrorTriplet IO AppData-commandLogic expr fps name typeMaps exprT (InputFileDiagram d) =+commandLogic expr fps name typeMaps exprT (InputFileDiagram d) mode =     return $ AppData [] int [] trigs name   where-    (int, trigs) = diagram2CopilotSpec d ComputeState--commandLogic expr fps name typeMaps exprT (InputFileSpec input) = do-    let spec = addMissingIdentifiers ids input-    -- Analyze the spec for incorrect identifiers and convert it to Copilot.-    -- If there is an error, we change the error to a message we control.-    let appData = mapLeft commandIncorrectSpec' $ do-          spec' <- specAnalyze spec-          res   <- spec2Copilot name typeMaps replace print spec'--          -- Pack the results-          let (ext, int, reqs, trigs, specN) = res+    (int, trigs) = diagram2CopilotSpec d mode -          return $ AppData ext int reqs trigs specN+commandLogic expr fps name typeMaps exprT (InputFileSpec input) _mode =      liftEither appData    where +    -- Analyze the spec for incorrect identifiers and convert it to Copilot.+    -- If there is an error, we change the error to a message we control.+    appData = mapLeft commandIncorrectSpec' $ do+      spec' <- specAnalyze spec+      res   <- spec2Copilot name typeMaps replace print spec'++      -- Pack the results+      let (ext, int, reqs, trigs, specN) = res++      return $ AppData ext int reqs trigs specN+     commandIncorrectSpec' = case (expr, fps) of       (Nothing,    [])   -> error "Both expression and file are missing"       (Nothing,    fps') -> commandIncorrectSpecF       (Just expr', _)    -> commandIncorrectSpecE expr' +    spec = addMissingIdentifiers ids input+     ExprPairT parse replace print ids def = exprT  -- ** Argument processing@@ -178,24 +187,24 @@ -- code. data CommandOptions = CommandOptions   { commandConditionExpr :: Maybe String-  , commandInputFiles  :: [FilePath]         -- ^ Input specification file(s).-  , commandTargetDir   :: FilePath           -- ^ Target directory where the-                                             -- application should be created.-  , commandTemplateDir :: Maybe FilePath     -- ^ Directory where the template-                                             -- is to be found.-  , commandFormat      :: String             -- ^ Format of the input file.-  , commandPropFormat  :: String             -- ^ Format used for input-                                             -- properties.-  , commandTypeMapping :: [(String, String)]-  , commandFilename    :: String-  , commandPropVia     :: Maybe String       -- ^ Use external command to-                                             -- pre-process system properties.-  , commandExtraVars   :: Maybe FilePath -- ^ File containing additional-                                         -- variables to make available to the-                                         -- template.+  , commandInputFiles    :: [FilePath]         -- ^ Input specification file(s).+  , commandTargetDir     :: FilePath           -- ^ Target directory where the+                                               -- application should be created.+  , commandTemplateDir   :: Maybe FilePath     -- ^ Directory where the template+                                               -- is to be found.+  , commandFormat        :: String             -- ^ Format of the input file.+  , commandPropFormat    :: String             -- ^ Format used for input+                                               -- properties.+  , commandTypeMapping   :: [(String, String)]+  , commandFilename      :: String+  , commandPropVia       :: Maybe String       -- ^ Use external command to+                                               -- pre-process system properties.+  , commandExtraVars     :: Maybe FilePath     -- ^ File containing additional+                                               -- variables to make available+                                               -- to the template.   } --- * Mapping of types from input format to Copilot+-- | Mapping of types from input format to Copilot. typeToCopilotTypeMapping :: [(String, String)] -> [(String, String)] typeToCopilotTypeMapping types =     [ ("bool",    "Bool")

@@ -1,5 +1,6 @@-{-# LANGUAGE DeriveGeneric   #-}-{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE DeriveGeneric     #-}+{-# LANGUAGE TemplateHaskell   #-}+{-# LANGUAGE OverloadedStrings #-} -- Copyright 2022 United States Government as represented by the Administrator -- of the National Aeronautics and Space Administration. All Rights Reserved. --@@ -36,7 +37,8 @@  -- External imports import Control.Monad.Except (ExceptT, throwError)-import Data.Aeson           (FromJSON (..))+import Data.Aeson           (FromJSON (..), Value (Object), (.:), withObject)+import Data.Aeson.KeyMap    (filterWithKey) import Data.Aeson.TH        (defaultOptions, deriveFromJSON, fieldLabelModifier) import Data.Char            (toLower) import Data.List            (find)@@ -64,6 +66,7 @@ data InputDef = InputDef     { inputName        :: String     , inputType        :: Maybe String+    , inputActive      :: Bool     , inputConnections :: [ Connection ]     }   deriving (Eq, Show)@@ -81,6 +84,7 @@     { topicScope :: String     , topicTopic :: String     , topicType  :: String+    , topicExtra :: Value  -- ^ Additional extra info.     }   deriving (Eq, Show) @@ -314,15 +318,27 @@ mergeMaybe x       Nothing = x mergeMaybe x       _       = x --- | Implement default instances of parser to read variable DB from JSON,--- dropping the prefix in each field name.+-- | Implement instances of parser to read variable DB from JSON, dropping the+-- prefix in each field name. deriveFromJSON   defaultOptions {fieldLabelModifier = toHead toLower . drop 4 }   ''TypeDef -deriveFromJSON-  defaultOptions {fieldLabelModifier = toHead toLower . drop 5 }-  ''TopicDef+instance FromJSON TopicDef where+  parseJSON = withObject "TopicDef" $ \obj -> do+    scope <- obj .: "scope"+    topic <- obj .: "topic"+    typeV <- obj .: "type"++    let extra = Object $+          filterWithKey (\k _ -> k `notElem` [ "scope", "topic", "type" ]) obj++    pure TopicDef+      { topicScope = scope+      , topicTopic = topic+      , topicType  = typeV+      , topicExtra = extra+      }  deriveFromJSON   defaultOptions {fieldLabelModifier = toHead toLower . drop 10 }

@@ -62,12 +62,13 @@ -- | Default imports for a 'Spec' that was converted into a 'Copilot.Spec'. defaultSpecImports :: [(String, Maybe String)] defaultSpecImports =-  [ ("Control.Monad.Writer",  Nothing)-  , ("Copilot.Language",      Nothing)-  , ("Copilot.Language.Spec", Nothing)-  , ("Data.Functor.Identity", Nothing)-  , ("Data.List",             Just "L")-  , ("Prelude",               Just "P")+  [ ("Control.Monad.Writer",          Nothing)+  , ("Copilot.Language",              Nothing)+  , ("Copilot.Language.Spec",         Nothing)+  , ("Copilot.Library.StateMachines", Nothing)+  , ("Data.Functor.Identity",         Nothing)+  , ("Data.List",                     Just "L")+  , ("Prelude",                       Just "P")   ]  -- | Render a 'Diagram' as a Haskell definition of a 'Copilot.Spec'.@@ -94,29 +95,7 @@ -- | Auxiliary definitions needed in the spec. auxiliaryDefinitions :: String auxiliaryDefinitions = unlines-  [ "stateMachine :: (Eq a, Typed a)"-  , "             => (a, a, Stream Bool, [(a, Stream Bool, a)], a)"-  , "             -> Stream a"-  , "stateMachine (initial, final, noInputData, transitions, bad) ="-  , "    state"-  , "  where"-  , "    state         = ifThenElses transitions"-  , "    previousState = [initial] ++ state"-  , ""-  , "    -- ifThenElses :: [(a, Stream Bool, a)] -> Stream a"-  , "    ifThenElses [] ="-  , "      ifThenElse"-  , "        (previousState == constant final && noInputData)"-  , "        (constant final)"-  , "        (constant bad)"-  , ""-  , "    ifThenElses ((s1, i, s2):ss) ="-  , "      ifThenElse"-  , "        (previousState == constant s1 && i)"-  , "        (constant s2)"-  , "        (ifThenElses ss)"-  , ""-  , "isDeterministic :: (Ord a, Eq a, Typed a)"+  [ "isDeterministic :: (Ord a, Eq a, Typed a)"   , "                => (a, a, Stream Bool, [(a, Stream Bool, a)], a)"   , "                -> Stream Bool"   , "isDeterministic (_, _, _, ts, _) = all $"

@@ -72,8 +72,8 @@   ExprPairT     (Lustre.pBoolSpec . Lustre.myLexer)     (\_ -> id)-    (Lustre.boolSpec2Copilot)-    (Lustre.boolSpecNames)+    Lustre.boolSpec2Copilot+    Lustre.boolSpecNames     (Lustre.BoolSpecSignal (Lustre.Ident "undefined")) exprPair "literal" = ExprPair $   ExprPairT@@ -86,9 +86,9 @@ exprPair _ = ExprPair $   ExprPairT     (SMV.pBoolSpec . SMV.myLexer)-    (substituteBoolExpr)-    (SMV.boolSpec2Copilot)-    (SMV.boolSpecNames)+    substituteBoolExpr+    SMV.boolSpec2Copilot+    SMV.boolSpecNames     (SMV.BoolSpecSignal (SMV.Ident "undefined"))  -- | Parse and print a value using an auxiliary Expression Pair.

@@ -0,0 +1,55 @@+{-# LANGUAGE DeriveGeneric #-}+-- Copyright 2024 United States Government as represented by the Administrator+-- of the National Aeronautics and Space Administration. All Rights Reserved.+--+-- Disclaimers+--+-- Licensed under the Apache License, Version 2.0 (the "License"); you may+-- not use this file except in compliance with the License. You may obtain a+-- copy of the License at+--+--      https://www.apache.org/licenses/LICENSE-2.0+--+-- Unless required by applicable law or agreed to in writing, software+-- distributed under the License is distributed on an "AS IS" BASIS, WITHOUT+-- WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the+-- License for the specific language governing permissions and limitations+-- under the License.+--+-- | Ogma projects.+module Data.Project where++-- External imports+import           Control.Exception (IOException, try)+import           Data.Aeson        (FromJSON, ToJSON, eitherDecodeStrict')+import qualified Data.ByteString   as BS+import           GHC.Generics      (Generic)++-- -- Internal imports+import Data.Either.Extra (mapLeft)++data Project = Project+    { projectName           :: Maybe String+    , projectInputFiles     :: [(FilePath, String, String)]+                               -- ^ File, format name, prop name+    , projectVariableFiles  :: Maybe FilePath+    , projectVariableDBFile :: Maybe FilePath+    , projectHandlerFile    :: Maybe FilePath+    , projectCommandPropVia :: Maybe FilePath+    , projectTemplateDir    :: Maybe FilePath+    , projectTargetDir      :: Maybe FilePath+    , projectExtraJSONFile  :: Maybe FilePath+    }+  deriving (Generic, Show)++instance FromJSON Project+instance ToJSON Project++-- | Read a project from a file.+readProject :: FilePath -> IO (Either String Project)+readProject path = do+  bytesResult <- try (BS.readFile path)+  pure $ case bytesResult of+           Left e      -> Left (show (e :: IOException))+           Right bytes -> mapLeft ("Failed to read project: " ++)+                        $ eitherDecodeStrict' bytes

@@ -123,9 +123,7 @@           if | isPrefixOf "XMLFormat" format              -> do let xmlFormat = read format                    content <- readFile fp-                   parseXMLSpec-                     (wrapper) (def) xmlFormat content-                     -- (fmap (fmap print) . wrapper) (print def) xmlFormat content+                   parseXMLSpec wrapper def xmlFormat content              | isPrefixOf "CSVFormat" format              -> do let csvFormat = read format                    content <- readFile fp@@ -139,7 +137,8 @@                    content <- B.safeReadFile fp                    case content of                      Left e  -> return $ Left e-                     Right b -> parseYAMLSpec wrapper yamlFormat (L.toStrict b)+                     Right b ->+                       parseYAMLSpec wrapper yamlFormat fp (L.toStrict b)              | otherwise              -> do let jsonFormat = read format                    content <- B.safeReadFile fp@@ -149,14 +148,13 @@                                      Left e  -> return $ Left e                                      Right v ->                                        parseJSONSpec-                                         (wrapper)+                                         wrapper                                          jsonFormat+                                         fp                                          v         case res of           Left e  -> return $ Left $ cannotOpenInputFile fp           Right x -> return $ Right x--  -- | Exception handler to deal with the case in which the trigger expression -- cannot be understood.

@@ -45,7 +45,7 @@     [ nameCStruct ++ " " ++ nameLocalVar ++ ";"     , ""     , "/**"-    , "* Make ICAROUS data available to Copilot and run monitors."+    , "* Make cFS data available to Copilot and run monitors."     , "*/"     , "void COPILOT_Process" ++ nameVar ++ "Monitor(void)"     , "{"

@@ -44,7 +44,7 @@   where     machine = unlines       [ "stateMachineS :: Stream Word8"-      , "stateMachineS = stateMachineGF stateMachine1"+      , "stateMachineS = stateMachine stateMachine1"       , ""       , "stateMachineProp :: Stream Bool"       , "stateMachineProp = " ++ propExpr

@@ -94,7 +94,7 @@                                 ]) implementation           where             propName = safeMap nameSubstitutions (internalVariableName i)-            implementation = (internalVariableExpr i)+            implementation = internalVariableExpr i      -- Encoding of requirements as boolean streams     reqs :: String@@ -123,8 +123,7 @@             -- transform the implementation into Copilot, applying a             -- substitution.             reqBody subs = reqName ++ " = " ++-                             (showExpr (exprTransform subs (requirementExpr i)))-+                             showExpr (exprTransform subs (requirementExpr i))      -- Main specification triggers     triggers :: String

@@ -25,12 +25,14 @@ import           Data.Aeson             (Value (..)) import           Data.Aeson.Key         (fromString) import qualified Data.Aeson.KeyMap      as M+import           Data.Bifunctor         (first) import qualified Data.ByteString        as BS import           Data.Char              (isSpace) import           Data.List              (intercalate) import           Data.Text              (unpack) import qualified Data.Vector            as V import qualified Data.Yaml              as Y+import           System.FilePath        (takeBaseName, takeFileName)  -- External imports: ogma-spec import Data.Either.Extra (mapLeft)@@ -47,7 +49,7 @@     , specExternalVarId         :: String     , specExternalVarType       :: Maybe String     , specRequirements          :: Maybe String-    , specRequirementId         :: Maybe String+    , specRequirementId         :: Maybe FieldSource     , specRequirementDesc       :: Maybe String     , specRequirementExpr       :: String     , specRequirementResultType :: Maybe String@@ -55,28 +57,63 @@     }   deriving (Read) +-- | Source used to populate the value of a field in a spec.+data FieldSource+    = Field String -- ^ A field of the YAML header+    | FileName     -- ^ Filename with extension+    | BaseName     -- ^ Filename without extension+  deriving (Show)++-- | Custom instance to read a 'FieldSource' that allows YAML field names to be+-- written down as plain strings.+instance Read FieldSource where+  readsPrec prec str =+    case lex str of+      [("Field", rest)]    -> first Field <$> readsPrec prec rest+      [("FileName", rest)] -> [(FileName, rest)]+      [("BaseName", rest)] -> [(BaseName, rest)]+      -- If it doesn't match a constructor, we attempt to read a string and+      -- treat it as the name of a YAML field.+      _                    -> first Field <$> readsPrec prec str+ -- | Parse a spec from a YAML file. parseYAMLSpec :: forall a               .  (String -> IO (Either String a))               -> YAMLFormat+              -> FilePath               -> BS.ByteString               -> IO (Either String (Spec a))-parseYAMLSpec parseExpr yamlFormat bs = runExceptT $ do+parseYAMLSpec parseExpr yamlFormat filepath bs = runExceptT $ do   value <- except $ mapLeft Y.prettyPrintParseException $ Y.decodeEither' bs    let values :: [Value]-      values = maybe [] (objectFieldValueList value) (specInternalVars yamlFormat)+      values =+        maybe [] (objectFieldValueList value) (specInternalVars yamlFormat)        internalVarDef :: Value -> Either String InternalVariableDef       internalVarDef value = do         let msg = "internal variable name"-        varId   <- valueToString msg =<< listToEither msg (objectFieldValues (specInternalVarId yamlFormat) value)+        varId   <- valueToString msg =<<+                     listToEither+                       msg+                       (objectFieldValues (specInternalVarId yamlFormat) value)          let msg = "internal variable type"-        varType <- maybe (Right "") (\e -> valueToString msg =<< (listToEither msg (objectFieldValues e value))) (specInternalVarType yamlFormat)+        varType <- maybe+                     (Right "")+                     (\e -> valueToString msg =<<+                              listToEither msg (objectFieldValues e value)+                     )+                     (specInternalVarType yamlFormat)          let msg = "internal variable expr"-        varExpr <- valueToString msg =<< listToEither msg (objectFieldValues (specInternalVarExpr yamlFormat) value)+        varExpr <- valueToString msg =<<+                     listToEither+                       msg+                       ( objectFieldValues+                           (specInternalVarExpr yamlFormat)+                           value+                       )          return $ InternalVariableDef                    { internalVariableName = varId@@ -87,17 +124,28 @@   internalVariableDefs <- except $ mapM internalVarDef values    let values :: [Value]-      values = maybe [] (objectFieldValueList value) (specExternalVars yamlFormat)+      values =+        maybe [] (objectFieldValueList value) (specExternalVars yamlFormat)        externalVarDef :: Value -> Either String ExternalVariableDef       externalVarDef value = do          let msg = "external variable name"         varId   <- valueToString msg-                      =<< listToEither msg (objectFieldValues (specExternalVarId yamlFormat) value)+                      =<< listToEither+                            msg+                            ( objectFieldValues+                                (specExternalVarId yamlFormat)+                                value+                            )          let msg = "external variable type"-        varType <- maybe (Right "") (\e -> valueToString msg =<< (listToEither msg (objectFieldValues e value))) (specExternalVarType yamlFormat)+        varType <- maybe+                     (Right "")+                     (\e -> valueToString msg =<<+                              listToEither msg (objectFieldValues e value)+                     )+                     (specExternalVarType yamlFormat)          return $ ExternalVariableDef                    { externalVariableName = varId@@ -107,28 +155,57 @@   externalVariableDefs <- except $ mapM externalVarDef values    let values :: [Value]-      values = maybe [value] (objectFieldValueList value) (specRequirements yamlFormat)+      values =+        maybe [value] (objectFieldValueList value) (specRequirements yamlFormat)        requirementDef value = do         let msg = "Requirement name"-        reqId <- except $ maybe (Right "") (\e -> valueToString msg =<< (listToEither msg (objectFieldValues e value))) (specRequirementId yamlFormat) +        -- Handle the case where the requirement ID is the file name, with or+        -- without extension.+        reqId <- case specRequirementId yamlFormat of+          Nothing        -> return ""+          Just FileName  -> return $ takeFileName filepath+          Just BaseName  -> return $ takeBaseName filepath+          Just (Field p) -> except $+            valueToString msg =<< listToEither msg (objectFieldValues p value)+         let msg = "Requirement expression"-        reqExpr <- except $ valueToString msg =<< listToEither msg (objectFieldValues (specRequirementExpr yamlFormat) value)+        reqExpr <- except $ valueToString msg =<<+                              listToEither+                                msg+                                ( objectFieldValues+                                    (specRequirementExpr yamlFormat)+                                    value+                                )         reqExpr' <- ExceptT $ parseExpr reqExpr          let msg = "Requirement description"-        reqDesc <- except $ maybe (Right "") (\e -> valueToString msg =<< (listToEither msg (objectFieldValues e value))) (specRequirementDesc yamlFormat)+        reqDesc <- except $+                     maybe+                       (Right "")+                       (\e -> valueToString msg =<<+                                listToEither msg (objectFieldValues e value)+                       )+                       (specRequirementDesc yamlFormat)         let reqDesc' = cleanString reqDesc          let msg = "Requirement result type"             ty :: Maybe (Either String String)-            ty = (\e -> valueToString msg =<< (listToEither msg (objectFieldValues e value))) <$> (specRequirementResultType yamlFormat)+            ty = (\e -> valueToString msg =<<+                          listToEither msg (objectFieldValues e value)+                 )+             <$> specRequirementResultType yamlFormat         reqResType <- except $ maybeEither ty          let msg = "Requirement result expression"             resultExpr :: Maybe (Either String String)-            resultExpr = (\e -> valueToString msg =<< (listToEither msg (objectFieldValues e value))) <$> (specRequirementResultExpr yamlFormat)+            resultExpr = (\e -> valueToString msg =<<+                                  listToEither+                                    msg+                                    (objectFieldValues e value)+                         )+                     <$> specRequirementResultExpr yamlFormat          reqResExpr  <- except $ maybeEither resultExpr         reqResExpr' <- ExceptT $ case reqResExpr of@@ -154,7 +231,8 @@ -- | Convert a string JSON value into a 'String'. valueToString :: String -> Value -> Either String String valueToString msg (String x) = Right $ unpack x-valueToString msg _          = Left $ "The YAML value provided for " ++ msg ++ " does not contain a string"+valueToString msg _          = Left $+  "The YAML value provided for " ++ msg ++ " does not contain a string"  -- | Object the values associated to a key of an object. --

@@ -12,9 +12,30 @@ #ifndef _copilot_cfs_msgids_h_ #define _copilot_cfs_msgids_h_ -#define COPILOT_CFS_CMD_MID     0x1882-#define COPILOT_CFS_SEND_HK_MID 0x1883-#define COPILOT_CFS_HK_TLM_MID  0x0883+{{#CFS_CMD_MID}}+#define COPILOT_CFS_CMD_MID        {{.}}+{{/CFS_CMD_MID}}+{{^CFS_CMD_MID}}+#define COPILOT_CFS_CMD_MID        0x1882+{{/CFS_CMD_MID}}+{{#CFS_REEVAL_CMD_MID}}+#define COPILOT_CFS_REEVAL_CMD_MID {{.}}+{{/CFS_REEVAL_CMD_MID}}+{{^CFS_REEVAL_CMD_MID}}+#define COPILOT_CFS_REEVAL_CMD_MID 0x1883+{{/CFS_REEVAL_CMD_MID}}+{{#CFS_SEND_HK_MID}}+#define COPILOT_CFS_SEND_HK_MID    {{.}}+{{/CFS_SEND_HK_MID}}+{{^CFS_SEND_HK_MID}}+#define COPILOT_CFS_SEND_HK_MID    0x1884+{{/CFS_SEND_HK_MID}}+{{#CFS_HK_TLM_MID}}+#define COPILOT_CFS_HK_TLM_MID     {{.}}+{{/CFS_HK_TLM_MID}}+{{^CFS_HK_TLM_MID}}+#define COPILOT_CFS_HK_TLM_MID     0x0883+{{/CFS_HK_TLM_MID}}  #endif /* _copilot_cfs_msgids_h_ */ 

@@ -1,14 +1,15 @@ {{#copilot}} import           Copilot.Compile.C99-import           Copilot.Language          hiding (prop)+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)+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           Copilot.Library.StateMachines (stateMachine)+import           Language.Copilot              (reify)+import           Prelude                       hiding ((&&), (||), (++), (<=), (>=), (<), (>), (==), (/=), not)  {{#copilot_extra_defs}} {{{.}}}@@ -33,31 +34,6 @@  notPreviousNot :: Stream Bool -> Stream Bool notPreviousNot = not . PTLTL.previous . not---- Initial state, final state, no transition signal, transitions, bad state-type StateMachineGF a = (a, a, Stream Bool, [(a, Stream Bool, a)], a)--stateMachineGF :: (Eq a, Typed a)-               => StateMachineGF a-               -> Stream a-stateMachineGF (initial, final, noInputData, transitions, bad) =-    state-  where-    state         = ifThenElses transitions-    previousState = [initial] ++ state--    -- ifThenElses :: [(a, Stream Bool, a)] -> Stream a-    ifThenElses [] =-      ifThenElse-        (previousState == constant final && noInputData)-        (constant final)-        (constant bad)--    ifThenElses ((s1, i, s2):ss) =-      ifThenElse-        (previousState == constant s1 && i)-        (constant s2)-        (ifThenElses ss)  -- | Complete specification. Calls C handler functions when properties are -- violated.

@@ -34,7 +34,8 @@  copilot_hk_tlm_t    COPILOT_HkTelemetryPkt; CFE_SB_PipeId_t    COPILOT_CommandPipe;-CFE_SB_MsgPtr_t    COPILOTMsgPtr;+CFE_MSG_Message_t *COPILOTMsgPtr;+CFE_SB_Buffer_t   *SBBufPtr;  static CFE_EVS_BinFilter_t  COPILOT_EventFilters[] =        {  /* Event ID    mask */@@ -49,22 +50,27 @@ /* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *  * *  * * * * **/ void COPILOT_AppMain( void ) {-    int32  status;-    uint32 RunStatus = CFE_ES_APP_RUN;+    CFE_Status_t status;+    uint32 RunStatus = CFE_ES_RunStatus_APP_RUN;      CFE_ES_PerfLogEntry(COPILOT_CFS_PERF_ID); -    COPILOT_AppInit();+    status = COPILOT_AppInit(); +    if (status != CFE_SUCCESS)+    {+        RunStatus = CFE_ES_RunStatus_APP_ERROR;+    }+     /*     ** COPILOT Runloop     */-    while (CFE_ES_RunLoop(&RunStatus) == TRUE)+    while (CFE_ES_RunLoop(&RunStatus) == true)     {         CFE_ES_PerfLogExit(COPILOT_CFS_PERF_ID);          /* Pend on receipt of command packet -- timeout set to 500 millisecs */-        status = CFE_SB_RcvMsg(&COPILOTMsgPtr, COPILOT_CommandPipe, 500);+        status = CFE_SB_ReceiveBuffer(&SBBufPtr, COPILOT_CommandPipe, 500);          CFE_ES_PerfLogEntry(COPILOT_CFS_PERF_ID); @@ -75,6 +81,8 @@      } +    CFE_ES_PerfLogExit(COPILOT_CFS_PERF_ID);+     CFE_ES_ExitApp(RunStatus);  } /* End of COPILOT_AppMain() */@@ -84,37 +92,75 @@ /* COPILOT_AppInit() --  initialization                                       */ /*                                                                            */ /* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * **/-void COPILOT_AppInit(void)+CFE_Status_t COPILOT_AppInit(void) {-    /*-    ** Register the app with Executive services-    */-    CFE_ES_RegisterApp() ;+    CFE_Status_t status;      /*     ** Register the events     */-    CFE_EVS_Register(COPILOT_EventFilters,+    status = CFE_EVS_Register(COPILOT_EventFilters,                      sizeof(COPILOT_EventFilters)/sizeof(CFE_EVS_BinFilter_t),-                     CFE_EVS_BINARY_FILTER);+                     CFE_EVS_EventFilter_BINARY); -    /*-    ** Create the Software Bus command pipe and subscribe to housekeeping-    **  messages-    */-    CFE_SB_CreatePipe(&COPILOT_CommandPipe, COPILOT_PIPE_DEPTH,"COPILOT_CMD_PIPE");+    if (status != CFE_SUCCESS)+    {+        CFE_ES_WriteToSysLog("Copilot App: Error Registering Events, RC = 0x%08lX\n", (unsigned long)status);+    }+    else+    {+        /*+        ** Create the Software Bus command pipe and subscribe to housekeeping+        **  messages+        */+        status = CFE_SB_CreatePipe(&COPILOT_CommandPipe, COPILOT_PIPE_DEPTH,"COPILOT_CMD_PIPE");++        if (status != CFE_SUCCESS)+        {+            CFE_EVS_SendEvent(COPILOT_CR_PIPE_ERR_EID,+                              CFE_EVS_EventType_ERROR,+                              "Copilot App: Error creating SB Command Pipe, RC = 0x%08lX",+                              (unsigned long)status);+        }+    }+     {{#msgIds}}-    CFE_SB_Subscribe({{.}}, COPILOT_CommandPipe);+    if (status == CFE_SUCCESS)+    {+        status = CFE_SB_Subscribe(CFE_SB_ValueToMsgId({{.}}), COPILOT_CommandPipe);++        if (status != CFE_SUCCESS)+        {+            CFE_EVS_SendEvent(COPILOT_CR_SUB_ERR_EID,+                              CFE_EVS_EventType_ERROR,+                              "Copilot App: Error subscribing to necessary messages, RC = 0x%08lX",+                              (unsigned long)status);+        }+    }     {{/msgIds}} +    if (status == CFE_SUCCESS)+    {+        status = CFE_SB_Subscribe(CFE_SB_ValueToMsgId(COPILOT_CFS_REEVAL_CMD_MID), COPILOT_CommandPipe); -    CFE_EVS_SendEvent (COPILOT_STARTUP_INF_EID, CFE_EVS_INFORMATION,+        if (status != CFE_SUCCESS)+        {+            CFE_EVS_SendEvent(COPILOT_CR_SUB_ERR_EID,+                              CFE_EVS_EventType_ERROR,+                              "Copilot App: Error subscribing to necessary messages, RC = 0x%08lX",+                              (unsigned long)status);+        }+    }++    CFE_EVS_SendEvent (COPILOT_STARTUP_INF_EID, CFE_EVS_EventType_INFORMATION,                "COPILOT App Initialized. Version %d.%d.%d.%d",                 COPILOT_CFS_MAJOR_VERSION,                 COPILOT_CFS_MINOR_VERSION,                 COPILOT_CFS_REVISION,                 COPILOT_CFS_MISSION_REV); +    return status;+ } /* End of COPILOT_AppInit() */  /* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * **/@@ -127,28 +173,42 @@ /* * * * * * * * * * * * * * * * * * * * * * * *  * * * * * * *  * *  * * * * */ void COPILOT_ProcessCommandPacket(void) {-    CFE_SB_MsgId_t  MsgId;+    {{#msgCases}}+    static CFE_SB_MsgId_t {{msgInfoId}}_s = CFE_SB_MSGID_RESERVED;+    {{/msgCases}} -    MsgId = CFE_SB_GetMsgId(COPILOTMsgPtr);+    static CFE_SB_MsgId_t COPILOT_CFS_REEVAL_CMD_MID_s = CFE_SB_MSGID_RESERVED; -    switch (MsgId)+    CFE_SB_MsgId_t MsgId = CFE_SB_INVALID_MSG_ID;++    if (!CFE_SB_IsValidMsgId(COPILOT_CFS_REEVAL_CMD_MID_s))     {+        COPILOT_CFS_REEVAL_CMD_MID_s = CFE_SB_ValueToMsgId(COPILOT_CFS_REEVAL_CMD_MID);         {{#msgCases}}-        case {{msgInfoId}}:-            COPILOT_Process{{msgInfoDesc}}();-            break;-+        {{msgInfoId}}_s = CFE_SB_ValueToMsgId({{msgInfoId}});         {{/msgCases}}--        default:-            COPILOT_HkTelemetryPkt.copilot_command_error_count++;-            CFE_EVS_SendEvent(COPILOT_COMMAND_ERR_EID,CFE_EVS_ERROR,-              "COPILOT: invalid command packet,MID = 0x%x", MsgId);-            break;     } -    return;+    CFE_MSG_GetMsgId(&SBBufPtr->Msg, &MsgId); +    if (CFE_SB_MsgId_Equal(MsgId, COPILOT_CFS_REEVAL_CMD_MID_s))+    {+        copilot_step();+    }+    {{#msgCases}}+    else if (CFE_SB_MsgId_Equal(MsgId, {{msgInfoId}}_s))+    {+        COPILOTMsgPtr = &SBBufPtr->Msg;+        COPILOT_Process{{msgInfoDesc}}();+    }+    {{/msgCases}}+    else+    {+        COPILOT_HkTelemetryPkt.copilot_command_error_count++;+        CFE_EVS_SendEvent(COPILOT_COMMAND_ERR_EID,CFE_EVS_EventType_ERROR,+          "COPILOT: invalid command packet,MID = 0x%x", CFE_SB_MsgIdToValue(MsgId));+    }+ } /* End COPILOT_ProcessCommandPacket */  {{#msgHandlers}}@@ -172,13 +232,13 @@     {{msgDataVarName}} = *msg;     {{/msgDataFromField}} +    {{#msgDataActive}}     // Run all copilot monitors.     copilot_step();+    {{/msgDataActive}} }  {{/msgHandlers}}-- {{#triggers}} /**  * Report copilot property violations.@@ -189,7 +249,7 @@ {{^triggerType}} void {{triggerName}}(void) { {{/triggerType}}-    CFE_EVS_SendEvent(COPILOT_COMMANDCPVIOL_INF_EID, CFE_EVS_ERROR,+    CFE_EVS_SendEvent(COPILOT_COMMANDCPVIOL_INF_EID, CFE_EVS_EventType_ERROR,         "COPILOT: violation: {{triggerName}}"); } {{/triggers}}

@@ -39,13 +39,13 @@ **       functions are not called from any other source module. */ void COPILOT_AppMain(void);-void COPILOT_AppInit(void);+CFE_Status_t COPILOT_AppInit(void); void COPILOT_ProcessCommandPacket(void); {{#msgCases}} void COPILOT_Process{{msgInfoDesc}}(void); {{/msgCases}} void COPILOT_ResetCounters(void); -boolean COPILOT_VerifyCmdLength(CFE_SB_MsgPtr_t msg, uint16 ExpectedLength);+bool COPILOT_VerifyCmdLength(CFE_MSG_Message_t *msg, size_t ExpectedLength);  #endif /* _copilot_app_h_ */

@@ -19,6 +19,8 @@ #define COPILOT_COMMANDCPVIOL_INF_EID       3 #define COPILOT_INVALID_MSGID_ERR_EID       4 #define COPILOT_LEN_ERR_EID                 5+#define COPILOT_CR_PIPE_ERR_EID             6+#define COPILOT_CR_SUB_ERR_EID              7  #endif /* _copilot_app_events_h_ */ 

@@ -18,7 +18,7 @@ */ typedef struct {-   uint8    CmdHeader[CFE_SB_CMD_HDR_SIZE];+   CFE_MSG_CommandHeader_t CmdHeader;  } COPILOT_NoArgsCmd_t; @@ -28,12 +28,12 @@ */ typedef struct {-    uint8              TlmHeader[CFE_SB_TLM_HDR_SIZE];-    uint8              copilot_command_error_count;-    uint8              copilot_command_count;-    uint8              spare[2];+    CFE_MSG_TelemetryHeader_t TlmHeader;+    uint8                     copilot_command_error_count;+    uint8                     copilot_command_count;+    uint8                     spare[2]; -}   OS_PACK copilot_hk_tlm_t  ;+}   copilot_hk_tlm_t  ;  #endif /* _copilot_cfs_msg_h_ */ 

@@ -1,16 +1,18 @@ import           Copilot.Compile.C99-import           Copilot.Language         hiding (max, min, prop)+import           Copilot.Language              hiding (max, min, prop) import           Copilot.Language.Prelude-import           Copilot.Library.LTL      (next)-import           Copilot.Library.MTL      hiding (alwaysBeen, since, trigger)-import qualified Copilot.Library.MTL      as MTL-import           Copilot.Library.PTLTL    (alwaysBeen, previous, since)-import qualified Copilot.Library.PTLTL    as PTLTL-import           Language.Copilot         (reify)-import           Language.Copilot         hiding (max, min)-import           Prelude                  hiding (max, min, mod, not, until,-                                           (&&), (++), (/=), (<), (<=), (==),-                                           (>), (>=), (||))+import           Copilot.Library.LTL           (next)+import           Copilot.Library.MTL           hiding (alwaysBeen, since,+                                                trigger)+import qualified Copilot.Library.MTL           as MTL+import           Copilot.Library.PTLTL         (alwaysBeen, previous, since)+import qualified Copilot.Library.PTLTL         as PTLTL+import           Copilot.Library.StateMachines (stateMachine)+import           Language.Copilot              (reify)+import           Language.Copilot              hiding (max, min)+import           Prelude                       hiding (max, min, mod, not,+                                                until, (&&), (++), (/=), (<),+                                                (<=), (==), (>), (>=), (||))  externalState :: Stream Word8 externalState = extern "{{{state}}}" Nothing@@ -28,21 +30,3 @@  main :: IO () main = reify spec >>= compile "{{{specName}}}"---- Initial state, final state, no transition signal, transitions, bad state-type StateMachineGF = ( Word8, Word8, Stream Bool, [(Word8, Stream Bool, Word8)], Word8)--stateMachineGF :: StateMachineGF -> Stream Word8-stateMachineGF (initialState, finalState, noInputData, transitions, badState) = state-  where-    state         = ifThenElses transitions-    previousState = [initialState] ++ state--    ifThenElses :: [(Word8, Stream Bool, Word8)] -> Stream Word8-    ifThenElses [] =-      ifThenElse (previousState == constant finalState && noInputData)-        (constant finalState)-        (constant badState)--    ifThenElses ((s1,i,s2):ss) =-      ifThenElse (previousState == constant s1 && i) (constant s2) (ifThenElses ss)

@@ -0,0 +1,49 @@+{{#copilot}}+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           Copilot.Library.StateMachines (stateMachine)+import           Language.Copilot              (reify)+import           Prelude                       hiding ((&&), (||), (++), (<=), (>=), (<), (>), (==), (/=), not)++{{#copilot_extra_defs}}+{{{.}}}+{{/copilot_extra_defs}}+{{{copilot.externs}}}+{{{copilot.internals}}}+{{{copilot.reqs}}}++-- | 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] ++)++notPreviousNot :: Stream Bool -> Stream Bool+notPreviousNot = not . PTLTL.previous . not++-- | Complete specification. Calls C handler functions when properties are+-- violated.+spec :: Spec+spec = do+{{{copilot.triggers}}}++main :: IO ()+main = reify spec >>= compile "{{{copilot.specName}}}"+{{/copilot}}+{{^copilot}}+-- No specification provided. Place your specification in this file.+{{/copilot}}

@@ -1,10 +1,11 @@ {{#commandDiagramsAny}} # Diagrams -{{#commandDiagramList}}+{{#commandDiagramsList}} ## Diagram -The diagram:+The diagram `{{summaryDiagramFile}}`:+  - Has {{summaryDiagramNumStates}} states. {{#summaryDiagramDeterministic}}  - Is deterministic.@@ -13,38 +14,40 @@  - Is not deterministic. {{/summaryDiagramDeterministic}} -{{/commandDiagramList}}+{{/commandDiagramsList}} {{/commandDiagramsAny}} {{#commandRequirementsAny}} # Requirements -## Summary+{{#commandRequirementList}}+## File `{{summaryRequirementsFile}}` -The project has {{commandRequirements}} requirements in total.+The file `{{summaryRequirementsFile}}` has {{summaryRequirements}} requirements+in total.  Of these requirements: -- {{commandRequirementsTrue}} requirements are constantly or always true.+- {{summaryRequirementsTrue}} requirements are constantly or always true. -- {{commandRequirementsFalse}} requirements are constantly or always false.+- {{summaryRequirementsFalse}} requirements are constantly or always false. -{{#commandRequirementsConsistent}}+{{#summaryRequirementsConsistent}} No inconsistencies detected in the requirements.-{{/commandRequirementsConsistent}}-{{^commandRequirementsConsistent}}+{{/summaryRequirementsConsistent}}+{{^summaryRequirementsConsistent}} The requirements are not mutually consistent: there is no way for all requirements to be true at the same time.-{{/commandRequirementsConsistent}}+{{/summaryRequirementsConsistent}}  The requirements mention: -- {{commandExternalVariables}} external variables.+- {{summaryExternalVariables}} external variables. -- {{commandInternalVariables}} internal variables.+- {{summaryInternalVariables}} internal variables.  ## Detailed list -{{#commandRequirementList}}+{{#summaryRequirementDetails}} ### {{summaryRequirementName}}  **Description:** {{summaryRequirementDesc}}@@ -63,5 +66,6 @@ {{/summaryRequirementFalse}} {{/summaryRequirementTrue}} +{{/summaryRequirementDetails}} {{/commandRequirementList}} {{/commandRequirementsAny}}

@@ -1,4 +1,4 @@-FROM osrf/space-ros:humble-2024.10.0+FROM osrf/space-ros:jazzy-2026.04.0  ARG USER=spaceros-user ARG PACKAGE_PATH=/home/${USER}/monitors@@ -13,9 +13,39 @@  SHELL ["/bin/bash", "-c"] WORKDIR ${PACKAGE_PATH}-RUN source /opt/spaceros/install/setup.bash && \-    colcon build --packages-select copilot           && \-    colcon build --packages-select test_requirements++ADD --chmod=644 https://raw.githubusercontent.com/ros/rosdistro/master/ros.key /usr/share/keyrings/ros-archive-keyring.gpg+RUN sudo apt-get update++ENV RMW_IMPLEMENTATION=rmw_cyclonedds_cpp+ENV ROS_DISTRO=jazzy++ADD manual-deps*.repos /tmp/+RUN if [ -f "/tmp/manual-deps.repos" ]; then \+      vcs import src < /tmp/manual-deps.repos; \+    fi++ADD excluded-pkgs*.txt /tmp/+RUN sudo rosdep init+RUN rosdep update+RUN source /opt/ros/spaceros/setup.bash && \+    if [ -f "/tmp/excluded-pkgs.txt" ]; then \+      rosdep install -y \+        --from-paths src --ignore-src \+        --rosdistro ${ROS_DISTRO} \+        --skip-keys "$(tr '\n' ' ' < '/tmp/excluded-pkgs.txt')"; \+    else \+      rosdep install -y \+        --from-paths src --ignore-src \+        --rosdistro ${ROS_DISTRO} ; \+    fi++ADD manually-installed-pkgs*.txt /tmp/+RUN source /opt/ros/spaceros/setup.bash && \+    colcon build --packages-select \+      copilot \+      test_requirements \+      $(find /tmp/ -maxdepth 1 -name "manually-installed-pkgs.txt" -exec cat {} +)  ADD screenrc /home/spaceros-user/.screenrc USER root

@@ -9,9 +9,18 @@ find_package(ament_cmake REQUIRED) find_package(rclcpp REQUIRED) find_package(std_msgs REQUIRED)+{{#target_extra_dependencies}}+find_package({{{.}}} REQUIRED)+{{/target_extra_dependencies}}  add_executable(copilot src/copilot_monitor.cpp)-ament_target_dependencies(copilot rclcpp std_msgs)+ament_target_dependencies(copilot+  rclcpp+  std_msgs+  {{#target_extra_dependencies}}+  {{{.}}}+  {{/target_extra_dependencies}}+)  # Uncomment to enable compiling the copilot logger # add_executable(copilot_logger src/copilot_logger.cpp)

@@ -8,11 +8,21 @@   <license>TODO: License declaration</license>    <buildtool_depend>ament_cmake</buildtool_depend>+  {{#package_extra_buildtool_depend}}+  <buildtool_depend>{{{.}}}</buildtool_depend>+  {{/package_extra_buildtool_depend}}+   <depend>rclcpp</depend>   <depend>std_msgs</depend>+  {{#package_extra_depend}}+  <depend>{{{.}}}</depend>+  {{/package_extra_depend}}    <test_depend>ament_lint_auto</test_depend>   <test_depend>ament_lint_common</test_depend>+  {{#package_extra_test_depend}}+  <test_depend>{{{.}}}</test_depend>+  {{/package_extra_test_depend}}    <export>     <build_type>ament_cmake</build_type>

@@ -1,14 +1,15 @@ {{#copilot}} import           Copilot.Compile.C99-import           Copilot.Language          hiding (prop)+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)+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           Copilot.Library.StateMachines (stateMachine)+import           Language.Copilot              (reify)+import           Prelude                       hiding ((&&), (||), (++), (<=), (>=), (<), (>), (==), (/=), not)  {{#copilot_extra_defs}} {{{.}}}@@ -33,31 +34,6 @@  notPreviousNot :: Stream Bool -> Stream Bool notPreviousNot = not . PTLTL.previous . not---- Initial state, final state, no transition signal, transitions, bad state-type StateMachineGF a = (a, a, Stream Bool, [(a, Stream Bool, a)], a)--stateMachineGF :: (Eq a, Typed a)-               => StateMachineGF a-               -> Stream a-stateMachineGF (initial, final, noInputData, transitions, bad) =-    state-  where-    state         = ifThenElses transitions-    previousState = [initial] ++ state--    -- ifThenElses :: [(a, Stream Bool, a)] -> Stream a-    ifThenElses [] =-      ifThenElse-        (previousState == constant final && noInputData)-        (constant final)-        (constant bad)--    ifThenElses ((s1, i, s2):ss) =-      ifThenElse-        (previousState == constant s1 && i)-        (constant s2)-        (ifThenElses ss)  -- | Complete specification. Calls C handler functions when properties are -- violated.

@@ -16,6 +16,9 @@ #include "std_msgs/msg/float32.hpp" #include "std_msgs/msg/float64.hpp" #include <cstdint>+{{#impl_extra_header}}+{{{.}}}+{{/impl_extra_header}} {{#copilot}} #include "{{{copilot.specName}}}_types.h" #include "{{{copilot.specName}}}.h"@@ -82,7 +85,12 @@   private:     {{#variables}}     void {{varDeclName}}_callback(const {{varDeclMsgType}}::SharedPtr msg) const {+      {{#varDeclMsgField}}+      {{varDeclName}} = msg->{{.}};+      {{/varDeclMsgField}}+      {{^varDeclMsgField}}       {{varDeclName}} = msg->data;+      {{/varDeclMsgField}}       step();     } 

@@ -9,10 +9,19 @@ find_package(ament_cmake REQUIRED) find_package(rclcpp REQUIRED) find_package(std_msgs REQUIRED)+{{#target_extra_dependencies}}+find_package({{{.}}} REQUIRED)+{{/target_extra_dependencies}}  # Uncomment to enable compiling the requirement tests add_executable(test_requirements src/test_requirements.cpp)-ament_target_dependencies(test_requirements rclcpp std_msgs)+ament_target_dependencies(test_requirements+  rclcpp+  std_msgs+  {{#target_extra_dependencies}}+  {{{.}}}+  {{/target_extra_dependencies}}+)  install(TARGETS   test_requirements

@@ -8,11 +8,21 @@   <license>TODO: License declaration</license>    <buildtool_depend>ament_cmake</buildtool_depend>+  {{#package_extra_buildtool_depend}}+  <buildtool_depend>{{{.}}}</buildtool_depend>+  {{/package_extra_buildtool_depend}}+   <depend>rclcpp</depend>   <depend>std_msgs</depend>+  {{#package_extra_depend}}+  <depend>{{{.}}}</depend>+  {{/package_extra_depend}}    <test_depend>ament_lint_auto</test_depend>   <test_depend>ament_lint_common</test_depend>+  {{#package_extra_test_depend}}+  <test_depend>{{{.}}}</test_depend>+  {{/package_extra_test_depend}}    <export>     <build_type>ament_cmake</build_type>

@@ -18,6 +18,9 @@ #include "std_msgs/msg/float32.hpp" #include "std_msgs/msg/float64.hpp" #include <cstdint>+{{#impl_extra_header}}+{{{.}}}+{{/impl_extra_header}}  using std::placeholders::_1; @@ -109,10 +112,18 @@     void tests_step_send () {  {{#testingVariables}}+       {{#varDeclMsgField}}+       {{varDeclType}} {{varDeclName}}_{{.}} = {{varDeclRandom}}();+       auto {{varDeclName}}_{{.}}_msg = {{varDeclMsgType}}();+       {{varDeclName}}_{{.}}_msg.{{.}} = {{varDeclName}}_{{.}};+       {{varDeclName}}_publisher_->publish({{varDeclName}}_{{.}}_msg);+       {{/varDeclMsgField}}+       {{^varDeclMsgField}}        {{varDeclType}} {{varDeclName}}_data = {{varDeclRandom}}();        auto {{varDeclName}}_data_msg = {{varDeclMsgType}}();        {{varDeclName}}_data_msg.data = {{varDeclName}}_data;        {{varDeclName}}_publisher_->publish({{varDeclName}}_data_msg);+       {{/varDeclMsgField}}  {{/testingVariables}} 

@@ -1,13 +1,14 @@ import           Copilot.Compile.C99-import           Copilot.Language          hiding (prop)+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)+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           Copilot.Library.StateMachines (stateMachine)+import           Language.Copilot              (reify)+import           Prelude                       hiding ((&&), (||), (++), (<=), (>=), (<), (>), (==), (/=), not)  {{#copilot_extra_defs}} {{{.}}}@@ -32,31 +33,6 @@  notPreviousNot :: Stream Bool -> Stream Bool notPreviousNot = not . PTLTL.previous . not---- Initial state, final state, no transition signal, transitions, bad state-type StateMachineGF a = (a, a, Stream Bool, [(a, Stream Bool, a)], a)--stateMachineGF :: (Eq a, Typed a)-               => StateMachineGF a-               -> Stream a-stateMachineGF (initial, final, noInputData, transitions, bad) =-    state-  where-    state         = ifThenElses transitions-    previousState = [initial] ++ state--    -- ifThenElses :: [(a, Stream Bool, a)] -> Stream a-    ifThenElses [] =-      ifThenElse-        (previousState == constant final && noInputData)-        (constant final)-        (constant bad)--    ifThenElses ((s1, i, s2):ss) =-      ifThenElse-        (previousState == constant s1 && i)-        (constant s2)-        (ifThenElses ss)  -- | Complete specification. Calls C handler functions when properties are -- violated.