ogma-core 1.1.0 → 1.2.0
raw patch · 7 files changed
+488/−414 lines, 7 filesdep +bytestringdep +ogma-language-jsonspecdep +ogma-specdep −ogma-language-fret-csdep ~ogma-extradep ~ogma-language-cdep ~ogma-language-cocospec
Dependencies added: bytestring, ogma-language-jsonspec, ogma-spec
Dependencies removed: ogma-language-fret-cs
Dependency ranges changed: ogma-extra, ogma-language-c, ogma-language-cocospec, ogma-language-copilot, ogma-language-fret-reqs, ogma-language-smv
Files
- CHANGELOG.md +5/−0
- ogma-core.cabal +11/−9
- src/Command/FPrimeApp.hs +31/−15
- src/Command/FRETComponentSpec2Copilot.hs +98/−39
- src/Command/ROSApp.hs +31/−15
- src/Language/Trans/FRETComponentSpec2Copilot.hs +0/−336
- src/Language/Trans/Spec2Copilot.hs +312/−0
CHANGELOG.md view
@@ -1,5 +1,10 @@ # Revision history for ogma-core +## [1.2.0] - 2024-01-21++* Version bump 1.2.0 (#117).+* Generalize JSON parser (#115).+ ## [1.1.0] - 2023-11-21 * Version bump 1.1.0 (#112).
ogma-core.cabal view
@@ -32,7 +32,7 @@ build-type: Simple name: ogma-core-version: 1.1.0+version: 1.2.0 homepage: http://nasa.gov license: OtherLicense license-file: LICENSE.pdf@@ -92,8 +92,8 @@ Language.Trans.CStruct2CopilotStruct Language.Trans.CStructs2Copilot Language.Trans.CStructs2MsgHandlers- Language.Trans.FRETComponentSpec2Copilot Language.Trans.FRETReqsDB2Copilot+ Language.Trans.Spec2Copilot Language.Trans.SMV2Copilot other-modules:@@ -105,17 +105,19 @@ build-depends: base >= 4.11.0.0 && < 5 , aeson >= 2.0.0.0 && < 2.2+ , bytestring , filepath , IfElse , mtl - , ogma-extra >= 1.1.0 && < 1.2- , ogma-language-c >= 1.1.0 && < 1.2- , ogma-language-cocospec >= 1.1.0 && < 1.2- , ogma-language-copilot >= 1.1.0 && < 1.2- , ogma-language-fret-cs >= 1.1.0 && < 1.2- , ogma-language-fret-reqs >= 1.1.0 && < 1.2- , ogma-language-smv >= 1.1.0 && < 1.2+ , ogma-extra >= 1.2.0 && < 1.3+ , ogma-language-c >= 1.2.0 && < 1.3+ , ogma-language-cocospec >= 1.2.0 && < 1.3+ , ogma-language-copilot >= 1.2.0 && < 1.3+ , ogma-language-fret-reqs >= 1.2.0 && < 1.3+ , ogma-language-jsonspec >= 1.2.0 && < 1.3+ , ogma-language-smv >= 1.2.0 && < 1.3+ , ogma-spec >= 1.2.0 && < 1.3 hs-source-dirs: src
src/Command/FPrimeApp.hs view
@@ -53,13 +53,14 @@ 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 @@ -- | 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 @@ -- -- 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 @@ -- | 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 @@ -- 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"+ }
src/Command/FRETComponentSpec2Copilot.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. --@@ -41,7 +42,8 @@ -- 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,13 +52,23 @@ 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 @@ -> 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-- -- Extract internal command options from external command options- let internalOptions = fretComponentSpec2CopilotOptions options+ let functions = fretExprPair (fretCS2CopilotUseCoCoSpec options) - let copilot = T.fretComponentSpec2Copilot internalOptions =<< fret+ copilot <- fretComponentSpec2Copilot' fp options functions let (mOutput, result) = fretComponentSpec2CopilotResult options fp copilot@@ -88,6 +94,34 @@ 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 @@ , 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 @@ 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 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)
src/Command/ROSApp.hs view
@@ -56,13 +56,14 @@ 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 @@ -- | 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 @@ -- -- 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 @@ -- | 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 @@ -- 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"+ }
− src/Language/Trans/FRETComponentSpec2Copilot.hs
@@ -1,336 +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 #-}---- | Transform a FRET Component Specification into a 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---- External imports-import Data.List ( intersect, 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--- 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- , internals- , reqs- , pure clock- , pure ftp- , pure pre- , pure tpre- , pure spec- , pure main'- ]-- where-- -- Import header block- 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)"- , ""- ]-- -- Extern streams- externs = concatMap externVarToDecl- (FRET.fretExternalVariables fretComponentSpec)- where- externVarToDecl i = [ FRET.fretExternalVariableName i- ++ " :: Stream "- ++ "("- ++ fretTypeToCopilotType- prefs- (FRET.fretExternalVariableType i)- ++ ")"-- , FRET.fretExternalVariableName i- ++ " = "- ++ "extern"- ++ " "- ++ show (FRET.fretExternalVariableName i)- ++ " "- ++ "Nothing"- , ""- ]-- -- Internal stream definitions- internals = concat- <$> mapM internalVarToDecl- (FRET.fretInternalVariables fretComponentSpec)- where- internalVarToDecl i = fmap (\implem ->- [ FRET.fretInternalVariableName i- ++ " :: Stream "- ++ "("- ++ fretTypeToCopilotType- prefs- (FRET.fretInternalVariableType i)- ++ ")"-- , FRET.fretInternalVariableName i- ++ " = "- ++ implem-- , ""- ]) implementation- where- implementation = if null (FRET.fretInternalVariableCopilot i)- then CoCoSpec.boolSpec2Copilot- <$> CoCoSpec.pBoolSpec- ( CoCoSpec.myLexer- $ FRET.fretInternalVariableLustre i- )- else pure (FRET.fretInternalVariableCopilot i)-- -- Encoding of requirements as boolean streams- reqs :: Either String [String]- reqs = concat <$> mapM reqToDecl (FRET.fretRequirements fretComponentSpec)- where- reqToDecl i = sequence- [ pure reqComment, pure reqSignature, reqBody, pure "" ]- where- -- Definition comment, which includes the requirement for- -- traceability purposes.- reqComment = "-- | " ++ FRET.fretRequirementName i ++ "\n" ++- "-- @" ++ "\n" ++- "-- " ++ FRET.fretRequirementFretish i ++ "\n" ++- "-- @"-- -- Definition type signature.- reqSignature = FRET.fretRequirementName i- ++ " :: " ++ "Stream" ++ " " ++ "Bool"-- -- Definition implementation, either in SMV or in CoCoSpec- reqBody = if fretCS2CopilotUseCoCoSpec prefs- then reqBodyCoCo- else reqBodyPT-- 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]- clock = [ ""- , "-- | Clock that increases in one-unit steps."- , "clock :: Stream Int64"- , "clock = [0] ++ (clock + 1)"- , ""- ]-- -- Auxiliary streams: first time point- ftp :: [String]- ftp = [ ""- , "-- | First Time Point"- , "ftp :: Stream Bool"- , "ftp = [True] ++ false"- , ""- ]-- -- Auxiliary streams: pre- pre = [ ""- , "pre :: Stream Bool -> Stream Bool"- , "pre = ([False] ++)"- ]-- -- Auxiliary streams: tpre- tpre = [ ""- , "tpre :: Stream Bool -> Stream Bool"- , "tpre = ([True] ++)"- ]-- -- Main specification- spec :: [String]- spec = [ ""- , "-- | 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)-- reqTrigger :: FRETRequirement -> String- reqTrigger r = " trigger " ++ show handlerName ++ " (not "- ++ propName ++ ") " ++ "[]"- where- handlerName = "handler" ++ FRET.fretRequirementName r- propName = FRET.fretRequirementName 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 ++ "\""- ]---- | 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- | not (null evnClash)- = Left $ "Name clash detected: " ++ show evnClash-- | not (null ivnClash)- = Left $ "Name clash detected: " ++ show ivnClash-- | not (null reqClash)- = Left $ "Name clash detected: " ++ show reqClash-- | otherwise- = Right $ foldr applySubstitution fretComponentSpec nameSubstitutions-- where-- -- Sets containing name clashes- ivnClash = internalVariableNames'- `intersect` (externalVariableNames' `union` requirementNames')-- evnClash = externalVariableNames'- `intersect` (internalVariableNames' `union` requirementNames')-- reqClash = requirementNames'- `intersect` (internalVariableNames'- `union` externalVariableNames')-- -- Names used.- internalVariableNames' = map snd internalVariableMap- externalVariableNames' = map snd externalVariableMap- requirementNames' = map snd requirementNameMap-- -- 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 fretInternalVariableName- $ fretInternalVariables fretComponentSpec-- externalVariableNames = map fretExternalVariableName- $ fretExternalVariables fretComponentSpec-- requirementNames = map fretRequirementName- $ fretRequirements fretComponentSpec
+ src/Language/Trans/Spec2Copilot.hs view
@@ -0,0 +1,312 @@+-- 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.++-- | 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.Spec2Copilot where++-- External imports+import Data.List ( intersect, lookup, union )+import Data.Maybe ( fromMaybe )++-- External imports: auxiliary+import Data.String.Extra ( sanitizeLCIdentifier, sanitizeUCIdentifier )++-- 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+-- 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+ , clock+ , ftp+ , pre+ , tpre+ , copilotSpec+ , main'+ ]++ where++ -- Import header block+ 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)"+ , ""+ ]++ -- Extern streams+ externs = concatMap externVarToDecl+ (externalVariables spec)+ where+ externVarToDecl i = [ propName+ ++ " :: Stream "+ ++ "("+ ++ safeMap typeMaps (externalVariableType i)+ ++ ")"++ , propName+ ++ " = "+ ++ "extern"+ ++ " "+ ++ show (externalVariableName i)+ ++ " "+ ++ "Nothing"+ , ""+ ]+ where+ propName = safeMap nameSubstitutions (externalVariableName i)++ -- Internal stream definitions+ internals = concatMap internalVarToDecl+ (internalVariables spec)+ where+ internalVarToDecl i = (\implem ->+ [ propName+ ++ " :: Stream "+ ++ "("+ ++ safeMap typeMaps (internalVariableType i)+ ++ ")"++ , propName+ ++ " = "+ ++ implem++ , ""+ ]) implementation+ where+ propName = safeMap nameSubstitutions (internalVariableName i)+ implementation = (internalVariableExpr i)++ -- Encoding of requirements as boolean streams+ reqs :: [String]+ reqs = concatMap reqToDecl (requirements spec)+ where+ reqToDecl i = [ reqComment, reqSignature+ , reqBody nameSubstitutions+ , ""+ ]+ where+ reqName = safeMap nameSubstitutions (requirementName i)++ -- Definition comment, which includes the requirement for+ -- traceability purposes.+ reqComment = "-- | " ++ requirementName i ++ "\n" +++ "-- @" ++ "\n" +++ "-- " ++ requirementDescription i ++ "\n" +++ "-- @"++ -- Definition type signature.+ reqSignature = reqName+ ++ " :: " ++ "Stream" ++ " " ++ "Bool"++ -- Definition implementation. We use an auxiliary function to+ -- transform the implementation into Copilot, applying a+ -- substitution.+ reqBody subs = reqName ++ " = " +++ (showExpr (exprTransform subs (requirementExpr i)))+++ -- Auxiliary streams: clock+ clock :: [String]+ clock = [ ""+ , "-- | Clock that increases in one-unit steps."+ , "clock :: Stream Int64"+ , "clock = [0] ++ (clock + 1)"+ , ""+ ]++ -- Auxiliary streams: first time point+ ftp :: [String]+ ftp = [ ""+ , "-- | First Time Point"+ , "ftp :: Stream Bool"+ , "ftp = [True] ++ false"+ , ""+ ]++ -- Auxiliary streams: pre+ pre = [ ""+ , "pre :: Stream Bool -> Stream Bool"+ , "pre = ([False] ++)"+ ]++ -- Auxiliary streams: tpre+ tpre = [ ""+ , "tpre :: Stream Bool -> Stream Bool"+ , "tpre = ([True] ++)"+ ]++ -- Main specification+ 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 (requirements spec)++ reqTrigger :: Requirement a -> String+ reqTrigger r = " trigger " ++ show handlerName ++ " (not "+ ++ propName ++ ") " ++ "[]"+ where+ 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 \"" ++ specName ++ "\""+ ]++ -- 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++ | not (null ivnClash)+ = Left $ "Name clash detected: " ++ show ivnClash++ | not (null reqClash)+ = Left $ "Name clash detected: " ++ show reqClash++ | otherwise+ = Right spec++ where++ -- Sets containing name clashes+ ivnClash = internalVariableNames'+ `intersect` (externalVariableNames' `union` requirementNames')++ evnClash = externalVariableNames'+ `intersect` (internalVariableNames' `union` requirementNames')++ reqClash = requirementNames'+ `intersect` (internalVariableNames'+ `union` externalVariableNames')++ -- Names used.+ internalVariableNames' = map snd internalVariableMap+ externalVariableNames' = map snd externalVariableMap+ requirementNames' = map snd requirementNameMap++ -- 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++ -- Variable/requirement names used in the component spec.+ internalVariableNames = map internalVariableName+ $ internalVariables spec++ externalVariableNames = map externalVariableName+ $ externalVariables spec++ requirementNames = map requirementName+ $ requirements spec++-- * 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