Merge branch 'release-1.3.0'. Refs #133.

ogma-cli/CHANGELOG.md

@@ -1,5 +1,9 @@
 # Revision history for ogma-cli
 
+## [1.3.0] - 2024-03-21
+
+* Version bump 1.3.0 (#133).
+
 ## [1.2.0] - 2024-01-21
 
 * Version bump 1.2.0 (#117).

ogma-cli/ogma-cli.cabal

@@ -32,7 +32,7 @@ cabal-version:       2.0
 build-type:          Simple
 
 name:                ogma-cli
-version:             1.2.0
+version:             1.3.0
 homepage:            http://nasa.gov
 license:             OtherLicense
 license-file:        LICENSE.pdf
@@ -141,7 +141,7 @@ executable ogma
   build-depends:
       base                 >= 4.11.0.0 && < 5
     , optparse-applicative
-    , ogma-core            >= 1.2.0 && < 1.3
+    , ogma-core            >= 1.3.0 && < 1.4
 
   hs-source-dirs:
     src

ogma-core/.hlint.yaml

@@ -6,7 +6,5 @@
 
 # We use data instead of newtype for uniformity.
 - ignore: { name: Use newtype instead of data
-          , within: [ Command.FRETReqsDB2Copilot
-                    , Language.Trans.FRETReqsDB2Copilot
-                    ]
+          , within: [ Command.FRETReqsDB2Copilot ]
           }

ogma-core/CHANGELOG.md

@@ -1,5 +1,14 @@
 # Revision history for ogma-core
 
+## [1.3.0] - 2024-03-21
+
+* Version bump 1.3.0 (#133).
+* Fix missing stream name substitution (#120).
+* Use generalized JSON parser for DB Spec (#122).
+* Fix translation of equivalence boolean operator from SMV (#126).
+* Sanitize handler names (#127).
+* Use same handler name in FPrime/ROS and Copilot (#130).
+
 ## [1.2.0] - 2024-01-21
 
 * Version bump 1.2.0 (#117).

ogma-core/ogma-core.cabal

@@ -32,7 +32,7 @@ cabal-version:       2.0
 build-type:          Simple
 
 name:                ogma-core
-version:             1.2.0
+version:             1.3.0
 homepage:            http://nasa.gov
 license:             OtherLicense
 license-file:        LICENSE.pdf
@@ -92,7 +92,6 @@ library
     Language.Trans.CStruct2CopilotStruct
     Language.Trans.CStructs2Copilot
     Language.Trans.CStructs2MsgHandlers
-    Language.Trans.FRETReqsDB2Copilot
     Language.Trans.Spec2Copilot
     Language.Trans.SMV2Copilot
 
@@ -110,14 +109,13 @@ library
     , IfElse
     , mtl
 
-    , ogma-extra              >= 1.2.0 && < 1.3
-    , ogma-language-c         >= 1.2.0 && < 1.3
-    , ogma-language-cocospec  >= 1.2.0 && < 1.3
-    , ogma-language-copilot   >= 1.2.0 && < 1.3
-    , ogma-language-fret-reqs >= 1.2.0 && < 1.3
-    , ogma-language-jsonspec  >= 1.2.0 && < 1.3
-    , ogma-language-smv       >= 1.2.0 && < 1.3
-    , ogma-spec               >= 1.2.0 && < 1.3
+    , ogma-extra              >= 1.3.0 && < 1.4
+    , ogma-language-c         >= 1.3.0 && < 1.4
+    , ogma-language-cocospec  >= 1.3.0 && < 1.4
+    , ogma-language-copilot   >= 1.3.0 && < 1.4
+    , ogma-language-jsonspec  >= 1.3.0 && < 1.4
+    , ogma-language-smv       >= 1.3.0 && < 1.4
+    , ogma-spec               >= 1.3.0 && < 1.4
 
   hs-source-dirs:
     src

ogma-core/src/Command/FPrimeApp.hs

@@ -246,7 +246,7 @@ fretCSExtractHandlers (Just cs) = map handlerNameF
                                 $ map requirementName
                                 $ requirements cs
   where
-    handlerNameF = ("handlerprop" ++) . sanitizeUCIdentifier
+    handlerNameF = ("handler" ++) . sanitizeUCIdentifier
 
 -- | Return the variable information needed to generate declarations
 -- and subscriptions for a given variable name and variable database.
@@ -741,15 +741,15 @@ ecCannotCopyTemplate = 1
 -- | JSONPath selectors for a FRET file
 fretFormat :: JSONFormat
 fretFormat = JSONFormat
-  { specInternalVars    = "..Internal_variables[*]"
+  { specInternalVars    = Just "..Internal_variables[*]"
   , specInternalVarId   = ".name"
   , specInternalVarExpr = ".assignmentCopilot"
-  , specInternalVarType = ".type"
-  , specExternalVars    = "..Other_variables[*]"
+  , specInternalVarType = Just ".type"
+  , specExternalVars    = Just "..Other_variables[*]"
   , specExternalVarId   = ".name"
-  , specExternalVarType = ".type"
+  , specExternalVarType = Just ".type"
   , specRequirements    = "..Requirements[*]"
   , specRequirementId   = ".name"
-  , specRequirementDesc = ".fretish"
+  , specRequirementDesc = Just ".fretish"
   , specRequirementExpr = ".ptLTL"
   }

ogma-core/src/Command/FRETComponentSpec2Copilot.hs

@@ -159,16 +159,16 @@ fretComponentSpec2CopilotResult options fp result = case result of
 -- | JSONPath selectors for a FRET file
 fretFormat :: Bool -> JSONFormat
 fretFormat useCoCoSpec = JSONFormat
-  { specInternalVars    = "..Internal_variables[*]"
+  { specInternalVars    = Just "..Internal_variables[*]"
   , specInternalVarId   = ".name"
   , specInternalVarExpr = ".assignmentCopilot"
-  , specInternalVarType = ".type"
-  , specExternalVars    = "..Other_variables[*]"
+  , specInternalVarType = Just ".type"
+  , specExternalVars    = Just "..Other_variables[*]"
   , specExternalVarId   = ".name"
-  , specExternalVarType = ".type"
+  , specExternalVarType = Just ".type"
   , specRequirements    = "..Requirements[*]"
   , specRequirementId   = ".name"
-  , specRequirementDesc = ".fretish"
+  , specRequirementDesc = Just ".fretish"
   , specRequirementExpr = if useCoCoSpec then ".CoCoSpecCode" else ".ptLTL"
   }
 

ogma-core/src/Command/FRETReqsDB2Copilot.hs

@@ -1,3 +1,4 @@
+{-# LANGUAGE ExistentialQuantification #-}
 -- Copyright 2020 United States Government as represented by the Administrator
 -- of the National Aeronautics and Space Administration. All Rights Reserved.
 --
@@ -30,9 +31,6 @@
 --
 -- | Transform a FRET requirements database containing a temporal logic
 -- specification into a Copilot specification.
---
--- This module makes use of
--- "Language.Trans.FRETReqsDB2Copilot", which does most of the work.
 module Command.FRETReqsDB2Copilot
     ( fretReqsDB2Copilot
     , FRETReqsDB2CopilotOptions(..)
@@ -43,21 +41,31 @@ module Command.FRETReqsDB2Copilot
 -- External imports
 import Control.Monad.IfElse ( awhen )
 import Data.Aeson           ( eitherDecode )
+import Data.List            ( nub, (\\) )
 
 -- External imports: auxiliary
 import Data.ByteString.Extra as B ( safeReadFile )
-import Data.List.Extra       ( headEither )
 
 -- Internal imports: auxiliary
 import Command.Result ( Result (..) )
 import Data.Location  ( Location (..) )
 
--- Internal imports: FRET files and conversion to Copilot
-import qualified Language.FRETReqsDB.AST           as FRET ( FRETReqsDB )
-import qualified Language.Trans.FRETReqsDB2Copilot as T
-  ( fret2CopilotModule
-  , FRETReqsDB2CopilotOptions(FRETReqsDB2CopilotOptions)
-  )
+-- Internal imports: Generic specification, parser.
+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.Trans.CoCoSpec2Copilot as CoCoSpec (boolSpec2Copilot,
+                                                              boolSpecNames)
+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.
@@ -71,42 +79,57 @@ fretReqsDB2Copilot :: FilePath -- ^ Path to a file containing a FRET
                    -> FRETReqsDB2CopilotOptions
                                -- ^ Customization options formula
                    -> IO (Result ErrorCode)
-fretReqsDB2Copilot fp useCoCoSpec = do
-
-  -- 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.
-  fret <- parseFret fp
+fretReqsDB2Copilot fp options = do
 
-  -- Extract internal command options from external command options
-  let internalOptions = fretReqsDB2CopilotOptions useCoCoSpec
+  let functions = fretExprPair (fretReqsDB2CopilotUseCoCoSpec options)
 
-  let copilot = T.fret2CopilotModule internalOptions =<< headEither =<< fret
+  copilot <- fretReqsDB2Copilot' fp options functions
 
   let (mOutput, result) =
-        fretReqsDB2CopilotResult useCoCoSpec fp copilot
+        fretReqsDB2CopilotResult options fp copilot
 
   awhen 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.
+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    = [("", "_")]
+
+  -- 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
+
+  -- Complement the specification with any missing/implicit definitions
+  let res' = fmap (addMissingIdentifiers ids) res
+
+  let copilot =
+        spec2Copilot name typeMaps replace showExpr =<< specAnalyze =<< res'
+
+  return copilot
+
 -- | Options used to customize the conversion of FRET Requirements Database
 -- to Copilot code.
 data FRETReqsDB2CopilotOptions = FRETReqsDB2CopilotOptions
   { fretReqsDB2CopilotUseCoCoSpec :: Bool
   , fretReqsDB2CopilotFilename    :: String
   }
 
--- | Parse a JSON file containing a FRET requirement database.
---
--- Returns a 'Left' with an error message if the file does not have the correct
--- format.
---
--- Throws an exception if the file cannot be read.
-parseFret :: FilePath -> IO (Either String [FRET.FRETReqsDB])
-parseFret fp = do
-  content <- B.safeReadFile fp
-  return $ eitherDecode =<< content
-
 -- * Error codes
 
 -- | Encoding of reasons why the command can fail.
@@ -119,24 +142,72 @@ type ErrorCode = Int
 ecFretReqsDBError :: ErrorCode
 ecFretReqsDBError = 1
 
--- * Input arguments
-
--- | Convert command input argument options to internal transformation function
--- input arguments.
-fretReqsDB2CopilotOptions :: FRETReqsDB2CopilotOptions
-                          -> T.FRETReqsDB2CopilotOptions
-fretReqsDB2CopilotOptions options =
-  T.FRETReqsDB2CopilotOptions
-      (fretReqsDB2CopilotUseCoCoSpec options)
-      (fretReqsDB2CopilotFilename options)
-
 -- * 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
+fretReqsDB2CopilotResult _options fp result = case result of
   Left msg -> (Nothing, Error ecFretReqsDBError 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"
+  }
+
+-- * 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
+  , exprIdents  :: 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)
+                                  (CoCoSpec.boolSpecNames)
+fretExprPair False = FRETExprPair (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.
+addMissingIdentifiers :: (a -> [String]) -> Spec a -> Spec a
+addMissingIdentifiers f s = s { externalVariables = vars' }
+  where
+    vars'   = externalVariables s ++ newVars
+    newVars = map (\n -> ExternalVariableDef n "") newVarNames
+
+    -- Names that are not defined anywhere
+    newVarNames = identifiers \\ existingNames
+
+    -- Identifiers being mentioned in the requirements.
+    identifiers = nub $ concatMap (f . requirementExpr) (requirements s)
+
+    -- Names that are defined in variables.
+    existingNames = map externalVariableName (externalVariables s)
+                 ++ map internalVariableName (internalVariables s)

ogma-core/src/Command/ROSApp.hs

@@ -250,7 +250,7 @@ fretCSExtractHandlers (Just cs) = map handlerNameF
                                 $ map requirementName
                                 $ requirements cs
   where
-    handlerNameF = ("handlerprop" ++) . sanitizeUCIdentifier
+    handlerNameF = ("handler" ++) . sanitizeUCIdentifier
 
 -- | Return the variable information needed to generate declarations
 -- and subscriptions for a given variable name and variable database.
@@ -716,15 +716,15 @@ ecCannotCopyTemplate = 1
 -- | JSONPath selectors for a FRET file
 fretFormat :: JSONFormat
 fretFormat = JSONFormat
-  { specInternalVars    = "..Internal_variables[*]"
+  { specInternalVars    = Just "..Internal_variables[*]"
   , specInternalVarId   = ".name"
   , specInternalVarExpr = ".assignmentCopilot"
-  , specInternalVarType = ".type"
-  , specExternalVars    = "..Other_variables[*]"
+  , specInternalVarType = Just ".type"
+  , specExternalVars    = Just "..Other_variables[*]"
   , specExternalVarId   = ".name"
-  , specExternalVarType = ".type"
+  , specExternalVarType = Just ".type"
   , specRequirements    = "..Requirements[*]"
   , specRequirementId   = ".name"
-  , specRequirementDesc = ".fretish"
+  , specRequirementDesc = Just ".fretish"
   , specRequirementExpr = ".ptLTL"
   }