packages feed

ogma-cli 1.4.1 → 1.5.0

raw patch · 10 files changed

+245/−338 lines, 10 filesdep ~basedep ~ogma-core

Dependency ranges changed: base, ogma-core

Files

CHANGELOG.md view
@@ -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).
ogma-cli.cabal view
@@ -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-                       <https://github.com/NASA-SW-VnV/fret NASA requirements elicitation tool FRET>-                       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 @@                      .                      - <https://copilot-language.github.io/ The Copilot web page>.                      .-                     - <https://github.com/NASA-SW-VnV/fret The FRET repository>.-                     .                      - <https://cfs.gsfc.nasa.gov/ The NASA Core Flight System web page>.                      .                      - <https://ros.org/ The Robot Operating System (ROS 2) web page>.@@ -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
src/CLI/CommandCFSApp.hs view
@@ -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 <https://cfs.gsfc.nasa.gov/ NASA core Flight System> (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
− src/CLI/CommandFretComponentSpec2Copilot.hs 
@@ -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"
− src/CLI/CommandFretReqsDB2Copilot.hs 
@@ -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"
src/CLI/CommandROSApp.hs view
@@ -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 <https://www.ros.org/ Robot Operating System> (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
+ src/CLI/CommandStandalone.hs view
@@ -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
src/CLI/CommandTop.hs view
@@ -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
src/Main.hs view
@@ -37,9 +37,8 @@ -- framework <https://cfs.gsfc.nasa.gov/ Copilot>. Currently, features -- supported are: ----- * Translation of ptLTL and Cocospec properties defined in a--- <https://github.com/NASA-SW-VnV/fret FRET> 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.
tests/Main.hs view
@@ -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.