diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,15 @@ # Revision history for ogma-cli +## [1.5.0] - 2024-11-21 + +* Version bump 1.5.0 (#178). +* Provide ability to customize template in cfs command (#157). +* Provide ability to customize template in ros command (#162). +* Introduce new standalone command (#170). +* Update README to demonstrate robotics (#172). +* Remove unused resources (#174). +* Add version bounds to base (#180). + ## [1.4.1] - 2024-09-21 * Version bump 1.4.1 (#155). diff --git a/ogma-cli.cabal b/ogma-cli.cabal --- a/ogma-cli.cabal +++ b/ogma-cli.cabal @@ -32,7 +32,7 @@ build-type: Simple name: ogma-cli -version: 1.4.1 +version: 1.5.0 homepage: https://github.com/nasa/ogma license: OtherLicense license-file: LICENSE.pdf @@ -50,9 +50,8 @@ . Some use cases supported by Ogma include: . - - Translating requirements defined in - - into corresponding monitors in Copilot. + - Translating requirements defined in structured natural + language into monitors in Copilot. . - Generating the glue code necessary to work with C structs in Copilot. @@ -91,11 +90,8 @@ > handlers Generate message handlers from C structs > cfs Generate a complete CFS/Copilot application > fprime Generate a complete F' monitoring component - > fret-component-spec Generate a Copilot file from a FRET Component - > Specification - > fret-reqs-db Generate a Copilot file from a FRET Requirements - > Database > ros Generate a ROS 2 monitoring application + > standalone Generate a Copilot file from an input specification . For further information, see: . @@ -103,8 +99,6 @@ . - . . - - . - . - . . - . @@ -132,16 +126,15 @@ CLI.CommandCStructs2Copilot CLI.CommandCStructs2MsgHandlers CLI.CommandFPrimeApp - CLI.CommandFretComponentSpec2Copilot - CLI.CommandFretReqsDB2Copilot CLI.CommandROSApp + CLI.CommandStandalone CLI.CommandTop CLI.Result build-depends: base >= 4.11.0.0 && < 5 , optparse-applicative - , ogma-core >= 1.4.1 && < 1.5 + , ogma-core >= 1.5.0 && < 1.6 hs-source-dirs: src @@ -160,7 +153,7 @@ Main.hs build-depends: - base + base >= 4.11.0.0 && < 5 , HUnit , process , test-framework diff --git a/src/CLI/CommandCFSApp.hs b/src/CLI/CommandCFSApp.hs --- a/src/CLI/CommandCFSApp.hs +++ b/src/CLI/CommandCFSApp.hs @@ -56,9 +56,10 @@ -- | Options needed to generate the cFS application. data CommandOpts = CommandOpts - { cFSAppTarget :: String - , cFSAppVarNames :: String - , cFSAppVarDB :: Maybe String + { cFSAppTarget :: String + , cFSAppTemplateDir :: Maybe String + , cFSAppVarNames :: String + , cFSAppVarDB :: Maybe String } -- | Create (cFS) @@ -68,7 +69,11 @@ -- This is just an uncurried version of "Command.CFSApp". command :: CommandOpts -> IO (Result ErrorCode) command c = - cFSApp (cFSAppTarget c) (cFSAppVarNames c) (cFSAppVarDB c) + cFSApp + (cFSAppTarget c) + (cFSAppTemplateDir c) + (cFSAppVarNames c) + (cFSAppVarDB c) -- * CLI @@ -87,6 +92,13 @@ <> value "copilot-cfs-demo" <> help strCFSAppDirArgDesc ) + <*> optional + ( strOption + ( long "app-template-dir" + <> metavar "DIR" + <> help strCFSAppTemplateDirArgDesc + ) + ) <*> strOption ( long "variable-file" <> metavar "FILENAME" @@ -105,6 +117,11 @@ -- | Argument target directory to cFS app generation command strCFSAppDirArgDesc :: String strCFSAppDirArgDesc = "Target directory" + +-- | Argument template directory to cFS app generation command +strCFSAppTemplateDirArgDesc :: String +strCFSAppTemplateDirArgDesc = + "Directory holding cFS application source template" -- | Argument variable list to cFS app generation command strCFSAppVarListArgDesc :: String diff --git a/src/CLI/CommandFretComponentSpec2Copilot.hs b/src/CLI/CommandFretComponentSpec2Copilot.hs deleted file mode 100644 --- a/src/CLI/CommandFretComponentSpec2Copilot.hs +++ /dev/null @@ -1,149 +0,0 @@ --- Copyright 2020 United States Government as represented by the Administrator --- of the National Aeronautics and Space Administration. All Rights Reserved. --- --- Disclaimers --- --- No Warranty: THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY --- OF ANY KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT --- LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO --- SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR A --- PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT THE --- SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT DOCUMENTATION, IF --- PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE. THIS AGREEMENT DOES NOT, IN --- ANY MANNER, CONSTITUTE AN ENDORSEMENT BY GOVERNMENT AGENCY OR ANY PRIOR --- RECIPIENT OF ANY RESULTS, RESULTING DESIGNS, HARDWARE, SOFTWARE PRODUCTS OR --- 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." --- --- Waiver and Indemnity: RECIPIENT AGREES TO WAIVE ANY AND ALL CLAIMS AGAINST --- THE UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS, AS WELL AS --- ANY PRIOR RECIPIENT. IF RECIPIENT'S USE OF THE SUBJECT SOFTWARE RESULTS IN --- ANY LIABILITIES, DEMANDS, DAMAGES, EXPENSES OR LOSSES ARISING FROM SUCH USE, --- INCLUDING ANY DAMAGES FROM PRODUCTS BASED ON, OR RESULTING FROM, RECIPIENT'S --- USE OF THE SUBJECT SOFTWARE, RECIPIENT SHALL INDEMNIFY AND HOLD HARMLESS THE --- UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS, AS WELL AS ANY --- PRIOR RECIPIENT, TO THE EXTENT PERMITTED BY LAW. RECIPIENT'S SOLE REMEDY --- FOR ANY SUCH MATTER SHALL BE THE IMMEDIATE, UNILATERAL TERMINATION OF THIS --- AGREEMENT. --- --- | CLI interface to the FRET CS 2 Copilot subcommand -module CLI.CommandFretComponentSpec2Copilot - ( - -- * Direct command access - command - , CommandOpts - , ErrorCode - - -- * CLI - , commandDesc - , commandOptsParser - ) - where - --- External imports -import Options.Applicative (Parser, help, long, metavar, short, showDefault, - strOption, switch, value) - --- External imports: command results -import Command.Result ( Result ) - --- External imports: actions or commands supported -import Command.FRETComponentSpec2Copilot ( ErrorCode, - FRETComponentSpec2CopilotOptions(..), - fretComponentSpec2Copilot ) - --- * Command - --- | Options to generate Copilot from FRET Component Specifications. -data CommandOpts = CommandOpts - { fretComponentSpecFileName :: FilePath - , fretComponentSpecCoCoSpec :: Bool - , fretComponentSpecIntType :: String - , fretComponentSpecRealType :: String - , fretComponentSpecTarget :: String - } - --- | Transform a FRET component specification into a Copilot specification. --- --- This is just an uncurried version of "Command.FRETComponentSpec2Copilot". -command :: CommandOpts -> IO (Result ErrorCode) -command c = - fretComponentSpec2Copilot - (fretComponentSpecFileName c) - internalCommandOpts - - where - - internalCommandOpts :: FRETComponentSpec2CopilotOptions - internalCommandOpts = FRETComponentSpec2CopilotOptions - { fretCS2CopilotUseCoCoSpec = fretComponentSpecCoCoSpec c - , fretCS2CopilotIntType = fretComponentSpecIntType c - , fretCS2CopilotRealType = fretComponentSpecRealType c - , fretCS2CopilotFilename = fretComponentSpecTarget c - } - --- * CLI - --- | Command description for CLI help. -commandDesc :: String -commandDesc = - "Generate a Copilot file from a FRET Component Specification" - --- | Subparser for the @fret-component-spec@ command, used to generate a --- Copilot specification from a FRET component specification file. -commandOptsParser :: Parser CommandOpts -commandOptsParser = CommandOpts - <$> strOption - ( long "fret-file-name" - <> metavar "FILENAME" - <> help strFretArgDesc - ) - <*> switch - ( long "cocospec" - <> help strFretCoCoDesc - ) - <*> strOption - ( long "map-int-to" - <> short 'i' - <> metavar "TYPE_NAME" - <> help strFretIntTypeDesc - <> showDefault - <> value "Int64" - ) - <*> strOption - ( long "map-real-to" - <> short 'r' - <> metavar "TYPE_NAME" - <> help strFretRealTypeDesc - <> showDefault - <> value "Float" - ) - <*> strOption - ( long "target-file-name" - <> metavar "FILENAME" - <> help strFretTargetDesc - <> showDefault - <> value "fret" - ) - --- | Argument FRET command description -strFretArgDesc :: String -strFretArgDesc = "FRET file with requirements." - --- | CoCoSpec flag description -strFretCoCoDesc :: String -strFretCoCoDesc = "Use CoCoSpec variant of TL properties" - --- | Int type mapping flag description. -strFretIntTypeDesc :: String -strFretIntTypeDesc = "Map integer variables to the given type" - --- | Real type mapping flag description. -strFretRealTypeDesc :: String -strFretRealTypeDesc = "Map real variables to the given type" - --- | Target file name flag description. -strFretTargetDesc :: String -strFretTargetDesc = "Filename prefix for monitoring files in target language" diff --git a/src/CLI/CommandFretReqsDB2Copilot.hs b/src/CLI/CommandFretReqsDB2Copilot.hs deleted file mode 100644 --- a/src/CLI/CommandFretReqsDB2Copilot.hs +++ /dev/null @@ -1,121 +0,0 @@ --- Copyright 2020 United States Government as represented by the Administrator --- of the National Aeronautics and Space Administration. All Rights Reserved. --- --- Disclaimers --- --- No Warranty: THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY --- OF ANY KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT --- LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO --- SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR A --- PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT THE --- SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT DOCUMENTATION, IF --- PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE. THIS AGREEMENT DOES NOT, IN --- ANY MANNER, CONSTITUTE AN ENDORSEMENT BY GOVERNMENT AGENCY OR ANY PRIOR --- RECIPIENT OF ANY RESULTS, RESULTING DESIGNS, HARDWARE, SOFTWARE PRODUCTS OR --- 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." --- --- Waiver and Indemnity: RECIPIENT AGREES TO WAIVE ANY AND ALL CLAIMS AGAINST --- THE UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS, AS WELL AS --- ANY PRIOR RECIPIENT. IF RECIPIENT'S USE OF THE SUBJECT SOFTWARE RESULTS IN --- ANY LIABILITIES, DEMANDS, DAMAGES, EXPENSES OR LOSSES ARISING FROM SUCH USE, --- INCLUDING ANY DAMAGES FROM PRODUCTS BASED ON, OR RESULTING FROM, RECIPIENT'S --- USE OF THE SUBJECT SOFTWARE, RECIPIENT SHALL INDEMNIFY AND HOLD HARMLESS THE --- UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS, AS WELL AS ANY --- PRIOR RECIPIENT, TO THE EXTENT PERMITTED BY LAW. RECIPIENT'S SOLE REMEDY --- FOR ANY SUCH MATTER SHALL BE THE IMMEDIATE, UNILATERAL TERMINATION OF THIS --- AGREEMENT. --- --- | CLI interface to the CStructs2Copilot subcommand -module CLI.CommandFretReqsDB2Copilot - ( - -- * Direct command access - command - , CommandOpts - , ErrorCode - - -- * CLI - , commandDesc - , commandOptsParser - ) - where - --- External imports -import Options.Applicative ( Parser, help, long, metavar, showDefault, - strOption, switch, value ) - --- External imports: command results -import Command.Result ( Result ) - --- External imports: actions or commands supported -import Command.FRETReqsDB2Copilot ( ErrorCode, FRETReqsDB2CopilotOptions (..), - fretReqsDB2Copilot ) - --- * Command - --- | Options to generate Copilot from FRET Requirements Databases. -data CommandOpts = CommandOpts - { fretReqsDBFileName :: FilePath - , fretReqsDBCoCoSpec :: Bool - , fretReqsDBTarget :: String - } - --- | Transform a FRET requirements database containing a temporal logic --- specification into a Copilot specification. --- --- This is just an uncurried version of "Command.FRETReqsDB2Copilot". -command :: CommandOpts -> IO (Result ErrorCode) -command c = - fretReqsDB2Copilot - (fretReqsDBFileName c) - internalCommandOpts - - where - - internalCommandOpts :: FRETReqsDB2CopilotOptions - internalCommandOpts = FRETReqsDB2CopilotOptions - { fretReqsDB2CopilotUseCoCoSpec = fretReqsDBCoCoSpec c - , fretReqsDB2CopilotFilename = fretReqsDBTarget c - } - --- * CLI - --- | Command description for CLI help. -commandDesc :: String -commandDesc = - "Generate a Copilot file from a FRET Requirements Database" - --- | Subparser for the @fret-reqs-db@ command, used to generate a Copilot --- specification from a FRET file containing requirements only. -commandOptsParser :: Parser CommandOpts -commandOptsParser = CommandOpts - <$> strOption - ( long "fret-file-name" - <> metavar "FILENAME" - <> help strFretArgDesc - ) - <*> switch - ( long "cocospec" - <> help strFretCoCoDesc - ) - <*> strOption - ( long "target-file-name" - <> metavar "FILENAME" - <> help strFretTargetDesc - <> showDefault - <> value "fret" - ) - --- | Argument FRET command description -strFretArgDesc :: String -strFretArgDesc = "FRET file with requirements." - --- | CoCoSpec flag description -strFretCoCoDesc :: String -strFretCoCoDesc = "Use CoCoSpec variant of TL properties" - --- | Target file name flag description. -strFretTargetDesc :: String -strFretTargetDesc = "Filename prefix for monitoring files in target language" diff --git a/src/CLI/CommandROSApp.hs b/src/CLI/CommandROSApp.hs --- a/src/CLI/CommandROSApp.hs +++ b/src/CLI/CommandROSApp.hs @@ -56,11 +56,12 @@ -- | Options needed to generate the ROS application. data CommandOpts = CommandOpts - { rosAppTarget :: String - , rosAppFRETFile :: Maybe String - , rosAppVarNames :: Maybe String - , rosAppVarDB :: Maybe String - , rosAppHandlers :: Maybe String + { rosAppTarget :: String + , rosAppTemplateDir :: Maybe String + , rosAppFRETFile :: Maybe String + , rosAppVarNames :: Maybe String + , rosAppVarDB :: Maybe String + , rosAppHandlers :: Maybe String } -- | Create (ROS) applications @@ -72,6 +73,7 @@ command c = rosApp (rosAppTarget c) + (rosAppTemplateDir c) (rosAppFRETFile c) (rosAppVarNames c) (rosAppVarDB c) @@ -96,6 +98,13 @@ ) <*> optional ( strOption + ( long "app-template-dir" + <> metavar "DIR" + <> help strROSAppTemplateDirArgDesc + ) + ) + <*> optional + ( strOption ( long "fret-file-name" <> metavar "FILENAME" <> help strROSAppFRETFileNameArgDesc @@ -126,6 +135,11 @@ -- | Argument target directory to ROS app generation command strROSAppDirArgDesc :: String strROSAppDirArgDesc = "Target directory" + +-- | Argument template directory to ROS app generation command +strROSAppTemplateDirArgDesc :: String +strROSAppTemplateDirArgDesc = + "Directory holding ROS application source template" -- | Argument FRET CS to ROS app generation command strROSAppFRETFileNameArgDesc :: String diff --git a/src/CLI/CommandStandalone.hs b/src/CLI/CommandStandalone.hs new file mode 100644 --- /dev/null +++ b/src/CLI/CommandStandalone.hs @@ -0,0 +1,167 @@ +-- Copyright 2020 United States Government as represented by the Administrator +-- of the National Aeronautics and Space Administration. All Rights Reserved. +-- +-- Disclaimers +-- +-- No Warranty: THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY +-- OF ANY KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT +-- LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO +-- SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR A +-- PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT THE +-- SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT DOCUMENTATION, IF +-- PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE. THIS AGREEMENT DOES NOT, IN +-- ANY MANNER, CONSTITUTE AN ENDORSEMENT BY GOVERNMENT AGENCY OR ANY PRIOR +-- RECIPIENT OF ANY RESULTS, RESULTING DESIGNS, HARDWARE, SOFTWARE PRODUCTS OR +-- 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." +-- +-- Waiver and Indemnity: RECIPIENT AGREES TO WAIVE ANY AND ALL CLAIMS AGAINST +-- THE UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS, AS WELL AS +-- ANY PRIOR RECIPIENT. IF RECIPIENT'S USE OF THE SUBJECT SOFTWARE RESULTS IN +-- ANY LIABILITIES, DEMANDS, DAMAGES, EXPENSES OR LOSSES ARISING FROM SUCH USE, +-- INCLUDING ANY DAMAGES FROM PRODUCTS BASED ON, OR RESULTING FROM, RECIPIENT'S +-- USE OF THE SUBJECT SOFTWARE, RECIPIENT SHALL INDEMNIFY AND HOLD HARMLESS THE +-- UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS, AS WELL AS ANY +-- PRIOR RECIPIENT, TO THE EXTENT PERMITTED BY LAW. RECIPIENT'S SOLE REMEDY +-- FOR ANY SUCH MATTER SHALL BE THE IMMEDIATE, UNILATERAL TERMINATION OF THIS +-- AGREEMENT. +-- +-- | CLI interface to the Standalone subcommand +module CLI.CommandStandalone + ( + -- * Direct command access + command + , CommandOpts + , ErrorCode + + -- * CLI + , commandDesc + , commandOptsParser + ) + where + +-- External imports +import Options.Applicative (Parser, help, long, metavar, many, short, + showDefault, strOption, switch, value) + +-- External imports: command results +import Command.Result ( Result(..) ) +import Data.Location ( Location(..) ) + +-- External imports: actions or commands supported +import Command.Standalone (standalone) +import qualified Command.Standalone + +-- * Command + +-- | Options to generate Copilot from specification. +data CommandOpts = CommandOpts + { standaloneFileName :: FilePath + , standaloneFormat :: String + , standalonePropFormat :: String + , standaloneTypes :: [String] + , standaloneTarget :: String + } + +-- | Transform an input specification into a Copilot specification. +command :: CommandOpts -> IO (Result ErrorCode) +command c = standalone (standaloneFileName c) internalCommandOpts + where + internalCommandOpts :: Command.Standalone.StandaloneOptions + internalCommandOpts = Command.Standalone.StandaloneOptions + { Command.Standalone.standaloneFormat = standaloneFormat c + , Command.Standalone.standalonePropFormat = standalonePropFormat c + , Command.Standalone.standaloneTypeMapping = types + , Command.Standalone.standaloneFilename = standaloneTarget c + } + + types :: [(String, String)] + types = map splitTypeMapping (standaloneTypes c) + + splitTypeMapping :: String -> (String, String) + splitTypeMapping s = (h, safeTail t) + where + (h, t) = span (/= ':') s + safeTail xs = if null xs then xs else tail xs + +-- * CLI + +-- | Command description for CLI help. +commandDesc :: String +commandDesc = + "Generate a standalone Copilot file from an input specification" + +-- | Subparser for the @standalone@ command, used to generate a Copilot +-- specification from an input specification file. +commandOptsParser :: Parser CommandOpts +commandOptsParser = CommandOpts + <$> strOption + ( long "file-name" + <> metavar "FILENAME" + <> help strStandaloneFilenameDesc + ) + <*> strOption + ( long "input-format" + <> short 'f' + <> metavar "FORMAT_NAME" + <> help strStandaloneFormatDesc + <> showDefault + <> value "fcs" + ) + <*> strOption + ( long "prop-format" + <> short 'p' + <> metavar "FORMAT_NAME" + <> help strStandalonePropFormatDesc + <> showDefault + <> value "smv" + ) + <*> many (strOption + ( long "map-type" + <> short 'm' + <> metavar "TYPE_NAME:TYPE_NAME" + <> help strStandaloneMapTypeDesc + ) + ) + <*> strOption + ( long "target-file-name" + <> metavar "FILENAME" + <> help strStandaloneTargetDesc + <> showDefault + <> value "monitor" + ) + +-- | Filename flag description. +strStandaloneFilenameDesc :: String +strStandaloneFilenameDesc = "File with properties or requirements" + +-- | Format flag description. +strStandaloneFormatDesc :: String +strStandaloneFormatDesc = "Format of the input file" + +-- | Property format flag description. +strStandalonePropFormatDesc :: String +strStandalonePropFormatDesc = "Format of temporal or boolean properties" + +-- | Type mapping flag description. +strStandaloneMapTypeDesc :: String +strStandaloneMapTypeDesc = "Map a type to another type" + +-- | Target file name flag description. +strStandaloneTargetDesc :: String +strStandaloneTargetDesc = + "Filename prefix for monitoring files in target language" + +-- * 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 diff --git a/src/CLI/CommandTop.hs b/src/CLI/CommandTop.hs --- a/src/CLI/CommandTop.hs +++ b/src/CLI/CommandTop.hs @@ -90,9 +90,8 @@ import qualified CLI.CommandCStructs2Copilot import qualified CLI.CommandCStructs2MsgHandlers import qualified CLI.CommandFPrimeApp -import qualified CLI.CommandFretComponentSpec2Copilot -import qualified CLI.CommandFretReqsDB2Copilot import qualified CLI.CommandROSApp +import qualified CLI.CommandStandalone -- * Command @@ -106,9 +105,8 @@ | CommandOptsCStructs2Copilot CLI.CommandCStructs2Copilot.CommandOpts | CommandOptsCStructs2MsgHandlers CLI.CommandCStructs2MsgHandlers.CommandOpts | CommandOptsFPrimeApp CLI.CommandFPrimeApp.CommandOpts - | CommandOptsFretComponentSpec2Copilot CLI.CommandFretComponentSpec2Copilot.CommandOpts - | CommandOptsFretReqsDB2Copilot CLI.CommandFretReqsDB2Copilot.CommandOpts | CommandOptsROSApp CLI.CommandROSApp.CommandOpts + | CommandOptsStandalone CLI.CommandStandalone.CommandOpts -- * CLI @@ -124,9 +122,8 @@ <> subcommandMsgHandlers <> subcommandCFSApp <> subcommandFPrimeApp - <> subcommandFretComponentSpec - <> subcommandFretReqs <> subcommandROSApp + <> subcommandStandalone ) -- | Modifier for the CStruct to Copilot Struct generation subcommand, linking @@ -159,28 +156,6 @@ (CommandOptsCFSApp <$> CLI.CommandCFSApp.commandOptsParser) CLI.CommandCFSApp.commandDesc --- | Modifier for the FRET component spec to copilot subcommand, linking the --- subcommand options and description to the command @fret-component-spec@ at --- top level. -subcommandFretComponentSpec :: Mod CommandFields CommandOpts -subcommandFretComponentSpec = - subcommand - "fret-component-spec" - (CommandOptsFretComponentSpec2Copilot - <$> CLI.CommandFretComponentSpec2Copilot.commandOptsParser) - CLI.CommandFretComponentSpec2Copilot.commandDesc - --- | Modifier for the FRET requirements DB to copilot subcommand, linking the --- subcommand options and description to the command @fret-reqs-db@ at top --- level. -subcommandFretReqs :: Mod CommandFields CommandOpts -subcommandFretReqs = - subcommand - "fret-reqs-db" - (CommandOptsFretReqsDB2Copilot - <$> CLI.CommandFretReqsDB2Copilot.commandOptsParser) - CLI.CommandFretReqsDB2Copilot.commandDesc - -- | Modifier for the ROS app expansion subcommand, linking the subcommand -- options and description to the command @ros@ at top level. subcommandROSApp :: Mod CommandFields CommandOpts @@ -199,6 +174,15 @@ (CommandOptsFPrimeApp <$> CLI.CommandFPrimeApp.commandOptsParser) CLI.CommandFPrimeApp.commandDesc +-- | Modifier for the standalone subcommand, linking the subcommand options and +-- description to the command @standalone@ at top level. +subcommandStandalone :: Mod CommandFields CommandOpts +subcommandStandalone = + subcommand + "standalone" + (CommandOptsStandalone <$> CLI.CommandStandalone.commandOptsParser) + CLI.CommandStandalone.commandDesc + -- * Command dispatcher -- | Command dispatcher that obtains the parameters from the command line and @@ -229,12 +213,10 @@ id <$> CLI.CommandCStructs2MsgHandlers.command c command (CommandOptsFPrimeApp c) = id <$> CLI.CommandFPrimeApp.command c -command (CommandOptsFretComponentSpec2Copilot c) = - id <$> CLI.CommandFretComponentSpec2Copilot.command c -command (CommandOptsFretReqsDB2Copilot c) = - id <$> CLI.CommandFretReqsDB2Copilot.command c command (CommandOptsROSApp c) = id <$> CLI.CommandROSApp.command c +command (CommandOptsStandalone c) = + id <$> CLI.CommandStandalone.command c -- We indicate to HLint that the use of (id <$>) above should not trigger a -- warning. Conceptually, there is a transformation taking place, but no change diff --git a/src/Main.hs b/src/Main.hs --- a/src/Main.hs +++ b/src/Main.hs @@ -37,9 +37,8 @@ -- framework . Currently, features -- supported are: -- --- * Translation of ptLTL and Cocospec properties defined in a --- file into corresponding --- expressions in Copilot. +-- * Translation properties defined in structured natural language into +-- corresponding expressions in Copilot. -- -- * Translation of C headers declaring structs into the corresponding Copilot -- Struct definitions. diff --git a/tests/Main.hs b/tests/Main.hs --- a/tests/Main.hs +++ b/tests/Main.hs @@ -42,16 +42,10 @@ , testCase "cli-cmd-cfs-fail" (runErrorCode ["cfs", "--incorrect-argument"] False) -- Should fail due to arguments being incorrect - , testCase "cli-cmd-fret-component-spec" (runErrorCode ["fret-component-spec", "--help" ] True) - -- Should pass - - , testCase "cli-cmd-fret-component-spec-fail" (runErrorCode ["fret-component-spec", "--incorrect-argument"] False) - -- Should fail due to arguments being incorrect - - , testCase "cli-cmd-fret-reqs-db" (runErrorCode ["fret-reqs-db", "--help" ] True) + , testCase "cli-cmd-fret-component-spec" (runErrorCode ["standalone", "--help" ] True) -- Should pass - , testCase "cli-cmd-fret-reqs-db-fail" (runErrorCode ["fret-reqs-db", "--incorrect-argument"] False) + , testCase "cli-cmd-fret-component-spec-fail" (runErrorCode ["standalone", "--incorrect-argument"] False) -- Should fail due to arguments being incorrect , testCase "fret-cmd-fret-parse-ok" (parseFretCopilot "examples/fret.json" True) @@ -133,7 +127,7 @@ assertBool errorMsg testPass where - args = ["fret-component-spec", "--fret-file-name", file] + args = ["standalone", "--file-name", file] errorMsg = "Parsing file " ++ file ++ " result unexpected." -- | Test FRET CoCoSpec-based parser for a particular file. @@ -155,7 +149,8 @@ (ec, _out, _err) <- readProcessWithExitCode "ogma" args "" assertBool errorMsg (ec == ExitSuccess) where - args = ["fret-reqs-db", "--fret-file-name", file, "--cocospec"] + args = [ "standalone", "--file-name", file, "--input-format", "fdb" + , "--prop-format", "cocospec"] errorMsg = "Parsing file " ++ file ++ " failed" -- | Test ogma by running it and checking the error code.