diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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). diff --git a/ogma-cli.cabal b/ogma-cli.cabal --- a/ogma-cli.cabal +++ b/ogma-cli.cabal @@ -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 @@ . - "", 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 diff --git a/src/CLI/CommandCFSApp.hs b/src/CLI/CommandCFSApp.hs --- a/src/CLI/CommandCFSApp.hs +++ b/src/CLI/CommandCFSApp.hs @@ -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 (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" diff --git a/src/CLI/CommandDiagram.hs b/src/CLI/CommandDiagram.hs --- a/src/CLI/CommandDiagram.hs +++ b/src/CLI/CommandDiagram.hs @@ -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 diff --git a/src/CLI/CommandFPrimeApp.hs b/src/CLI/CommandFPrimeApp.hs --- a/src/CLI/CommandFPrimeApp.hs +++ b/src/CLI/CommandFPrimeApp.hs @@ -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 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" diff --git a/src/CLI/CommandROSApp.hs b/src/CLI/CommandROSApp.hs --- a/src/CLI/CommandROSApp.hs +++ b/src/CLI/CommandROSApp.hs @@ -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 (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" diff --git a/src/CLI/CommandStandalone.hs b/src/CLI/CommandStandalone.hs --- a/src/CLI/CommandStandalone.hs +++ b/src/CLI/CommandStandalone.hs @@ -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" diff --git a/src/Main.hs b/src/Main.hs --- a/src/Main.hs +++ b/src/Main.hs @@ -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 . Currently, features -- supported are: -- diff --git a/tests/Main.hs b/tests/Main.hs --- a/tests/Main.hs +++ b/tests/Main.hs @@ -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. diff --git a/tests/fcs-example1.json b/tests/fcs-example1.json new file mode 100644 --- /dev/null +++ b/tests/fcs-example1.json @@ -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 ((((! flight_mode) & (Y flight_mode)) & (Y TRUE)) -> (Y (((O[=10] (((conflict_detected) & ((Y (! (conflict_detected))) | (flight_mode & ((! (Y TRUE)) | (Y (! flight_mode)))))) & (! (( replanning_mode ))))) -> (O[<10] ((flight_mode & ((! (Y TRUE)) | (Y (! flight_mode)))) | (( replanning_mode ))))) S (((O[=10] (((conflict_detected) & ((Y (! (conflict_detected))) | (flight_mode & ((! (Y TRUE)) | (Y (! flight_mode)))))) & (! (( replanning_mode ))))) -> (O[<10] ((flight_mode & ((! (Y TRUE)) | (Y (! flight_mode)))) | (( replanning_mode ))))) & (flight_mode & ((! (Y TRUE)) | (Y (! flight_mode))))))))) & (((! ((! flight_mode) & (Y flight_mode))) S ((! ((! flight_mode) & (Y flight_mode))) & (flight_mode & ((! (Y TRUE)) | (Y (! flight_mode)))))) -> (((O[=10] (((conflict_detected) & ((Y (! (conflict_detected))) | (flight_mode & ((! (Y TRUE)) | (Y (! flight_mode)))))) & (! (( replanning_mode ))))) -> (O[<10] ((flight_mode & ((! (Y TRUE)) | (Y (! flight_mode)))) | (( replanning_mode ))))) S (((O[=10] (((conflict_detected) & ((Y (! (conflict_detected))) | (flight_mode & ((! (Y TRUE)) | (Y (! flight_mode)))))) & (! (( replanning_mode ))))) -> (O[<10] ((flight_mode & ((! (Y TRUE)) | (Y (! flight_mode)))) | (( replanning_mode ))))) & (flight_mode & ((! (Y TRUE)) | (Y (! flight_mode))))))))", + "fretish": "Meaning not specified" + } + ] + } +} diff --git a/tests/fdb-example1.json b/tests/fdb-example1.json new file mode 100644 --- /dev/null +++ b/tests/fdb-example1.json @@ -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_flight_mode & (! LAST))) | (X (((Lin_flight_mode | LAST) V (((! (conflict_detected)) & ((! LAST) & ((X (conflict_detected)) & (! (Lin_flight_mode | LAST))))) -> ((X ((F[<=10] (( replanning_mode ))) | (F[<10] (Lin_flight_mode | LAST)))) & (! (Lin_flight_mode | LAST))))) & ((conflict_detected) -> ((F[<=10] (( replanning_mode ))) | (F[<10] (Lin_flight_mode | LAST)))))))) & (flight_mode -> (((Lin_flight_mode | LAST) V (((! (conflict_detected)) & ((! LAST) & ((X (conflict_detected)) & (! (Lin_flight_mode | LAST))))) -> ((X ((F[<=10] (( replanning_mode ))) | (F[<10] (Lin_flight_mode | LAST)))) & (! (Lin_flight_mode | LAST))))) & ((conflict_detected) -> ((F[<=10] (( replanning_mode ))) | (F[<10] (Lin_flight_mode | LAST)))))))", + "pt": "((H ((Lin_flight_mode & (! FTP)) -> (Y (((O[=10] (((conflict_detected) & ((Y (! (conflict_detected))) | Fin_flight_mode)) & (! (( replanning_mode ))))) -> (O[<10] (Fin_flight_mode | (( replanning_mode ))))) S (((O[=10] (((conflict_detected) & ((Y (! (conflict_detected))) | Fin_flight_mode)) & (! (( replanning_mode ))))) -> (O[<10] (Fin_flight_mode | (( replanning_mode ))))) & Fin_flight_mode))))) & (((! Lin_flight_mode) S ((! Lin_flight_mode) & Fin_flight_mode)) -> (((O[=10] (((conflict_detected) & ((Y (! (conflict_detected))) | Fin_flight_mode)) & (! (( replanning_mode ))))) -> (O[<10] (Fin_flight_mode | (( replanning_mode ))))) S (((O[=10] (((conflict_detected) & ((Y (! (conflict_detected))) | Fin_flight_mode)) & (! (( replanning_mode ))))) -> (O[<10] (Fin_flight_mode | (( replanning_mode ))))) & Fin_flight_mode))))", + "ftExpanded": "((LAST V ((! ((((! flight_mode) & (! LAST)) & (X flight_mode)) & (! LAST))) | (X (((((flight_mode & (! LAST)) & (X (! flight_mode))) | LAST) V (((! (conflict_detected)) & ((! LAST) & ((X (conflict_detected)) & (! (((flight_mode & (! LAST)) & (X (! flight_mode))) | LAST))))) -> ((X ((F[<=10] (( replanning_mode ))) | (F[<10] (((flight_mode & (! LAST)) & (X (! flight_mode))) | LAST)))) & (! (((flight_mode & (! LAST)) & (X (! flight_mode))) | LAST))))) & ((conflict_detected) -> ((F[<=10] (( replanning_mode ))) | (F[<10] (((flight_mode & (! LAST)) & (X (! flight_mode))) | LAST)))))))) & (flight_mode -> (((((flight_mode & (! LAST)) & (X (! flight_mode))) | LAST) V (((! (conflict_detected)) & ((! LAST) & ((X (conflict_detected)) & (! (((flight_mode & (! LAST)) & (X (! flight_mode))) | LAST))))) -> ((X ((F[<=10] (( replanning_mode ))) | (F[<10] (((flight_mode & (! LAST)) & (X (! flight_mode))) | LAST)))) & (! (((flight_mode & (! LAST)) & (X (! flight_mode))) | LAST))))) & ((conflict_detected) -> ((F[<=10] (( replanning_mode ))) | (F[<10] (((flight_mode & (! LAST)) & (X (! flight_mode))) | LAST)))))))", + "ptExpanded": "((H ((((! flight_mode) & (Y flight_mode)) & (Y TRUE)) -> (Y (((O[=10] (((conflict_detected) & ((Y (! (conflict_detected))) | (flight_mode & ((! (Y TRUE)) | (Y (! flight_mode)))))) & (! (( replanning_mode ))))) -> (O[<10] ((flight_mode & ((! (Y TRUE)) | (Y (! flight_mode)))) | (( replanning_mode ))))) S (((O[=10] (((conflict_detected) & ((Y (! (conflict_detected))) | (flight_mode & ((! (Y TRUE)) | (Y (! flight_mode)))))) & (! (( replanning_mode ))))) -> (O[<10] ((flight_mode & ((! (Y TRUE)) | (Y (! flight_mode)))) | (( replanning_mode ))))) & (flight_mode & ((! (Y TRUE)) | (Y (! flight_mode))))))))) & (((! ((! flight_mode) & (Y flight_mode))) S ((! ((! flight_mode) & (Y flight_mode))) & (flight_mode & ((! (Y TRUE)) | (Y (! flight_mode)))))) -> (((O[=10] (((conflict_detected) & ((Y (! (conflict_detected))) | (flight_mode & ((! (Y TRUE)) | (Y (! flight_mode)))))) & (! (( replanning_mode ))))) -> (O[<10] ((flight_mode & ((! (Y TRUE)) | (Y (! flight_mode)))) | (( replanning_mode ))))) S (((O[=10] (((conflict_detected) & ((Y (! (conflict_detected))) | (flight_mode & ((! (Y TRUE)) | (Y (! flight_mode)))))) & (! (( replanning_mode ))))) -> (O[<10] ((flight_mode & ((! (Y TRUE)) | (Y (! flight_mode)))) | (( replanning_mode ))))) & (flight_mode & ((! (Y TRUE)) | (Y (! flight_mode))))))))", + "component": "planner_module", + "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 = flight_mode, TC = (conflict_detected), n = 10, Response = (( replanning_mode )).", + "description": "ENFORCED: in every interval where flight_mode holds.\nTRIGGER: first point in the interval if (conflict_detected) is true and any point in the interval where (conflict_detected) becomes true (from false).\nREQUIRES: for every trigger, RES must hold at some point with distance <=10 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" + } +] diff --git a/tests/reduced_geofence_msgs.h b/tests/reduced_geofence_msgs.h new file mode 100644 --- /dev/null +++ b/tests/reduced_geofence_msgs.h @@ -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; diff --git a/tests/reduced_geofence_msgs_bad.h b/tests/reduced_geofence_msgs_bad.h new file mode 100644 --- /dev/null +++ b/tests/reduced_geofence_msgs_bad.h @@ -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;