diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,14 @@ # Revision history for ogma-core +## [1.3.0] - 2024-03-21 + +* Version bump 1.3.0 (#133). +* Fix missing stream name substitution (#120). +* Use generalized JSON parser for DB Spec (#122). +* Fix translation of equivalence boolean operator from SMV (#126). +* Sanitize handler names (#127). +* Use same handler name in FPrime/ROS and Copilot (#130). + ## [1.2.0] - 2024-01-21 * Version bump 1.2.0 (#117). diff --git a/ogma-core.cabal b/ogma-core.cabal --- a/ogma-core.cabal +++ b/ogma-core.cabal @@ -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 diff --git a/src/Command/FPrimeApp.hs b/src/Command/FPrimeApp.hs --- a/src/Command/FPrimeApp.hs +++ b/src/Command/FPrimeApp.hs @@ -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" } diff --git a/src/Command/FRETComponentSpec2Copilot.hs b/src/Command/FRETComponentSpec2Copilot.hs --- a/src/Command/FRETComponentSpec2Copilot.hs +++ b/src/Command/FRETComponentSpec2Copilot.hs @@ -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" } diff --git a/src/Command/FRETReqsDB2Copilot.hs b/src/Command/FRETReqsDB2Copilot.hs --- a/src/Command/FRETReqsDB2Copilot.hs +++ b/src/Command/FRETReqsDB2Copilot.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE ExistentialQuantification #-} -- Copyright 2020 United States Government as represented by the Administrator -- of the National Aeronautics and Space Administration. All Rights Reserved. -- @@ -30,9 +31,6 @@ -- -- | Transform a FRET requirements database containing a temporal logic -- specification into a Copilot specification. --- --- This module makes use of --- "Language.Trans.FRETReqsDB2Copilot", which does most of the work. module Command.FRETReqsDB2Copilot ( fretReqsDB2Copilot , FRETReqsDB2CopilotOptions(..) @@ -43,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) diff --git a/src/Command/ROSApp.hs b/src/Command/ROSApp.hs --- a/src/Command/ROSApp.hs +++ b/src/Command/ROSApp.hs @@ -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" } diff --git a/src/Language/Trans/FRETReqsDB2Copilot.hs b/src/Language/Trans/FRETReqsDB2Copilot.hs deleted file mode 100644 --- a/src/Language/Trans/FRETReqsDB2Copilot.hs +++ /dev/null @@ -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 ++ "\"" - ] diff --git a/src/Language/Trans/SMV2Copilot.hs b/src/Language/Trans/SMV2Copilot.hs --- a/src/Language/Trans/SMV2Copilot.hs +++ b/src/Language/Trans/SMV2Copilot.hs @@ -83,7 +83,7 @@ ++ ")" BoolSpecEquivs spec1 spec2 -> "(" ++ boolSpec2Copilot spec1 - ++ " " ++ "<==>" + ++ " " ++ "==" ++ " " ++ boolSpec2Copilot spec2 ++ ")" diff --git a/src/Language/Trans/Spec2Copilot.hs b/src/Language/Trans/Spec2Copilot.hs --- a/src/Language/Trans/Spec2Copilot.hs +++ b/src/Language/Trans/Spec2Copilot.hs @@ -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).