packages feed

ogma-cli (empty) → 1.0.6

raw patch · 13 files changed

+1283/−0 lines, 13 filesdep +HUnitdep +basedep +ogma-coresetup-changedbinary-added

Dependencies added: HUnit, base, ogma-core, optparse-applicative, process, test-framework, test-framework-hunit, unix

Files

+ CHANGELOG.md view
@@ -0,0 +1,37 @@+# Revision history for ogma-cli++## [1.0.6] - 2022-11-21++* Version bump 1.0.6 (#64).+* Update license in cabal file to OtherLicense (#62).+* Add empty file to keep directory structure in distributable package (#65).++## [1.0.5] - 2022-09-21++* Version bump 1.0.5 (#60).+* Update README to reflect that GHC 9.2 is supported (#55).++## [1.0.4] - 2022-07-21++* Version bump 1.0.4 (#53).+* Address all hlint suggestions (#51).++## [1.0.3] - 2022-05-21++* Version bump 1.0.3 (#49).+* Enable CI (#47).+* Conformance with style guide (partial) (#45).++## [1.0.2] - 2022-03-21++* Version bump 1.0.2 (#43).+* Address HLint warning (#41).++## [1.0.1] - 2022-01-21++* Version bump 1.0.1 (#39).+* Merge imports (#33).++## [1.0.0] - 2021-11-22++* Initial release.
+ LICENSE.pdf view

binary file changed (absent → 117991 bytes)

+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ ogma-cli.cabal view
@@ -0,0 +1,153 @@+-- 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.++cabal-version:       2.0+build-type:          Simple++name:                ogma-cli+version:             1.0.6+homepage:            http://nasa.gov+license:             OtherLicense+license-file:        LICENSE.pdf+author:              Ivan Perez, Alwyn Goodloe+maintainer:          ivan.perezdominguez@nasa.gov+category:            Aerospace+extra-source-files:  CHANGELOG.md++synopsis:            Ogma: Helper tool to interoperate between Copilot and other languages.++description:         Ogma is a tool to facilitate the integration of safe runtime monitors into+                     other systems. Ogma extends+                     <https://github.com/Copilot-Language/copilot Copilot>, a high-level runtime+                     verification framework that generates hard real-time C99 code.+                     .+                     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.+                     .+                     - Generating the glue code necessary to work with C+                       structs in Copilot.+                     .+                     - Generating+                       <https://cfs.gsfc.nasa.gov/ NASA Core Flight System>+                       applications that use Copilot for monitoring data+                       received from the message bus.+                     .+                     - Generating message handlers for NASA Core Flight System+                       applications to make external data in structs available+                       to a Copilot monitor.+                     .+                     The main invocation with @--help@ lists sub-commands available.+                     .+                     >$ ogma --help+                     >ogma - an anything-to-Copilot application generator+                     >+                     >Usage: ogma COMMAND+                     >  Generate complete or partial Copilot applications from multiple languages+                     >+                     >Available options:+                     >  -h,--help                Show this help text+                     >+                     >Available commands:+                     >  structs                  Generate Copilot structs from C structs+                     >  handlers                 Generate message handlers from C structs+                     >  cfs                      Generate a complete CFS/Copilot application+                     >  fret-component-spec      Generate a Copilot file from a FRET Component+                     >                           Specification+                     >  fret-reqs-db             Generate a Copilot file from a FRET Requirements+                     >                           Database+                     .+                     For further information, see:+                     .+                     - <https://github.com/nasa/ogma The Ogma repository>.+                     .+                     - <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://ntrs.nasa.gov/citations/20200003164 "Copilot 3">, Perez, Dedden and Goodloe. 2020.+                     .+                     - <https://shemesh.larc.nasa.gov/people/cam/publications/FMAS2020_3.pdf "From Requirements to Autonomous Flight">, Dutle et al. 2020.++executable ogma++  main-is:+    Main.hs++  other-modules:+    CLI.CommandCFSApp+    CLI.CommandCStructs2Copilot+    CLI.CommandCStructs2MsgHandlers+    CLI.CommandFretComponentSpec2Copilot+    CLI.CommandFretReqsDB2Copilot+    CLI.CommandTop+    CLI.Result++  build-depends:+      base                 >= 4.11.0.0 && < 5+    , optparse-applicative+    , ogma-core            >= 1.0.0 && < 1.1++  hs-source-dirs:+    src++  default-language:+    Haskell2010++  ghc-options:+    -Wall++test-suite test-ogma+  type:+    exitcode-stdio-1.0++  main-is:+    Main.hs++  build-depends:+      base+    , HUnit+    , process+    , test-framework+    , test-framework-hunit+    , unix++  hs-source-dirs:+    tests++  default-language:+    Haskell2010++  ghc-options:+    -Wall
+ src/CLI/CommandCFSApp.hs view
@@ -0,0 +1,117 @@+-- 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 CFSApp subcommand.+module CLI.CommandCFSApp+    (+      -- * Direct command access+      command+    , CommandOpts+    , ErrorCode++      -- * CLI+    , commandDesc+    , commandOptsParser+    )+  where++-- External imports+import Options.Applicative ( Parser, help, long, metavar, optional, showDefault,+                             strOption, value )++-- External imports: command results+import Command.Result ( Result )++-- External imports: actions or commands supported+import Command.CFSApp ( ErrorCode, cFSApp )++-- * Command++-- | Options needed to generate the cFS application.+data CommandOpts = CommandOpts+  { cFSAppTarget   :: String+  , cFSAppVarNames :: String+  , cFSAppVarDB    :: Maybe String+  }++-- | Create <https://cfs.gsfc.nasa.gov/ NASA core Flight System> (cFS)+-- applications that subscribe to the communication bus and call Copilot when+-- new messages arrive.+--+-- This is just an uncurried version of "Command.CFSApp".+command :: CommandOpts -> IO (Result ErrorCode)+command c =+  cFSApp (cFSAppTarget c) (cFSAppVarNames c) (cFSAppVarDB c)++-- * CLI++-- | cFS command description+commandDesc :: String+commandDesc = "Generate a complete cFS/Copilot application"++-- | Subparser for the @cfs@ command, used to generate a NASA Core Flight+-- System application connected to Copilot monitors.+commandOptsParser :: Parser CommandOpts+commandOptsParser = CommandOpts+  <$> strOption+        (  long "app-target-dir"+        <> metavar "DIR"+        <> showDefault+        <> value "copilot-cfs-demo"+        <> help strCFSAppDirArgDesc+        )+  <*> strOption+        (  long "variable-file"+        <> metavar "FILENAME"+        <> showDefault+        <> value "variables"+        <> help strCFSAppVarListArgDesc+        )+  <*> optional+        ( strOption+            (  long "variable-db"+            <> metavar "FILENAME"+            <> help strCFSAppVarDBArgDesc+            )+        )++-- | Argument target directory to cFS app generation command+strCFSAppDirArgDesc :: String+strCFSAppDirArgDesc = "Target directory"++-- | Argument variable list to cFS app generation command+strCFSAppVarListArgDesc :: String+strCFSAppVarListArgDesc =+  "File containing list of cFS/ICAROUS variables to make accessible"++-- | Argument variable database to cFS app generation command+strCFSAppVarDBArgDesc :: String+strCFSAppVarDBArgDesc =+  "File containing a DB of known cFS/ICAROUS variables"
+ src/CLI/CommandCStructs2Copilot.hs view
@@ -0,0 +1,86 @@+-- 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.CommandCStructs2Copilot+    (+      -- * Direct command access+      command+    , CommandOpts+    , ErrorCode++      -- * CLI+    , commandDesc+    , commandOptsParser+    )+  where++-- External imports+import Options.Applicative ( Parser, help, long, metavar, strOption )++-- External imports: command results+import Command.Result ( Result )++-- External imports: actions or commands supported+import Command.CStructs2Copilot ( ErrorCode, cstructs2Copilot )++-- * Command++-- | A Copilot correspondence for a C struct can be generated by providing+-- the path to the file that declares the struct.+newtype CommandOpts = CommandOpts+  { cstructsFileName :: FilePath }++-- | Generate Copilot struct definitions and instances from structs defined in+-- a C header file.+--+-- This is just an uncurried version of "Command.CStructs2Copilot".+command :: CommandOpts -> IO (Result ErrorCode)+command c = cstructs2Copilot (cstructsFileName c)++-- * CLI++-- | Command description for CLI help.+commandDesc :: String+commandDesc = "Generate Copilot structs from C structs"++-- | Subparser for the @structs@ command, used to generate Copilot declarations+-- from C structs.+commandOptsParser :: Parser CommandOpts+commandOptsParser = CommandOpts+  <$> strOption+        (  long "header-file-name"+        <> metavar "FILENAME"+        <> help strStructsHeaderArgDesc+        )++-- | Argument C header file to struct conversion command+strStructsHeaderArgDesc :: String+strStructsHeaderArgDesc = "C header file with struct definitions"
+ src/CLI/CommandCStructs2MsgHandlers.hs view
@@ -0,0 +1,85 @@+-- 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.CommandCStructs2MsgHandlers+    (+      -- * Direct command access+      command+    , CommandOpts+    , ErrorCode++      -- * CLI+    , commandDesc+    , commandOptsParser+    )+  where++-- External imports+import Options.Applicative ( Parser, help, long, metavar, strOption )++-- External imports: command results+import Command.Result ( Result )++-- External imports: actions or commands supported+import Command.CStructs2MsgHandlers ( ErrorCode, cstructs2MsgHandlers )++-- * Command++-- | Options to generate message handlers from C struct definitions.+newtype CommandOpts = CommandOpts+  { msgHandlersFileName :: FilePath }++-- | Generate C methods that process NASA Core Flight System messages dealing+-- with the structs defined in a header file.+--+-- This is just an uncurried version of "Command.CStructs2MsgHandlers".+command :: CommandOpts -> IO (Result ErrorCode)+command c = cstructs2MsgHandlers (msgHandlersFileName c)++-- * CLI++-- | Command description for CLI help.+commandDesc :: String+commandDesc = "Generate message handlers from C structs"++-- | Subparser for the @handlers@ command, used to generate message handers+-- from C structs.+commandOptsParser :: Parser CommandOpts+commandOptsParser = CommandOpts+  <$> strOption+        (  long "header-file-name"+        <> metavar "FILENAME"+        <> help strMsgHandlersHeaderArgDesc+        )++-- | Argument C header file to handler generation command+strMsgHandlersHeaderArgDesc :: String+strMsgHandlersHeaderArgDesc = "C header file with struct definitions"
+ src/CLI/CommandFretComponentSpec2Copilot.hs view
@@ -0,0 +1,136 @@+-- 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+  }++-- | 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+      }++-- * 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"+        )++-- | 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"
+ src/CLI/CommandFretReqsDB2Copilot.hs view
@@ -0,0 +1,107 @@+-- 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, strOption, switch )++-- 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+  }++-- | 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+      }++-- * 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+        )++-- | Argument FRET command description+strFretArgDesc :: String+strFretArgDesc = "FRET file with requirements."++-- | CoCoSpec flag description+strFretCoCoDesc :: String+strFretCoCoDesc = "Use CoCoSpec variant of TL properties"
+ src/CLI/CommandTop.hs view
@@ -0,0 +1,234 @@+-- 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 parsing, handling, and execution.+--+-- The full module CLI is just a sum of all the subcommands with their+-- respective CLI options.+--+-- This module defines:+--+-- - A 'CommandOpts' type that represents all options to the program,+-- the subcommand executed, and any options for that subcommand.+--+-- - A 'commandOptsParser' parser for the subcommands and their arguments,+-- delegating the argument parsing to each subcommand's own CLI parser.+--+-- - A 'command' function that dispatcher processing of the execution to the+-- appropriate subcommand.+--+-- - An 'ErrorCode' type that represents reasons why the program may have+-- failed.+--+-- Each of the subcommands is defined using the same standard interface.++-- This module is merely a sum of all subcommands:+--+-- - The type 'CommandOpts' is the sum of all respective subcommand options+-- (whose types all share the same name but have different representations).+--+-- - The parser is a sum of all subparsers, each attached to a specific+-- command name defined in this module.+--+-- - The command function is merely a dispatcher that detects the subcommand+-- that must be executed, extracts the input, runs it, and translates the+-- subcommands result into a top-level command result.+--+-- - The error code is a plain representation that collapses the local+-- subcommand error codes into a few possible values.++module CLI.CommandTop+    (+      -- * Direct command access+      CommandOpts+    , command+    , ErrorCode++      -- * CLI+    , commandDesc+    , commandOptsParser+    )+  where++-- External imports+import           Options.Applicative ( CommandFields, Mod, Parser, helper, info,+                                       progDesc, subparser, (<**>) )+import qualified Options.Applicative as OptParse++-- External imports: command results+import Command.Result ( Result )++-- Internal imports: subcommands+import qualified CLI.CommandCFSApp+import qualified CLI.CommandCStructs2Copilot+import qualified CLI.CommandCStructs2MsgHandlers+import qualified CLI.CommandFretComponentSpec2Copilot+import qualified CLI.CommandFretReqsDB2Copilot++-- * Command++-- | Commands supported by Ogma and their arguments.++-- All subcommands use the same interface, so they all use the type name+-- @CommandOpts@ to capture their respective arguments. These types are+-- different for each subcommand.+data CommandOpts =+    CommandOptsCFSApp                    CLI.CommandCFSApp.CommandOpts+  | CommandOptsCStructs2Copilot          CLI.CommandCStructs2Copilot.CommandOpts+  | CommandOptsCStructs2MsgHandlers      CLI.CommandCStructs2MsgHandlers.CommandOpts+  | CommandOptsFretComponentSpec2Copilot CLI.CommandFretComponentSpec2Copilot.CommandOpts+  | CommandOptsFretReqsDB2Copilot        CLI.CommandFretReqsDB2Copilot.CommandOpts++-- * CLI++-- | Command description for CLI help.+commandDesc :: String+commandDesc =+  "Generate complete or partial Copilot applications from multiple languages"++-- | Subparser for multiple subcommands.+commandOptsParser :: Parser CommandOpts+commandOptsParser = subparser+  (  subcommandCStructs+  <> subcommandMsgHandlers+  <> subcommandCFSApp+  <> subcommandFretComponentSpec+  <> subcommandFretReqs+  )++-- | Modifier for the CStruct to Copilot Struct generation subcommand, linking+-- the subcommand options and description to the command @structs@ at top+-- level.+subcommandCStructs :: Mod CommandFields CommandOpts+subcommandCStructs =+  subcommand+    "structs"+    (CommandOptsCStructs2Copilot+       <$> CLI.CommandCStructs2Copilot.commandOptsParser)+    CLI.CommandCStructs2Copilot.commandDesc++-- | Modifier for the msg handler generation subcommand, linking the subcommand+-- options and description to the command @handlers@ at top level.+subcommandMsgHandlers :: Mod CommandFields CommandOpts+subcommandMsgHandlers =+  subcommand+    "handlers"+    (CommandOptsCStructs2MsgHandlers+       <$> CLI.CommandCStructs2MsgHandlers.commandOptsParser)+    CLI.CommandCStructs2MsgHandlers.commandDesc++-- | Modifier for the CFS app expansion subcommand, linking the subcommand+-- options and description to the command @cfs@ at top level.+subcommandCFSApp :: Mod CommandFields CommandOpts+subcommandCFSApp =+  subcommand+    "cfs"+    (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++-- * Command dispatcher++-- | Command dispatcher that obtains the parameters from the command line and+-- passes them as arguments to the actual function that will process them,+-- transforming the local result into a global program result.++-- This function is implemented as a combination of three processes or+-- functions: one that adapts the input to the inner function (down), the+-- actual function implementing the command, and a translation of the local+-- result into a global result that can be reported to users (up). In this+-- case, the commands are all using the same (and compatible) exit codes, but+-- they might not do so. This is captured by the fmap of the function id on+-- each processing command.+--+-- The function that adapts the inputs simply passes the arguments obtained+-- from the command line one by one. Composition with this function uncurries+-- the next function to work over the product as defined by the record that+-- accompanies each command definition in the type OgmaCLICommand.+--+-- Neither this nor the internal commands not know, and need to know, that they+-- run in CLI.+command :: CommandOpts -> IO (Result ErrorCode)+command (CommandOptsCFSApp c) =+  id <$> CLI.CommandCFSApp.command c+command (CommandOptsCStructs2Copilot c) =+  id <$> CLI.CommandCStructs2Copilot.command c+command (CommandOptsCStructs2MsgHandlers c) =+  id <$> CLI.CommandCStructs2MsgHandlers.command c+command (CommandOptsFretComponentSpec2Copilot c) =+  id <$> CLI.CommandFretComponentSpec2Copilot.command c+command (CommandOptsFretReqsDB2Copilot c) =+  id <$> CLI.CommandFretReqsDB2Copilot.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+-- is required because the types used by the internal functions and the+-- top-level command to represent results are the same, and the error codes are+-- non-overlapping.+{-# ANN command "HLint: ignore Functor law" #-}++-- * Error codes++-- | Encoding of reasons why the command can fail.+--+-- The error code used is 1 for user error, 2 for internal bug.+type ErrorCode = Int++-- * Auxiliary defs++-- | Build a subcommand modifier from a command name, option parser and command+-- description.+subcommand :: String+           -> Parser CommandOpts+           -> String+           -> Mod CommandFields CommandOpts+subcommand entry parser desc =+  OptParse.command entry (info (parser <**> helper) (progDesc desc))
+ src/CLI/Result.hs view
@@ -0,0 +1,57 @@+-- 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.+--+-- | Process a result of a command in a way suitable for command-line+-- interaction.+module CLI.Result where++-- External imports+import System.Exit ( ExitCode (ExitFailure, ExitSuccess), exitWith )+import System.IO   ( hPutStrLn, stderr )++-- External imports: command results+import Command.Result ( Result (Error, Success) )+import Data.Location  ( Location (..) )++{- HLINT ignore "Use exitSuccess" -}+-- | Process a result, report any pending messages, and exit with an error code+-- if necessary.+processResult :: Result Int -> IO ()+processResult Success            = exitWith ExitSuccess+processResult (Error ec msg loc) = do+    hPutStrLn stderr $ showLocation loc ++ "error: " ++ msg+    exitWith (ExitFailure ec)+  where+    -- | Show locations in a standard way in user messages.+    showLocation :: Location -> String+    showLocation LocationNothing        = "<no location info>: "+    showLocation (LocationFile f)       = f ++ ": "+    showLocation (LocationFileLine f l) = f ++ ":" ++ show l ++ ": "+    showLocation (LocationFileLC f l c) = f ++ ":" ++ show l ++ ":" ++ show c ++ ": "
+ src/Main.hs view
@@ -0,0 +1,81 @@+-- 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.+--+-- | Ogma: Tool to interoperate between <https://cfs.gsfc.nasa.gov/ Copilot>+-- and other languages.+--+-- 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+-- 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 of C headers declaring structs into the corresponding Copilot+-- Struct definitions.+--+-- * Translation of C headers declaring structs into CFS message handlers that+-- copy data in global variables.+--+-- * Generate NASA core Flight System (cFS) applications for runtime monitoring+-- using Copilot.+--+-- More information can be obtained by calling ogma with the argument @--help@.+module Main+    ( main )+  where++-- External imports+import Options.Applicative (ParserInfo, execParser, fullDesc, header, helper,+                            info, progDesc, (<**>))++-- Internal imports: CLI parsing, handling, and processing of results.+import CLI.CommandTop ( CommandOpts, command, commandDesc, commandOptsParser )+import CLI.Result     ( processResult )++-- | Ogma: Helper tool to interoperate between Copilot and other languages.+main :: IO ()+main = execParser fullCLIOpts >>= command >>= processResult++-- | Full program options.+fullCLIOpts :: ParserInfo CommandOpts+fullCLIOpts = info (commandOptsParser <**> helper)+  (  fullDesc+  <> progDesc commandDesc+  <> header strProgramSummary+  )++-- | Short program description+strProgramSummary :: String+strProgramSummary =+  "ogma - an anything-to-Copilot application generator"
+ tests/Main.hs view
@@ -0,0 +1,188 @@+-- | Test Ogma+module Main where++import Data.List                      ( intercalate )+import Data.Monoid                    ( mempty )+import System.Exit                    ( ExitCode (ExitSuccess) )+import System.Process                 ( readProcessWithExitCode )+import Test.Framework                 ( Test, defaultMainWithOpts )+import Test.Framework.Providers.HUnit ( testCase )+import Test.HUnit                     ( assertBool )++-- | Run all unit tests on Ogma.+main :: IO ()+main =+  defaultMainWithOpts tests mempty++-- | All unit tests for Ogma+tests :: [Test.Framework.Test]+tests =+  [+    testCase "cli-main-ok" (runErrorCode ["--help" ] True)+    -- Should pass++  , testCase "cli-main-fail" (runErrorCode ["hfdsafdkajdfaskl"] False)+    -- Should fail due to arguments being incorrect++  , testCase "cli-cmd-structs" (runErrorCode ["structs", "--help" ] True)+    -- Should pass++  , testCase "cli-cmd-structs-fail" (runErrorCode ["structs", "--incorrect-argument"] False)+    -- Should fail due to arguments being incorrect++  , testCase "cli-cmd-handlers" (runErrorCode ["handlers", "--help" ] True)+    -- Should pass++  , testCase "cli-cmd-handlers-fail" (runErrorCode ["handlers", "--incorrect-argument"] False)+    -- Should fail due to arguments being incorrect++  , testCase "cli-cmd-cfs" (runErrorCode ["cfs", "--help" ] True)+    -- Should pass++  , 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)+    -- Should pass++  , testCase "cli-cmd-fret-reqs-db-fail" (runErrorCode ["fret-reqs-db", "--incorrect-argument"] False)+    -- Should fail due to arguments being incorrect++  , testCase "fret-cmd-fret-parse-ok" (parseFretCopilot "examples/fret.json" True)+    -- Should pass++  , testCase "fret-cmd-fret-file-not-found" (parseFretCopilot "tests/file-invalid.json" False)+    -- Should fail because the file does not exist++  , testCase "fret-cmd-fret-parse-fail-1" (parseFretCopilot "tests/commands-fret-error-parsing-failed-1.json" False)+    -- Should fail because the opening bracket is [ and not {++  , testCase "fret-cmd-fret-parse-fail-2" (parseFretCopilot "tests/commands-fret-error-parsing-failed-2.json" False)+    -- Should fail because a field is missing in an external variable++  , testCase "fret-cmd-fret-parse-fail-3" (parseFretCopilot "tests/commands-fret-error-parsing-failed-3.json" False)+    -- Should fail because a field is missing in an internal variable++  , testCase "fret-test2" (parseFretCoCoSpec "tests/fret-example1.json")+    -- Should pass++  , testCase "structs-parse-ok" (testCStructs2Copilot "tests/reduced_geofence_msgs.h" True)+    -- Should pass++  , testCase "structs-parse-fail-1" (testCStructs2Copilot "tests/reduced_geofence_msgs_bad.h" False)+    -- Should fail because a keyword is incorrect+  ]++-- | Test C struct parser for a particular file.+--+-- This test uses the Copilot backend for C header files, so it generates+-- Copilot types and instances. It may be convenient to run this action in a+-- temporary directory.+--+-- This IO action fails if any of the following are true:+--   * Ogma cannot be found in the current PATH.+--   * Ogma cannot be executed.+--   * The given file is not found or accessible.+--   * The format in the given file is incorrect.+--   * Ogma fails due to an internal error or bug.+--   * The output file cannot be created due to lack of space or permissions.+--+testCStructs2Copilot :: FilePath  -- ^ Path to a C header file with structs+                     -> Bool+                     -> IO ()+testCStructs2Copilot file success = do+    (ec, _out, _err) <- readProcessWithExitCode "ogma" args ""++    -- True if success is expected and detected, or niether expected nor+    -- detected.+    let testPass = success == (ec == ExitSuccess)++    assertBool errorMsg testPass+  where+    args     = ["structs", "--header-file-name", file]+    errorMsg = "Result of processing file " ++ file ++ " failed"++-- | Test FRET parser for a particular file.+--+-- This test uses the Copilot backend for FRET files, so it generates a Copilot+-- file. It may be convenient to run this action in a temporary directory.+--+-- This IO action fails if any of the following are true:+--   * Ogma cannot be found in the current PATH.+--   * Ogma cannot be executed.+--   * The given file is not found or accessible.+--   * The format in the given file is incorrect.+--   * Ogma fails due to an internal error or bug.+--   * The output file cannot be created due to lack of space or permissions.+--+parseFretCopilot :: FilePath  -- ^ Path to a FRET/JSON requirements file+                 -> Bool+                 -> IO ()+parseFretCopilot file success = do+    (ec, _out, _err) <- readProcessWithExitCode "ogma" args ""++    -- True if success is expected and detected, or niether expected nor+    -- detected.+    let testPass = success == (ec == ExitSuccess)++    assertBool errorMsg testPass+  where+    args     = ["fret-component-spec", "--fret-file-name", file]+    errorMsg = "Parsing file " ++ file ++ " result unexpected."++-- | Test FRET CoCoSpec-based parser for a particular file.+--+-- This test uses the Copilot backend for FRET files, so it generates a Copilot+-- file. It may be convenient to run this action in a temporary directory.+--+-- This IO action fails if any of the following are true:+--   * Ogma cannot be found in the current PATH.+--   * Ogma cannot be executed.+--   * The given file is not found or accessible.+--   * The format in the given file is incorrect.+--   * Ogma fails due to an internal error or bug.+--   * The output file cannot be created due to lack of space or permissions.+--+parseFretCoCoSpec :: FilePath  -- ^ Path to a FRET/JSON requirements file+                  -> IO ()+parseFretCoCoSpec file = do+    (ec, _out, _err) <- readProcessWithExitCode "ogma" args ""+    assertBool errorMsg (ec == ExitSuccess)+  where+    args     = ["fret-reqs-db", "--fret-file-name", file, "--cocospec"]+    errorMsg = "Parsing file " ++ file ++ " failed"++-- | Test ogma by running it and checking the error code.+--+-- This tests just whether ogma finishes with an error code or not. If files+-- may be generated for the command being tested, it may be convenient to run+-- this action in a temporary directory.+--+-- This IO action fails if any of the following are true:+--   * Ogma cannot be found in the current PATH.+--   * Ogma cannot be executed.+--   * The given command is not valid.+--   * Ogma fails due to an internal error or bug.+--   * Output files cannot be created due to lack of space or permissions.+--+runErrorCode :: [String] -- ^ Arguments to pass to ogma+             -> Bool+             -> IO ()+runErrorCode args success = do+    (ec, _out, _err) <- readProcessWithExitCode "ogma" args ""++    -- True if success is expected and detected, or niether expected nor+    -- detected.+    let testPass = success == (ec == ExitSuccess)++    assertBool errorMsg testPass+  where+    errorMsg = "Testing ogma's CLI parser with arguments "+             ++ intercalate "," args+             ++ " failed"