diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -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).
diff --git a/ogma-core.cabal b/ogma-core.cabal
--- a/ogma-core.cabal
+++ b/ogma-core.cabal
@@ -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
diff --git a/src/Command/CFSApp.hs b/src/Command/CFSApp.hs
--- a/src/Command/CFSApp.hs
+++ b/src/Command/CFSApp.hs
@@ -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
diff --git a/src/Command/Common.hs b/src/Command/Common.hs
--- a/src/Command/Common.hs
+++ b/src/Command/Common.hs
@@ -1,5 +1,4 @@
{-# LANGUAGE ExistentialQuantification #-}
-{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
-- Copyright 2022 United States Government as represented by the Administrator
diff --git a/src/Command/Diagram.hs b/src/Command/Diagram.hs
--- a/src/Command/Diagram.hs
+++ b/src/Command/Diagram.hs
@@ -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
diff --git a/src/Command/FPrimeApp.hs b/src/Command/FPrimeApp.hs
--- a/src/Command/FPrimeApp.hs
+++ b/src/Command/FPrimeApp.hs
@@ -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
diff --git a/src/Command/Overview.hs b/src/Command/Overview.hs
--- a/src/Command/Overview.hs
+++ b/src/Command/Overview.hs
@@ -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)
diff --git a/src/Command/ROSApp.hs b/src/Command/ROSApp.hs
--- a/src/Command/ROSApp.hs
+++ b/src/Command/ROSApp.hs
@@ -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
diff --git a/src/Command/Report.hs b/src/Command/Report.hs
--- a/src/Command/Report.hs
+++ b/src/Command/Report.hs
@@ -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
diff --git a/src/Command/Search.hs b/src/Command/Search.hs
new file mode 100644
--- /dev/null
+++ b/src/Command/Search.hs
@@ -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)
diff --git a/src/Command/Standalone.hs b/src/Command/Standalone.hs
--- a/src/Command/Standalone.hs
+++ b/src/Command/Standalone.hs
@@ -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")
diff --git a/src/Command/VariableDB.hs b/src/Command/VariableDB.hs
--- a/src/Command/VariableDB.hs
+++ b/src/Command/VariableDB.hs
@@ -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 }
diff --git a/src/Data/Diagram/Analysis.hs b/src/Data/Diagram/Analysis.hs
--- a/src/Data/Diagram/Analysis.hs
+++ b/src/Data/Diagram/Analysis.hs
@@ -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 $"
diff --git a/src/Data/ExprPair.hs b/src/Data/ExprPair.hs
--- a/src/Data/ExprPair.hs
+++ b/src/Data/ExprPair.hs
@@ -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.
diff --git a/src/Data/Project.hs b/src/Data/Project.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Project.hs
@@ -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
diff --git a/src/Data/Spec/Parser.hs b/src/Data/Spec/Parser.hs
--- a/src/Data/Spec/Parser.hs
+++ b/src/Data/Spec/Parser.hs
@@ -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.
diff --git a/src/Language/Trans/CStructs2MsgHandlers.hs b/src/Language/Trans/CStructs2MsgHandlers.hs
--- a/src/Language/Trans/CStructs2MsgHandlers.hs
+++ b/src/Language/Trans/CStructs2MsgHandlers.hs
@@ -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)"
, "{"
diff --git a/src/Language/Trans/Diagram2Copilot.hs b/src/Language/Trans/Diagram2Copilot.hs
--- a/src/Language/Trans/Diagram2Copilot.hs
+++ b/src/Language/Trans/Diagram2Copilot.hs
@@ -44,7 +44,7 @@
where
machine = unlines
[ "stateMachineS :: Stream Word8"
- , "stateMachineS = stateMachineGF stateMachine1"
+ , "stateMachineS = stateMachine stateMachine1"
, ""
, "stateMachineProp :: Stream Bool"
, "stateMachineProp = " ++ propExpr
diff --git a/src/Language/Trans/Spec2Copilot.hs b/src/Language/Trans/Spec2Copilot.hs
--- a/src/Language/Trans/Spec2Copilot.hs
+++ b/src/Language/Trans/Spec2Copilot.hs
@@ -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
diff --git a/src/Language/YAMLSpec/Parser.hs b/src/Language/YAMLSpec/Parser.hs
--- a/src/Language/YAMLSpec/Parser.hs
+++ b/src/Language/YAMLSpec/Parser.hs
@@ -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.
--
diff --git a/templates/cfs/copilot/fsw/platform_inc/copilot_cfs_msgids.h b/templates/cfs/copilot/fsw/platform_inc/copilot_cfs_msgids.h
--- a/templates/cfs/copilot/fsw/platform_inc/copilot_cfs_msgids.h
+++ b/templates/cfs/copilot/fsw/platform_inc/copilot_cfs_msgids.h
@@ -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_ */
diff --git a/templates/cfs/copilot/fsw/src/Properties.hs b/templates/cfs/copilot/fsw/src/Properties.hs
--- a/templates/cfs/copilot/fsw/src/Properties.hs
+++ b/templates/cfs/copilot/fsw/src/Properties.hs
@@ -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.
diff --git a/templates/cfs/copilot/fsw/src/copilot_cfs.c b/templates/cfs/copilot/fsw/src/copilot_cfs.c
--- a/templates/cfs/copilot/fsw/src/copilot_cfs.c
+++ b/templates/cfs/copilot/fsw/src/copilot_cfs.c
@@ -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}}
diff --git a/templates/cfs/copilot/fsw/src/copilot_cfs.h b/templates/cfs/copilot/fsw/src/copilot_cfs.h
--- a/templates/cfs/copilot/fsw/src/copilot_cfs.h
+++ b/templates/cfs/copilot/fsw/src/copilot_cfs.h
@@ -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_ */
diff --git a/templates/cfs/copilot/fsw/src/copilot_cfs_events.h b/templates/cfs/copilot/fsw/src/copilot_cfs_events.h
--- a/templates/cfs/copilot/fsw/src/copilot_cfs_events.h
+++ b/templates/cfs/copilot/fsw/src/copilot_cfs_events.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_ */
diff --git a/templates/cfs/copilot/fsw/src/copilot_cfs_msg.h b/templates/cfs/copilot/fsw/src/copilot_cfs_msg.h
--- a/templates/cfs/copilot/fsw/src/copilot_cfs_msg.h
+++ b/templates/cfs/copilot/fsw/src/copilot_cfs_msg.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_ */
diff --git a/templates/diagram/Copilot.hs b/templates/diagram/Copilot.hs
--- a/templates/diagram/Copilot.hs
+++ b/templates/diagram/Copilot.hs
@@ -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)
diff --git a/templates/fprime/Copilot.hs b/templates/fprime/Copilot.hs
new file mode 100644
--- /dev/null
+++ b/templates/fprime/Copilot.hs
@@ -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}}
diff --git a/templates/report/Report.md b/templates/report/Report.md
--- a/templates/report/Report.md
+++ b/templates/report/Report.md
@@ -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}}
diff --git a/templates/ros/Dockerfile b/templates/ros/Dockerfile
--- a/templates/ros/Dockerfile
+++ b/templates/ros/Dockerfile
@@ -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
diff --git a/templates/ros/copilot/CMakeLists.txt b/templates/ros/copilot/CMakeLists.txt
--- a/templates/ros/copilot/CMakeLists.txt
+++ b/templates/ros/copilot/CMakeLists.txt
@@ -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)
diff --git a/templates/ros/copilot/package.xml b/templates/ros/copilot/package.xml
--- a/templates/ros/copilot/package.xml
+++ b/templates/ros/copilot/package.xml
@@ -8,11 +8,21 @@
TODO: License declaration
ament_cmake
+ {{#package_extra_buildtool_depend}}
+ {{{.}}}
+ {{/package_extra_buildtool_depend}}
+
rclcpp
std_msgs
+ {{#package_extra_depend}}
+ {{{.}}}
+ {{/package_extra_depend}}
ament_lint_auto
ament_lint_common
+ {{#package_extra_test_depend}}
+ {{{.}}}
+ {{/package_extra_test_depend}}
ament_cmake
diff --git a/templates/ros/copilot/src/Copilot.hs b/templates/ros/copilot/src/Copilot.hs
--- a/templates/ros/copilot/src/Copilot.hs
+++ b/templates/ros/copilot/src/Copilot.hs
@@ -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.
diff --git a/templates/ros/copilot/src/copilot_monitor.cpp b/templates/ros/copilot/src/copilot_monitor.cpp
--- a/templates/ros/copilot/src/copilot_monitor.cpp
+++ b/templates/ros/copilot/src/copilot_monitor.cpp
@@ -16,6 +16,9 @@
#include "std_msgs/msg/float32.hpp"
#include "std_msgs/msg/float64.hpp"
#include
+{{#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();
}
diff --git a/templates/ros/test_requirements/CMakeLists.txt b/templates/ros/test_requirements/CMakeLists.txt
--- a/templates/ros/test_requirements/CMakeLists.txt
+++ b/templates/ros/test_requirements/CMakeLists.txt
@@ -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
diff --git a/templates/ros/test_requirements/package.xml b/templates/ros/test_requirements/package.xml
--- a/templates/ros/test_requirements/package.xml
+++ b/templates/ros/test_requirements/package.xml
@@ -8,11 +8,21 @@
TODO: License declaration
ament_cmake
+ {{#package_extra_buildtool_depend}}
+ {{{.}}}
+ {{/package_extra_buildtool_depend}}
+
rclcpp
std_msgs
+ {{#package_extra_depend}}
+ {{{.}}}
+ {{/package_extra_depend}}
ament_lint_auto
ament_lint_common
+ {{#package_extra_test_depend}}
+ {{{.}}}
+ {{/package_extra_test_depend}}
ament_cmake
diff --git a/templates/ros/test_requirements/src/test_requirements.cpp b/templates/ros/test_requirements/src/test_requirements.cpp
--- a/templates/ros/test_requirements/src/test_requirements.cpp
+++ b/templates/ros/test_requirements/src/test_requirements.cpp
@@ -18,6 +18,9 @@
#include "std_msgs/msg/float32.hpp"
#include "std_msgs/msg/float64.hpp"
#include
+{{#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}}
diff --git a/templates/standalone/Copilot.hs b/templates/standalone/Copilot.hs
--- a/templates/standalone/Copilot.hs
+++ b/templates/standalone/Copilot.hs
@@ -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.