Merge branch 'release-1.0.9'. Refs #93.

ogma-cli/CHANGELOG.md

@@ -1,5 +1,14 @@
 # Revision history for ogma-cli
 
+## [1.0.9] - 2023-05-21
+
+* Version bump 1.0.9 (#93).
+* Rename ROS2 to ROS 2 (#83).
+* Allow customizing the names of the C files generated by Copilot (#80).
+* Re-order README's TOC to match order of contents (#88).
+* Fix rendering of quotes in URLs in package description (#72).
+* List FPrime backend as supported use case in package description (#91).
+
 ## [1.0.8] - 2023-03-21
 
 * Version bump 1.0.8 (#81).

ogma-cli/README.md

@@ -46,9 +46,9 @@ verification framework that generates hard real-time C99 code.
 - [Usage](#usage)
   - [Language Transformations: FRET](#language-transformations-fret)
   - [cFS Application Generation](#cfs-application-generation)
-  - [Struct Interface Generation](#struct-interface-generation)
   - [ROS Application Generation](#ros-application-generation)
   - [F' Component Generation](#f-component-generation)
+  - [Struct Interface Generation](#struct-interface-generation)
 - [Contributions](#contributions)
 - [Acknowledgements](#acknowledgements)
 - [License](#license)
@@ -117,7 +117,7 @@ Available commands:
                            Specification
   fret-reqs-db             Generate a Copilot file from a FRET Requirements
                            Database
-  ros                      Generate a ROS2 monitoring package
+  ros                      Generate a ROS 2 monitoring package
 ```
 
 ## Language transformations: FRET
@@ -292,6 +292,21 @@ Note that Copilot supports only a limited subset of numeric types, which
 must be instances of the type class
 [`Typed`](https://hackage.haskell.org/package/copilot-core/docs/Copilot-Core-Type.html#t:Typed).
 
+**Name customization**
+
+All FRET-related commands allow for customization of the target C filenames via
+an argument `--target-file-name`. For example, the following execution causes
+the C files produced by Copilot to be called `monitor.c`, `monitor.h` and
+`monitor_types.h`, as opposed to the default names `fret.c`, `fret.h` and
+`fret_types.h`, respectively:
+
+```sh
+$ ogma fret-component-spec --cocospec --fret-file-name examples/fret-reqs-small.json --target-file-name monitor > FretCopilot.hs
+$ runhaskell FretCopilot.hs
+$ ls monitor*
+monitor.c  monitor.h  monitor_types.h
+```
+
 ## cFS Application Generation
 
 [NASA Core Flight System](https://cfs.gsfc.nasa.gov/) (cFS) is a flight
@@ -497,8 +512,7 @@ FPrime's Reference Application:
 
 ```sh
 $ ogma fprime --fret-file-name Export.json --variable-db fprime-variable-db --app-target-dir fprime_demo
-$ ogma fret-component-spec --fret-file-name Export.json > Spec.hs
-$ sed -i -e 's/compile "fret"/compile "copilot"/g' Spec.hs
+$ ogma fret-component-spec --fret-file-name Export.json --target-file-name copilot > Spec.hs
 $ cd fprime_demo/
 $ runhaskell ../Spec.hs
 $ docker build -t fprime .

ogma-cli/ogma-cli.cabal

@@ -32,7 +32,7 @@ cabal-version:       2.0
 build-type:          Simple
 
 name:                ogma-cli
-version:             1.0.8
+version:             1.0.9
 homepage:            http://nasa.gov
 license:             OtherLicense
 license-file:        LICENSE.pdf
@@ -67,10 +67,14 @@ description:         Ogma is a tool to facilitate the integration of safe runtim
                        to a Copilot monitor.
                      .
                      - Generating
-                       <https://ros.org Robot Operating System (ROS2)>
+                       <https://ros.org Robot Operating System (ROS 2)>
                        applications that use Copilot for monitoring data
                        received from different topics.
                      .
+                     - Generating
+                       <https://github.com/nasa/fprime F'>
+                       components that use Copilot for monitoring.
+                     .
                      The main invocation with @--help@ lists sub-commands available.
                      .
                      >$ ogma --help
@@ -91,7 +95,7 @@ description:         Ogma is a tool to facilitate the integration of safe runtim
                      >                           Specification
                      >  fret-reqs-db             Generate a Copilot file from a FRET Requirements
                      >                           Database
-                     >  ros                      Generate a ROS2 monitoring application
+                     >  ros                      Generate a ROS 2 monitoring application
                      .
                      For further information, see:
                      .
@@ -103,11 +107,13 @@ description:         Ogma is a tool to facilitate the integration of safe runtim
                      .
                      - <https://cfs.gsfc.nasa.gov/ The NASA Core Flight System web page>.
                      .
-                     - <https://ros.org/ The Robot Operating System (ROS2) web page>.
+                     - <https://ros.org/ The Robot Operating System (ROS 2) web page>.
+                     .
+                     - <https://github.com/nasa/fprime The F' repository>.
                      .
-                     - <https://ntrs.nasa.gov/citations/20200003164 "Copilot 3">, Perez, Dedden and Goodloe. 2020.
+                     - "<https://ntrs.nasa.gov/citations/20200003164 Copilot 3>", Perez, Dedden and Goodloe. 2020.
                      .
-                     - <https://shemesh.larc.nasa.gov/people/cam/publications/FMAS2020_3.pdf "From Requirements to Autonomous Flight">, Dutle et al. 2020.
+                     - "<https://shemesh.larc.nasa.gov/people/cam/publications/FMAS2020_3.pdf From Requirements to Autonomous Flight>", Dutle et al. 2020.
 
 -- Ogma packages should be uncurated so that only the official maintainers make
 -- changes.
@@ -135,7 +141,7 @@ executable ogma
   build-depends:
       base                 >= 4.11.0.0 && < 5
     , optparse-applicative
-    , ogma-core            >= 1.0.8 && < 1.1
+    , ogma-core            >= 1.0.9 && < 1.1
 
   hs-source-dirs:
     src

ogma-cli/src/CLI/CommandFretComponentSpec2Copilot.hs

@@ -62,6 +62,7 @@ data CommandOpts = CommandOpts
   , fretComponentSpecCoCoSpec :: Bool
   , fretComponentSpecIntType  :: String
   , fretComponentSpecRealType :: String
+  , fretComponentSpecTarget   :: String
   }
 
 -- | Transform a FRET component specification into a Copilot specification.
@@ -80,6 +81,7 @@ command c =
       { fretCS2CopilotUseCoCoSpec = fretComponentSpecCoCoSpec c
       , fretCS2CopilotIntType     = fretComponentSpecIntType  c
       , fretCS2CopilotRealType    = fretComponentSpecRealType c
+      , fretCS2CopilotFilename    = fretComponentSpecTarget   c
       }
 
 -- * CLI
@@ -118,6 +120,13 @@ commandOptsParser = CommandOpts
         <> showDefault
         <> value "Float"
         )
+  <*> strOption
+        (  long "target-file-name"
+        <> metavar "FILENAME"
+        <> help strFretTargetDesc
+        <> showDefault
+        <> value "fret"
+        )
 
 -- | Argument FRET command description
 strFretArgDesc :: String
@@ -134,3 +143,7 @@ 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"

ogma-cli/src/CLI/CommandFretReqsDB2Copilot.hs

@@ -43,7 +43,8 @@ module CLI.CommandFretReqsDB2Copilot
   where
 
 -- External imports
-import Options.Applicative ( Parser, help, long, metavar, strOption, switch )
+import Options.Applicative ( Parser, help, long, metavar, showDefault,
+                             strOption, switch, value )
 
 -- External imports: command results
 import Command.Result ( Result )
@@ -58,6 +59,7 @@ import Command.FRETReqsDB2Copilot ( ErrorCode, FRETReqsDB2CopilotOptions (..),
 data CommandOpts = CommandOpts
   { fretReqsDBFileName :: FilePath
   , fretReqsDBCoCoSpec :: Bool
+  , fretReqsDBTarget   :: String
   }
 
 -- | Transform a FRET requirements database containing a temporal logic
@@ -75,6 +77,7 @@ command c =
     internalCommandOpts :: FRETReqsDB2CopilotOptions
     internalCommandOpts = FRETReqsDB2CopilotOptions
       { fretReqsDB2CopilotUseCoCoSpec = fretReqsDBCoCoSpec c
+      , fretReqsDB2CopilotFilename    = fretReqsDBTarget   c
       }
 
 -- * CLI
@@ -97,6 +100,13 @@ commandOptsParser = CommandOpts
         (  long "cocospec"
         <> help strFretCoCoDesc
         )
+  <*> strOption
+        (  long "target-file-name"
+        <> metavar "FILENAME"
+        <> help strFretTargetDesc
+        <> showDefault
+        <> value "fret"
+        )
 
 -- | Argument FRET command description
 strFretArgDesc :: String
@@ -105,3 +115,7 @@ 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"

ogma-cli/src/CLI/CommandROSApp.hs

@@ -81,7 +81,7 @@ command c =
 
 -- | ROS command description
 commandDesc :: String
-commandDesc = "Generate a ROS2 monitoring package"
+commandDesc = "Generate a ROS 2 monitoring package"
 
 -- | Subparser for the @ros@ command, used to generate a Robot Operating System
 -- application connected to Copilot monitors.

ogma-core/CHANGELOG.md

@@ -1,5 +1,11 @@
 # Revision history for ogma-core
 
+## [1.0.9] - 2023-05-21
+
+* Version bump 1.0.9 (#93).
+* Allow customizing the names of the C files generated by Copilot (#80).
+* Translate ZtoPre and YtoPre to Copilot (#86).
+
 ## [1.0.8] - 2023-03-21
 
 * Version bump 1.0.8 (#81).

ogma-core/ogma-core.cabal

@@ -32,7 +32,7 @@ cabal-version:       2.0
 build-type:          Simple
 
 name:                ogma-core
-version:             1.0.8
+version:             1.0.9
 homepage:            http://nasa.gov
 license:             OtherLicense
 license-file:        LICENSE.pdf
@@ -109,13 +109,13 @@ library
     , IfElse
     , mtl
 
-    , ogma-extra              >= 1.0.8 && < 1.1
-    , ogma-language-c         >= 1.0.8 && < 1.1
-    , ogma-language-cocospec  >= 1.0.8 && < 1.1
-    , ogma-language-copilot   >= 1.0.8 && < 1.1
-    , ogma-language-fret-cs   >= 1.0.8 && < 1.1
-    , ogma-language-fret-reqs >= 1.0.8 && < 1.1
-    , ogma-language-smv       >= 1.0.8 && < 1.1
+    , ogma-extra              >= 1.0.9 && < 1.1
+    , ogma-language-c         >= 1.0.9 && < 1.1
+    , ogma-language-cocospec  >= 1.0.9 && < 1.1
+    , ogma-language-copilot   >= 1.0.9 && < 1.1
+    , ogma-language-fret-cs   >= 1.0.9 && < 1.1
+    , ogma-language-fret-reqs >= 1.0.9 && < 1.1
+    , ogma-language-smv       >= 1.0.9 && < 1.1
 
   hs-source-dirs:
     src

ogma-core/src/Command/FRETComponentSpec2Copilot.hs

@@ -94,6 +94,7 @@ data FRETComponentSpec2CopilotOptions = FRETComponentSpec2CopilotOptions
   { fretCS2CopilotUseCoCoSpec :: Bool
   , fretCS2CopilotIntType     :: String
   , fretCS2CopilotRealType    :: String
+  , fretCS2CopilotFilename    :: String
   }
 
 -- | Parse a JSON file containing a FRET component specification.
@@ -130,6 +131,7 @@ fretComponentSpec2CopilotOptions options =
       (fretCS2CopilotUseCoCoSpec options)
       (fretCS2CopilotIntType options)
       (fretCS2CopilotRealType options)
+      (fretCS2CopilotFilename options)
 
 -- * Result
 

ogma-core/src/Command/FRETReqsDB2Copilot.hs

@@ -93,6 +93,7 @@ fretReqsDB2Copilot fp useCoCoSpec = do
 -- to Copilot code.
 data FRETReqsDB2CopilotOptions = FRETReqsDB2CopilotOptions
   { fretReqsDB2CopilotUseCoCoSpec :: Bool
+  , fretReqsDB2CopilotFilename    :: String
   }
 
 -- | Parse a JSON file containing a FRET requirement database.
@@ -127,6 +128,7 @@ fretReqsDB2CopilotOptions :: FRETReqsDB2CopilotOptions
 fretReqsDB2CopilotOptions options =
   T.FRETReqsDB2CopilotOptions
       (fretReqsDB2CopilotUseCoCoSpec options)
+      (fretReqsDB2CopilotFilename options)
 
 -- * Result
 

ogma-core/src/Language/Trans/CoCoSpec2Copilot.hs

@@ -130,6 +130,8 @@ const2Copilot BoolConstFTP   = "ftp"
 -- operator.
 opOnePre2Copilot :: Op1Pre -> String
 opOnePre2Copilot Op1Pre    = "pre"
+opOnePre2Copilot Op1YtoPre = "pre"
+opOnePre2Copilot Op1ZtoPre = "tpre"
 opOnePre2Copilot Op1Once   = "PTLTL.eventuallyPrev"
 opOnePre2Copilot Op1Hist   = "PTLTL.alwaysBeen"
 opOnePre2Copilot Op1Y      = "PTLTL.previous"

ogma-core/src/Language/Trans/FRETComponentSpec2Copilot.hs

@@ -57,6 +57,7 @@ data FRETComponentSpec2CopilotOptions = FRETComponentSpec2CopilotOptions
   { fretCS2CopilotUseCoCoSpec :: Bool
   , fretCS2CopilotIntType     :: String
   , fretCS2CopilotRealType    :: String
+  , fretCS2CopilotFilename    :: String
   }
 
 -- | Transform a FRET TL specification into a Copilot specification.
@@ -86,6 +87,7 @@ fretComponentSpec2Copilot' prefs fretComponentSpec =
       , pure clock
       , pure ftp
       , pure pre
+      , pure tpre
       , pure spec
       , pure main'
       ]
@@ -222,6 +224,12 @@ fretComponentSpec2Copilot' prefs fretComponentSpec =
           , "pre = ([False] ++)"
           ]
 
+    -- Auxiliary streams: tpre
+    tpre = [ ""
+           , "tpre :: Stream Bool -> Stream Bool"
+           , "tpre = ([True] ++)"
+           ]
+
     -- Main specification
     spec :: [String]
     spec = [ ""
@@ -249,7 +257,8 @@ fretComponentSpec2Copilot' prefs fretComponentSpec =
     main' :: [String]
     main' = [ ""
             , "main :: IO ()"
-            , "main = reify spec >>= compile \"fret\""
+            , "main = reify spec >>= compile \""
+                 ++ fretCS2CopilotFilename prefs ++ "\""
             ]
 
 -- | Return the corresponding type in Copilot matching a given FRET type.

ogma-core/src/Language/Trans/FRETReqsDB2Copilot.hs

@@ -62,6 +62,7 @@ import qualified Language.FRETReqsDB.AST as FRET ( FRETReqsDB, semantics,
 -- to Copilot code.
 data FRETReqsDB2CopilotOptions = FRETReqsDB2CopilotOptions
   { fretReqsDB2CopilotUseCoCoSpec :: Bool
+  , fretReqsDB2CopilotFilename    :: String
   }
 
 -- | Return a string with the contents of the Copilot module that implements a
@@ -93,10 +94,12 @@ fret2CopilotModule' prefs smvSpec cocoSpec = unlines $ concat sections
                               else SMV.boolSpecNames smvSpec
 
     sections | fretReqsDB2CopilotUseCoCoSpec prefs
-             = [ imports, propDef, externs, clock, ftp, undef, spec, main' ]
+             = [ imports, propDef, externs, clock, ftp, undef, tpre, spec
+               , main'
+               ]
 
              | otherwise
-             = [ imports, propDef, externs, clock, ftp, spec, main' ]
+             = [ imports, propDef, externs, clock, ftp, tpre, spec, main' ]
 
     imports :: [String]
     imports =
@@ -144,6 +147,11 @@ fret2CopilotModule' prefs smvSpec cocoSpec = unlines $ concat sections
                , "pre = undefined"
                ]
 
+    tpre     = [ ""
+               , "tpre :: Stream Bool -> Stream Bool"
+               , "tpre = ([True] ++)"
+               ]
+
     spec     = [ ""
                , "-- | Complete specification. Calls the C function void handler(); when"
                , "-- the property is violated."
@@ -155,5 +163,6 @@ fret2CopilotModule' prefs smvSpec cocoSpec = unlines $ concat sections
 
     main'    = [ ""
                , "main :: IO ()"
-               , "main = reify spec >>= compile \"fret\""
+               , "main = reify spec >>= compile \""
+                    ++ fretReqsDB2CopilotFilename prefs ++ "\""
                ]