diff --git a/ogma-core/CHANGELOG.md b/ogma-core/CHANGELOG.md
index f7ec75f7..ad6cd472 100644
--- a/ogma-core/CHANGELOG.md
+++ b/ogma-core/CHANGELOG.md
@@ -1,5 +1,9 @@
# Revision history for ogma-core
+## [1.X.Y] - 2024-01-21
+
+* Generalize JSON parser (#115).
+
## [1.1.0] - 2023-11-21
* Version bump 1.1.0 (#112).
diff --git a/ogma-core/ogma-core.cabal b/ogma-core/ogma-core.cabal
index 87c37bc2..1478e07a 100644
--- a/ogma-core/ogma-core.cabal
+++ b/ogma-core/ogma-core.cabal
@@ -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,6 +105,7 @@ library
build-depends:
base >= 4.11.0.0 && < 5
, aeson >= 2.0.0.0 && < 2.2
+ , bytestring
, filepath
, IfElse
, mtl
@@ -113,9 +114,10 @@ library
, 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-jsonspec >= 1.1.0 && < 1.2
, ogma-language-smv >= 1.1.0 && < 1.2
+ , ogma-spec >= 1.1.0 && < 1.2
hs-source-dirs:
src
diff --git a/ogma-core/src/Command/FPrimeApp.hs b/ogma-core/src/Command/FPrimeApp.hs
index 66d060f1..da60c156 100644
--- a/ogma-core/src/Command/FPrimeApp.hs
+++ b/ogma-core/src/Command/FPrimeApp.hs
@@ -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"
+ }
diff --git a/ogma-core/src/Command/FRETComponentSpec2Copilot.hs b/ogma-core/src/Command/FRETComponentSpec2Copilot.hs
index b0ee34a7..697f4278 100644
--- a/ogma-core/src/Command/FRETComponentSpec2Copilot.hs
+++ b/ogma-core/src/Command/FRETComponentSpec2Copilot.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,15 +84,9 @@ 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
@@ -88,6 +94,34 @@ fretComponentSpec2Copilot fp options = do
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)
diff --git a/ogma-core/src/Command/ROSApp.hs b/ogma-core/src/Command/ROSApp.hs
index 306ffff9..d3e2f79e 100644
--- a/ogma-core/src/Command/ROSApp.hs
+++ b/ogma-core/src/Command/ROSApp.hs
@@ -56,13 +56,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 )
@@ -157,14 +158,13 @@ rosApp' 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
@@ -223,7 +223,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 String)
-> Maybe [String]
-> Maybe [String]
-> Either ErrorTriplet ()
@@ -236,19 +236,19 @@ checkArguments _ _ _ = Right ()
-- | Extract the variables from a FRET component specification, and sanitize
-- them to be used in ROS.
-fretCSExtractExternalVariables :: Maybe FRETComponentSpec -> [String]
+fretCSExtractExternalVariables :: Maybe (Spec String) -> [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 String) -> [String]
fretCSExtractHandlers Nothing = []
fretCSExtractHandlers (Just cs) = map handlerNameF
- $ map fretRequirementName
- $ fretRequirements cs
+ $ map requirementName
+ $ requirements cs
where
handlerNameF = ("handlerprop" ++) . sanitizeUCIdentifier
@@ -712,3 +712,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"
+ }
diff --git a/ogma-core/src/Language/Trans/FRETComponentSpec2Copilot.hs b/ogma-core/src/Language/Trans/Spec2Copilot.hs
similarity index 50%
rename from ogma-core/src/Language/Trans/FRETComponentSpec2Copilot.hs
rename to ogma-core/src/Language/Trans/Spec2Copilot.hs
index d262997c..a23e69bc 100644
--- a/ogma-core/src/Language/Trans/FRETComponentSpec2Copilot.hs
+++ b/ogma-core/src/Language/Trans/Spec2Copilot.hs
@@ -1,4 +1,4 @@
--- Copyright 2020 United States Government as represented by the Administrator
+-- Copyright 2024 United States Government as represented by the Administrator
-- of the National Aeronautics and Space Administration. All Rights Reserved.
--
-- Disclaimers
@@ -27,69 +27,48 @@
-- 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.
---
-{-# LANGUAGE OverloadedStrings #-}
--- | Transform a FRET Component Specification into a Copilot specification.
+-- | Transform an Ogma specification into a standalone 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 representable
-- in the abstract syntax tree.
-module Language.Trans.FRETComponentSpec2Copilot where
+module Language.Trans.Spec2Copilot where
-- External imports
-import Data.List ( intersect, union )
+import Data.List ( intersect, lookup, union )
import Data.Maybe ( fromMaybe )
-- External imports: auxiliary
import Data.String.Extra ( sanitizeLCIdentifier, sanitizeUCIdentifier )
--- Internal imports: language ASTs, transformers
-import qualified Language.CoCoSpec.ParCoCoSpec as CoCoSpec ( myLexer,
- pBoolSpec )
-import Language.FRETComponentSpec.AST as FRET
-import qualified Language.Trans.CoCoSpec2Copilot as CoCoSpec ( boolSpec2Copilot )
-import Language.Trans.SMV2Copilot as SMV ( boolSpec2Copilot )
-
--- | Options used to customize the conversion of FRET Component Specifications
--- to Copilot code.
-data FRETComponentSpec2CopilotOptions = FRETComponentSpec2CopilotOptions
- { fretCS2CopilotUseCoCoSpec :: Bool
- , fretCS2CopilotIntType :: String
- , fretCS2CopilotRealType :: String
- , fretCS2CopilotFilename :: String
- }
-
--- | Transform a FRET TL specification into a Copilot specification.
---
--- This function may fail with a 'Left' value if the resulting Copilot
--- specification would contain name clashes or other errors.
-fretComponentSpec2Copilot :: FRETComponentSpec2CopilotOptions
- -> FRETComponentSpec
- -> Either String String
-fretComponentSpec2Copilot prefs parseResult =
- fretComponentSpec2Copilot' prefs =<< fret2CopilotAnalyze parseResult
-
--- | For a given FRET file, return the corresponding Copilot file, or an error
+-- External imports: ogma-spec
+import Data.OgmaSpec (ExternalVariableDef (..), InternalVariableDef (..),
+ Requirement (..), Spec (..))
+
+-- | For a given spec, return the corresponding Copilot file, or an error
-- message if such file cannot be generated.
--
-- PRE: there are no name clashes between the variables and names used in the
--- FRET specification and any definitions in Haskell's Prelude or in Copilot.
-fretComponentSpec2Copilot' :: FRETComponentSpec2CopilotOptions
- -> FRETComponentSpec
- -> Either String String
-fretComponentSpec2Copilot' prefs fretComponentSpec =
- unlines . concat <$> sequence
- [ pure imports
- , pure externs
+-- specification and any definitions in Haskell's Prelude or in Copilot.
+spec2Copilot :: String -- Spec / target file name
+ -> [(String, String)] -- Type substitution table
+ -> ([(String, String)] -> a -> a) -- Expr subsitution function
+ -> (a -> String) -- Expr show function
+ -> Spec a -- Specification
+ -> Either String String
+spec2Copilot specName typeMaps exprTransform showExpr spec =
+ pure $ unlines $ concat
+ [ imports
+ , externs
, internals
, reqs
- , pure clock
- , pure ftp
- , pure pre
- , pure tpre
- , pure spec
- , pure main'
+ , clock
+ , ftp
+ , pre
+ , tpre
+ , copilotSpec
+ , main'
]
where
@@ -115,90 +94,75 @@ fretComponentSpec2Copilot' prefs fretComponentSpec =
-- Extern streams
externs = concatMap externVarToDecl
- (FRET.fretExternalVariables fretComponentSpec)
+ (externalVariables spec)
where
- externVarToDecl i = [ FRET.fretExternalVariableName i
+ externVarToDecl i = [ propName
++ " :: Stream "
++ "("
- ++ fretTypeToCopilotType
- prefs
- (FRET.fretExternalVariableType i)
+ ++ safeMap typeMaps (externalVariableType i)
++ ")"
- , FRET.fretExternalVariableName i
+ , propName
++ " = "
++ "extern"
++ " "
- ++ show (FRET.fretExternalVariableName i)
+ ++ show (externalVariableName i)
++ " "
++ "Nothing"
, ""
]
+ where
+ propName = safeMap nameSubstitutions (externalVariableName i)
-- Internal stream definitions
- internals = concat
- <$> mapM internalVarToDecl
- (FRET.fretInternalVariables fretComponentSpec)
+ internals = concatMap internalVarToDecl
+ (internalVariables spec)
where
- internalVarToDecl i = fmap (\implem ->
- [ FRET.fretInternalVariableName i
+ internalVarToDecl i = (\implem ->
+ [ propName
++ " :: Stream "
++ "("
- ++ fretTypeToCopilotType
- prefs
- (FRET.fretInternalVariableType i)
+ ++ safeMap typeMaps (internalVariableType i)
++ ")"
- , FRET.fretInternalVariableName i
+ , propName
++ " = "
++ implem
, ""
]) implementation
where
- implementation = if null (FRET.fretInternalVariableCopilot i)
- then CoCoSpec.boolSpec2Copilot
- <$> CoCoSpec.pBoolSpec
- ( CoCoSpec.myLexer
- $ FRET.fretInternalVariableLustre i
- )
- else pure (FRET.fretInternalVariableCopilot i)
+ propName = safeMap nameSubstitutions (internalVariableName i)
+ implementation = (internalVariableExpr i)
-- Encoding of requirements as boolean streams
- reqs :: Either String [String]
- reqs = concat <$> mapM reqToDecl (FRET.fretRequirements fretComponentSpec)
+ reqs :: [String]
+ reqs = concatMap reqToDecl (requirements spec)
where
- reqToDecl i = sequence
- [ pure reqComment, pure reqSignature, reqBody, pure "" ]
+ reqToDecl i = [ reqComment, reqSignature
+ , reqBody nameSubstitutions
+ , ""
+ ]
where
+ reqName = safeMap nameSubstitutions (requirementName i)
+
-- Definition comment, which includes the requirement for
-- traceability purposes.
- reqComment = "-- | " ++ FRET.fretRequirementName i ++ "\n" ++
+ reqComment = "-- | " ++ requirementName i ++ "\n" ++
"-- @" ++ "\n" ++
- "-- " ++ FRET.fretRequirementFretish i ++ "\n" ++
+ "-- " ++ requirementDescription i ++ "\n" ++
"-- @"
-- Definition type signature.
- reqSignature = FRET.fretRequirementName i
+ reqSignature = reqName
++ " :: " ++ "Stream" ++ " " ++ "Bool"
- -- Definition implementation, either in SMV or in CoCoSpec
- reqBody = if fretCS2CopilotUseCoCoSpec prefs
- then reqBodyCoCo
- else reqBodyPT
+ -- Definition implementation. We use an auxiliary function to
+ -- transform the implementation into Copilot, applying a
+ -- substitution.
+ reqBody subs = reqName ++ " = " ++
+ (showExpr (exprTransform subs (requirementExpr i)))
- reqBodyPT = fmap (\e -> FRET.fretRequirementName i ++ " = "
- ++ SMV.boolSpec2Copilot e
- )
- (fromMaybe (Left $ "No requirement for " ++ show i)
- (FRET.fretRequirementPTExpanded i))
-
- reqBodyCoCo = fmap
- (\e -> FRET.fretRequirementName i ++ " = "
- ++ CoCoSpec.boolSpec2Copilot e
- )
- (fromMaybe (Left $ "No requirement for " ++ show i)
- (FRET.fretRequirementCoCoSpec i))
-- Auxiliary streams: clock
clock :: [String]
@@ -231,55 +195,62 @@ fretComponentSpec2Copilot' prefs fretComponentSpec =
]
-- Main specification
- spec :: [String]
- spec = [ ""
- , "-- | Complete specification. Calls the C function void "
- ++ " handler(); when"
- , "-- the property is violated."
- , "spec :: Spec"
- , "spec = do"
- ]
- ++ triggers
- ++ [ "" ]
+ copilotSpec :: [String]
+ copilotSpec = [ ""
+ , "-- | Complete specification. Calls the C function void "
+ ++ " handler(); when"
+ , "-- the property is violated."
+ , "spec :: Spec"
+ , "spec = do"
+ ]
+ ++ triggers
+ ++ [ "" ]
where
triggers :: [String]
- triggers = fmap reqTrigger (FRET.fretRequirements fretComponentSpec)
+ triggers = fmap reqTrigger (requirements spec)
- reqTrigger :: FRETRequirement -> String
+ reqTrigger :: Requirement a -> String
reqTrigger r = " trigger " ++ show handlerName ++ " (not "
++ propName ++ ") " ++ "[]"
where
- handlerName = "handler" ++ FRET.fretRequirementName r
- propName = FRET.fretRequirementName r
+ handlerName = "handler" ++ requirementName r
+ propName = requirementName r
-- Main program that compiles specification to C in two files (code and
-- header).
main' :: [String]
main' = [ ""
, "main :: IO ()"
- , "main = reify spec >>= compile \""
- ++ fretCS2CopilotFilename prefs ++ "\""
+ , "main = reify spec >>= compile \"" ++ specName ++ "\""
]
--- | Return the corresponding type in Copilot matching a given FRET type.
-fretTypeToCopilotType :: FRETComponentSpec2CopilotOptions -> String -> String
-fretTypeToCopilotType _options "bool" = "Bool"
-fretTypeToCopilotType options "int" = fretCS2CopilotIntType options
-fretTypeToCopilotType options "integer" = fretCS2CopilotIntType options
-fretTypeToCopilotType options "real" = fretCS2CopilotRealType options
-fretTypeToCopilotType _options "string" = "String"
-fretTypeToCopilotType _options x = x
-
--- | Analyze a FRET-Copilot file and determine if there will be any name
--- clashes after the conversion to Copilot.
---
--- This function does not compare against Haskell's prelude or Copilot's
--- modules. It simply makes simple conversions to comply with Copilot/Haskell's
--- grammar (e.g., variable/function names start with lowercase) and determines
--- if the conversion would make two definitions in the given specification
--- produce name clashes between them.
-fret2CopilotAnalyze :: FRETComponentSpec -> Either String FRETComponentSpec
-fret2CopilotAnalyze fretComponentSpec
+ -- Map from a variable name to its desired identifier in the code
+ -- generated.
+ internalVariableMap =
+ map (\x -> (x, sanitizeLCIdentifier x)) internalVariableNames
+
+ externalVariableMap =
+ map (\x -> (x, sanitizeLCIdentifier x)) externalVariableNames
+
+ requirementNameMap =
+ map (\x -> (x, "prop" ++ sanitizeUCIdentifier x)) requirementNames
+
+ nameSubstitutions = internalVariableMap
+ ++ externalVariableMap
+ ++ requirementNameMap
+
+ -- Variable/requirement names used in the component spec.
+ internalVariableNames = map internalVariableName
+ $ internalVariables spec
+
+ externalVariableNames = map externalVariableName
+ $ externalVariables spec
+
+ requirementNames = map requirementName
+ $ requirements spec
+
+specAnalyze :: Spec a -> Either String (Spec a)
+specAnalyze spec
| not (null evnClash)
= Left $ "Name clash detected: " ++ show evnClash
@@ -290,7 +261,7 @@ fret2CopilotAnalyze fretComponentSpec
= Left $ "Name clash detected: " ++ show reqClash
| otherwise
- = Right $ foldr applySubstitution fretComponentSpec nameSubstitutions
+ = Right spec
where
@@ -321,16 +292,21 @@ fret2CopilotAnalyze fretComponentSpec
requirementNameMap =
map (\x -> (x, "prop" ++ sanitizeUCIdentifier x)) requirementNames
- nameSubstitutions = internalVariableMap
- ++ externalVariableMap
- ++ requirementNameMap
-
-- Variable/requirement names used in the component spec.
- internalVariableNames = map fretInternalVariableName
- $ fretInternalVariables fretComponentSpec
+ internalVariableNames = map internalVariableName
+ $ internalVariables spec
+
+ externalVariableNames = map externalVariableName
+ $ externalVariables spec
- externalVariableNames = map fretExternalVariableName
- $ fretExternalVariables fretComponentSpec
+ requirementNames = map requirementName
+ $ requirements spec
- requirementNames = map fretRequirementName
- $ fretRequirements fretComponentSpec
+-- * Auxiliary
+
+-- | Substitute a string based on a given substitution table.
+--
+-- This function leaves the key unchanged if it cannot be found in the
+-- substitution table.
+safeMap :: [(String, String)] -> String -> String
+safeMap ls k = fromMaybe k $ lookup k ls
diff --git a/ogma-language-fret-cs/CHANGELOG.md b/ogma-language-fret-cs/CHANGELOG.md
deleted file mode 100644
index 38a32f2b..00000000
--- a/ogma-language-fret-cs/CHANGELOG.md
+++ /dev/null
@@ -1,57 +0,0 @@
-# Revision history for ogma-language-fret-cs
-
-## [1.1.0] - 2023-11-21
-
-* Version bump 1.1.0 (#112).
-
-## [1.0.11] - 2023-09-21
-
-* Version bump 1.0.11 (#103).
-
-## [1.0.10] - 2023-07-21
-
-* Version bump 1.0.10 (#98).
-* Improve parsing error messages (#96).
-
-## [1.0.9] - 2023-05-21
-
-* Version bump 1.0.9 (#93).
-
-## [1.0.8] - 2023-03-21
-
-* Version bump 1.0.8 (#81).
-* Mark package as uncurated (#74).
-
-## [1.0.7] - 2023-01-21
-* Version bump 1.0.7 (#69).
-
-## [1.0.6] - 2022-11-21
-
-* Version bump 1.0.6 (#64).
-* Update license in cabal file to OtherLicense (#62).
-
-## [1.0.5] - 2022-09-21
-
-* Version bump 1.0.5 (#60).
-* Bump version bounds of Aeson; adjust code to work with Aeson 2 (#55).
-* Support floating point numbers in SMV expressions (#58).
-
-## [1.0.4] - 2022-07-21
-
-* Version bump 1.0.4 (#53).
-
-## [1.0.3] - 2022-05-21
-
-* Version bump 1.0.3 (#49).
-
-## [1.0.2] - 2022-03-21
-
-* Version bump 1.0.2 (#43).
-
-## [1.0.1] - 2022-01-21
-
-* Version bump 1.0.1 (#39).
-
-## [1.0.0] - 2021-11-22
-
-* Initial release.
diff --git a/ogma-language-fret-cs/src/Language/FRETComponentSpec/AST.hs b/ogma-language-fret-cs/src/Language/FRETComponentSpec/AST.hs
deleted file mode 100644
index bafa44b8..00000000
--- a/ogma-language-fret-cs/src/Language/FRETComponentSpec/AST.hs
+++ /dev/null
@@ -1,262 +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.
---
-{-# LANGUAGE OverloadedStrings #-}
-{- HLINT ignore "Functor law" -}
-
--- | Representation and parser of FRET Component Specifications.
---
--- FRET files are JSON files, implemented in Haskell using type classes, so the
--- parser is defined in the same module as the AST to avoid having orphan
--- instances.
-module Language.FRETComponentSpec.AST where
-
--- External imports
-import Data.Aeson ( FromJSON (..), Value (Object), (.:) )
-import Data.Aeson.Types ( prependFailure, typeMismatch )
-import Data.Aeson.Key ( toString )
-import qualified Data.Aeson.KeyMap as M
-
--- Internal imports
-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 )
-
--- | Abstract representation of a FRET file.
-data FRETComponentSpec = FRETComponentSpec
- { fretName :: String
- , fretInternalVariables :: [ FRETInternalVariableDef ]
- , fretExternalVariables :: [ FRETExternalVariableDef ]
- , fretRequirements :: [ FRETRequirement ]
- }
- deriving (Show)
-
--- | Instance to parse FRET semantics keys in JSON format.
-instance FromJSON FRETComponentSpec where
- parseJSON (Object v)
- | (specName, Object specValues) <- head (M.toList v)
- = FRETComponentSpec (toString specName)
- <$> specValues .: "Internal_variables"
- <*> specValues .: "Other_variables"
- <*> specValues .: "Requirements"
-
- | (specName, specValues) <- head (M.toList v)
- = prependFailure "parsing FRET Component Specification failed, "
- (typeMismatch "Object" specValues)
-
- parseJSON invalid =
- prependFailure "parsing FRET Component Specification failed, "
- (typeMismatch "Object" invalid)
-
--- | Internal variable definition, with a given name, its type and either a
--- Lustre or a Copilot expression.
-data FRETInternalVariableDef = FRETInternalVariableDef
- { fretInternalVariableName :: String
- , fretInternalVariableType :: String
- , fretInternalVariableLustre :: String
- , fretInternalVariableCopilot :: String
- }
- deriving (Show)
-
-instance FromJSON FRETInternalVariableDef where
- parseJSON (Object v) = FRETInternalVariableDef
- <$> v .: "name"
- <*> v .: "type"
- <*> v .: "assignmentLustre"
- <*> v .: "assignmentCopilot"
-
- parseJSON invalid =
- prependFailure "parsing FRET Internal Variable definition failed, "
- (typeMismatch "Object" invalid)
-
--- | External variable definition, with a given name and type.
---
--- The value of external variables is assigned outside Copilot, so they have no
--- defining expression in this type..
-data FRETExternalVariableDef = FRETExternalVariableDef
- { fretExternalVariableName :: String
- , fretExternalVariableType :: String
- }
- deriving (Show)
-
-instance FromJSON FRETExternalVariableDef where
- parseJSON (Object v) = FRETExternalVariableDef
- <$> v .: "name"
- <*> v .: "type"
-
- parseJSON invalid =
- prependFailure "parsing FRET External Variable failed, "
- (typeMismatch "Object" invalid)
-
--- | Requirement with a given name and a CoCoSpec expression.
-data FRETRequirement = FRETRequirement
- { fretRequirementName :: String
- , fretRequirementCoCoSpec :: Maybe (Either String CoCoSpec.BoolSpec)
- , fretRequirementPTExpanded :: Maybe (Either String SMV.BoolSpec)
- , fretRequirementFretish :: String
- }
- deriving (Show)
-
-instance FromJSON FRETRequirement where
- parseJSON (Object v) = do
- n <- v .: "name"
-
- coco <- fmap (CoCoSpec.pBoolSpec . CoCoSpec.myLexer)
- <$> v .: "CoCoSpecCode"
- coco' <-
- case coco of
- Nothing -> fail $ noField "CoCoSpecCode" n
- Just (Left s) -> fail $ noParse "CoCoSpecCode" n s
- Just (Right _) -> return coco
-
- ptltl <- fmap (SMV.pBoolSpec . SMV.myLexer) <$> v .: "ptLTL"
- ptltl' <-
- case ptltl of
- Nothing -> fail $ noField "ptLTL" n
- Just (Left s) -> fail $ noParse "ptLTL" n s
- Just (Right _) -> return ptltl
-
- fretish <- v .: "fretish"
-
- return $ FRETRequirement n coco' ptltl' fretish
-
- where
-
- noField field req = concat
- [ "error: requirement ", show req , " does not have a ", field
- , " field"
- ]
-
- noParse field req err = concat
- [ "error: parsing of ", field, " field of requirement ", show req
- , " failed with ", err
- ]
-
-
- parseJSON invalid =
- prependFailure "parsing FRET Requirement failed, "
- (typeMismatch "Object" invalid)
-
--- | Apply a variable subsitution to variables and requirements in a FRET
--- file.
-applySubstitution :: (String, String) -> FRETComponentSpec -> FRETComponentSpec
-applySubstitution sub file =
- FRETComponentSpec tlName
- tlInternalVariables
- tlExternalVariables
- tlReqs
- where
-
- -- Result component spec fields
- tlName = fretName file
- tlInternalVariables = map internalVarMapF $ fretInternalVariables file
- tlExternalVariables = map externalVarMapF $ fretExternalVariables file
- tlReqs = map reqMapF $ fretRequirements file
-
- -- Mapping function for fields with names to substitute
- internalVarMapF x = x { fretInternalVariableName =
- subsName sub (fretInternalVariableName x) }
-
- externalVarMapF x = x { fretExternalVariableName =
- subsName sub (fretExternalVariableName x)}
-
- reqMapF x = x { fretRequirementName =
- subsName sub (fretRequirementName x)
-
- , fretRequirementPTExpanded =
- fmap (fmap (subBS sub)) (fretRequirementPTExpanded x)
- }
-
- -- Substitute name x if it matches the old name oName
- subsName (oName, nName) x = if x == oName then nName else x
-
- -- Substitute a name in all identifiers in a boolean expression
- subBS sub' = mapBoolSpecIdent (subsName sub')
-
- -- Traverse a boolean expression applying a function to all identifiers
- mapBoolSpecIdent :: (String -> String) -> SMV.BoolSpec -> SMV.BoolSpec
- mapBoolSpecIdent f boolSpec =
- case boolSpec of
- SMV.BoolSpecSignal (SMV.Ident i) -> SMV.BoolSpecSignal (SMV.Ident (f i))
-
- SMV.BoolSpecConst bc -> SMV.BoolSpecConst bc
-
- SMV.BoolSpecNum e -> SMV.BoolSpecNum (mapNumExprIdent f e)
-
- SMV.BoolSpecCmp spec1 op2 spec2 -> SMV.BoolSpecCmp
- (mapBoolSpecIdent f spec1) op2
- (mapBoolSpecIdent f spec2)
-
- SMV.BoolSpecNeg spec -> SMV.BoolSpecNeg (mapBoolSpecIdent f spec)
-
- SMV.BoolSpecAnd spec1 spec2 -> SMV.BoolSpecAnd
- (mapBoolSpecIdent f spec1)
- (mapBoolSpecIdent f spec2)
-
- SMV.BoolSpecOr spec1 spec2 -> SMV.BoolSpecOr
- (mapBoolSpecIdent f spec1)
- (mapBoolSpecIdent f spec2)
-
- SMV.BoolSpecXor spec1 spec2 -> SMV.BoolSpecXor
- (mapBoolSpecIdent f spec1)
- (mapBoolSpecIdent f spec2)
-
- SMV.BoolSpecImplies spec1 spec2 -> SMV.BoolSpecImplies
- (mapBoolSpecIdent f spec1)
- (mapBoolSpecIdent f spec2)
-
- SMV.BoolSpecEquivs spec1 spec2 -> SMV.BoolSpecEquivs
- (mapBoolSpecIdent f spec1)
- (mapBoolSpecIdent f spec2)
-
- SMV.BoolSpecOp1 op spec -> SMV.BoolSpecOp1 op (mapBoolSpecIdent f spec)
-
- SMV.BoolSpecOp2 spec1 op2 spec2 -> SMV.BoolSpecOp2
- (mapBoolSpecIdent f spec1) op2
- (mapBoolSpecIdent f spec2)
-
- -- Traverse a numeric expression applying a function to all identifiers
- mapNumExprIdent :: (String -> String) -> SMV.NumExpr -> SMV.NumExpr
- mapNumExprIdent f numExpr =
- case numExpr of
- SMV.NumId (SMV.Ident i) -> SMV.NumId (SMV.Ident (f i))
- SMV.NumConstI c -> SMV.NumConstI c
- SMV.NumConstD c -> SMV.NumConstD c
- SMV.NumAdd expr1 op expr2 -> SMV.NumAdd
- (mapNumExprIdent f expr1)
- op
- (mapNumExprIdent f expr2)
- SMV.NumMult expr1 op expr2 -> SMV.NumMult
- (mapNumExprIdent f expr1)
- op
- (mapNumExprIdent f expr2)
diff --git a/ogma-language-fret-cs/tests/Main.hs b/ogma-language-fret-cs/tests/Main.hs
deleted file mode 100644
index d139a36d..00000000
--- a/ogma-language-fret-cs/tests/Main.hs
+++ /dev/null
@@ -1,81 +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.
---
--- | Test FRETCS language library.
-module Main where
-
--- External imports
-import Data.Aeson ( eitherDecode )
-import Data.Either ( isLeft, isRight )
-import Test.Framework ( Test, defaultMainWithOpts )
-import Test.Framework.Providers.QuickCheck2 ( testProperty )
-import Test.QuickCheck ( Property )
-import Test.QuickCheck.Monadic ( assert, monadicIO, run )
-
--- External imports: auxiliary
-import Data.ByteString.Extra as B ( safeReadFile )
-
--- Internal imports
-import Language.FRETComponentSpec.AST ( FRETComponentSpec )
-
--- | Run all unit tests for the FRETCS parser.
-main :: IO ()
-main =
- defaultMainWithOpts tests mempty
-
--- | All unit tests for the FRETCS parser.
-tests :: [Test.Framework.Test]
-tests =
- [ testProperty "Parse FRETCS (correct case)" propParseFRETCSOk
- , testProperty "Parse FRETCS (incorrect case)" propParseFRETCSFail
- ]
-
--- | Test the FRETCS parser on a well-formed boolean specification.
-propParseFRETCSOk :: Property
-propParseFRETCSOk = monadicIO $ do
- content <- run $ parseFretComponentSpec "tests/fret_good.json"
- assert (isRight content)
-
--- | Test the FRETCS parser on an incorrect boolean specification.
-propParseFRETCSFail :: Property
-propParseFRETCSFail = monadicIO $ do
- componentSpec <- run $ parseFretComponentSpec "tests/fret_bad.json"
- assert (isLeft componentSpec)
-
--- | 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
- componentSpec <- B.safeReadFile fp
- return $ eitherDecode =<< componentSpec
diff --git a/ogma-language-fret-cs/tests/fret_bad.json b/ogma-language-fret-cs/tests/fret_bad.json
deleted file mode 100644
index 75e6ffa1..00000000
--- a/ogma-language-fret-cs/tests/fret_bad.json
+++ /dev/null
@@ -1,21 +0,0 @@
-{
- "RTSASpec": {
- "Middle_variables": [],
- "Other_variables": [
- {"name":"param_is_short", "type":"bool"},
- {"name":"param_value_short", "type":"real"},
- {"name":"param_value_long", "type":"real"},
- {"name":"upper_param_limit", "type":"real"},
- {"name":"lower_param_limit", "type":"real"},
- {"name":"envelope_issue", "type":"bool"}
- ],
- "Requirements": [
- {
- "name": "behnazOne",
- "CoCoSpecCode": "",
- "ptltl": "((H ((((! flight_mode) & (Y flight_mode)) & (Y TRUE)) -> (Y (((O[=10] (((conflict_detected) & ((Y (! (conflict_detected))) | (flight_mode & ((! (Y TRUE)) | (Y (! flight_mode)))))) & (! (( replanning_mode ))))) -> (O[<10] ((flight_mode & ((! (Y TRUE)) | (Y (! flight_mode)))) | (( replanning_mode ))))) S (((O[=10] (((conflict_detected) & ((Y (! (conflict_detected))) | (flight_mode & ((! (Y TRUE)) | (Y (! flight_mode)))))) & (! (( replanning_mode ))))) -> (O[<10] ((flight_mode & ((! (Y TRUE)) | (Y (! flight_mode)))) | (( replanning_mode ))))) & (flight_mode & ((! (Y TRUE)) | (Y (! flight_mode))))))))) & (((! ((! flight_mode) & (Y flight_mode))) S ((! ((! flight_mode) & (Y flight_mode))) & (flight_mode & ((! (Y TRUE)) | (Y (! flight_mode)))))) -> (((O[=10] (((conflict_detected) & ((Y (! (conflict_detected))) | (flight_mode & ((! (Y TRUE)) | (Y (! flight_mode)))))) & (! (( replanning_mode ))))) -> (O[<10] ((flight_mode & ((! (Y TRUE)) | (Y (! flight_mode)))) | (( replanning_mode ))))) S (((O[=10] (((conflict_detected) & ((Y (! (conflict_detected))) | (flight_mode & ((! (Y TRUE)) | (Y (! flight_mode)))))) & (! (( replanning_mode ))))) -> (O[<10] ((flight_mode & ((! (Y TRUE)) | (Y (! flight_mode)))) | (( replanning_mode ))))) & (flight_mode & ((! (Y TRUE)) | (Y (! flight_mode))))))))",
- "fretish": "Meaning not specified"
- }
- ]
- }
-}
diff --git a/ogma-language-fret-cs/tests/fret_good.json b/ogma-language-fret-cs/tests/fret_good.json
deleted file mode 100644
index 5ab0feff..00000000
--- a/ogma-language-fret-cs/tests/fret_good.json
+++ /dev/null
@@ -1,21 +0,0 @@
-{
- "RTSASpec": {
- "Internal_variables": [],
- "Other_variables": [
- {"name":"param_is_short", "type":"bool"},
- {"name":"param_value_short", "type":"real"},
- {"name":"param_value_long", "type":"real"},
- {"name":"upper_param_limit", "type":"real"},
- {"name":"lower_param_limit", "type":"real"},
- {"name":"envelope_issue", "type":"bool"}
- ],
- "Requirements": [
- {
- "name": "behnazOne",
- "CoCoSpecCode": "true",
- "ptLTL": "((H ((((! flight_mode) & (Y flight_mode)) & (Y TRUE)) -> (Y (((O[=10] (((conflict_detected) & ((Y (! (conflict_detected))) | (flight_mode & ((! (Y TRUE)) | (Y (! flight_mode)))))) & (! (( replanning_mode ))))) -> (O[<10] ((flight_mode & ((! (Y TRUE)) | (Y (! flight_mode)))) | (( replanning_mode ))))) S (((O[=10] (((conflict_detected) & ((Y (! (conflict_detected))) | (flight_mode & ((! (Y TRUE)) | (Y (! flight_mode)))))) & (! (( replanning_mode ))))) -> (O[<10] ((flight_mode & ((! (Y TRUE)) | (Y (! flight_mode)))) | (( replanning_mode ))))) & (flight_mode & ((! (Y TRUE)) | (Y (! flight_mode))))))))) & (((! ((! flight_mode) & (Y flight_mode))) S ((! ((! flight_mode) & (Y flight_mode))) & (flight_mode & ((! (Y TRUE)) | (Y (! flight_mode)))))) -> (((O[=10] (((conflict_detected) & ((Y (! (conflict_detected))) | (flight_mode & ((! (Y TRUE)) | (Y (! flight_mode)))))) & (! (( replanning_mode ))))) -> (O[<10] ((flight_mode & ((! (Y TRUE)) | (Y (! flight_mode)))) | (( replanning_mode ))))) S (((O[=10] (((conflict_detected) & ((Y (! (conflict_detected))) | (flight_mode & ((! (Y TRUE)) | (Y (! flight_mode)))))) & (! (( replanning_mode ))))) -> (O[<10] ((flight_mode & ((! (Y TRUE)) | (Y (! flight_mode)))) | (( replanning_mode ))))) & (flight_mode & ((! (Y TRUE)) | (Y (! flight_mode))))))))",
- "fretish": "Meaning not specified"
- }
- ]
- }
-}
diff --git a/ogma-language-jsonspec/CHANGELOG.md b/ogma-language-jsonspec/CHANGELOG.md
new file mode 100644
index 00000000..c5b18e28
--- /dev/null
+++ b/ogma-language-jsonspec/CHANGELOG.md
@@ -0,0 +1,5 @@
+# Revision history for ogma-language-jsonspec
+
+## [1.X.Y] - 2024-01-21
+
+* Initial release (#115).
diff --git a/ogma-language-fret-cs/LICENSE.pdf b/ogma-language-jsonspec/LICENSE.pdf
similarity index 100%
rename from ogma-language-fret-cs/LICENSE.pdf
rename to ogma-language-jsonspec/LICENSE.pdf
diff --git a/ogma-language-fret-cs/Setup.hs b/ogma-language-jsonspec/Setup.hs
similarity index 100%
rename from ogma-language-fret-cs/Setup.hs
rename to ogma-language-jsonspec/Setup.hs
diff --git a/ogma-language-fret-cs/ogma-language-fret-cs.cabal b/ogma-language-jsonspec/ogma-language-jsonspec.cabal
similarity index 77%
rename from ogma-language-fret-cs/ogma-language-fret-cs.cabal
rename to ogma-language-jsonspec/ogma-language-jsonspec.cabal
index ba2fd46a..14a725e0 100644
--- a/ogma-language-fret-cs/ogma-language-fret-cs.cabal
+++ b/ogma-language-jsonspec/ogma-language-jsonspec.cabal
@@ -1,4 +1,4 @@
--- Copyright 2020 United States Government as represented by the Administrator
+-- Copyright 2024 United States Government as represented by the Administrator
-- of the National Aeronautics and Space Administration. All Rights Reserved.
--
-- Disclaimers
@@ -31,7 +31,7 @@
cabal-version: 2.0
build-type: Simple
-name: ogma-language-fret-cs
+name: ogma-language-jsonspec
version: 1.1.0
homepage: http://nasa.gov
license: OtherLicense
@@ -43,14 +43,14 @@ extra-source-files: CHANGELOG.md
tests/fret_good.json
tests/fret_bad.json
-synopsis: Ogma: Runtime Monitor translator: FRET Component Specification Frontend
+synopsis: Ogma: Runtime Monitor translator: JSON Frontend
description: Ogma is a tool to facilitate the integration of safe runtime monitors into
other systems. Ogma extends
, a high-level runtime
verification framework that generates hard real-time C99 code.
.
- This library contains a frontend to read FRET Component Specifications.
+ This library contains a frontend to read specifications from JSON files.
-- Ogma packages should be uncurated so that only the official maintainers make
-- changes.
@@ -62,14 +62,17 @@ x-curation: uncurated
library
exposed-modules:
- Language.FRETComponentSpec.AST
+ Language.JSONSpec.Parser
build-depends:
base >= 4.11.0.0 && < 5
, aeson >= 2.0.0.0 && < 2.2
+ , jsonpath >= 0.3 && < 0.4
+ , text
+ , megaparsec
+ , bytestring
- , ogma-language-cocospec >= 1.1.0 && < 1.2
- , ogma-language-smv >= 1.1.0 && < 1.2
+ , ogma-spec >= 1.1.0 && < 1.2
hs-source-dirs:
src
@@ -79,30 +82,3 @@ library
ghc-options:
-Wall
-
-test-suite unit-tests
- type:
- exitcode-stdio-1.0
-
- main-is:
- Main.hs
-
- build-depends:
- base >= 4.11.0.0 && < 5
-
- , aeson >= 2.0.0.0 && < 2.2
- , QuickCheck
- , test-framework
- , test-framework-quickcheck2
-
- , ogma-extra >= 1.1.0 && < 1.2
- , ogma-language-fret-cs
-
- hs-source-dirs:
- tests
-
- default-language:
- Haskell2010
-
- ghc-options:
- -Wall
diff --git a/ogma-language-jsonspec/src/Language/JSONSpec/Parser.hs b/ogma-language-jsonspec/src/Language/JSONSpec/Parser.hs
new file mode 100644
index 00000000..4d079da7
--- /dev/null
+++ b/ogma-language-jsonspec/src/Language/JSONSpec/Parser.hs
@@ -0,0 +1,194 @@
+-- Copyright 2024 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.
+--
+
+-- | Parser for Ogma specs stored in JSON files.
+module Language.JSONSpec.Parser where
+
+-- External imports
+import Data.Aeson (FromJSON (..), Value (..), decode, (.:))
+import Data.Aeson.Key (toString)
+import qualified Data.Aeson.KeyMap as M
+import Data.Aeson.Types (prependFailure, typeMismatch)
+import Data.Bifunctor (first)
+import Data.ByteString.Lazy (fromStrict)
+import Data.JSONPath.Execute
+import Data.JSONPath.Parser
+import Data.JSONPath.Types
+import Data.Text (pack, unpack)
+import qualified Data.Text as T
+import qualified Data.Text.Encoding as T
+import qualified Data.Text.IO as T
+import Text.Megaparsec (eof, errorBundlePretty, parse)
+
+-- External imports: ogma-spec
+import Data.OgmaSpec
+
+data JSONFormat = JSONFormat
+ { specInternalVars :: String
+ , specInternalVarId :: String
+ , specInternalVarExpr :: String
+ , specInternalVarType :: String
+ , specExternalVars :: String
+ , specExternalVarId :: String
+ , specExternalVarType :: String
+ , specRequirements :: String
+ , specRequirementId :: String
+ , specRequirementDesc :: String
+ , specRequirementExpr :: String
+ }
+
+data JSONFormatInternal = JSONFormatInternal
+ { jfiInternalVars :: [JSONPathElement]
+ , jfiInternalVarId :: [JSONPathElement]
+ , jfiInternalVarExpr :: [JSONPathElement]
+ , jfiInternalVarType :: [JSONPathElement]
+ , jfiExternalVars :: [JSONPathElement]
+ , jfiExternalVarId :: [JSONPathElement]
+ , jfiExternalVarType :: [JSONPathElement]
+ , jfiRequirements :: [JSONPathElement]
+ , jfiRequirementId :: [JSONPathElement]
+ , jfiRequirementDesc :: [JSONPathElement]
+ , jfiRequirementExpr :: [JSONPathElement]
+ }
+
+parseJSONFormat :: JSONFormat -> Either String JSONFormatInternal
+parseJSONFormat jsonFormat = do
+ jfi2 <- showErrors $ parseJSONPath (pack (specInternalVars jsonFormat))
+ jfi3 <- showErrors $ parseJSONPath (pack (specInternalVarId jsonFormat))
+ jfi4 <- showErrors $ parseJSONPath (pack (specInternalVarExpr jsonFormat))
+ jfi5 <- showErrors $ parseJSONPath (pack (specInternalVarType jsonFormat))
+ jfi6 <- showErrors $ parseJSONPath (pack (specExternalVars jsonFormat))
+ jfi7 <- showErrors $ parseJSONPath (pack (specExternalVarId jsonFormat))
+ jfi8 <- showErrors $ parseJSONPath (pack (specExternalVarType jsonFormat))
+ jfi9 <- showErrors $ parseJSONPath (pack (specRequirements jsonFormat))
+ jfi10 <- showErrors $ parseJSONPath (pack (specRequirementId jsonFormat))
+ jfi11 <- showErrors $ parseJSONPath (pack (specRequirementDesc jsonFormat))
+ jfi12 <- showErrors $ parseJSONPath (pack (specRequirementExpr jsonFormat))
+ return $ JSONFormatInternal
+ { jfiInternalVars = jfi2
+ , jfiInternalVarId = jfi3
+ , jfiInternalVarExpr = jfi4
+ , jfiInternalVarType = jfi5
+ , jfiExternalVars = jfi6
+ , jfiExternalVarId = jfi7
+ , jfiExternalVarType = jfi8
+ , jfiRequirements = jfi9
+ , jfiRequirementId = jfi10
+ , jfiRequirementDesc = jfi11
+ , jfiRequirementExpr = jfi12
+ }
+
+parseJSONSpec :: (String -> Either String a) -> JSONFormat -> Value -> Either String (Spec a)
+parseJSONSpec parseExpr jsonFormat value = do
+ jsonFormatInternal <- parseJSONFormat jsonFormat
+
+ let values :: [Value]
+ values = executeJSONPath (jfiInternalVars jsonFormatInternal) value
+
+ internalVarDef :: Value -> Either String InternalVariableDef
+ internalVarDef value = do
+ let msg = "internal variable name"
+ varId <- valueToString msg =<< (listToEither msg (executeJSONPath (jfiInternalVarId jsonFormatInternal) value))
+
+ let msg = "internal variable type"
+ varType <- valueToString msg =<< (listToEither msg (executeJSONPath (jfiInternalVarType jsonFormatInternal) value))
+
+ let msg = "internal variable expr"
+ varExpr <- valueToString msg =<< (listToEither msg (executeJSONPath (jfiInternalVarExpr jsonFormatInternal) value))
+
+ return $ InternalVariableDef
+ { internalVariableName = varId
+ , internalVariableType = varType
+ , internalVariableExpr = varExpr
+ }
+
+ internalVariableDefs <- mapM internalVarDef values
+
+ let values :: [Value]
+ values = executeJSONPath (jfiExternalVars jsonFormatInternal) value
+
+ externalVarDef :: Value -> Either String ExternalVariableDef
+ externalVarDef value = do
+
+ let msg = "external variable name"
+ varId <- valueToString msg =<< (listToEither msg (executeJSONPath (jfiExternalVarId jsonFormatInternal) value))
+
+ let msg = "external variable type"
+ varType <- valueToString msg =<< (listToEither msg (executeJSONPath (jfiExternalVarType jsonFormatInternal) value))
+
+ return $ ExternalVariableDef
+ { externalVariableName = varId
+ , externalVariableType = varType
+ }
+
+ externalVariableDefs <- mapM externalVarDef values
+
+ let values :: [Value]
+ values = executeJSONPath (jfiRequirements jsonFormatInternal) value
+
+ -- requirementDef :: Value -> Either String (Requirement a)
+ requirementDef value = do
+ let msg = "Requirement name"
+ reqId <- valueToString msg =<< (listToEither msg (executeJSONPath (jfiRequirementId jsonFormatInternal) value))
+
+ let msg = "Requirement expression"
+ reqExpr <- valueToString msg =<< (listToEither msg (executeJSONPath (jfiRequirementExpr jsonFormatInternal) value))
+ reqExpr' <- parseExpr reqExpr
+
+ let msg = "Requirement description"
+ reqDesc <- valueToString msg =<< (listToEither msg (executeJSONPath (jfiRequirementDesc jsonFormatInternal) value))
+
+ return $ Requirement
+ { requirementName = reqId
+ , requirementExpr = reqExpr'
+ , requirementDescription = reqDesc
+ }
+
+ requirements <- mapM requirementDef values
+
+ return $ Spec internalVariableDefs externalVariableDefs requirements
+
+valueToString :: String -> Value -> Either String String
+valueToString msg (String x) = Right $ unpack x
+valueToString msg _ = Left $ "The JSON value provided for " ++ msg ++ " does not contain a string"
+
+listToEither :: String -> [a] -> Either String a
+listToEither _ [x] = Right x
+listToEither msg [] = Left $ "Failed to find a value for " ++ msg
+listToEither msg _ = Left $ "Unexpectedly found multiple values for " ++ msg
+
+-- | Parse a JSONPath expression, returning its element components.
+parseJSONPath :: T.Text -> Either String [JSONPathElement]
+parseJSONPath = first errorBundlePretty . parse (jsonPath eof) ""
+
+showErrors :: Show a => Either a b -> Either String b
+showErrors (Left s) = Left (show s)
+showErrors (Right x) = Right x
diff --git a/ogma-language-smv/CHANGELOG.md b/ogma-language-smv/CHANGELOG.md
index dc888eb1..969a24aa 100644
--- a/ogma-language-smv/CHANGELOG.md
+++ b/ogma-language-smv/CHANGELOG.md
@@ -1,5 +1,9 @@
# Revision history for ogma-language-smv
+## [1.X.Y] - 2024-01-21
+
+* Introduce identifier substitution functions (#115).
+
## [1.1.0] - 2023-11-21
* Version bump 1.1.0 (#112).
diff --git a/ogma-language-smv/ogma-language-smv.cabal b/ogma-language-smv/ogma-language-smv.cabal
index 68ef21d9..a77235eb 100644
--- a/ogma-language-smv/ogma-language-smv.cabal
+++ b/ogma-language-smv/ogma-language-smv.cabal
@@ -77,6 +77,7 @@ library
Language.SMV.LexSMV
Language.SMV.ParSMV
Language.SMV.PrintSMV
+ Language.SMV.Substitution
autogen-modules:
Language.SMV.AbsSMV
diff --git a/ogma-language-smv/src/Language/SMV/Substitution.hs b/ogma-language-smv/src/Language/SMV/Substitution.hs
new file mode 100644
index 00000000..f22c474c
--- /dev/null
+++ b/ogma-language-smv/src/Language/SMV/Substitution.hs
@@ -0,0 +1,69 @@
+module Language.SMV.Substitution where
+
+import qualified Language.SMV.AbsSMV as SMV
+
+substituteBoolExpr subs e = foldr subBS e subs
+
+-- Substitute name x if it matches the old name oName
+subsName (oName, nName) x = if x == oName then nName else x
+
+-- Substitute a name in all identifiers in a boolean expression
+subBS sub' = mapBoolSpecIdent (subsName sub')
+
+-- Traverse a boolean expression applying a function to all identifiers
+mapBoolSpecIdent :: (String -> String) -> SMV.BoolSpec -> SMV.BoolSpec
+mapBoolSpecIdent f boolSpec =
+ case boolSpec of
+ SMV.BoolSpecSignal (SMV.Ident i) -> SMV.BoolSpecSignal (SMV.Ident (f i))
+
+ SMV.BoolSpecConst bc -> SMV.BoolSpecConst bc
+
+ SMV.BoolSpecNum e -> SMV.BoolSpecNum (mapNumExprIdent f e)
+
+ SMV.BoolSpecCmp spec1 op2 spec2 -> SMV.BoolSpecCmp
+ (mapBoolSpecIdent f spec1) op2
+ (mapBoolSpecIdent f spec2)
+
+ SMV.BoolSpecNeg spec -> SMV.BoolSpecNeg (mapBoolSpecIdent f spec)
+
+ SMV.BoolSpecAnd spec1 spec2 -> SMV.BoolSpecAnd
+ (mapBoolSpecIdent f spec1)
+ (mapBoolSpecIdent f spec2)
+
+ SMV.BoolSpecOr spec1 spec2 -> SMV.BoolSpecOr
+ (mapBoolSpecIdent f spec1)
+ (mapBoolSpecIdent f spec2)
+
+ SMV.BoolSpecXor spec1 spec2 -> SMV.BoolSpecXor
+ (mapBoolSpecIdent f spec1)
+ (mapBoolSpecIdent f spec2)
+
+ SMV.BoolSpecImplies spec1 spec2 -> SMV.BoolSpecImplies
+ (mapBoolSpecIdent f spec1)
+ (mapBoolSpecIdent f spec2)
+
+ SMV.BoolSpecEquivs spec1 spec2 -> SMV.BoolSpecEquivs
+ (mapBoolSpecIdent f spec1)
+ (mapBoolSpecIdent f spec2)
+
+ SMV.BoolSpecOp1 op spec -> SMV.BoolSpecOp1 op (mapBoolSpecIdent f spec)
+
+ SMV.BoolSpecOp2 spec1 op2 spec2 -> SMV.BoolSpecOp2
+ (mapBoolSpecIdent f spec1) op2
+ (mapBoolSpecIdent f spec2)
+
+-- Traverse a numeric expression applying a function to all identifiers
+mapNumExprIdent :: (String -> String) -> SMV.NumExpr -> SMV.NumExpr
+mapNumExprIdent f numExpr =
+ case numExpr of
+ SMV.NumId (SMV.Ident i) -> SMV.NumId (SMV.Ident (f i))
+ SMV.NumConstI c -> SMV.NumConstI c
+ SMV.NumConstD c -> SMV.NumConstD c
+ SMV.NumAdd expr1 op expr2 -> SMV.NumAdd
+ (mapNumExprIdent f expr1)
+ op
+ (mapNumExprIdent f expr2)
+ SMV.NumMult expr1 op expr2 -> SMV.NumMult
+ (mapNumExprIdent f expr1)
+ op
+ (mapNumExprIdent f expr2)
diff --git a/ogma-spec/CHANGELOG.md b/ogma-spec/CHANGELOG.md
new file mode 100644
index 00000000..da9dcb72
--- /dev/null
+++ b/ogma-spec/CHANGELOG.md
@@ -0,0 +1,5 @@
+# Revision history for ogma-spec
+
+## [1.X.Y] - 2024-01-21
+
+* Initial release (#115).
diff --git a/ogma-spec/LICENSE.pdf b/ogma-spec/LICENSE.pdf
new file mode 100644
index 00000000..d4333fb2
Binary files /dev/null and b/ogma-spec/LICENSE.pdf differ
diff --git a/ogma-spec/Setup.hs b/ogma-spec/Setup.hs
new file mode 100644
index 00000000..9a994af6
--- /dev/null
+++ b/ogma-spec/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/ogma-spec/ogma-spec.cabal b/ogma-spec/ogma-spec.cabal
new file mode 100644
index 00000000..c80149e1
--- /dev/null
+++ b/ogma-spec/ogma-spec.cabal
@@ -0,0 +1,77 @@
+-- Copyright 2024 United States Government as represented by the Administrator
+-- of the National Aeronautics and Space Administration. All Rights Reserved.
+--
+-- Disclaimers
+--
+-- No Warranty: THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY
+-- OF ANY KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT
+-- LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO
+-- SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR A
+-- PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT THE
+-- SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT DOCUMENTATION, IF
+-- PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE. THIS AGREEMENT DOES NOT, IN
+-- ANY MANNER, CONSTITUTE AN ENDORSEMENT BY GOVERNMENT AGENCY OR ANY PRIOR
+-- RECIPIENT OF ANY RESULTS, RESULTING DESIGNS, HARDWARE, SOFTWARE PRODUCTS OR
+-- ANY OTHER APPLICATIONS RESULTING FROM USE OF THE SUBJECT SOFTWARE. FURTHER,
+-- GOVERNMENT AGENCY DISCLAIMS ALL WARRANTIES AND LIABILITIES REGARDING
+-- THIRD-PARTY SOFTWARE, IF PRESENT IN THE ORIGINAL SOFTWARE, AND DISTRIBUTES
+-- IT "AS IS."
+--
+-- Waiver and Indemnity: RECIPIENT AGREES TO WAIVE ANY AND ALL CLAIMS AGAINST
+-- THE UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS, AS WELL AS
+-- ANY PRIOR RECIPIENT. IF RECIPIENT'S USE OF THE SUBJECT SOFTWARE RESULTS IN
+-- ANY LIABILITIES, DEMANDS, DAMAGES, EXPENSES OR LOSSES ARISING FROM SUCH USE,
+-- INCLUDING ANY DAMAGES FROM PRODUCTS BASED ON, OR RESULTING FROM, RECIPIENT'S
+-- USE OF THE SUBJECT SOFTWARE, RECIPIENT SHALL INDEMNIFY AND HOLD HARMLESS THE
+-- UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS, AS WELL AS ANY
+-- PRIOR RECIPIENT, TO THE EXTENT PERMITTED BY LAW. RECIPIENT'S SOLE REMEDY
+-- FOR ANY SUCH MATTER SHALL BE THE IMMEDIATE, UNILATERAL TERMINATION OF THIS
+-- AGREEMENT.
+
+cabal-version: 2.0
+build-type: Simple
+
+name: ogma-spec
+version: 1.1.0
+homepage: http://nasa.gov
+license: OtherLicense
+license-file: LICENSE.pdf
+author: Ivan Perez, Alwyn Goodloe
+maintainer: ivan.perezdominguez@nasa.gov
+category: Aerospace
+extra-source-files: CHANGELOG.md
+ tests/fret_good.json
+ tests/fret_bad.json
+
+synopsis: Ogma: Runtime Monitor translator: JSON Frontend
+
+description: Ogma is a tool to facilitate the integration of safe runtime monitors into
+ other systems. Ogma extends
+ , a high-level runtime
+ verification framework that generates hard real-time C99 code.
+ .
+ This library contains an abstract representation of an Ogma specification.
+
+-- Ogma packages should be uncurated so that only the official maintainers make
+-- changes.
+--
+-- Because this is a NASA project, we want to make sure that users obtain
+-- exactly what we publish, unmodified by anyone external to our project.
+x-curation: uncurated
+
+library
+
+ exposed-modules:
+ Data.OgmaSpec
+
+ build-depends:
+ base >= 4.11.0.0 && < 5
+
+ hs-source-dirs:
+ src
+
+ default-language:
+ Haskell2010
+
+ ghc-options:
+ -Wall
diff --git a/ogma-spec/src/Data/OgmaSpec.hs b/ogma-spec/src/Data/OgmaSpec.hs
new file mode 100644
index 00000000..e7ef13b6
--- /dev/null
+++ b/ogma-spec/src/Data/OgmaSpec.hs
@@ -0,0 +1,67 @@
+-- Copyright 2024 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.
+--
+-- | Abstract representation of an Ogma specification.
+module Data.OgmaSpec where
+
+-- | Abstract representation of an Ogma specification.
+data Spec a = Spec
+ { internalVariables :: [ InternalVariableDef ]
+ , externalVariables :: [ ExternalVariableDef ]
+ , requirements :: [ Requirement a ]
+ }
+ deriving (Show)
+
+-- | Internal variable definition, with a given name, its type and definining
+-- expression.
+data InternalVariableDef = InternalVariableDef
+ { internalVariableName :: String
+ , internalVariableType :: String
+ , internalVariableExpr :: String
+ }
+ deriving (Show)
+
+-- | External variable definition, with a given name and type.
+--
+-- The value of external variables is assigned outside Copilot, so they have no
+-- defining expression in this type.
+data ExternalVariableDef = ExternalVariableDef
+ { externalVariableName :: String
+ , externalVariableType :: String
+ }
+ deriving (Show)
+
+-- | Requirement with a given name and a boolean expression.
+data Requirement a = Requirement
+ { requirementName :: String
+ , requirementExpr :: a
+ , requirementDescription :: String
+ }
+ deriving (Show)