ogma-core 1.2.0 → 1.3.0
raw patch · 9 files changed
+151/−242 lines, 9 filesdep −ogma-language-fret-reqsdep ~ogma-extradep ~ogma-language-cdep ~ogma-language-cocospec
Dependencies removed: ogma-language-fret-reqs
Dependency ranges changed: ogma-extra, ogma-language-c, ogma-language-cocospec, ogma-language-copilot, ogma-language-jsonspec, ogma-language-smv, ogma-spec
Files
- CHANGELOG.md +9/−0
- ogma-core.cabal +8/−10
- src/Command/FPrimeApp.hs +6/−6
- src/Command/FRETComponentSpec2Copilot.hs +5/−5
- src/Command/FRETReqsDB2Copilot.hs +114/−43
- src/Command/ROSApp.hs +6/−6
- src/Language/Trans/FRETReqsDB2Copilot.hs +0/−169
- src/Language/Trans/SMV2Copilot.hs +1/−1
- src/Language/Trans/Spec2Copilot.hs +2/−2
CHANGELOG.md view
@@ -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.cabal view
@@ -32,7 +32,7 @@ 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 @@ Language.Trans.CStruct2CopilotStruct Language.Trans.CStructs2Copilot Language.Trans.CStructs2MsgHandlers- Language.Trans.FRETReqsDB2Copilot Language.Trans.Spec2Copilot Language.Trans.SMV2Copilot @@ -110,14 +109,13 @@ , 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
src/Command/FPrimeApp.hs view
@@ -246,7 +246,7 @@ $ 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 @@ -- | 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" }
src/Command/FRETComponentSpec2Copilot.hs view
@@ -159,16 +159,16 @@ -- | 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" }
src/Command/FRETReqsDB2Copilot.hs view
@@ -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,22 +41,32 @@ -- 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,24 +79,50 @@ -> 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@@ -96,17 +130,6 @@ , 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,17 +142,6 @@ 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.@@ -137,6 +149,65 @@ -> 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)
src/Command/ROSApp.hs view
@@ -250,7 +250,7 @@ $ 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 @@ -- | 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" }
− src/Language/Trans/FRETReqsDB2Copilot.hs
@@ -1,169 +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.------- | Transform a FRET temporal logic specification contained in a requirements--- database into a Copilot specification.------ Ideally, 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.FRETReqsDB2Copilot- ( FRETReqsDB2CopilotOptions(..)- , fret2CopilotModule- )- where---- External imports-import Data.List ( nub, sort )---- Internal imports: SMV-import qualified Language.SMV.AbsSMV as SMV ( BoolSpec (..) )-import qualified Language.Trans.SMV2Copilot as SMV ( boolSpec2Copilot,- boolSpecNames )---- Internal imports: CoCoSpec-import qualified Language.CoCoSpec.AbsCoCoSpec as CoCoSpec ( BoolSpec (..) )-import qualified Language.Trans.CoCoSpec2Copilot as CoCoSpec ( boolSpec2Copilot,- boolSpecNames )--import qualified Language.FRETReqsDB.AST as FRET ( FRETReqsDB, semantics,- semanticsCoCoSpec,- semanticsFretish )---- | Options used to customize the conversion of FRET Component Specifications--- to Copilot code.-data FRETReqsDB2CopilotOptions = FRETReqsDB2CopilotOptions- { fretReqsDB2CopilotUseCoCoSpec :: Bool- , fretReqsDB2CopilotFilename :: String- }---- | Return a string with the contents of the Copilot module that implements a--- CoCoSpec BoolSpec.------ PRE: The BoolSpec does not use any identifiers that exist in Copilot,--- or any of @prop@, @clock@, @ftp@, @ot@, @pre@. All identifiers used are--- valid C99 identifiers.-fret2CopilotModule :: FRETReqsDB2CopilotOptions- -> FRET.FRETReqsDB- -> Either String String-fret2CopilotModule prefs x = do- cocoSpec <- FRET.semanticsCoCoSpec $ FRET.semantics x- smvSpec <- FRET.semanticsFretish $ FRET.semantics x- pure $ fret2CopilotModule' prefs smvSpec cocoSpec--fret2CopilotModule' :: FRETReqsDB2CopilotOptions- -> SMV.BoolSpec- -> CoCoSpec.BoolSpec- -> String-fret2CopilotModule' prefs smvSpec cocoSpec = unlines $ concat sections- where- specS = if fretReqsDB2CopilotUseCoCoSpec prefs- then CoCoSpec.boolSpec2Copilot cocoSpec- else SMV.boolSpec2Copilot smvSpec-- idents = nub $ sort $ if fretReqsDB2CopilotUseCoCoSpec prefs- then CoCoSpec.boolSpecNames cocoSpec- else SMV.boolSpecNames smvSpec-- sections | fretReqsDB2CopilotUseCoCoSpec prefs- = [ imports, propDef, externs, clock, ftp, undef, tpre, spec- , main'- ]-- | otherwise- = [ imports, propDef, externs, clock, ftp, tpre, spec, main' ]-- imports :: [String]- imports =- [ "import Copilot.Compile.C99"- , "import Copilot.Language hiding (prop)"- , "import Copilot.Language.Prelude"- , "import Copilot.Library.LTL (next)"- , "import Copilot.Library.MTL hiding (since,"- ++ " alwaysBeen, trigger)"- , "import Copilot.Library.PTLTL (since, previous,"- ++ " alwaysBeen)"- , "import qualified Copilot.Library.PTLTL as PTLTL"- , "import qualified Copilot.Library.MTL as MTL"- , "import Language.Copilot (reify)"- , "import Prelude hiding ((&&), (||), (++), (<=), (>=),"- ++ " (<), (>), (==), (/=), not)"- , ""- ]-- propDef = [ ""- , "-- | Property to monitor."- , "prop :: Stream Bool"- , "prop = " ++ specS- , ""- ]-- externs = map (\i -> i ++ " = extern " ++ show i ++ " Nothing") idents-- clock = [ ""- , "-- | Clock that increases in one-unit steps."- , "clock :: Stream Int64"- , "clock = [0] ++ (clock + 1)"- , ""- ]-- ftp = [ ""- , "-- | First Time Point"- , "ftp :: Stream Bool"- , "ftp = [True] ++ false"- , ""- ]-- undef = [ "ot :: Int -> Int -> Stream Bool -> Stream Bool"- , "ot = undefined"- , "pre :: Stream Bool -> Stream Bool"- , "pre = undefined"- ]-- tpre = [ ""- , "tpre :: Stream Bool -> Stream Bool"- , "tpre = ([True] ++)"- ]-- spec = [ ""- , "-- | Complete specification. Calls the C function void handler(); when"- , "-- the property is violated."- , "spec :: Spec"- , "spec = do"- , " trigger \"handler\" prop []"- , ""- ]-- main' = [ ""- , "main :: IO ()"- , "main = reify spec >>= compile \""- ++ fretReqsDB2CopilotFilename prefs ++ "\""- ]
src/Language/Trans/SMV2Copilot.hs view
@@ -83,7 +83,7 @@ ++ ")" BoolSpecEquivs spec1 spec2 -> "(" ++ boolSpec2Copilot spec1- ++ " " ++ "<==>"+ ++ " " ++ "==" ++ " " ++ boolSpec2Copilot spec2 ++ ")"
src/Language/Trans/Spec2Copilot.hs view
@@ -213,8 +213,8 @@ reqTrigger r = " trigger " ++ show handlerName ++ " (not " ++ propName ++ ") " ++ "[]" where- handlerName = "handler" ++ requirementName r- propName = requirementName r+ handlerName = "handler" ++ sanitizeUCIdentifier (requirementName r)+ propName = safeMap nameSubstitutions (requirementName r) -- Main program that compiles specification to C in two files (code and -- header).