Merge branch 'release-1.2.0'. Refs #117.

Author: ivanperez-keera

ogma-cli/CHANGELOG.md

@@ -1,5 +1,10 @@
 # Revision history for ogma-cli
 
+## [1.2.0] - 2024-01-21
+
+* Version bump 1.2.0 (#117).
+* Re-structure README around on backends (#75).
+
 ## [1.1.0] - 2023-11-21
 
 * Version bump 1.1.0 (#112).

ogma-cli/README.md

@@ -32,7 +32,7 @@ cabal-version:       2.0
 build-type:          Simple
 
 name:                ogma-cli
-version:             1.1.0
+version:             1.2.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.1.0 && < 1.2
+    , ogma-core            >= 1.2.0 && < 1.3
 
   hs-source-dirs:
     src

ogma-cli/ogma-cli.cabal

@@ -1,5 +1,10 @@
 # Revision history for ogma-core
 
+## [1.2.0] - 2024-01-21
+
+* Version bump 1.2.0 (#117).
+* Generalize JSON parser (#115).
+
 ## [1.1.0] - 2023-11-21
 
 * Version bump 1.1.0 (#112).

ogma-core/CHANGELOG.md

@@ -32,7 +32,7 @@ cabal-version:       2.0
 build-type:          Simple
 
 name:                ogma-core
-version:             1.1.0
+version:             1.2.0
 homepage:            http://nasa.gov
 license:             OtherLicense
 license-file:        LICENSE.pdf
@@ -92,8 +92,8 @@ library
     Language.Trans.CStruct2CopilotStruct
     Language.Trans.CStructs2Copilot
     Language.Trans.CStructs2MsgHandlers
-    Language.Trans.FRETComponentSpec2Copilot
     Language.Trans.FRETReqsDB2Copilot
+    Language.Trans.Spec2Copilot
     Language.Trans.SMV2Copilot
 
   other-modules:
@@ -105,17 +105,19 @@ library
   build-depends:
       base                    >= 4.11.0.0 && < 5
     , aeson                   >= 2.0.0.0  && < 2.2
+    , bytestring
     , filepath
     , IfElse
     , mtl
 
-    , ogma-extra              >= 1.1.0 && < 1.2
-    , ogma-language-c         >= 1.1.0 && < 1.2
-    , ogma-language-cocospec  >= 1.1.0 && < 1.2
-    , ogma-language-copilot   >= 1.1.0 && < 1.2
-    , ogma-language-fret-cs   >= 1.1.0 && < 1.2
-    , ogma-language-fret-reqs >= 1.1.0 && < 1.2
-    , ogma-language-smv       >= 1.1.0 && < 1.2
+    , 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
 
   hs-source-dirs:
     src

ogma-core/ogma-core.cabal

@@ -53,13 +53,14 @@ import Data.ByteString.Extra  as B ( safeReadFile )
 import Data.String.Extra      ( sanitizeLCIdentifier, sanitizeUCIdentifier )
 import System.Directory.Extra ( copyDirectoryRecursive )
 
+-- External imports: ogma
+import Data.OgmaSpec            (Spec, externalVariableName, externalVariables,
+                                 requirementName, requirements)
+import Language.JSONSpec.Parser (JSONFormat (..), parseJSONSpec)
+
 -- Internal imports: auxiliary
 import Command.Result                 ( Result (..) )
 import Data.Location                  ( Location (..) )
-import Language.FRETComponentSpec.AST ( FRETComponentSpec,
-                                        fretExternalVariableName,
-                                        fretExternalVariables,
-                                        fretRequirementName, fretRequirements )
 
 -- Internal imports
 import Paths_ogma_core ( getDataDir )
@@ -153,14 +154,13 @@ fprimeApp' targetDir varNames varDB monitors =
 -- | Process FRET component spec, if available, and return its abstract
 -- representation.
 parseOptionalFRETCS :: Maybe FilePath
-                    -> ExceptT ErrorTriplet IO (Maybe FRETComponentSpec)
+                    -> ExceptT ErrorTriplet IO (Maybe (Spec String))
 parseOptionalFRETCS Nothing   = return Nothing
 parseOptionalFRETCS (Just fp) = do
   -- Throws an exception if the file cannot be read.
   content <- liftIO $ B.safeReadFile fp
-
-  let fretCS :: Either String FRETComponentSpec
-      fretCS = eitherDecode =<< content
+  let fretCS :: Either String (Spec String)
+      fretCS = parseJSONSpec return fretFormat =<< eitherDecode =<< content
 
   case fretCS of
     Left e   -> throwError $ cannotOpenFRETFile fp e
@@ -219,7 +219,7 @@ parseOptionalVarDBFile (Just fp) = do
 --
 -- If a FRET file is not provided, then the user must provide BOTH a variable
 -- list, and a list of handlers.
-checkArguments :: Maybe FRETComponentSpec
+checkArguments :: Maybe (Spec a)
                -> Maybe [String]
                -> Maybe [String]
                -> Either ErrorTriplet ()
@@ -232,19 +232,19 @@ checkArguments _       _         _         = Right ()
 
 -- | Extract the variables from a FRET component specification, and sanitize
 -- them to be used in FPrime.
-fretCSExtractExternalVariables :: Maybe FRETComponentSpec -> [String]
+fretCSExtractExternalVariables :: Maybe (Spec a) -> [String]
 fretCSExtractExternalVariables Nothing   = []
 fretCSExtractExternalVariables (Just cs) = map sanitizeLCIdentifier
-                                         $ map fretExternalVariableName
-                                         $ fretExternalVariables cs
+                                         $ map externalVariableName
+                                         $ externalVariables cs
 
 -- | Extract the requirements from a FRET component specification, and sanitize
 -- them to match the names of the handlers used by Copilot.
-fretCSExtractHandlers :: Maybe FRETComponentSpec -> [String]
+fretCSExtractHandlers :: Maybe (Spec a) -> [String]
 fretCSExtractHandlers Nothing   = []
 fretCSExtractHandlers (Just cs) = map handlerNameF
-                                $ map fretRequirementName
-                                $ fretRequirements cs
+                                $ map requirementName
+                                $ requirements cs
   where
     handlerNameF = ("handlerprop" ++) . sanitizeUCIdentifier
 
@@ -737,3 +737,19 @@ ecCannotOpenHandlersFile = 1
 -- permissions or some I/O error.
 ecCannotCopyTemplate :: ErrorCode
 ecCannotCopyTemplate = 1
+
+-- | JSONPath selectors for a FRET file
+fretFormat :: JSONFormat
+fretFormat = JSONFormat
+  { specInternalVars    = "..Internal_variables[*]"
+  , specInternalVarId   = ".name"
+  , specInternalVarExpr = ".assignmentCopilot"
+  , specInternalVarType = ".type"
+  , specExternalVars    = "..Other_variables[*]"
+  , specExternalVarId   = ".name"
+  , specExternalVarType = ".type"
+  , specRequirements    = "..Requirements[*]"
+  , specRequirementId   = ".name"
+  , specRequirementDesc = ".fretish"
+  , specRequirementExpr = ".ptLTL"
+  }

ogma-core/src/Command/FPrimeApp.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.
 --
@@ -41,7 +42,8 @@ module Command.FRETComponentSpec2Copilot
 
 -- External imports
 import Control.Monad.IfElse ( awhen )
-import Data.Aeson           ( eitherDecode )
+import Data.Aeson           ( eitherDecode, decode )
+import Data.ByteString.Lazy (fromStrict)
 
 -- External imports: auxiliary
 import Data.ByteString.Extra as B ( safeReadFile )
@@ -50,12 +52,22 @@ import Data.ByteString.Extra as B ( safeReadFile )
 import Command.Result ( Result (..) )
 import Data.Location  ( Location (..) )
 
--- Internal imports
-import           Language.FRETComponentSpec.AST           ( FRETComponentSpec )
-import qualified Language.Trans.FRETComponentSpec2Copilot as T
-  ( fretComponentSpec2Copilot
-  , FRETComponentSpec2CopilotOptions(FRETComponentSpec2CopilotOptions)
-  )
+-- 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.
@@ -72,22 +84,44 @@ fretComponentSpec2Copilot :: FilePath -- ^ Path to a file containing a FRET
                           -> IO (Result ErrorCode)
 fretComponentSpec2Copilot fp options = 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 <- parseFretComponentSpec fp
+  let functions = fretExprPair (fretCS2CopilotUseCoCoSpec options)
 
-  -- Extract internal command options from external command options
-  let internalOptions = fretComponentSpec2CopilotOptions options
-
-  let copilot = T.fretComponentSpec2Copilot internalOptions =<< fret
+  copilot <- fretComponentSpec2Copilot' fp options functions
 
   let (mOutput, result) =
         fretComponentSpec2CopilotResult 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.
+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
@@ -97,17 +131,6 @@ data FRETComponentSpec2CopilotOptions = FRETComponentSpec2CopilotOptions
   , fretCS2CopilotFilename    :: String
   }
 
--- | Parse a JSON file containing a FRET component specification.
---
--- 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.
-parseFretComponentSpec :: FilePath -> IO (Either String FRETComponentSpec)
-parseFretComponentSpec fp = do
-  content <- B.safeReadFile fp
-  return $ eitherDecode =<< content
-
 -- * Error codes
 
 -- | Encoding of reasons why the command can fail.
@@ -120,19 +143,6 @@ type ErrorCode = Int
 ecFretCSError :: ErrorCode
 ecFretCSError = 1
 
--- * Input arguments
-
--- | Convert command input argument options to internal transformation function
--- input arguments.
-fretComponentSpec2CopilotOptions :: FRETComponentSpec2CopilotOptions
-                                 -> T.FRETComponentSpec2CopilotOptions
-fretComponentSpec2CopilotOptions options =
-  T.FRETComponentSpec2CopilotOptions
-      (fretCS2CopilotUseCoCoSpec options)
-      (fretCS2CopilotIntType options)
-      (fretCS2CopilotRealType options)
-      (fretCS2CopilotFilename options)
-
 -- * Result
 
 -- | Process the result of the transformation function.
@@ -143,3 +153,52 @@ fretComponentSpec2CopilotResult :: FRETComponentSpec2CopilotOptions
 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    = "..Internal_variables[*]"
+  , specInternalVarId   = ".name"
+  , specInternalVarExpr = ".assignmentCopilot"
+  , specInternalVarType = ".type"
+  , specExternalVars    = "..Other_variables[*]"
+  , specExternalVarId   = ".name"
+  , specExternalVarType = ".type"
+  , specRequirements    = "..Requirements[*]"
+  , specRequirementId   = ".name"
+  , specRequirementDesc = ".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)