ogma-cli 1.6.0 → 1.7.0
raw patch · 13 files changed
+359/−98 lines, 13 filesdep ~ogma-core
Dependency ranges changed: ogma-core
Files
- CHANGELOG.md +22/−0
- ogma-cli.cabal +8/−3
- src/CLI/CommandCFSApp.hs +108/−20
- src/CLI/CommandDiagram.hs +2/−1
- src/CLI/CommandFPrimeApp.hs +35/−20
- src/CLI/CommandROSApp.hs +35/−20
- src/CLI/CommandStandalone.hs +34/−30
- src/Main.hs +1/−1
- tests/Main.hs +3/−3
- tests/fcs-example1.json +21/−0
- tests/fdb-example1.json +66/−0
- tests/reduced_geofence_msgs.h +12/−0
- tests/reduced_geofence_msgs_bad.h +12/−0
CHANGELOG.md view
@@ -1,5 +1,27 @@ # Revision history for ogma-cli +## [1.7.0] - 2025-03-21++* Version bump 1.7.0 (#269).+* Add all auxiliary test files to distributable Cabal package (#216).+* Remove extraneous EOL character (#224).+* Update installation instructions to use cabal install (#149).+* Update README with new cFS template variables (#229).+* Expose handlers-file argument to cFS backend (#234).+* Expose template-vars argument to cFS backend (#106).+* Document new template variables in README (#237).+* Fix formatting of template variables in README (#222).+* Update README with new ROS template variables (#244).+* Update README with new FPrime template variables (#246).+* Adjust CLI to match new backend API (#248).+* Expose template-vars argument to ROS, FPrime, standalone backends (#250).+* Expose spec processing arguments to cFS backend in CLI (#252).+* Use new sample spec with ROS backend in CI job (#107).+* Update examples, Github Actions, README to use new variable DB format (#256).+* Update README, ROS example with ability to pass data to handlers (#219).+* Update README, Github Actions with new dependencies (#263).+* Update to support boolean expressions in the Lustre language (#267).+ ## [1.6.0] - 2025-01-21 * Version bump 1.6.0 (#208).
ogma-cli.cabal view
@@ -15,7 +15,7 @@ -- ANY OTHER APPLICATIONS RESULTING FROM USE OF THE SUBJECT SOFTWARE. FURTHER, -- GOVERNMENT AGENCY DISCLAIMS ALL WARRANTIES AND LIABILITIES REGARDING -- THIRD-PARTY SOFTWARE, IF PRESENT IN THE ORIGINAL SOFTWARE, AND DISTRIBUTES--- IT "AS IS." +-- IT "AS IS." -- -- Waiver and Indemnity: RECIPIENT AGREES TO WAIVE ANY AND ALL CLAIMS AGAINST -- THE UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS, AS WELL AS@@ -32,7 +32,7 @@ build-type: Simple name: ogma-cli-version: 1.6.0+version: 1.7.0 homepage: https://github.com/nasa/ogma bug-reports: https://github.com/nasa/ogma/issues license: OtherLicense@@ -114,6 +114,11 @@ . - "<https://shemesh.larc.nasa.gov/people/cam/publications/FMAS2020_3.pdf From Requirements to Autonomous Flight>", Dutle et al. 2020. +extra-source-files: tests/fcs-example1.json+ tests/fdb-example1.json+ tests/reduced_geofence_msgs.h+ tests/reduced_geofence_msgs_bad.h+ -- Ogma packages should be uncurated so that only the official maintainers make -- changes. --@@ -145,7 +150,7 @@ build-depends: base >= 4.11.0.0 && < 5 , optparse-applicative >= 0.14 && < 0.19- , ogma-core >= 1.6.0 && < 1.7+ , ogma-core >= 1.7.0 && < 1.8 hs-source-dirs: src
src/CLI/CommandCFSApp.hs view
@@ -43,23 +43,30 @@ where -- External imports-import Options.Applicative ( Parser, help, long, metavar, optional, showDefault,- strOption, value )+import Options.Applicative ( Parser, help, long, metavar, optional, short,+ showDefault, strOption, value ) -- External imports: command results import Command.Result ( Result ) -- External imports: actions or commands supported-import Command.CFSApp ( ErrorCode, cFSApp )+import Command.CFSApp ( ErrorCode )+import qualified Command.CFSApp -- * Command -- | Options needed to generate the cFS application. data CommandOpts = CommandOpts- { cFSAppTarget :: String- , cFSAppTemplateDir :: Maybe String- , cFSAppVarNames :: String- , cFSAppVarDB :: Maybe String+ { cFSAppInputFile :: Maybe String+ , cFSAppTarget :: String+ , cFSAppTemplateDir :: Maybe String+ , cFSAppVarNames :: Maybe String+ , cFSAppVarDB :: Maybe String+ , cFSAppHandlers :: Maybe String+ , cFSAppFormat :: String+ , cFSAppPropFormat :: String+ , cFSAppPropVia :: Maybe String+ , cFSAppTemplateVars :: Maybe String } -- | Create <https://cfs.gsfc.nasa.gov/ NASA core Flight System> (cFS)@@ -68,12 +75,20 @@ -- -- This is just an uncurried version of "Command.CFSApp". command :: CommandOpts -> IO (Result ErrorCode)-command c =- cFSApp- (cFSAppTarget c)- (cFSAppTemplateDir c)- (cFSAppVarNames c)- (cFSAppVarDB c)+command c = Command.CFSApp.command options+ where+ options = Command.CFSApp.CommandOptions+ { Command.CFSApp.commandInputFile = cFSAppInputFile c+ , Command.CFSApp.commandTargetDir = cFSAppTarget c+ , Command.CFSApp.commandTemplateDir = cFSAppTemplateDir c+ , Command.CFSApp.commandVariables = cFSAppVarNames c+ , Command.CFSApp.commandVariableDB = cFSAppVarDB c+ , Command.CFSApp.commandHandlers = cFSAppHandlers c+ , Command.CFSApp.commandFormat = cFSAppFormat c+ , Command.CFSApp.commandPropFormat = cFSAppPropFormat c+ , Command.CFSApp.commandPropVia = cFSAppPropVia c+ , Command.CFSApp.commandExtraVars = cFSAppTemplateVars c+ } -- * CLI @@ -85,7 +100,14 @@ -- System application connected to Copilot monitors. commandOptsParser :: Parser CommandOpts commandOptsParser = CommandOpts- <$> strOption+ <$> optional+ ( strOption+ ( long "input-file"+ <> metavar "FILENAME"+ <> help strCFSAppFileNameArgDesc+ )+ )+ <*> strOption ( long "app-target-dir" <> metavar "DIR" <> showDefault@@ -99,12 +121,12 @@ <> help strCFSAppTemplateDirArgDesc ) )- <*> strOption- ( long "variable-file"- <> metavar "FILENAME"- <> showDefault- <> value "variables"- <> help strCFSAppVarListArgDesc+ <*> optional+ ( strOption+ ( long "variable-file"+ <> metavar "FILENAME"+ <> help strCFSAppVarListArgDesc+ ) ) <*> optional ( strOption@@ -113,6 +135,43 @@ <> help strCFSAppVarDBArgDesc ) )+ <*> optional+ ( strOption+ ( long "handlers-file"+ <> metavar "FILENAME"+ <> help strCFSAppHandlerListArgDesc+ )+ )+ <*> strOption+ ( long "input-format"+ <> short 'f'+ <> metavar "FORMAT_NAME"+ <> help strCFSAppFormatDesc+ <> showDefault+ <> value "fcs"+ )+ <*> strOption+ ( long "prop-format"+ <> short 'p'+ <> metavar "FORMAT_NAME"+ <> help strCFSAppPropFormatDesc+ <> showDefault+ <> value "smv"+ )+ <*> optional+ ( strOption+ ( long "parse-prop-via"+ <> metavar "COMMAND"+ <> help strCFSAppPropViaDesc+ )+ )+ <*> optional+ ( strOption+ ( long "template-vars"+ <> metavar "FILENAME"+ <> help strCFSAppTemplateVarsArgDesc+ )+ ) -- | Argument target directory to cFS app generation command strCFSAppDirArgDesc :: String@@ -123,6 +182,12 @@ strCFSAppTemplateDirArgDesc = "Directory holding cFS application source template" +-- | Argument input file to CFS app generation command+strCFSAppFileNameArgDesc :: String+strCFSAppFileNameArgDesc =+ "File containing input specification"++ -- | Argument variable list to cFS app generation command strCFSAppVarListArgDesc :: String strCFSAppVarListArgDesc =@@ -132,3 +197,26 @@ strCFSAppVarDBArgDesc :: String strCFSAppVarDBArgDesc = "File containing a DB of known cFS/ICAROUS variables"++-- | Argument handler list to cFS app generation command+strCFSAppHandlerListArgDesc :: String+strCFSAppHandlerListArgDesc =+ "File containing list of Copilot handlers used in the specification"++-- | Format flag description.+strCFSAppFormatDesc :: String+strCFSAppFormatDesc = "Format of the input file"++-- | Property format flag description.+strCFSAppPropFormatDesc :: String+strCFSAppPropFormatDesc = "Format of temporal or boolean properties"++-- | External command to pre-process individual properties.+strCFSAppPropViaDesc :: String+strCFSAppPropViaDesc =+ "Command to pre-process individual properties"++-- | Argument template variables to cFS app generation command+strCFSAppTemplateVarsArgDesc :: String+strCFSAppTemplateVarsArgDesc =+ "JSON file containing additional variables to expand in template"
src/CLI/CommandDiagram.hs view
@@ -124,7 +124,8 @@ parseDiagramMode _ = Nothing parseDiagramPropFormat :: String -> Maybe Command.Diagram.DiagramPropFormat- parseDiagramPropFormat "cocospec" = Just Command.Diagram.CoCoSpec+ parseDiagramPropFormat "lustre" = Just Command.Diagram.Lustre+ parseDiagramPropFormat "cocospec" = parseDiagramPropFormat "lustre" parseDiagramPropFormat "inputs" = Just Command.Diagram.Inputs parseDiagramPropFormat "literal" = Just Command.Diagram.Literal parseDiagramPropFormat "smv" = Just Command.Diagram.SMV
src/CLI/CommandFPrimeApp.hs view
@@ -50,22 +50,23 @@ import Command.Result ( Result ) -- External imports: actions or commands supported-import Command.FPrimeApp (ErrorCode, fprimeApp)+import Command.FPrimeApp (ErrorCode) import qualified Command.FPrimeApp -- * Command -- | Options needed to generate the FPrime component. data CommandOpts = CommandOpts- { fprimeAppInputFile :: Maybe String- , fprimeAppTarget :: String- , fprimeAppTemplateDir :: Maybe String- , fprimeAppVarNames :: Maybe String- , fprimeAppVarDB :: Maybe String- , fprimeAppHandlers :: Maybe String- , fprimeAppFormat :: String- , fprimeAppPropFormat :: String- , fprimeAppPropVia :: Maybe String+ { fprimeAppInputFile :: Maybe String+ , fprimeAppTarget :: String+ , fprimeAppTemplateDir :: Maybe String+ , fprimeAppVariables :: Maybe String+ , fprimeAppVarDB :: Maybe String+ , fprimeAppHandlers :: Maybe String+ , fprimeAppFormat :: String+ , fprimeAppPropFormat :: String+ , fprimeAppPropVia :: Maybe String+ , fprimeAppTemplateVars :: Maybe String } -- | Create <https://github.com/nasa/fprime FPrime> component that subscribe@@ -74,18 +75,20 @@ -- -- This is just a wrapper around "Command.fprimeApp". command :: CommandOpts -> IO (Result ErrorCode)-command c = fprimeApp (fprimeAppInputFile c) options+command c = Command.FPrimeApp.command options where options =- Command.FPrimeApp.FPrimeAppOptions- { Command.FPrimeApp.fprimeAppTargetDir = fprimeAppTarget c- , Command.FPrimeApp.fprimeAppTemplateDir = fprimeAppTemplateDir c- , Command.FPrimeApp.fprimeAppVarNames = fprimeAppVarNames c- , Command.FPrimeApp.fprimeAppVariableDB = fprimeAppVarDB c- , Command.FPrimeApp.fprimeAppHandlers = fprimeAppHandlers c- , Command.FPrimeApp.fprimeAppFormat = fprimeAppFormat c- , Command.FPrimeApp.fprimeAppPropFormat = fprimeAppPropFormat c- , Command.FPrimeApp.fprimeAppPropVia = fprimeAppPropVia c+ Command.FPrimeApp.CommandOptions+ { Command.FPrimeApp.commandInputFile = fprimeAppInputFile c+ , Command.FPrimeApp.commandTargetDir = fprimeAppTarget c+ , Command.FPrimeApp.commandTemplateDir = fprimeAppTemplateDir c+ , Command.FPrimeApp.commandVariables = fprimeAppVariables c+ , Command.FPrimeApp.commandVariableDB = fprimeAppVarDB c+ , Command.FPrimeApp.commandHandlers = fprimeAppHandlers c+ , Command.FPrimeApp.commandFormat = fprimeAppFormat c+ , Command.FPrimeApp.commandPropFormat = fprimeAppPropFormat c+ , Command.FPrimeApp.commandPropVia = fprimeAppPropVia c+ , Command.FPrimeApp.commandExtraVars = fprimeAppTemplateVars c } -- * CLI@@ -163,6 +166,13 @@ <> help strFPrimeAppPropViaDesc ) )+ <*> optional+ ( strOption+ ( long "template-vars"+ <> metavar "FILENAME"+ <> help strFPrimeAppTemplateVarsArgDesc+ )+ ) -- | Argument target directory to FPrime component generation command strFPrimeAppDirArgDesc :: String@@ -205,3 +215,8 @@ strFPrimeAppPropViaDesc :: String strFPrimeAppPropViaDesc = "Command to pre-process individual properties"++-- | Additional template variable file flag description.+strFPrimeAppTemplateVarsArgDesc :: String+strFPrimeAppTemplateVarsArgDesc =+ "JSON file containing additional variables to expand in template"
src/CLI/CommandROSApp.hs view
@@ -50,22 +50,23 @@ import Command.Result ( Result ) -- External imports: actions or commands supported-import Command.ROSApp (ErrorCode, rosApp)+import Command.ROSApp (ErrorCode) import qualified Command.ROSApp -- * Command -- | Options needed to generate the ROS application. data CommandOpts = CommandOpts- { rosAppInputFile :: Maybe String- , rosAppTarget :: String- , rosAppTemplateDir :: Maybe String- , rosAppVarNames :: Maybe String- , rosAppVarDB :: Maybe String- , rosAppHandlers :: Maybe String- , rosAppFormat :: String- , rosAppPropFormat :: String- , rosAppPropVia :: Maybe String+ { rosAppInputFile :: Maybe String+ , rosAppTarget :: String+ , rosAppTemplateDir :: Maybe String+ , rosAppVarNames :: Maybe String+ , rosAppVarDB :: Maybe String+ , rosAppHandlers :: Maybe String+ , rosAppFormat :: String+ , rosAppPropFormat :: String+ , rosAppPropVia :: Maybe String+ , rosAppTemplateVars :: Maybe String } -- | Create <https://www.ros.org/ Robot Operating System> (ROS) applications@@ -74,17 +75,19 @@ -- -- This is just a wrapper around "Command.ROSApp". command :: CommandOpts -> IO (Result ErrorCode)-command c = rosApp (rosAppInputFile c) options+command c = Command.ROSApp.command options where- options = Command.ROSApp.ROSAppOptions- { Command.ROSApp.rosAppTargetDir = rosAppTarget c- , Command.ROSApp.rosAppTemplateDir = rosAppTemplateDir c- , Command.ROSApp.rosAppVariables = rosAppVarNames c- , Command.ROSApp.rosAppVariableDB = rosAppVarDB c- , Command.ROSApp.rosAppHandlers = rosAppHandlers c- , Command.ROSApp.rosAppFormat = rosAppFormat c- , Command.ROSApp.rosAppPropFormat = rosAppPropFormat c- , Command.ROSApp.rosAppPropVia = rosAppPropVia c+ options = Command.ROSApp.CommandOptions+ { Command.ROSApp.commandInputFile = rosAppInputFile c+ , Command.ROSApp.commandTargetDir = rosAppTarget c+ , Command.ROSApp.commandTemplateDir = rosAppTemplateDir c+ , Command.ROSApp.commandVariables = rosAppVarNames c+ , Command.ROSApp.commandVariableDB = rosAppVarDB c+ , Command.ROSApp.commandHandlers = rosAppHandlers c+ , Command.ROSApp.commandFormat = rosAppFormat c+ , Command.ROSApp.commandPropFormat = rosAppPropFormat c+ , Command.ROSApp.commandPropVia = rosAppPropVia c+ , Command.ROSApp.commandExtraVars = rosAppTemplateVars c } -- * CLI@@ -162,6 +165,13 @@ <> help strROSAppPropViaDesc ) )+ <*> optional+ ( strOption+ ( long "template-vars"+ <> metavar "FILENAME"+ <> help strROSAppTemplateVarsArgDesc+ )+ ) -- | Argument target directory to ROS app generation command strROSAppDirArgDesc :: String@@ -204,3 +214,8 @@ strROSAppPropViaDesc :: String strROSAppPropViaDesc = "Command to pre-process individual properties"++-- | Additional template variable file flag description.+strROSAppTemplateVarsArgDesc :: String+strROSAppTemplateVarsArgDesc =+ "JSON file containing additional variables to expand in template"
src/CLI/CommandStandalone.hs view
@@ -51,36 +51,40 @@ import Data.Location ( Location(..) ) -- External imports: actions or commands supported-import Command.Standalone (standalone)+import Command.Standalone (ErrorCode) import qualified Command.Standalone -- * Command -- | Options to generate Copilot from specification. data CommandOpts = CommandOpts- { standaloneTargetDir :: FilePath- , standaloneTemplateDir :: Maybe FilePath- , standaloneFileName :: FilePath- , standaloneFormat :: String- , standalonePropFormat :: String- , standaloneTypes :: [String]- , standaloneTarget :: String- , standalonePropVia :: Maybe String+ { standaloneTargetDir :: FilePath+ , standaloneTemplateDir :: Maybe FilePath+ , standaloneFileName :: FilePath+ , standaloneFormat :: String+ , standalonePropFormat :: String+ , standaloneTypes :: [String]+ , standaloneTarget :: String+ , standalonePropVia :: Maybe String+ , standaloneTemplateVars :: Maybe String } -- | Transform an input specification into a Copilot specification. command :: CommandOpts -> IO (Result ErrorCode)-command c = standalone (standaloneFileName c) internalCommandOpts+command c =+ Command.Standalone.command internalCommandOpts where- internalCommandOpts :: Command.Standalone.StandaloneOptions- internalCommandOpts = Command.Standalone.StandaloneOptions- { Command.Standalone.standaloneTargetDir = standaloneTargetDir c- , Command.Standalone.standaloneTemplateDir = standaloneTemplateDir c- , Command.Standalone.standaloneFormat = standaloneFormat c- , Command.Standalone.standalonePropFormat = standalonePropFormat c- , Command.Standalone.standaloneTypeMapping = types- , Command.Standalone.standaloneFilename = standaloneTarget c- , Command.Standalone.standalonePropVia = standalonePropVia c+ internalCommandOpts :: Command.Standalone.CommandOptions+ internalCommandOpts = Command.Standalone.CommandOptions+ { Command.Standalone.commandInputFile = standaloneFileName c+ , Command.Standalone.commandTargetDir = standaloneTargetDir c+ , Command.Standalone.commandTemplateDir = standaloneTemplateDir c+ , Command.Standalone.commandFormat = standaloneFormat c+ , Command.Standalone.commandPropFormat = standalonePropFormat c+ , Command.Standalone.commandTypeMapping = types+ , Command.Standalone.commandFilename = standaloneTarget c+ , Command.Standalone.commandPropVia = standalonePropVia c+ , Command.Standalone.commandExtraVars = standaloneTemplateVars c } types :: [(String, String)]@@ -159,6 +163,13 @@ <> help strStandalonePropViaDesc ) )+ <*> optional+ ( strOption+ ( long "template-vars"+ <> metavar "FILENAME"+ <> help strStandaloneTemplateVarsArgDesc+ )+ ) -- | Target dir flag description. strStandaloneTargetDirDesc :: String@@ -194,14 +205,7 @@ strStandalonePropViaDesc = "Command to pre-process individual properties" --- * Error codes---- | Encoding of reasons why the command can fail.------ The error code used is 1 for user error.-type ErrorCode = Int---- | Error: the specification file cannot be read due to the format being--- unknown.-ecSpecError :: ErrorCode-ecSpecError = 2+-- | Additional template variable file flag description.+strStandaloneTemplateVarsArgDesc :: String+strStandaloneTemplateVarsArgDesc =+ "JSON file containing additional variables to expand in template"
src/Main.hs view
@@ -33,7 +33,7 @@ -- -- Ogma is a tool to facilitate integration of safe runtime monitors into other -- systems. It takes information from a system created in a language (e.g.,--- CoCoSpec ) and produces specifications for the runtime verification+-- Lustre) and produces specifications for the runtime verification -- framework <https://cfs.gsfc.nasa.gov/ Copilot>. Currently, features -- supported are: --
tests/Main.hs view
@@ -48,7 +48,7 @@ , testCase "cli-cmd-standalone-fail" (runErrorCode ["standalone", "--incorrect-argument"] False) -- Should fail due to arguments being incorrect - , testCase "cli-cmd-standalone-fcs" (parseStandaloneFCS "examples/fcs-2.json" True)+ , testCase "cli-cmd-standalone-fcs" (parseStandaloneFCS "tests/fcs-example1.json" True) -- Should pass , testCase "cli-cmd-standalone-file-not-found" (parseStandaloneFCS "tests/file-invalid.json" False)@@ -130,7 +130,7 @@ args = ["standalone", "--file-name", file] errorMsg = "Parsing file " ++ file ++ " result unexpected." --- | Test standalone backend for FDB format and CoCoSpec.+-- | Test standalone backend for FDB format and Lustre. -- -- This test uses the standalone backend, so it generates a Copilot file. It -- may be convenient to run this action in a temporary directory.@@ -150,7 +150,7 @@ assertBool errorMsg (ec == ExitSuccess) where args = [ "standalone", "--file-name", file, "--input-format", "fdb"- , "--prop-format", "cocospec"]+ , "--prop-format", "lustre"] errorMsg = "Parsing file " ++ file ++ " failed" -- | Test ogma by running it and checking the error code.
+ tests/fcs-example1.json view
@@ -0,0 +1,21 @@+{+ "RTSASpec": {+ "Internal_variables": [],+ "Other_variables": [+ {"name":"param_is_short", "type":"bool"},+ {"name":"param_value_short", "type":"real"},+ {"name":"param_value_long", "type":"real"},+ {"name":"upper_param_limit", "type":"real"},+ {"name":"lower_param_limit", "type":"real"},+ {"name":"envelope_issue", "type":"bool"}+ ],+ "Requirements": [+ {+ "name": "behnazOne",+ "CoCoSpecCode": "true",+ "ptLTL": "((H ((((! <b><i>flight_mode</i></b>) & (Y <b><i>flight_mode</i></b>)) & (Y TRUE)) -> (Y (((O[=<b><i>10</i></b>] ((<b><i>(conflict_detected)</i></b> & ((Y (! <b><i>(conflict_detected)</i></b>)) | (<b><i>flight_mode</i></b> & ((! (Y TRUE)) | (Y (! <b><i>flight_mode</i></b>)))))) & (! <b><i>(( replanning_mode ))</i></b>))) -> (O[<<b><i>10</i></b>] ((<b><i>flight_mode</i></b> & ((! (Y TRUE)) | (Y (! <b><i>flight_mode</i></b>)))) | <b><i>(( replanning_mode ))</i></b>))) S (((O[=<b><i>10</i></b>] ((<b><i>(conflict_detected)</i></b> & ((Y (! <b><i>(conflict_detected)</i></b>)) | (<b><i>flight_mode</i></b> & ((! (Y TRUE)) | (Y (! <b><i>flight_mode</i></b>)))))) & (! <b><i>(( replanning_mode ))</i></b>))) -> (O[<<b><i>10</i></b>] ((<b><i>flight_mode</i></b> & ((! (Y TRUE)) | (Y (! <b><i>flight_mode</i></b>)))) | <b><i>(( replanning_mode ))</i></b>))) & (<b><i>flight_mode</i></b> & ((! (Y TRUE)) | (Y (! <b><i>flight_mode</i></b>))))))))) & (((! ((! <b><i>flight_mode</i></b>) & (Y <b><i>flight_mode</i></b>))) S ((! ((! <b><i>flight_mode</i></b>) & (Y <b><i>flight_mode</i></b>))) & (<b><i>flight_mode</i></b> & ((! (Y TRUE)) | (Y (! <b><i>flight_mode</i></b>)))))) -> (((O[=<b><i>10</i></b>] ((<b><i>(conflict_detected)</i></b> & ((Y (! <b><i>(conflict_detected)</i></b>)) | (<b><i>flight_mode</i></b> & ((! (Y TRUE)) | (Y (! <b><i>flight_mode</i></b>)))))) & (! <b><i>(( replanning_mode ))</i></b>))) -> (O[<<b><i>10</i></b>] ((<b><i>flight_mode</i></b> & ((! (Y TRUE)) | (Y (! <b><i>flight_mode</i></b>)))) | <b><i>(( replanning_mode ))</i></b>))) S (((O[=<b><i>10</i></b>] ((<b><i>(conflict_detected)</i></b> & ((Y (! <b><i>(conflict_detected)</i></b>)) | (<b><i>flight_mode</i></b> & ((! (Y TRUE)) | (Y (! <b><i>flight_mode</i></b>)))))) & (! <b><i>(( replanning_mode ))</i></b>))) -> (O[<<b><i>10</i></b>] ((<b><i>flight_mode</i></b> & ((! (Y TRUE)) | (Y (! <b><i>flight_mode</i></b>)))) | <b><i>(( replanning_mode ))</i></b>))) & (<b><i>flight_mode</i></b> & ((! (Y TRUE)) | (Y (! <b><i>flight_mode</i></b>))))))))",+ "fretish": "Meaning not specified"+ }+ ]+ }+}
+ tests/fdb-example1.json view
@@ -0,0 +1,66 @@+[+ {+ "reqid": "test_req1",+ "parent_reqid": "",+ "project": "Test",+ "rationale": "",+ "fulltext": "during flight_mode when conflict_detected planner_module shall within 10 seconds satisfy (replanning_mode).",+ "semantics": {+ "type": "nasa",+ "scope": {+ "type": "in"+ },+ "condition": "regular",+ "timing": "within",+ "response": "satisfaction",+ "variables": {+ "regular": [+ "conflict_detected",+ "replanning_mode"+ ],+ "modes": [+ "flight_mode"+ ]+ },+ "scope_mode": "flight_mode",+ "scopeTextRange": [+ 0,+ 17+ ],+ "regular_condition": "(conflict_detected)",+ "qualifier_word": "when",+ "pre_condition": "(conflict_detected)",+ "conditionTextRange": [+ 19,+ 40+ ],+ "component_name": "planner_module",+ "componentTextRange": [+ 42,+ 55+ ],+ "duration": [+ "10"+ ],+ "timingTextRange": [+ 63,+ 79+ ],+ "post_condition": "(( replanning_mode ))",+ "responseTextRange": [+ 81,+ 105+ ],+ "ft": "((LAST V ((! (Fin_<b><i>flight_mode</i></b> & (! LAST))) | (X (((Lin_<b><i>flight_mode</i></b> | LAST) V (((! <b><i>(conflict_detected)</i></b>) & ((! LAST) & ((X <b><i>(conflict_detected)</i></b>) & (! (Lin_<b><i>flight_mode</i></b> | LAST))))) -> ((X ((F[<=<b><i>10</i></b>] <b><i>(( replanning_mode ))</i></b>) | (F[<<b><i>10</i></b>] (Lin_<b><i>flight_mode</i></b> | LAST)))) & (! (Lin_<b><i>flight_mode</i></b> | LAST))))) & (<b><i>(conflict_detected)</i></b> -> ((F[<=<b><i>10</i></b>] <b><i>(( replanning_mode ))</i></b>) | (F[<<b><i>10</i></b>] (Lin_<b><i>flight_mode</i></b> | LAST)))))))) & (<b><i>flight_mode</i></b> -> (((Lin_<b><i>flight_mode</i></b> | LAST) V (((! <b><i>(conflict_detected)</i></b>) & ((! LAST) & ((X <b><i>(conflict_detected)</i></b>) & (! (Lin_<b><i>flight_mode</i></b> | LAST))))) -> ((X ((F[<=<b><i>10</i></b>] <b><i>(( replanning_mode ))</i></b>) | (F[<<b><i>10</i></b>] (Lin_<b><i>flight_mode</i></b> | LAST)))) & (! (Lin_<b><i>flight_mode</i></b> | LAST))))) & (<b><i>(conflict_detected)</i></b> -> ((F[<=<b><i>10</i></b>] <b><i>(( replanning_mode ))</i></b>) | (F[<<b><i>10</i></b>] (Lin_<b><i>flight_mode</i></b> | LAST)))))))",+ "pt": "((H ((Lin_<b><i>flight_mode</i></b> & (! FTP)) -> (Y (((O[=<b><i>10</i></b>] ((<b><i>(conflict_detected)</i></b> & ((Y (! <b><i>(conflict_detected)</i></b>)) | Fin_<b><i>flight_mode</i></b>)) & (! <b><i>(( replanning_mode ))</i></b>))) -> (O[<<b><i>10</i></b>] (Fin_<b><i>flight_mode</i></b> | <b><i>(( replanning_mode ))</i></b>))) S (((O[=<b><i>10</i></b>] ((<b><i>(conflict_detected)</i></b> & ((Y (! <b><i>(conflict_detected)</i></b>)) | Fin_<b><i>flight_mode</i></b>)) & (! <b><i>(( replanning_mode ))</i></b>))) -> (O[<<b><i>10</i></b>] (Fin_<b><i>flight_mode</i></b> | <b><i>(( replanning_mode ))</i></b>))) & Fin_<b><i>flight_mode</i></b>))))) & (((! Lin_<b><i>flight_mode</i></b>) S ((! Lin_<b><i>flight_mode</i></b>) & Fin_<b><i>flight_mode</i></b>)) -> (((O[=<b><i>10</i></b>] ((<b><i>(conflict_detected)</i></b> & ((Y (! <b><i>(conflict_detected)</i></b>)) | Fin_<b><i>flight_mode</i></b>)) & (! <b><i>(( replanning_mode ))</i></b>))) -> (O[<<b><i>10</i></b>] (Fin_<b><i>flight_mode</i></b> | <b><i>(( replanning_mode ))</i></b>))) S (((O[=<b><i>10</i></b>] ((<b><i>(conflict_detected)</i></b> & ((Y (! <b><i>(conflict_detected)</i></b>)) | Fin_<b><i>flight_mode</i></b>)) & (! <b><i>(( replanning_mode ))</i></b>))) -> (O[<<b><i>10</i></b>] (Fin_<b><i>flight_mode</i></b> | <b><i>(( replanning_mode ))</i></b>))) & Fin_<b><i>flight_mode</i></b>))))",+ "ftExpanded": "((LAST V ((! ((((! <b><i>flight_mode</i></b>) & (! LAST)) & (X <b><i>flight_mode</i></b>)) & (! LAST))) | (X (((((<b><i>flight_mode</i></b> & (! LAST)) & (X (! <b><i>flight_mode</i></b>))) | LAST) V (((! <b><i>(conflict_detected)</i></b>) & ((! LAST) & ((X <b><i>(conflict_detected)</i></b>) & (! (((<b><i>flight_mode</i></b> & (! LAST)) & (X (! <b><i>flight_mode</i></b>))) | LAST))))) -> ((X ((F[<=<b><i>10</i></b>] <b><i>(( replanning_mode ))</i></b>) | (F[<<b><i>10</i></b>] (((<b><i>flight_mode</i></b> & (! LAST)) & (X (! <b><i>flight_mode</i></b>))) | LAST)))) & (! (((<b><i>flight_mode</i></b> & (! LAST)) & (X (! <b><i>flight_mode</i></b>))) | LAST))))) & (<b><i>(conflict_detected)</i></b> -> ((F[<=<b><i>10</i></b>] <b><i>(( replanning_mode ))</i></b>) | (F[<<b><i>10</i></b>] (((<b><i>flight_mode</i></b> & (! LAST)) & (X (! <b><i>flight_mode</i></b>))) | LAST)))))))) & (<b><i>flight_mode</i></b> -> (((((<b><i>flight_mode</i></b> & (! LAST)) & (X (! <b><i>flight_mode</i></b>))) | LAST) V (((! <b><i>(conflict_detected)</i></b>) & ((! LAST) & ((X <b><i>(conflict_detected)</i></b>) & (! (((<b><i>flight_mode</i></b> & (! LAST)) & (X (! <b><i>flight_mode</i></b>))) | LAST))))) -> ((X ((F[<=<b><i>10</i></b>] <b><i>(( replanning_mode ))</i></b>) | (F[<<b><i>10</i></b>] (((<b><i>flight_mode</i></b> & (! LAST)) & (X (! <b><i>flight_mode</i></b>))) | LAST)))) & (! (((<b><i>flight_mode</i></b> & (! LAST)) & (X (! <b><i>flight_mode</i></b>))) | LAST))))) & (<b><i>(conflict_detected)</i></b> -> ((F[<=<b><i>10</i></b>] <b><i>(( replanning_mode ))</i></b>) | (F[<<b><i>10</i></b>] (((<b><i>flight_mode</i></b> & (! LAST)) & (X (! <b><i>flight_mode</i></b>))) | LAST)))))))",+ "ptExpanded": "((H ((((! <b><i>flight_mode</i></b>) & (Y <b><i>flight_mode</i></b>)) & (Y TRUE)) -> (Y (((O[=<b><i>10</i></b>] ((<b><i>(conflict_detected)</i></b> & ((Y (! <b><i>(conflict_detected)</i></b>)) | (<b><i>flight_mode</i></b> & ((! (Y TRUE)) | (Y (! <b><i>flight_mode</i></b>)))))) & (! <b><i>(( replanning_mode ))</i></b>))) -> (O[<<b><i>10</i></b>] ((<b><i>flight_mode</i></b> & ((! (Y TRUE)) | (Y (! <b><i>flight_mode</i></b>)))) | <b><i>(( replanning_mode ))</i></b>))) S (((O[=<b><i>10</i></b>] ((<b><i>(conflict_detected)</i></b> & ((Y (! <b><i>(conflict_detected)</i></b>)) | (<b><i>flight_mode</i></b> & ((! (Y TRUE)) | (Y (! <b><i>flight_mode</i></b>)))))) & (! <b><i>(( replanning_mode ))</i></b>))) -> (O[<<b><i>10</i></b>] ((<b><i>flight_mode</i></b> & ((! (Y TRUE)) | (Y (! <b><i>flight_mode</i></b>)))) | <b><i>(( replanning_mode ))</i></b>))) & (<b><i>flight_mode</i></b> & ((! (Y TRUE)) | (Y (! <b><i>flight_mode</i></b>))))))))) & (((! ((! <b><i>flight_mode</i></b>) & (Y <b><i>flight_mode</i></b>))) S ((! ((! <b><i>flight_mode</i></b>) & (Y <b><i>flight_mode</i></b>))) & (<b><i>flight_mode</i></b> & ((! (Y TRUE)) | (Y (! <b><i>flight_mode</i></b>)))))) -> (((O[=<b><i>10</i></b>] ((<b><i>(conflict_detected)</i></b> & ((Y (! <b><i>(conflict_detected)</i></b>)) | (<b><i>flight_mode</i></b> & ((! (Y TRUE)) | (Y (! <b><i>flight_mode</i></b>)))))) & (! <b><i>(( replanning_mode ))</i></b>))) -> (O[<<b><i>10</i></b>] ((<b><i>flight_mode</i></b> & ((! (Y TRUE)) | (Y (! <b><i>flight_mode</i></b>)))) | <b><i>(( replanning_mode ))</i></b>))) S (((O[=<b><i>10</i></b>] ((<b><i>(conflict_detected)</i></b> & ((Y (! <b><i>(conflict_detected)</i></b>)) | (<b><i>flight_mode</i></b> & ((! (Y TRUE)) | (Y (! <b><i>flight_mode</i></b>)))))) & (! <b><i>(( replanning_mode ))</i></b>))) -> (O[<<b><i>10</i></b>] ((<b><i>flight_mode</i></b> & ((! (Y TRUE)) | (Y (! <b><i>flight_mode</i></b>)))) | <b><i>(( replanning_mode ))</i></b>))) & (<b><i>flight_mode</i></b> & ((! (Y TRUE)) | (Y (! <b><i>flight_mode</i></b>))))))))",+ "component": "<b><i>planner_module</i></b>",+ "CoCoSpecCode": "((H(((( not flight_mode) and (pre (flight_mode))) and ( not FTP)) => (pre (SI( (flight_mode and (FTP or (pre ( not flight_mode)))), ((OT(10,10,( ( (conflict_detected) and ( ( Y ( not (conflict_detected) ) ) or ( flight_mode and ( FTP or ( Y not flight_mode ) ) ) ) ) and ( not (( replanning_mode )) ) ))) => (OT(10-1,0,( ( flight_mode and ( FTP or ( Y not flight_mode ) ) ) or (( replanning_mode )) )))) ))))) and ((SI( (flight_mode and (FTP or (pre ( not flight_mode)))), ( not (( not flight_mode) and (pre (flight_mode)))) )) => (SI( (flight_mode and (FTP or (pre ( not flight_mode)))), ((OT(10,10,( ( (conflict_detected) and ( ( Y ( not (conflict_detected) ) ) or ( flight_mode and ( FTP or ( Y not flight_mode ) ) ) ) ) and ( not (( replanning_mode )) ) ))) => (OT(10-1,0,( ( flight_mode and ( FTP or ( Y not flight_mode ) ) ) or (( replanning_mode )) )))) ))))",+ "diagramVariables": "M = <b><i>flight_mode</i></b>, TC = <b><i>(conflict_detected)</i></b>, n = <b><i>10</i></b>, Response = <b><i>(( replanning_mode ))</i></b>.",+ "description": "ENFORCED: in every interval where <b><i>flight_mode</i></b> holds.\nTRIGGER: first point in the interval if <b><i>(conflict_detected)</i></b> is true and any point in the interval where <b><i>(conflict_detected)</i></b> becomes true (from false).\nREQUIRES: for every trigger, RES must hold at some point with distance <=<b><i>10</i></b> from the trigger, except if the end of the interval occurs sooner.",+ "diagram": "_media/user-interface/examples/svgDiagrams/in_regular_within_satisfaction.svg"+ },+ "_id": "fbc0a840-a04b-11ea-b135-098996762962"+ }+]
+ tests/reduced_geofence_msgs.h view
@@ -0,0 +1,12 @@+/**+ * @struct geofence_parameters_t+ * @brief data structure containing information about the parameters used by the geofence app+ */+typedef struct{+ uint8_t TlmHeader[CFE_SB_TLM_HDR_SIZE];+ double lookahead;+ double hthreshold;+ double vthreshold;+ double hstepback;+ double vstepback;+}geofence_parameters_t;
+ tests/reduced_geofence_msgs_bad.h view
@@ -0,0 +1,12 @@+/**+ * @struct geofence_parameters_t+ * @brief data structure containing information about the parameters used by the geofence app+ */+typeduuuef struct{+ uint8_t TlmHeader[CFE_SB_TLM_HDR_SIZE];+ double lookahead;+ double hthreshold;+ double vthreshold;+ double hstepback;+ double vstepback;+}geofence_parameters_t;