diff --git a/docs/fret.png b/docs/fret.png deleted file mode 100644 index fbb63e60..00000000 Binary files a/docs/fret.png and /dev/null differ diff --git a/docs/xplane.png b/docs/xplane.png deleted file mode 100644 index 2a710ae6..00000000 Binary files a/docs/xplane.png and /dev/null differ diff --git a/ogma-cli/CHANGELOG.md b/ogma-cli/CHANGELOG.md index 00e5d435..b30fceb3 100644 --- a/ogma-cli/CHANGELOG.md +++ b/ogma-cli/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/README.md b/ogma-cli/README.md index 6d22e140..005dd2bc 100644 --- a/ogma-cli/README.md +++ b/ogma-cli/README.md @@ -27,6 +27,12 @@ verification framework that generates hard real-time C99 code. Integration of monitors into larger applications (e.g., simulators).

+

+ Monitoring within ROS simulation video +
+ Integration of monitors into robotics applications. +

+ ## Table of Contents - [Installation](#installation) @@ -115,9 +121,10 @@ flags to customize the list of known variables, so that projects can maintain their own variable databases beyond what Ogma includes by default. cFS applications are generated using the Ogma command `cfs`, which receives -three main arguments: +four main arguments: - `--app-target-dir DIR`: location where the cFS application files must be stored. +- `--app-template-dir DIR`: location of the cFS application template to use. - `--variable-file FILENAME`: a file containing a list of variables that must be made available to the monitor. - `--variable-db FILENAME`: a file containing a database of known variables, @@ -187,6 +194,45 @@ void COPILOT_ProcessIcarousPosition(void) } ``` +### Template Customization + +By default, Ogma uses a pre-defined template to generate the cFS monitoring +application. It's possible to customize the output by providing a directory +with a set of files with a cFS application template, which Ogma will use +instead. + +To choose this feature, one must call Ogma's `cfs` command with the argument +`--app-template-dir DIR`, where `DIR` is the path to a directory containing a +cFS application template. For example, assuming that the directory +`my_template` contains a custom cFS application template, one can execute: + +``` +$ ogma cfs --app-template-dir my_template/ --variable-db examples/cfs-variable-db --variable-file examples/cfs-variables +``` + +Ogma will copy the files in that directory to the target path, filling in +several holes with specific information: + +- `{{variablesS}}`: this will be replaced by a list of variable declarations, + one for each global variable that holds information read from the cFS +software bus that must be made accessible to the monitoring code. + +- `{{msgSubscriptionsS}}`: this will be replaced by a list of calls to + `CFE_SB_Subscribe`, subscribing to the necessary information coming in the +software bus. + +- `{{msgCasesS}}`: this will be replaced by a switch case statements that match + the ID of an incoming message, to handle information being received that must +be updated and would trigger a re-evaluation of the monitors. + +- `{{msgHandlerS}}`: this will be replaced by function definitions of the + functions that will be called to actually update the variables with +information coming from the software bus, and re-evaluate the monitors. + +We understand that this level of customization may be insufficient for your +application. If that is the case, feel free to reach out to our team to discuss +how we could make the template expansion system more versatile. + ## ROS Application Generation The Robot Operating System (ROS) is a framework to build robot applications. @@ -196,9 +242,10 @@ the data needed by the monitors and report any violations. At present, support for ROS app generation is considered preliminary. ROS applications are generated using the Ogma command `ros`, which receives -four main arguments: +five main arguments: - `--app-target-dir DIR`: location where the ROS application files must be stored. +- `--app-template-dir DIR`: location of the ROS application template to use. - `--variable-file FILENAME`: a file containing a list of variables that must be made available to the monitor. - `--variable-db FILENAME`: a file containing a database of known variables, @@ -259,6 +306,74 @@ and the last step of the script `.github/workflows/repo-ghc-8.6-cabal-2.4-ros.yml`, which generates a ROS monitor with multiple variables and compiles the resulting code. +### Template Customization + +By default, Ogma uses a pre-defined template to generate the ROS monitoring +package. It's possible to customize the output by providing a directory with a +set of files with a ROS package template, which Ogma will use instead. + +To choose this feature, one must call Ogma's `ros` command with the argument +`--app-template-dir DIR`, where `DIR` is the path to a directory containing a +ROS 2 package template. For example, assuming that the directory `my_template` +contains a custom ROS package template, one can execute: + +``` +$ ogma ros --app-template-dir my_template/ --handlers filename --variable-file variables --variable-db ros-variable-db --app-target-dir ros_demo +``` + +Ogma will copy the files in that directory to the target path, filling in +several holes with specific information. For the monitoring node, the variables +are: + +- `{{variablesS}}`: this will be replaced by a list of variable declarations, + one for each global variable that holds information read from the ROS +software bus that must be made accessible to the monitoring code. + +- `{{msgSubscriptionsS}}`: this will be replaced by a list of calls to + `create_subscription`, subscribing to the necessary information coming in the +software bus. + +- `{{msgPublisherS}}`: this will be replaced by a list of calls to + `create_publisher`, to create topics to report property violations on the +software bus. + +- `{{msgHandlerInClassS}}`: this will be replaced by the functions that will be + called to report a property violation via one of the property violation +topics (publishers). + +- `{{msgCallbacks}}`: this will be replaced by function definitions of the + functions that will be called to actually update the variables with +information coming from the software bus, and re-evaluate the monitors. + +- `{{msgSubscriptionDeclrs}}`: this will be replaced by declarations of + subscriptions used in `{{msgSubscriptionsS}}`. + +- `{{msgPublisherDeclrs}}`: this will be replaced by declarations of publishers + used in `{{msgPublishersS}}`. + +- `{{msgHandlerGlobalS}}`: this will be replaced by top-level functions that + call the handlers from the single monitoring class instance (singleton). + +Ogma will also generate a logging node that can be used for debugging purposes, +to print property violations to a log. This second node listens to the messages +published by the monitoring node in the software bus. For that node, the +variables used are: + +- `{{logMsgSubscriptionsS}}`: this will be replaced by a list of calls to + `create_subscription`, subscribing to the necessary information coming in the +software bus. + +- `{{logMsgCallbacks}}`: this will be replaced by function definitions of the + functions called to report the violations in the log. These functions are +used as handlers to incoming messages in the subscriptions. + +- `{{logMsgSubscriptionDeclrs}}`: this will be replaced by declarations of + subscriptions used in `{{logMsgSubscriptionsS}}`. + +We understand that this level of customization may be insufficient for your +application. If that is the case, feel free to reach out to our team to discuss +how we could make the template expansion system more versatile. + ### Current limitations The user must place the code generated by Copilot monitors in two files, diff --git a/ogma-cli/ogma-cli.cabal b/ogma-cli/ogma-cli.cabal index 0a2559d5..7665eeec 100644 --- a/ogma-cli/ogma-cli.cabal +++ b/ogma-cli/ogma-cli.cabal @@ -32,7 +32,7 @@ cabal-version: 2.0 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 @@ description: Ogma is a tool to facilitate the integration of safe runtim . 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 @@ description: Ogma is a tool to facilitate the integration of safe runtim > 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 @@ description: Ogma is a tool to facilitate the integration of safe runtim . - . . - - . - . - . . - . @@ -132,16 +126,15 @@ executable ogma 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 @@ test-suite test-ogma Main.hs build-depends: - base + base >= 4.11.0.0 && < 5 , HUnit , process , test-framework diff --git a/ogma-cli/src/CLI/CommandCFSApp.hs b/ogma-cli/src/CLI/CommandCFSApp.hs index a5574080..1a44a72b 100644 --- a/ogma-cli/src/CLI/CommandCFSApp.hs +++ b/ogma-cli/src/CLI/CommandCFSApp.hs @@ -56,9 +56,10 @@ import Command.CFSApp ( ErrorCode, cFSApp ) -- | 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 @@ data CommandOpts = CommandOpts -- 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 @@ commandOptsParser = CommandOpts <> value "copilot-cfs-demo" <> help strCFSAppDirArgDesc ) + <*> optional + ( strOption + ( long "app-template-dir" + <> metavar "DIR" + <> help strCFSAppTemplateDirArgDesc + ) + ) <*> strOption ( long "variable-file" <> metavar "FILENAME" @@ -106,6 +118,11 @@ commandOptsParser = CommandOpts 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 strCFSAppVarListArgDesc = diff --git a/ogma-cli/src/CLI/CommandFretComponentSpec2Copilot.hs b/ogma-cli/src/CLI/CommandFretComponentSpec2Copilot.hs deleted file mode 100644 index d571def1..00000000 --- a/ogma-cli/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/ogma-cli/src/CLI/CommandFretReqsDB2Copilot.hs b/ogma-cli/src/CLI/CommandFretReqsDB2Copilot.hs deleted file mode 100644 index 26f1b2e9..00000000 --- a/ogma-cli/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/ogma-cli/src/CLI/CommandROSApp.hs b/ogma-cli/src/CLI/CommandROSApp.hs index 9fac9ba3..2762c86f 100644 --- a/ogma-cli/src/CLI/CommandROSApp.hs +++ b/ogma-cli/src/CLI/CommandROSApp.hs @@ -56,11 +56,12 @@ import Command.ROSApp ( ErrorCode, rosApp ) -- | 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 :: CommandOpts -> IO (Result ErrorCode) command c = rosApp (rosAppTarget c) + (rosAppTemplateDir c) (rosAppFRETFile c) (rosAppVarNames c) (rosAppVarDB c) @@ -94,6 +96,13 @@ commandOptsParser = CommandOpts <> value "ros" <> help strROSAppDirArgDesc ) + <*> optional + ( strOption + ( long "app-template-dir" + <> metavar "DIR" + <> help strROSAppTemplateDirArgDesc + ) + ) <*> optional ( strOption ( long "fret-file-name" @@ -127,6 +136,11 @@ commandOptsParser = CommandOpts 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 strROSAppFRETFileNameArgDesc = diff --git a/ogma-cli/src/CLI/CommandStandalone.hs b/ogma-cli/src/CLI/CommandStandalone.hs new file mode 100644 index 00000000..b4cd7377 --- /dev/null +++ b/ogma-cli/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/ogma-cli/src/CLI/CommandTop.hs b/ogma-cli/src/CLI/CommandTop.hs index 6da1b454..c6fb03f8 100644 --- a/ogma-cli/src/CLI/CommandTop.hs +++ b/ogma-cli/src/CLI/CommandTop.hs @@ -90,9 +90,8 @@ import qualified CLI.CommandCFSApp 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 @@ data CommandOpts = | 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 @@ commandOptsParser = subparser <> subcommandMsgHandlers <> subcommandCFSApp <> subcommandFPrimeApp - <> subcommandFretComponentSpec - <> subcommandFretReqs <> subcommandROSApp + <> subcommandStandalone ) -- | Modifier for the CStruct to Copilot Struct generation subcommand, linking @@ -159,28 +156,6 @@ subcommandCFSApp = (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 @@ subcommandFPrimeApp = (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 @@ command (CommandOptsCStructs2MsgHandlers c) = 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/ogma-cli/src/Main.hs b/ogma-cli/src/Main.hs index 6535a987..de74c303 100644 --- a/ogma-cli/src/Main.hs +++ b/ogma-cli/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/ogma-cli/tests/Main.hs b/ogma-cli/tests/Main.hs index fa134de8..20706b4e 100644 --- a/ogma-cli/tests/Main.hs +++ b/ogma-cli/tests/Main.hs @@ -42,16 +42,10 @@ tests = , 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) + , testCase "cli-cmd-fret-component-spec" (runErrorCode ["standalone", "--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) + , 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 @@ parseFretCopilot file success = do 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 @@ parseFretCoCoSpec file = do (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. diff --git a/ogma-core/CHANGELOG.md b/ogma-core/CHANGELOG.md index 4796c588..3955b267 100644 --- a/ogma-core/CHANGELOG.md +++ b/ogma-core/CHANGELOG.md @@ -1,5 +1,16 @@ # Revision history for ogma-core +## [1.5.0] - 2024-11-21 + +* Version bump 1.5.0 (#178). +* Fix incorrect path when using Space ROS humble-2024.10.0 (#158). +* Use template expansion system to generate cFS monitoring application (#157). +* Use template expansion system to generate ROS monitoring application (#162). +* Fix comment in generated Copilot spec (#164). +* Add missing notPreviousNot to generated spec (#168). +* Introduce new standalone command (#170). +* Correct name in documentation (#176). + ## [1.4.1] - 2024-09-21 * Version bump 1.4.1 (#155). diff --git a/ogma-core/data/formats/fcs_cocospec b/ogma-core/data/formats/fcs_cocospec new file mode 100644 index 00000000..cf41054f --- /dev/null +++ b/ogma-core/data/formats/fcs_cocospec @@ -0,0 +1,13 @@ +JSONFormat + { specInternalVars = Just "..Internal_variables[*]" + , specInternalVarId = ".name" + , specInternalVarExpr = ".assignmentCopilot" + , specInternalVarType = Just ".type" + , specExternalVars = Just "..Other_variables[*]" + , specExternalVarId = ".name" + , specExternalVarType = Just ".type" + , specRequirements = "..Requirements[*]" + , specRequirementId = ".name" + , specRequirementDesc = Just ".fretish" + , specRequirementExpr = ".CoCoSpecCode" + } diff --git a/ogma-core/data/formats/fcs_smv b/ogma-core/data/formats/fcs_smv new file mode 100644 index 00000000..708abce1 --- /dev/null +++ b/ogma-core/data/formats/fcs_smv @@ -0,0 +1,13 @@ +JSONFormat + { specInternalVars = Just "..Internal_variables[*]" + , specInternalVarId = ".name" + , specInternalVarExpr = ".assignmentCopilot" + , specInternalVarType = Just ".type" + , specExternalVars = Just "..Other_variables[*]" + , specExternalVarId = ".name" + , specExternalVarType = Just ".type" + , specRequirements = "..Requirements[*]" + , specRequirementId = ".name" + , specRequirementDesc = Just ".fretish" + , specRequirementExpr = ".ptLTL" + } diff --git a/ogma-core/data/formats/fdb_cocospec b/ogma-core/data/formats/fdb_cocospec new file mode 100644 index 00000000..1519b0fe --- /dev/null +++ b/ogma-core/data/formats/fdb_cocospec @@ -0,0 +1,13 @@ +JSONFormat + { specInternalVars = Nothing + , specInternalVarId = "" + , specInternalVarExpr = "" + , specInternalVarType = Nothing + , specExternalVars = Just ".semantics.variables..*.*" + , specExternalVarId = "" + , specExternalVarType = Nothing + , specRequirements = "$[:]" + , specRequirementId = ".reqid" + , specRequirementDesc = Just ".fulltext" + , specRequirementExpr = ".semantics.CoCoSpecCode" + } diff --git a/ogma-core/data/formats/fdb_smv b/ogma-core/data/formats/fdb_smv new file mode 100644 index 00000000..59252cf7 --- /dev/null +++ b/ogma-core/data/formats/fdb_smv @@ -0,0 +1,13 @@ +JSONFormat + { specInternalVars = Nothing + , specInternalVarId = "" + , specInternalVarExpr = "" + , specInternalVarType = Nothing + , specExternalVars = Just ".semantics.variables..*.*" + , specExternalVarId = "" + , specExternalVarType = Nothing + , specRequirements = "$[:]" + , specRequirementId = ".reqid" + , specRequirementDesc = Just ".fulltext" + , specRequirementExpr = ".semantics.ptExpanded" + } diff --git a/ogma-core/ogma-core.cabal b/ogma-core/ogma-core.cabal index 975a0f8c..97743b34 100644 --- a/ogma-core/ogma-core.cabal +++ b/ogma-core/ogma-core.cabal @@ -32,7 +32,7 @@ cabal-version: 2.0 build-type: Simple name: ogma-core -version: 1.4.1 +version: 1.5.0 homepage: https://github.com/nasa/ogma license: OtherLicense license-file: LICENSE.pdf @@ -62,11 +62,16 @@ data-files: templates/copilot-cfs/CMakeLists.txt templates/copilot-cfs/fsw/src/copilot_cfs_events.h templates/ros/Dockerfile templates/ros/copilot/CMakeLists.txt - templates/ros/copilot/src/.keep + templates/ros/copilot/src/copilot_logger.cpp + templates/ros/copilot/src/copilot_monitor.cpp templates/ros/copilot/package.xml templates/fprime/CMakeLists.txt templates/fprime/Dockerfile templates/fprime/instance-copilot + data/formats/fcs_smv + data/formats/fcs_cocospec + data/formats/fdb_smv + data/formats/fdb_cocospec -- Ogma packages should be uncurated so that only the official maintainers make -- changes. @@ -82,10 +87,9 @@ library Command.CStructs2Copilot Command.CStructs2MsgHandlers Command.FPrimeApp - Command.FRETComponentSpec2Copilot - Command.FRETReqsDB2Copilot Command.Result Command.ROSApp + Command.Standalone Data.Location @@ -108,14 +112,15 @@ library , bytestring , filepath , mtl - - , ogma-extra >= 1.4.1 && < 1.5 - , ogma-language-c >= 1.4.1 && < 1.5 - , ogma-language-cocospec >= 1.4.1 && < 1.5 - , ogma-language-copilot >= 1.4.1 && < 1.5 - , ogma-language-jsonspec >= 1.4.1 && < 1.5 - , ogma-language-smv >= 1.4.1 && < 1.5 - , ogma-spec >= 1.4.1 && < 1.5 + , text >= 1.2.3.1 && < 2.1 + + , ogma-extra >= 1.5.0 && < 1.6 + , ogma-language-c >= 1.5.0 && < 1.6 + , ogma-language-cocospec >= 1.5.0 && < 1.6 + , ogma-language-copilot >= 1.5.0 && < 1.6 + , ogma-language-jsonspec >= 1.5.0 && < 1.6 + , ogma-language-smv >= 1.5.0 && < 1.6 + , ogma-spec >= 1.5.0 && < 1.6 hs-source-dirs: src diff --git a/ogma-core/src/Command/CFSApp.hs b/ogma-core/src/Command/CFSApp.hs index 26bdc8ff..1c5b35f1 100644 --- a/ogma-core/src/Command/CFSApp.hs +++ b/ogma-core/src/Command/CFSApp.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE OverloadedStrings #-} -- Copyright 2020 United States Government as represented by the Administrator -- of the National Aeronautics and Space Administration. All Rights Reserved. -- @@ -45,16 +46,17 @@ module Command.CFSApp where -- External imports -import qualified Control.Exception as E -import Data.List ( find ) -import System.FilePath ( () ) - --- External imports: auxiliary -import System.Directory.Extra ( copyDirectoryRecursive ) +import qualified Control.Exception as E +import Data.Aeson (decode, object, (.=)) +import Data.List (find) +import Data.Text (Text) +import Data.Text.Lazy (pack, unpack) +import System.FilePath ( () ) -- Internal imports: auxiliary -import Command.Result ( Result (..) ) -import Data.Location ( Location (..) ) +import Command.Result ( Result (..) ) +import Data.Location ( Location (..) ) +import System.Directory.Extra ( copyTemplate ) -- Internal imports import Paths_ogma_core ( getDataDir ) @@ -62,13 +64,14 @@ import Paths_ogma_core ( getDataDir ) -- | Generate a new CFS application connected to Copilot. cFSApp :: FilePath -- ^ Target directory where the application -- should be created. + -> Maybe FilePath -- ^ Directory where the template is to be found. -> FilePath -- ^ File containing a list of variables to make -- available to Copilot. -> Maybe FilePath -- ^ File containing a list of known variables -- with their types and the message IDs they -- can be obtained from. -> IO (Result ErrorCode) -cFSApp targetDir varNameFile varDBFile = do +cFSApp targetDir mTemplateDir varNameFile varDBFile = do -- We first try to open the two files we need to fill in details in the CFS -- app template. @@ -97,12 +100,13 @@ cFSApp targetDir varNameFile varDBFile = do Right varNames -> do -- Obtain template dir - dataDir <- getDataDir - let templateDir = dataDir "templates" "copilot-cfs" + templateDir <- case mTemplateDir of + Just x -> return x + Nothing -> do + dataDir <- getDataDir + return $ dataDir "templates" "copilot-cfs" E.handle (return . cannotCopyTemplate) $ do - -- Expand template - copyDirectoryRecursive templateDir targetDir let f n o@(oVars, oIds, oInfos, oDatas) = case variableMap varDB n of @@ -113,10 +117,18 @@ cFSApp targetDir varNameFile varDBFile = do -- This is a Data.List.unzip4 let (vars, ids, infos, datas) = foldr f ([], [], [], []) varNames - let cfsFileName = targetDir "fsw" "src" "copilot_cfs.c" - cfsFileContents = unlines $ fileContents vars ids infos datas + let (variablesS, msgSubscriptionS, msgCasesS, msgHandlerS) = + appComponents vars ids infos datas + subst = object $ + [ "variablesS" .= pack variablesS + , "msgSubscriptionsS" .= pack msgSubscriptionS + , "msgCasesS" .= pack msgCasesS + , "msgHandlerS" .= pack msgHandlerS + ] + + -- Expand template + copyTemplate templateDir subst targetDir - writeFile cfsFileName cfsFileContents return Success -- | Predefined list of Icarous variables that are known to Ogma @@ -170,9 +182,10 @@ data MsgData = MsgData , msgDataVarType :: String } --- | Return the contents of the main CFS application. -fileContents :: [VarDecl] -> [MsgInfoId] -> [MsgInfo] -> [MsgData] -> [String] -fileContents variables msgIds msgNames msgDatas = cfsFileContents +-- | Return the components that are customized in a cFS application. +appComponents :: [VarDecl] -> [MsgInfoId] -> [MsgInfo] -> [MsgData] + -> (String, String, String, String) +appComponents variables msgIds msgNames msgDatas = cfsFileContents where variablesS = unlines $ map toVarDecl variables toVarDecl varDecl = varDeclType varDecl ++ " " ++ varDeclName varDecl ++ ";" @@ -205,157 +218,11 @@ fileContents variables msgIds msgNames msgDatas = cfsFileContents ] cfsFileContents = - [ "/********************************************************************" - , "** File: copilot_cfs.c" - , "**" - , "** Purpose:" - , "** This file contains the source code for the Copilot App." - , "**" - , "*********************************************************************/" - , "" - , "/*" - , "** Include Files:" - , "*/" - , "" - , "#include \"copilot_cfs.h\"" - , "#include \"copilot_cfs_perfids.h\"" - , "#include \"copilot_cfs_msgids.h\"" - , "#include \"copilot_cfs_msg.h\"" - , "#include \"copilot_cfs_events.h\"" - , "#include \"copilot_cfs_version.h\"" - , "#include \"Icarous_msgids.h\"" - , "#include \"Icarous_msg.h\"" - , "" - , variablesS - , "void split(void);" - , "void step(void);" - , "" - , "/*" - , "** global data" - , "*/" - , "" - , "copilot_hk_tlm_t COPILOT_HkTelemetryPkt;" - , "CFE_SB_PipeId_t COPILOT_CommandPipe;" - , "CFE_SB_MsgPtr_t COPILOTMsgPtr;" - , "" - , "static CFE_EVS_BinFilter_t COPILOT_EventFilters[] =" - , " { /* Event ID mask */" - , " {COPILOT_STARTUP_INF_EID, 0x0000}," - , " {COPILOT_COMMAND_ERR_EID, 0x0000}," - , " {COPILOT_COMMANDCPVIOL_INF_EID, 0x0000}," - , " };" - , "" - , "/* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */" - , "/* COPILOT_AppMain() -- App entry point and main process loop */" - , "/* */" - , "/* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */" - , "void COPILOT_AppMain( void )" - , "{" - , " int32 status;" - , " uint32 RunStatus = CFE_ES_APP_RUN;" - , "" - , " CFE_ES_PerfLogEntry(COPILOT_CFS_PERF_ID);" - , "" - , " COPILOT_AppInit();" - , "" - , " /*" - , " ** COPILOT Runloop" - , " */" - , " while (CFE_ES_RunLoop(&RunStatus) == TRUE)" - , " {" - , " CFE_ES_PerfLogExit(COPILOT_CFS_PERF_ID);" - , "" - , " // Pend on receipt of command packet" - , " // (timeout set to 500 millisecs)" - , " status = CFE_SB_RcvMsg (&COPILOTMsgPtr," - , " COPILOT_CommandPipe," - , " 500);" - , " " - , " CFE_ES_PerfLogEntry(COPILOT_CFS_PERF_ID);" - , "" - , " if (status == CFE_SUCCESS)" - , " {" - , " COPILOT_ProcessCommandPacket();" - , " }" - , "" - , " }" - , "" - , " CFE_ES_ExitApp(RunStatus);" - , "" - , "} /* End of COPILOT_AppMain() */" - , "" - , "/* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */" - , "/* */" - , "/* COPILOT_AppInit() -- initialization */" - , "/* */" - , "/* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */" - , "void COPILOT_AppInit(void)" - , "{" - , " // Register the app with Executive services" - , " CFE_ES_RegisterApp();" - , "" - , " // Register the events" - , " CFE_EVS_Register(COPILOT_EventFilters," - , " sizeof(COPILOT_EventFilters) / " - ++ "sizeof(CFE_EVS_BinFilter_t)," - , " CFE_EVS_BINARY_FILTER);" - , "" - , " // Create the Software Bus command pipe and subscribe to " - , " // housekeeping messages" - , " CFE_SB_CreatePipe(&COPILOT_CommandPipe, COPILOT_PIPE_DEPTH," - ++ "\"COPILOT_CMD_PIPE\");" + ( variablesS , msgSubscriptionS - , "" - , " CFE_EVS_SendEvent (COPILOT_STARTUP_INF_EID," - , " CFE_EVS_INFORMATION," - , " \"COPILOT App Initialized. Ver %d.%d.%d.%d\"," - , " COPILOT_CFS_MAJOR_VERSION," - , " COPILOT_CFS_MINOR_VERSION, " - , " COPILOT_CFS_REVISION, " - , " COPILOT_CFS_MISSION_REV);" - , "" - , "} /* End of COPILOT_AppInit() */" - , "" - , "/* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */" - , "/* Name: COPILOT_ProcessCommandPacket */" - , "/* */" - , "/* Purpose: */" - , "/* This routine will process any packet that is received */" - , "/* on the COPILOT command pipe. */" - , "/* */" - , "/* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */" - , "void COPILOT_ProcessCommandPacket(void)" - , "{" - , " CFE_SB_MsgId_t MsgId;" - , "" - , " MsgId = CFE_SB_GetMsgId(COPILOTMsgPtr);" - , "" - , " switch (MsgId)" - , " {" , msgCasesS - , " default:" - , " COPILOT_HkTelemetryPkt.copilot_command_error_count++;" - , " CFE_EVS_SendEvent(COPILOT_COMMAND_ERR_EID,CFE_EVS_ERROR," - , " " - ++ "\"COPILOT: invalid command packet,MID = 0x%x\"," - , " MsgId);" - , " break;" - , " }" - , "" - , " return;" - , "" - , "} /* End COPILOT_ProcessCommandPacket */" - , "" , msgHandlerS - , "" - , "/**" - , " * Report copilot property violations." - , " */" - , "void split(void) {" - , " CFE_EVS_SendEvent(COPILOT_COMMANDCPVIOL_INF_EID, CFE_EVS_ERROR," - , " \"COPILOT: violation\");" - , "}" - ] + ) -- * Exception handlers diff --git a/ogma-core/src/Command/FRETComponentSpec2Copilot.hs b/ogma-core/src/Command/FRETComponentSpec2Copilot.hs deleted file mode 100644 index 74ed887c..00000000 --- a/ogma-core/src/Command/FRETComponentSpec2Copilot.hs +++ /dev/null @@ -1,204 +0,0 @@ -{-# LANGUAGE ExistentialQuantification #-} --- 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. --- --- | Transform a FRET component specification into a Copilot specification. --- --- This module makes use of --- "Language.Trans.FRETComponentSpec2Copilot", which does most of the work. -module Command.FRETComponentSpec2Copilot - ( fretComponentSpec2Copilot - , FRETComponentSpec2CopilotOptions(..) - , ErrorCode - ) - where - --- External imports -import Data.Aeson ( eitherDecode, decode ) -import Data.ByteString.Lazy (fromStrict) -import Data.Foldable (for_) - --- External imports: auxiliary -import Data.ByteString.Extra as B ( safeReadFile ) - --- Internal imports: auxiliary -import Command.Result ( Result (..) ) -import Data.Location ( Location (..) ) - --- Internal imports: language ASTs, transformers -import Data.OgmaSpec (Spec) - -import qualified Language.CoCoSpec.AbsCoCoSpec as CoCoSpec -import qualified Language.CoCoSpec.ParCoCoSpec as CoCoSpec ( myLexer, - pBoolSpec ) - -import Language.JSONSpec.Parser (JSONFormat (..), parseJSONSpec) - -import qualified Language.SMV.AbsSMV as SMV -import qualified Language.SMV.ParSMV as SMV (myLexer, pBoolSpec) -import Language.SMV.Substitution (substituteBoolExpr) - -import qualified Language.Trans.CoCoSpec2Copilot as CoCoSpec (boolSpec2Copilot) -import Language.Trans.SMV2Copilot as SMV (boolSpec2Copilot) -import Language.Trans.Spec2Copilot (spec2Copilot, specAnalyze) - --- | Print the contents of a Copilot module that implements the Past-time TL --- formula in a FRET file. --- --- PRE: The file given is readable, contains a valid FRET file with a PT --- formula in the @ptExpanded@ key, the formula does not use any identifiers --- that exist in Copilot, or any of @prop@, @clock@, @ftp@. All identifiers --- used are valid C99 identifiers. -fretComponentSpec2Copilot :: FilePath -- ^ Path to a file containing a FRET - -- Component Specification - -> FRETComponentSpec2CopilotOptions - -- ^ Customization options - -- formula - -> IO (Result ErrorCode) -fretComponentSpec2Copilot fp options = do - - let functions = fretExprPair (fretCS2CopilotUseCoCoSpec options) - - copilot <- fretComponentSpec2Copilot' fp options functions - - let (mOutput, result) = - fretComponentSpec2CopilotResult options fp copilot - - for_ mOutput putStrLn - return result - --- | Print the contents of a Copilot module that implements the Past-time TL --- formula in a FRET file, using a subexpression handler. --- --- PRE: The file given is readable, contains a valid FRET file with a PT --- formula in the @ptExpanded@ key, the formula does not use any identifiers --- that exist in Copilot, or any of @prop@, @clock@, @ftp@. All identifiers --- used are valid C99 identifiers. -fretComponentSpec2Copilot' :: FilePath - -> FRETComponentSpec2CopilotOptions - -> FRETExprPair - -> IO (Either String String) -fretComponentSpec2Copilot' fp options (FRETExprPair parse replace print) = do - let name = fretCS2CopilotFilename options - useCoCoSpec = fretCS2CopilotUseCoCoSpec options - typeMaps = fretTypeToCopilotTypeMapping options - - -- All of the following operations use Either to return error messages. The - -- use of the monadic bind to pass arguments from one function to the next - -- will cause the program to stop at the earliest error. - content <- B.safeReadFile fp - res <- case content of - Left s -> return $ Left s - Right b -> return $ parseJSONSpec parse (fretFormat useCoCoSpec) =<< eitherDecode b - - let copilot = spec2Copilot name typeMaps replace print =<< specAnalyze =<< res - - return copilot - --- | Options used to customize the conversion of FRET Component Specifications --- to Copilot code. -data FRETComponentSpec2CopilotOptions = FRETComponentSpec2CopilotOptions - { fretCS2CopilotUseCoCoSpec :: Bool - , fretCS2CopilotIntType :: String - , fretCS2CopilotRealType :: String - , fretCS2CopilotFilename :: String - } - --- * Error codes - --- | Encoding of reasons why the command can fail. --- --- The error code used is 1 for user error. -type ErrorCode = Int - --- | Error: the FRET Component Spec file cannot be read due to the file being --- unreadable or the format being incorrect. -ecFretCSError :: ErrorCode -ecFretCSError = 1 - --- * Result - --- | Process the result of the transformation function. -fretComponentSpec2CopilotResult :: FRETComponentSpec2CopilotOptions - -> FilePath - -> Either String String - -> (Maybe String, Result ErrorCode) -fretComponentSpec2CopilotResult options fp result = case result of - Left msg -> (Nothing, Error ecFretCSError msg (LocationFile fp)) - Right t -> (Just t, Success) - --- * Parser - --- | JSONPath selectors for a FRET file -fretFormat :: Bool -> JSONFormat -fretFormat useCoCoSpec = JSONFormat - { specInternalVars = Just "..Internal_variables[*]" - , specInternalVarId = ".name" - , specInternalVarExpr = ".assignmentCopilot" - , specInternalVarType = Just ".type" - , specExternalVars = Just "..Other_variables[*]" - , specExternalVarId = ".name" - , specExternalVarType = Just ".type" - , specRequirements = "..Requirements[*]" - , specRequirementId = ".name" - , specRequirementDesc = Just ".fretish" - , specRequirementExpr = if useCoCoSpec then ".CoCoSpecCode" else ".ptLTL" - } - --- * Mapping of types from FRET to Copilot -fretTypeToCopilotTypeMapping :: FRETComponentSpec2CopilotOptions - -> [(String, String)] -fretTypeToCopilotTypeMapping options = - [ ("bool", "Bool") - , ("int", fretCS2CopilotIntType options) - , ("integer", fretCS2CopilotIntType options) - , ("real", fretCS2CopilotRealType options) - , ("string", "String") - ] - --- * Handler for boolean expressions - --- | Handler for boolean expressions that knows how to parse them, replace --- variables in them, and convert them to Copilot. -data FRETExprPair = forall a . FRETExprPair - { exprParse :: String -> Either String a - , exprReplace :: [(String, String)] -> a -> a - , exprPrint :: a -> String - } - --- | Return a handler depending on whether it should be for CoCoSpec boolean --- expressions or for SMV boolean expressions. -fretExprPair :: Bool -> FRETExprPair -fretExprPair True = FRETExprPair (CoCoSpec.pBoolSpec . CoCoSpec.myLexer) - (\_ -> id) - (CoCoSpec.boolSpec2Copilot) -fretExprPair False = FRETExprPair (SMV.pBoolSpec . SMV.myLexer) - (substituteBoolExpr) - (SMV.boolSpec2Copilot) diff --git a/ogma-core/src/Command/ROSApp.hs b/ogma-core/src/Command/ROSApp.hs index 9528b34f..9c673706 100644 --- a/ogma-core/src/Command/ROSApp.hs +++ b/ogma-core/src/Command/ROSApp.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE OverloadedStrings #-} -- Copyright 2022 United States Government as represented by the Administrator -- of the National Aeronautics and Space Administration. All Rights Reserved. -- @@ -46,15 +47,16 @@ module Command.ROSApp import qualified Control.Exception as E import Control.Monad.Except (ExceptT, liftEither, liftIO, runExceptT, throwError) -import Data.Aeson (eitherDecode) +import Data.Aeson (eitherDecode, object, (.=)) import Data.List (find, intersperse) import Data.Maybe (fromMaybe) +import Data.Text.Lazy (pack) import System.FilePath (()) -- External imports: auxiliary import Data.ByteString.Extra as B (safeReadFile) import Data.String.Extra (sanitizeLCIdentifier, sanitizeUCIdentifier) -import System.Directory.Extra (copyDirectoryRecursive) +import System.Directory.Extra (copyTemplate) -- External imports: ogma import Data.OgmaSpec (Spec, externalVariableName, externalVariables, @@ -73,6 +75,7 @@ import Paths_ogma_core ( getDataDir ) -- | Generate a new ROS application connected to Copilot. rosApp :: FilePath -- ^ Target directory where the application -- should be created. + -> Maybe FilePath -- ^ Directory where the template is to be found. -> Maybe FilePath -- ^ FRET Component specification file. -> Maybe FilePath -- ^ File containing a list of variables to make -- available to Copilot. @@ -83,7 +86,7 @@ rosApp :: FilePath -- ^ Target directory where the application -- Copilot specification. The handlers are assumed -- to receive no arguments. -> IO (Result ErrorCode) -rosApp targetDir fretCSFile varNameFile varDBFile handlersFile = +rosApp targetDir mTemplateDir fretCSFile varNameFile varDBFile handlersFile = processResult $ do cs <- parseOptionalFRETCS fretCSFile vs <- parseOptionalVariablesFile varNameFile @@ -95,13 +98,15 @@ rosApp targetDir fretCSFile varNameFile varDBFile handlersFile = let varNames = fromMaybe (fretCSExtractExternalVariables cs) vs monitors = fromMaybe (fretCSExtractHandlers cs) rs - e <- liftIO $ rosApp' targetDir varNames varDB monitors + e <- liftIO $ rosApp' targetDir mTemplateDir varNames varDB monitors liftEither e -- | Generate a new ROS application connected to Copilot, by copying the -- template and filling additional necessary files. rosApp' :: FilePath -- ^ Target directory where the -- application should be created. + -> Maybe FilePath -- ^ Directory where the template + -- is to be found. -> [String] -- ^ List of variable names -- (data sources). -> [(String, String, String, String)] -- ^ List of variables with their @@ -112,14 +117,14 @@ rosApp' :: FilePath -- ^ Target directory where the -- to the monitors (or -- requirements monitored). -> IO (Either ErrorTriplet ()) -rosApp' targetDir varNames varDB monitors = +rosApp' targetDir mTemplateDir varNames varDB monitors = E.handle (return . Left . cannotCopyTemplate) $ do -- Obtain template dir - dataDir <- getDataDir - let templateDir = dataDir "templates" "ros" - - -- Expand template - copyDirectoryRecursive templateDir targetDir + templateDir <- case mTemplateDir of + Just x -> return x + Nothing -> do + dataDir <- getDataDir + return $ dataDir "templates" "ros" let f n o@(oVars, oIds, oInfos, oDatas) = case variableMap varDB n of @@ -135,21 +140,29 @@ rosApp' targetDir varNames varDB monitors = let (vars, ids, infos, datas) = foldr f ([], [], [], []) varNames - let rosFileName = - targetDir "copilot" "src" "copilot_monitor.cpp" - rosFileContents = - unlines $ - rosMonitorContents varNames vars ids infos datas monitors - - writeFile rosFileName rosFileContents - - let rosFileName = - targetDir "copilot" "src" "copilot_logger.cpp" - rosFileContents = - unlines $ - rosLoggerContents varNames vars ids infos datas monitors - - writeFile rosFileName rosFileContents + let (variablesS, msgSubscriptionS, msgPublisherS, + msgHandlerInClassS, msgCallbacks, msgSubscriptionDeclrs, + msgPublisherDeclrs, msgHandlerGlobalS) = + rosMonitorComponents varNames vars ids infos datas monitors + + (logMsgSubscriptionS, logMsgCallbacks, logMsgSubscriptionDeclrs) = + rosLoggerComponents varNames vars ids infos datas monitors + + subst = object $ + [ "variablesS" .= pack variablesS + , "msgSubscriptionS" .= pack msgSubscriptionS + , "msgPublisherS" .= pack msgPublisherS + , "msgHandlerInClassS" .= pack msgHandlerInClassS + , "msgCallbacks" .= pack msgCallbacks + , "msgSubscriptionDeclrs" .= pack msgSubscriptionDeclrs + , "msgPublisherDeclrs" .= pack msgPublisherDeclrs + , "msgHandlerGlobalS" .= pack msgHandlerGlobalS + , "logMsgSubscriptionS" .= pack logMsgSubscriptionS + , "logMsgCallbacks" .= pack logMsgCallbacks + , "logMsgSubscriptionDeclrs" .= pack logMsgSubscriptionDeclrs + ] + + copyTemplate templateDir subst targetDir return $ Right () @@ -301,52 +314,24 @@ data MsgData = MsgData -- * ROS apps content -- | Return the contents of the main ROS application. -rosMonitorContents :: [String] -- Variables - -> [VarDecl] - -> [MsgInfoId] - -> [MsgInfo] - -> [MsgData] - -> [String] -- Monitors - -> [String] -rosMonitorContents varNames variables msgIds msgNames msgDatas monitors = - [ "#include " - , "#include " - , "" - , "#include \"rclcpp/rclcpp.hpp\"" - , "" - , typeIncludes - , copilotIncludes - , "using std::placeholders::_1;" - , "" - , variablesS - , "class CopilotRV : public rclcpp::Node {" - , " public:" - , " CopilotRV() : Node(\"copilotrv\") {" +rosMonitorComponents + :: [String] -- Variables + -> [VarDecl] + -> [MsgInfoId] + -> [MsgInfo] + -> [MsgData] + -> [String] -- Monitors + -> (String, String, String, String, String, String, String, String) +rosMonitorComponents varNames variables msgIds msgNames msgDatas monitors = + ( variablesS , msgSubscriptionS , msgPublisherS - , " }" - , "" , msgHandlerInClassS - , " // Needed so we can report messages to the log." - , " static CopilotRV& getInstance() {" - , " static CopilotRV instance;" - , " return instance;" - , " }" - , "" - , " private:" , msgCallbacks , msgSubscriptionDeclrs , msgPublisherDeclrs - , "};" - , "" , msgHandlerGlobalS - , "int main(int argc, char* argv[]) {" - , " rclcpp::init(argc, argv);" - , " rclcpp::spin(std::make_shared());" - , " rclcpp::shutdown();" - , " return 0;" - , "}" - ] + ) where @@ -369,27 +354,6 @@ rosMonitorContents varNames variables msgIds msgNames msgDatas monitors = publisher = monitor ++ "_publisher_" - typeIncludes = unlines - [ "#include \"std_msgs/msg/bool.hpp\"" - , "#include \"std_msgs/msg/empty.hpp\"" - , "#include \"std_msgs/msg/u_int8.hpp\"" - , "#include \"std_msgs/msg/u_int16.hpp\"" - , "#include \"std_msgs/msg/u_int32.hpp\"" - , "#include \"std_msgs/msg/u_int64.hpp\"" - , "#include \"std_msgs/msg/int8.hpp\"" - , "#include \"std_msgs/msg/int16.hpp\"" - , "#include \"std_msgs/msg/int32.hpp\"" - , "#include \"std_msgs/msg/int64.hpp\"" - , "#include \"std_msgs/msg/float32.hpp\"" - , "#include \"std_msgs/msg/float64.hpp\"" - , "#include " - ] - - copilotIncludes = unlines - [ "#include \"monitor.h\"" - , "#include \"monitor.c\"" - ] - variablesS = unlines $ map toVarDecl variables toVarDecl varDecl = varDeclType' varDecl ++ " " ++ varDeclName varDecl ++ ";" @@ -515,50 +479,18 @@ rosMonitorContents varNames variables msgIds msgNames msgDatas monitors = publisher = nm ++ "_publisher_" -- | Return the contents of the logger ROS application. -rosLoggerContents :: [String] -- Variables - -> [VarDecl] - -> [MsgInfoId] - -> [MsgInfo] - -> [MsgData] - -> [String] -- Monitors - -> [String] -rosLoggerContents varNames variables msgIds msgNames msgDatas monitors = - rosFileContents +rosLoggerComponents :: [String] -- Variables + -> [VarDecl] + -> [MsgInfoId] + -> [MsgInfo] + -> [MsgData] + -> [String] -- Monitors + -> (String, String, String) +rosLoggerComponents varNames variables msgIds msgNames msgDatas monitors = + (msgSubscriptionS, msgCallbacks, msgSubscriptionDeclrs) where - rosFileContents = - [ "#include " - , "#include " - , "" - , "#include \"rclcpp/rclcpp.hpp\"" - , "" - , typeIncludes - , "using std::placeholders::_1;" - , "" - , "class CopilotLogger : public rclcpp::Node {" - , " public:" - , " CopilotLogger() : Node(\"copilotlogger\") {" - , msgSubscriptionS - , " }" - , "" - , " private:" - , msgCallbacks - , msgSubscriptionDeclrs - , "};" - , "" - , "int main(int argc, char* argv[]) {" - , " rclcpp::init(argc, argv);" - , " rclcpp::spin(std::make_shared());" - , " rclcpp::shutdown();" - , " return 0;" - , "}" - ] - - typeIncludes = unlines - [ "#include \"std_msgs/msg/empty.hpp\"" - ] - msgSubscriptionS = unlines $ concat $ intersperse [""] diff --git a/ogma-core/src/Command/FRETReqsDB2Copilot.hs b/ogma-core/src/Command/Standalone.hs similarity index 51% rename from ogma-core/src/Command/FRETReqsDB2Copilot.hs rename to ogma-core/src/Command/Standalone.hs index 7dc52b9c..5d963141 100644 --- a/ogma-core/src/Command/FRETReqsDB2Copilot.hs +++ b/ogma-core/src/Command/Standalone.hs @@ -29,37 +29,43 @@ -- FOR ANY SUCH MATTER SHALL BE THE IMMEDIATE, UNILATERAL TERMINATION OF THIS -- AGREEMENT. -- --- | Transform a FRET requirements database containing a temporal logic --- specification into a Copilot specification. -module Command.FRETReqsDB2Copilot - ( fretReqsDB2Copilot - , FRETReqsDB2CopilotOptions(..) +-- | Transform a specification into a standalone Copilot specification. +module Command.Standalone + ( standalone + , StandaloneOptions(..) , ErrorCode ) where -- External imports -import Data.Aeson (eitherDecode) -import Data.Foldable (for_) -import Data.List (nub, (\\)) +import Data.Aeson (decode, eitherDecode) +import Data.ByteString.Lazy (fromStrict, pack) +import Data.Foldable (for_) +import Data.List (nub, (\\)) +import Data.Maybe (fromMaybe) +import System.FilePath (()) -- External imports: auxiliary import Data.ByteString.Extra as B ( safeReadFile ) -- Internal imports: auxiliary -import Command.Result ( Result (..) ) -import Data.Location ( Location (..) ) +import Command.Result (Result (..)) +import Data.Location (Location (..)) +import Paths_ogma_core (getDataDir) --- Internal imports: Generic specification, parser. -import Data.OgmaSpec (ExternalVariableDef (..), - InternalVariableDef (..), Requirement (..), - Spec (..)) +-- Internal imports: language ASTs, transformers +import Data.OgmaSpec (ExternalVariableDef (..), InternalVariableDef (..), + Requirement (..), Spec (..)) import Language.JSONSpec.Parser (JSONFormat (..), parseJSONSpec) -- Internal imports: language ASTs, transformers -import qualified Language.CoCoSpec.ParCoCoSpec as CoCoSpec (myLexer, pBoolSpec) -import qualified Language.SMV.ParSMV as SMV (myLexer, pBoolSpec) -import Language.SMV.Substitution (substituteBoolExpr) +import qualified Language.CoCoSpec.AbsCoCoSpec as CoCoSpec +import qualified Language.CoCoSpec.ParCoCoSpec as CoCoSpec ( myLexer, + pBoolSpec ) + +import qualified Language.SMV.AbsSMV as SMV +import qualified Language.SMV.ParSMV as SMV (myLexer, pBoolSpec) +import Language.SMV.Substitution (substituteBoolExpr) import qualified Language.Trans.CoCoSpec2Copilot as CoCoSpec (boolSpec2Copilot, boolSpecNames) @@ -67,45 +73,49 @@ import Language.Trans.SMV2Copilot as SMV (boolSpec2Copilot, boolSpecNames) import Language.Trans.Spec2Copilot (spec2Copilot, specAnalyze) --- | Print the contents of a Copilot module that implements the Past-time TL --- formula in a FRET file. +-- | Print the contents of a Copilot module that implements the spec in an +-- input file. -- --- PRE: The file given is readable, contains a valid FRET file with a PT --- formula in the @ptExpanded@ key, the formula does not use any identifiers --- that exist in Copilot, or any of @prop@, @clock@, @ftp@. All identifiers +-- PRE: The file given is readable, contains a valid file with recognizable +-- format, the formulas in the file do not use any identifiers that exist in +-- Copilot, or any of @prop@, @clock@, @ftp@, @notPreviousNot@. All identifiers -- used are valid C99 identifiers. -fretReqsDB2Copilot :: FilePath -- ^ Path to a file containing a FRET - -- Requirements Database - -> FRETReqsDB2CopilotOptions - -- ^ Customization options formula - -> IO (Result ErrorCode) -fretReqsDB2Copilot fp options = do +standalone :: FilePath -- ^ Path to a file containing a specification + -> StandaloneOptions -- ^ Customization options + -> IO (Result ErrorCode) +standalone fp options = do - let functions = fretExprPair (fretReqsDB2CopilotUseCoCoSpec options) + let functions = exprPair (standalonePropFormat options) - copilot <- fretReqsDB2Copilot' fp options functions + copilot <- standalone' fp options functions - let (mOutput, result) = - fretReqsDB2CopilotResult options fp copilot + let (mOutput, result) = standaloneResult options fp copilot for_ mOutput putStrLn return result --- | Print the contents of a Copilot module that implements the Past-time TL --- formula in a FRET file, using a subexpression handler. +-- | Print the contents of a Copilot module that implements the spec in an +-- input file, using a subexpression handler. -- --- PRE: The file given is readable, contains a valid FRET file with a PT --- formula in the @ptExpanded@ key, the formula does not use any identifiers --- that exist in Copilot, or any of @prop@, @clock@, @ftp@. All identifiers +-- PRE: The file given is readable, contains a valid file with recognizable +-- format, the formulas in the file do not use any identifiers that exist in +-- Copilot, or any of @prop@, @clock@, @ftp@, @notPreviousNot@. All identifiers -- used are valid C99 identifiers. -fretReqsDB2Copilot' :: FilePath - -> FRETReqsDB2CopilotOptions - -> FRETExprPair - -> IO (Either String String) -fretReqsDB2Copilot' fp options (FRETExprPair parse replace showExpr ids) = do - let name = fretReqsDB2CopilotFilename options - useCoCoSpec = fretReqsDB2CopilotUseCoCoSpec options - typeMaps = [("", "_")] +standalone' :: FilePath + -> StandaloneOptions + -> ExprPair + -> IO (Either String String) +standalone' fp options (ExprPair parse replace print ids) = do + let name = standaloneFilename options + typeMaps = typeToCopilotTypeMapping options + + -- Obtain format file + dataDir <- getDataDir + let formatFile = + dataDir "data" "formats" + (standaloneFormat options ++ "_" ++ standalonePropFormat options) + + format <- read <$> readFile formatFile -- All of the following operations use Either to return error messages. The -- use of the monadic bind to pass arguments from one function to the next @@ -113,21 +123,22 @@ fretReqsDB2Copilot' fp options (FRETExprPair parse replace showExpr ids) = do content <- B.safeReadFile fp res <- case content of Left s -> return $ Left s - Right b -> return $ parseJSONSpec parse (fretFormat useCoCoSpec) =<< eitherDecode b + Right b -> return $ parseJSONSpec parse format =<< eitherDecode b -- Complement the specification with any missing/implicit definitions let res' = fmap (addMissingIdentifiers ids) res - let copilot = - spec2Copilot name typeMaps replace showExpr =<< specAnalyze =<< res' + let copilot = spec2Copilot name typeMaps replace print =<< specAnalyze =<< res' return copilot --- | Options used to customize the conversion of FRET Requirements Database --- to Copilot code. -data FRETReqsDB2CopilotOptions = FRETReqsDB2CopilotOptions - { fretReqsDB2CopilotUseCoCoSpec :: Bool - , fretReqsDB2CopilotFilename :: String +-- | Options used to customize the conversion of specifications to Copilot +-- code. +data StandaloneOptions = StandaloneOptions + { standaloneFormat :: String + , standalonePropFormat :: String + , standaloneTypeMapping :: [(String, String)] + , standaloneFilename :: String } -- * Error codes @@ -137,45 +148,43 @@ data FRETReqsDB2CopilotOptions = FRETReqsDB2CopilotOptions -- The error code used is 1 for user error. type ErrorCode = Int --- | Error: the FRET Requirements DB file cannot be read due to the file being --- unreadable or the format being incorrect. -ecFretReqsDBError :: ErrorCode -ecFretReqsDBError = 1 +-- | Error: the input file cannot be read due to it being unreadable or the +-- format being incorrect. +ecStandaloneError :: ErrorCode +ecStandaloneError = 1 -- * Result -- | Process the result of the transformation function. -fretReqsDB2CopilotResult :: FRETReqsDB2CopilotOptions - -> FilePath - -> Either String String - -> (Maybe String, Result ErrorCode) -fretReqsDB2CopilotResult _options fp result = case result of - Left msg -> (Nothing, Error ecFretReqsDBError msg (LocationFile fp)) +standaloneResult :: StandaloneOptions + -> FilePath + -> Either String String + -> (Maybe String, Result ErrorCode) +standaloneResult options fp result = case result of + Left msg -> (Nothing, Error ecStandaloneError msg (LocationFile fp)) Right t -> (Just t, Success) --- * Parser - --- | JSONPath selectors for a FRET file -fretFormat :: Bool -> JSONFormat -fretFormat useCoCoSpec = JSONFormat - { specInternalVars = Nothing - , specInternalVarId = "" - , specInternalVarExpr = "" - , specInternalVarType = Nothing - , specExternalVars = Just ".semantics.variables..*.*" - , specExternalVarId = "" - , specExternalVarType = Nothing - , specRequirements = "$[:]" - , specRequirementId = ".reqid" - , specRequirementDesc = Just ".fulltext" - , specRequirementExpr = if useCoCoSpec then ".semantics.CoCoSpecCode" else ".semantics.ptExpanded" - } +-- * Mapping of types from input format to Copilot +typeToCopilotTypeMapping :: StandaloneOptions -> [(String, String)] +typeToCopilotTypeMapping options = + [ ("bool", "Bool") + , ("int", intType) + , ("integer", intType) + , ("real", realType) + , ("string", "String") + , ("", "_") + ] + where + intType = fromMaybe "Int64" $ lookup "int" types + realType = fromMaybe "Float" $ lookup "real" types + + types = standaloneTypeMapping options -- * Handler for boolean expressions -- | Handler for boolean expressions that knows how to parse them, replace -- variables in them, and convert them to Copilot. -data FRETExprPair = forall a . FRETExprPair +data ExprPair = forall a . ExprPair { exprParse :: String -> Either String a , exprReplace :: [(String, String)] -> a -> a , exprPrint :: a -> String @@ -183,16 +192,17 @@ data FRETExprPair = forall a . FRETExprPair } -- | Return a handler depending on whether it should be for CoCoSpec boolean --- expressions or for SMV boolean expressions. -fretExprPair :: Bool -> FRETExprPair -fretExprPair True = FRETExprPair (CoCoSpec.pBoolSpec . CoCoSpec.myLexer) - (\_ -> id) - (CoCoSpec.boolSpec2Copilot) - (CoCoSpec.boolSpecNames) -fretExprPair False = FRETExprPair (SMV.pBoolSpec . SMV.myLexer) - (substituteBoolExpr) - (SMV.boolSpec2Copilot) - (SMV.boolSpecNames) +-- expressions or for SMV boolean expressions. We default to SMV if not format +-- is given. +exprPair :: String -> ExprPair +exprPair "cocospec" = ExprPair (CoCoSpec.pBoolSpec . CoCoSpec.myLexer) + (\_ -> id) + (CoCoSpec.boolSpec2Copilot) + (CoCoSpec.boolSpecNames) +exprPair _ = ExprPair (SMV.pBoolSpec . SMV.myLexer) + (substituteBoolExpr) + (SMV.boolSpec2Copilot) + (SMV.boolSpecNames) -- | Add to a spec external variables for all identifiers mentioned in -- expressions that are not defined anywhere. diff --git a/ogma-core/src/Language/Trans/SMV2Copilot.hs b/ogma-core/src/Language/Trans/SMV2Copilot.hs index bdb0c6d7..7e48842c 100644 --- a/ogma-core/src/Language/Trans/SMV2Copilot.hs +++ b/ogma-core/src/Language/Trans/SMV2Copilot.hs @@ -29,7 +29,7 @@ -- AGREEMENT. -- --- | Transform a FRET TL specification into a Copilot specification. +-- | Transform an SMV TL specification into a Copilot specification. -- -- Normally, this module would be implemented as a conversion between ASTs, -- but we want to add comments to the generated code, which are not @@ -40,7 +40,7 @@ import Language.SMV.AbsSMV (AdditiveOp (..), BoolConst (..), BoolSpec (..), Ident (..), MultOp (..), NumExpr (..), Number (..), Op1Name (..), OpOne (..), OpTwo (..), OrdOp (..)) --- | Return the Copilot representation of a FRET BoolSpec. +-- | Return the Copilot representation of an SMV BoolSpec. -- -- This function returns the temporal property only. The string does not -- contain any top-level names, any imports, or auxiliary definitions that may @@ -96,7 +96,7 @@ boolSpec2Copilot b = case b of ++ " " ++ boolSpec2Copilot spec2 ++ ")" --- | Return the Copilot representation of a FRET boolean constant. +-- | Return the Copilot representation of an SMV boolean constant. const2Copilot :: BoolConst -> String const2Copilot BoolConstTrue = "true" const2Copilot BoolConstFalse = "false" @@ -119,17 +119,17 @@ numExpr2Copilot (NumMult x op y) = "(" ++ numExpr2Copilot y ++ ")" --- | Return the Copilot representation of a FRET additive operator. +-- | Return the Copilot representation of an SMV additive operator. additiveOp2Copilot :: AdditiveOp -> String additiveOp2Copilot OpPlus = "+" additiveOp2Copilot OpMinus = "-" --- | Return the Copilot representation of a FRET multiplicative operator. +-- | Return the Copilot representation of an SMV multiplicative operator. multOp2Copilot :: MultOp -> String multOp2Copilot OpTimes = "*" multOp2Copilot OpDiv = "/" --- | Return the Copilot representation of a FRET comparison operator. +-- | Return the Copilot representation of an SMV comparison operator. ordOp2Copilot :: OrdOp -> String ordOp2Copilot OrdOpLT = "<" ordOp2Copilot OrdOpLE = "<=" @@ -138,13 +138,13 @@ ordOp2Copilot OrdOpNE = "/=" ordOp2Copilot OrdOpGT = ">" ordOp2Copilot OrdOpGE = ">=" --- | Return the Copilot representation of a unary logical FRET operator. +-- | Return the Copilot representation of a unary logical SMV operator. opOne2Copilot :: OpOne -> String opOne2Copilot (Op1Alone x) = opOneAlone2Copilot x opOne2Copilot (Op1MTL x op v) = opOneMTL2Copilot x op v opOne2Copilot (Op1MTLRange op mn mx) = opOneMTLRange2Copilot op mn mx --- | Return the Copilot representation of a unary logical non-MTL FRET +-- | Return the Copilot representation of a unary logical non-MTL SMV -- operator. opOneAlone2Copilot :: Op1Name -> String opOneAlone2Copilot Op1Pre = "pre" @@ -156,7 +156,7 @@ opOneAlone2Copilot Op1Z = "notPreviousNot" opOneAlone2Copilot Op1Hist = "PTLTL.alwaysBeen" opOneAlone2Copilot Op1O = "PTLTL.eventuallyPrev" --- | Return the Copilot representation of a unary logical MTL FRET operator. +-- | Return the Copilot representation of a unary logical MTL SMV operator. opOneMTL2Copilot :: Op1Name -> OrdOp -> Number -> String opOneMTL2Copilot operator _comparison number = opOneMTL2Copilot' operator ++ " " ++ show (0 :: Int) @@ -164,7 +164,7 @@ opOneMTL2Copilot operator _comparison number = ++ " " ++ "clock" ++ " " ++ show (1 :: Int) --- | Return the Copilot representation of a unary logical MTL FRET operator +-- | Return the Copilot representation of a unary logical MTL SMV operator -- that uses an explicit range. opOneMTLRange2Copilot :: Op1Name -> Number -> Number -> String opOneMTLRange2Copilot operator mn mx = @@ -173,7 +173,7 @@ opOneMTLRange2Copilot operator mn mx = ++ " " ++ "clock" ++ " " ++ show (1 :: Int) --- | Return the Copilot representation of a unary logical possibly MTL FRET +-- | Return the Copilot representation of a unary logical possibly MTL SMV -- operator. opOneMTL2Copilot' :: Op1Name -> String opOneMTL2Copilot' Op1Pre = "pre" @@ -185,11 +185,11 @@ opOneMTL2Copilot' Op1Z = "notPreviousNot" opOneMTL2Copilot' Op1Hist = "MTL.alwaysBeen" opOneMTL2Copilot' Op1O = "MTL.eventuallyPrev" --- | Return the Copilot representation of a FRET number. +-- | Return the Copilot representation of an SMV number. number2Copilot :: Number -> String number2Copilot (NumberInt n) = show n --- | Return the Copilot representation of a binary logical non-MTL FRET +-- | Return the Copilot representation of a binary logical non-MTL SMV -- operator. opTwo2Copilot :: OpTwo -> String opTwo2Copilot Op2S = "`since`" @@ -197,7 +197,7 @@ opTwo2Copilot Op2T = "`triggers`" opTwo2Copilot Op2V = "`releases`" opTwo2Copilot Op2U = "`until`" --- | Return the Copilot representation of a FRET identifier. +-- | Return the Copilot representation of an SMV identifier. ident2Copilot :: Ident -> String ident2Copilot (Ident i) = i diff --git a/ogma-core/src/Language/Trans/Spec2Copilot.hs b/ogma-core/src/Language/Trans/Spec2Copilot.hs index 99e1fb6a..8a75ca67 100644 --- a/ogma-core/src/Language/Trans/Spec2Copilot.hs +++ b/ogma-core/src/Language/Trans/Spec2Copilot.hs @@ -67,6 +67,7 @@ spec2Copilot specName typeMaps exprTransform showExpr spec = , ftp , pre , tpre + , notPreviousNot , copilotSpec , main' ] @@ -194,12 +195,19 @@ spec2Copilot specName typeMaps exprTransform showExpr spec = , "tpre = ([True] ++)" ] + -- Auxiliary streams: notPreviousNot + notPreviousNot :: [String] + notPreviousNot = [ "" + , "notPreviousNot :: Stream Bool -> Stream Bool" + , "notPreviousNot = not . PTLTL.previous . not" + ] + -- Main specification copilotSpec :: [String] copilotSpec = [ "" - , "-- | Complete specification. Calls the C function void " - ++ " handler(); when" - , "-- the property is violated." + , "-- | Complete specification. Calls C handler functions" + ++ " when" + , "-- properties are violated." , "spec :: Spec" , "spec = do" ] diff --git a/ogma-core/templates/copilot-cfs/fsw/src/copilot_cfs.c b/ogma-core/templates/copilot-cfs/fsw/src/copilot_cfs.c index 74917cf9..7f9d0ff9 100644 --- a/ogma-core/templates/copilot-cfs/fsw/src/copilot_cfs.c +++ b/ogma-core/templates/copilot-cfs/fsw/src/copilot_cfs.c @@ -19,7 +19,7 @@ #include "Icarous_msgids.h" #include "Icarous_msg.h" -position_t my_position; +{{variablesS}} void split(void); void step(void); @@ -98,7 +98,7 @@ void COPILOT_AppInit(void) ** messages */ CFE_SB_CreatePipe(&COPILOT_CommandPipe, COPILOT_PIPE_DEPTH,"COPILOT_CMD_PIPE"); - CFE_SB_Subscribe(ICAROUS_POSITION_MID, COPILOT_CommandPipe); +{{msgSubscriptionsS}} CFE_EVS_SendEvent (COPILOT_STARTUP_INF_EID, CFE_EVS_INFORMATION, "COPILOT App Initialized. Version %d.%d.%d.%d", @@ -125,9 +125,7 @@ void COPILOT_ProcessCommandPacket(void) switch (MsgId) { - case ICAROUS_POSITION_MID: - COPILOT_ProcessIcarousPosition(); - break; +{{ msgCasesS }} default: COPILOT_HkTelemetryPkt.copilot_command_error_count++; CFE_EVS_SendEvent(COPILOT_COMMAND_ERR_EID,CFE_EVS_ERROR, @@ -139,18 +137,7 @@ void COPILOT_ProcessCommandPacket(void) } /* End COPILOT_ProcessCommandPacket */ -/** - * Make ICAROUS data available to Copilot and run monitors. - */ -void COPILOT_ProcessIcarousPosition(void) -{ - position_t* msg; - msg = (position_t*) COPILOTMsgPtr; - my_position = *msg; - - // Run all copilot monitors. - step(); -} +{{msgHandlerS}} /** * Report copilot property violations. diff --git a/ogma-core/templates/ros/Dockerfile b/ogma-core/templates/ros/Dockerfile index 5c14dbd4..ce627fa3 100644 --- a/ogma-core/templates/ros/Dockerfile +++ b/ogma-core/templates/ros/Dockerfile @@ -1,4 +1,4 @@ -FROM osrf/space-ros:latest +FROM osrf/space-ros:humble-2024.10.0 ARG USER=spaceros-user ARG PACKAGE_PATH=/home/${USER}/monitors @@ -12,5 +12,5 @@ USER ${USER} SHELL ["/bin/bash", "-c"] WORKDIR ${PACKAGE_PATH} -RUN source ${ROS_PATH}/install/setup.bash && \ +RUN source /opt/spaceros/install/setup.bash && \ colcon build diff --git a/ogma-core/templates/ros/copilot/src/.keep b/ogma-core/templates/ros/copilot/src/.keep deleted file mode 100644 index e69de29b..00000000 diff --git a/ogma-core/templates/ros/copilot/src/copilot_logger.cpp b/ogma-core/templates/ros/copilot/src/copilot_logger.cpp new file mode 100644 index 00000000..fbda764f --- /dev/null +++ b/ogma-core/templates/ros/copilot/src/copilot_logger.cpp @@ -0,0 +1,27 @@ +#include +#include + +#include "rclcpp/rclcpp.hpp" + +#include "std_msgs/msg/empty.hpp" +using std::placeholders::_1; + +class CopilotLogger : public rclcpp::Node { + public: + CopilotLogger() : Node("copilotlogger") { +{{{logMsgSubscriptionS}}} + } + + private: +{{{logMsgCallbacks}}} +{{{logMsgSubscriptionDeclrs}}} +}; + +int main(int argc, char* argv[]) { + rclcpp::init(argc, argv); + rclcpp::spin(std::make_shared()); + rclcpp::shutdown(); + return 0; +} + + diff --git a/ogma-core/templates/ros/copilot/src/copilot_monitor.cpp b/ogma-core/templates/ros/copilot/src/copilot_monitor.cpp new file mode 100644 index 00000000..2d495fa0 --- /dev/null +++ b/ogma-core/templates/ros/copilot/src/copilot_monitor.cpp @@ -0,0 +1,52 @@ +#include +#include + +#include "rclcpp/rclcpp.hpp" + +#include "std_msgs/msg/bool.hpp" +#include "std_msgs/msg/empty.hpp" +#include "std_msgs/msg/u_int8.hpp" +#include "std_msgs/msg/u_int16.hpp" +#include "std_msgs/msg/u_int32.hpp" +#include "std_msgs/msg/u_int64.hpp" +#include "std_msgs/msg/int8.hpp" +#include "std_msgs/msg/int16.hpp" +#include "std_msgs/msg/int32.hpp" +#include "std_msgs/msg/int64.hpp" +#include "std_msgs/msg/float32.hpp" +#include "std_msgs/msg/float64.hpp" +#include +#include "monitor.h" +#include "monitor.c" + +using std::placeholders::_1; + +{{{variablesS}}} +class CopilotRV : public rclcpp::Node { + public: + CopilotRV() : Node("copilotrv") { +{{{msgSubscriptionS}}} +{{{msgPublisherS}}} + } + +{{{msgHandlerInClassS}}} + // Needed so we can report messages to the log. + static CopilotRV& getInstance() { + static CopilotRV instance; + return instance; + } + + private: +{{{msgCallbacks}}} +{{{msgSubscriptionDeclrs}}} +{{{msgPublisherDeclrs}}} +}; + +{{{msgHandlerGlobalS}}} +int main(int argc, char* argv[]) { + rclcpp::init(argc, argv); + rclcpp::spin(std::make_shared()); + rclcpp::shutdown(); + return 0; +} + diff --git a/ogma-core/tests/Main.hs b/ogma-core/tests/Main.hs index da71f6ee..4565d216 100644 --- a/ogma-core/tests/Main.hs +++ b/ogma-core/tests/Main.hs @@ -7,14 +7,9 @@ import Test.Framework.Providers.HUnit ( testCase ) import Test.HUnit ( assertBool ) -- Internal imports -import Command.CStructs2Copilot ( cstructs2Copilot ) -import Command.FRETComponentSpec2Copilot ( FRETComponentSpec2CopilotOptions (..) - , fretComponentSpec2Copilot - ) -import Command.FRETReqsDB2Copilot ( FRETReqsDB2CopilotOptions (..) - , fretReqsDB2Copilot - ) -import Command.Result ( isSuccess ) +import Command.CStructs2Copilot (cstructs2Copilot) +import Command.Result (isSuccess) +import Command.Standalone (StandaloneOptions (..), standalone) -- | Run all unit tests on ogma-core. main :: IO () @@ -106,13 +101,13 @@ testFretComponentSpec2Copilot :: FilePath -- ^ Path to a FRET/JSON requirements -> Bool -> IO () testFretComponentSpec2Copilot file success = do - let opts = FRETComponentSpec2CopilotOptions - { fretCS2CopilotUseCoCoSpec = False - , fretCS2CopilotIntType = "Int64" - , fretCS2CopilotRealType = "Float" - , fretCS2CopilotFilename = "fret" + let opts = StandaloneOptions + { standaloneFormat = "fcs" + , standalonePropFormat = "smv" + , standaloneTypeMapping = [("int", "Int64"), ("real", "Float")] + , standaloneFilename = "fret" } - result <- fretComponentSpec2Copilot file opts + result <- standalone file opts -- True if success is expected and detected, or niether expected nor -- detected. @@ -138,11 +133,13 @@ testFretReqsDBCoCoSpec2Copilot :: FilePath -- ^ Path to a FRET/JSON -> Bool -> IO () testFretReqsDBCoCoSpec2Copilot file success = do - let opts = FRETReqsDB2CopilotOptions - { fretReqsDB2CopilotUseCoCoSpec = True - , fretReqsDB2CopilotFilename = "fret" + let opts = StandaloneOptions + { standaloneFormat = "fdb" + , standalonePropFormat = "cocospec" + , standaloneTypeMapping = [] + , standaloneFilename = "fret" } - result <- fretReqsDB2Copilot file opts + result <- standalone file opts -- True if success is expected and detected, or niether expected nor -- detected. diff --git a/ogma-extra/CHANGELOG.md b/ogma-extra/CHANGELOG.md index defe47b1..8d4d22ce 100644 --- a/ogma-extra/CHANGELOG.md +++ b/ogma-extra/CHANGELOG.md @@ -1,5 +1,10 @@ # Revision history for ogma-extra +## [1.5.0] - 2024-11-21 + +* Version bump 1.5.0 (#178). +* Introduce template expansion functionality (#162). + ## [1.4.1] - 2024-09-21 * Version bump 1.4.1 (#155). diff --git a/ogma-extra/ogma-extra.cabal b/ogma-extra/ogma-extra.cabal index c4ca300a..3388b999 100644 --- a/ogma-extra/ogma-extra.cabal +++ b/ogma-extra/ogma-extra.cabal @@ -32,7 +32,7 @@ cabal-version: 2.0 build-type: Simple name: ogma-extra -version: 1.4.1 +version: 1.5.0 homepage: https://github.com/nasa/ogma license: OtherLicense license-file: LICENSE.pdf @@ -68,11 +68,14 @@ library System.Directory.Extra build-depends: - base >= 4.11.0.0 && < 5 + base >= 4.11.0.0 && < 5 + , aeson >= 2.0.0.0 && < 2.2 , bytestring , Cabal , directory , filepath + , microstache >= 1.0 && < 1.1 + , text >= 1.2.3.1 && < 2.1 hs-source-dirs: src diff --git a/ogma-extra/src/System/Directory/Extra.hs b/ogma-extra/src/System/Directory/Extra.hs index eb276012..01ebfdc4 100644 --- a/ogma-extra/src/System/Directory/Extra.hs +++ b/ogma-extra/src/System/Directory/Extra.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE OverloadedStrings #-} -- Copyright 2020 United States Government as represented by the Administrator -- of the National Aeronautics and Space Administration. All Rights Reserved. -- @@ -32,17 +33,28 @@ module System.Directory.Extra ( copyDirectoryRecursive , copyFile' + , copyTemplate ) where -- External imports +import Control.Monad ( filterM, forM_ ) import qualified Control.Exception as E +import Data.Aeson ( Value (..) ) +import qualified Data.ByteString.Lazy as B +import Data.Text.Lazy ( pack, unpack ) +import Data.Text.Lazy.Encoding ( encodeUtf8 ) import Distribution.Simple.Utils ( getDirectoryContentsRecursive ) import System.Directory ( copyFile, - createDirectoryIfMissing ) + createDirectoryIfMissing, + doesFileExist ) import System.Exit ( ExitCode (ExitFailure), exitWith ) -import System.FilePath ( takeDirectory, () ) +import System.FilePath ( makeRelative, splitFileName, + takeDirectory, () ) import System.IO ( hPutStrLn, stderr ) +import Text.Microstache ( compileMustacheFile, + compileMustacheText, + renderMustache ) -- | Copy all files from one directory to another. copyDirectoryRecursive :: FilePath -- ^ Source directory @@ -79,3 +91,48 @@ copyDirectoryRecursiveErrorHandler sourceDir targetDir _exception = do hPutStrLn stderr $ "ogma: error: cannot copy " ++ sourceDir ++ " to " ++ targetDir exitWith (ExitFailure 1) + +-- * Generic template handling + +-- | Copy a template directory into a target location, expanding variables +-- provided in a map in a JSON value, both in the file contents and in the +-- filepaths themselves. +copyTemplate :: FilePath -> Value -> FilePath -> IO () +copyTemplate templateDir subst targetDir = do + + -- Get all files (not directories) in the template dir. To keep a directory, + -- create an empty file in it (e.g., .keep). + tmplContents <- map (templateDir ) . filter (`notElem` ["..", "."]) + <$> getDirectoryContentsRecursive templateDir + tmplFiles <- filterM doesFileExist tmplContents + + -- Copy files to new locations, expanding their name and contents as + -- mustache templates. + forM_ tmplFiles $ \fp -> do + + -- New file name in target directory, treating file + -- name as mustache template. + let fullPath = targetDir newFP + where + -- If file name has mustache markers, expand, otherwise use + -- relative file path + newFP = either (const relFP) + (unpack . (`renderMustache` subst)) + fpAsTemplateE + + -- Local file name within template dir + relFP = makeRelative templateDir fp + + -- Apply mustache substitutions to file name + fpAsTemplateE = compileMustacheText "fp" (pack relFP) + + -- File contents, treated as a mustache template. + contents <- encodeUtf8 <$> (`renderMustache` subst) + <$> compileMustacheFile fp + + -- Create target directory if necessary + let dirName = fst $ splitFileName fullPath + createDirectoryIfMissing True dirName + + -- Write expanded contents to expanded file path + B.writeFile fullPath contents diff --git a/ogma-language-c/CHANGELOG.md b/ogma-language-c/CHANGELOG.md index a5dbee56..209fcd31 100644 --- a/ogma-language-c/CHANGELOG.md +++ b/ogma-language-c/CHANGELOG.md @@ -1,5 +1,9 @@ # Revision history for ogma-language-c +## [1.5.0] - 2024-11-21 + +* Version bump 1.5.0 (#178). + ## [1.4.1] - 2024-09-21 * Version bump 1.4.1 (#155). diff --git a/ogma-language-c/ogma-language-c.cabal b/ogma-language-c/ogma-language-c.cabal index 54c62152..d29072a3 100644 --- a/ogma-language-c/ogma-language-c.cabal +++ b/ogma-language-c/ogma-language-c.cabal @@ -32,7 +32,7 @@ cabal-version: 2.0 build-type: Custom name: ogma-language-c -version: 1.4.1 +version: 1.5.0 homepage: https://github.com/nasa/ogma license: OtherLicense license-file: LICENSE.pdf diff --git a/ogma-language-cocospec/CHANGELOG.md b/ogma-language-cocospec/CHANGELOG.md index d886d2ba..540fa36e 100644 --- a/ogma-language-cocospec/CHANGELOG.md +++ b/ogma-language-cocospec/CHANGELOG.md @@ -1,5 +1,9 @@ # Revision history for ogma-language-cocospec +## [1.5.0] - 2024-11-21 + +* Version bump 1.5.0 (#178). + ## [1.4.1] - 2024-09-21 * Version bump 1.4.1 (#155). diff --git a/ogma-language-cocospec/ogma-language-cocospec.cabal b/ogma-language-cocospec/ogma-language-cocospec.cabal index 23000570..d201c865 100644 --- a/ogma-language-cocospec/ogma-language-cocospec.cabal +++ b/ogma-language-cocospec/ogma-language-cocospec.cabal @@ -32,7 +32,7 @@ cabal-version: 2.0 build-type: Custom name: ogma-language-cocospec -version: 1.4.1 +version: 1.5.0 homepage: https://github.com/nasa/ogma license: OtherLicense license-file: LICENSE.pdf diff --git a/ogma-language-copilot/CHANGELOG.md b/ogma-language-copilot/CHANGELOG.md index ff2a5f85..6c944cd2 100644 --- a/ogma-language-copilot/CHANGELOG.md +++ b/ogma-language-copilot/CHANGELOG.md @@ -1,5 +1,9 @@ # Revision history for ogma-language-copilot +## [1.5.0] - 2024-11-21 + +* Version bump 1.5.0 (#178). + ## [1.4.1] - 2024-09-21 * Version bump 1.4.1 (#155). diff --git a/ogma-language-copilot/ogma-language-copilot.cabal b/ogma-language-copilot/ogma-language-copilot.cabal index ee0fefe7..0db0e6dd 100644 --- a/ogma-language-copilot/ogma-language-copilot.cabal +++ b/ogma-language-copilot/ogma-language-copilot.cabal @@ -32,7 +32,7 @@ cabal-version: 2.0 build-type: Simple name: ogma-language-copilot -version: 1.4.1 +version: 1.5.0 homepage: https://github.com/nasa/ogma license: OtherLicense license-file: LICENSE.pdf diff --git a/ogma-language-jsonspec/CHANGELOG.md b/ogma-language-jsonspec/CHANGELOG.md index 9907db66..944adb82 100644 --- a/ogma-language-jsonspec/CHANGELOG.md +++ b/ogma-language-jsonspec/CHANGELOG.md @@ -1,5 +1,10 @@ # Revision history for ogma-language-jsonspec +## [1.5.0] - 2024-11-21 + +* Version bump 1.5.0 (#178). +* Make JSONFormat readable (#170). + ## [1.4.1] - 2024-09-21 * Version bump 1.4.1 (#155). diff --git a/ogma-language-jsonspec/ogma-language-jsonspec.cabal b/ogma-language-jsonspec/ogma-language-jsonspec.cabal index a31a5783..d6c77881 100644 --- a/ogma-language-jsonspec/ogma-language-jsonspec.cabal +++ b/ogma-language-jsonspec/ogma-language-jsonspec.cabal @@ -32,7 +32,7 @@ cabal-version: 2.0 build-type: Simple name: ogma-language-jsonspec -version: 1.4.1 +version: 1.5.0 homepage: https://github.com/nasa/ogma license: OtherLicense license-file: LICENSE.pdf @@ -70,7 +70,7 @@ library , megaparsec , bytestring - , ogma-spec >= 1.4.1 && < 1.5 + , ogma-spec >= 1.5.0 && < 1.6 hs-source-dirs: src diff --git a/ogma-language-jsonspec/src/Language/JSONSpec/Parser.hs b/ogma-language-jsonspec/src/Language/JSONSpec/Parser.hs index 973e494c..d57be333 100644 --- a/ogma-language-jsonspec/src/Language/JSONSpec/Parser.hs +++ b/ogma-language-jsonspec/src/Language/JSONSpec/Parser.hs @@ -52,18 +52,19 @@ import Text.Megaparsec (eof, errorBundlePretty, parse) import Data.OgmaSpec data JSONFormat = JSONFormat - { specInternalVars :: Maybe String - , specInternalVarId :: String - , specInternalVarExpr :: String - , specInternalVarType :: Maybe String - , specExternalVars :: Maybe String - , specExternalVarId :: String - , specExternalVarType :: Maybe String - , specRequirements :: String - , specRequirementId :: String - , specRequirementDesc :: Maybe String - , specRequirementExpr :: String - } + { specInternalVars :: Maybe String + , specInternalVarId :: String + , specInternalVarExpr :: String + , specInternalVarType :: Maybe String + , specExternalVars :: Maybe String + , specExternalVarId :: String + , specExternalVarType :: Maybe String + , specRequirements :: String + , specRequirementId :: String + , specRequirementDesc :: Maybe String + , specRequirementExpr :: String + } + deriving (Read) data JSONFormatInternal = JSONFormatInternal { jfiInternalVars :: Maybe [JSONPathElement] diff --git a/ogma-language-smv/CHANGELOG.md b/ogma-language-smv/CHANGELOG.md index cc75e126..3b71957c 100644 --- a/ogma-language-smv/CHANGELOG.md +++ b/ogma-language-smv/CHANGELOG.md @@ -1,5 +1,9 @@ # Revision history for ogma-language-smv +## [1.5.0] - 2024-11-21 + +* Version bump 1.5.0 (#178). + ## [1.4.1] - 2024-09-21 * Version bump 1.4.1 (#155). diff --git a/ogma-language-smv/ogma-language-smv.cabal b/ogma-language-smv/ogma-language-smv.cabal index 2cfb5c4c..5b7bc35f 100644 --- a/ogma-language-smv/ogma-language-smv.cabal +++ b/ogma-language-smv/ogma-language-smv.cabal @@ -32,7 +32,7 @@ cabal-version: 2.0 build-type: Custom name: ogma-language-smv -version: 1.4.1 +version: 1.5.0 homepage: https://github.com/nasa/ogma license: OtherLicense license-file: LICENSE.pdf diff --git a/ogma-spec/CHANGELOG.md b/ogma-spec/CHANGELOG.md index 2ba4bcf0..36f9bdc5 100644 --- a/ogma-spec/CHANGELOG.md +++ b/ogma-spec/CHANGELOG.md @@ -1,5 +1,9 @@ # Revision history for ogma-spec +## [1.5.0] - 2024-11-21 + +* Version bump 1.5.0 (#178). + ## [1.4.1] - 2024-09-21 * Version bump 1.4.1 (#155). diff --git a/ogma-spec/ogma-spec.cabal b/ogma-spec/ogma-spec.cabal index 0e89ebf4..ec171fe9 100644 --- a/ogma-spec/ogma-spec.cabal +++ b/ogma-spec/ogma-spec.cabal @@ -32,7 +32,7 @@ cabal-version: 2.0 build-type: Simple name: ogma-spec -version: 1.4.1 +version: 1.5.0 homepage: https://github.com/nasa/ogma license: OtherLicense license-file: LICENSE.pdf