diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,32 @@ # Revision history for ogma-core +## [1.14.0] - 2026-05-21 + +* Version bump (1.14.0) (#425). +* Bump upper version constraints on Copilot packages (#377). +* Lower upper version bound on `megaparsec` (#380). +* Bump upper version constraint on Quickcheck (#382). +* Adjust `Common.Diagram` module to use `Command.Common.ExprPair` (#384). +* Add support for reading diagrams to overview command (#386). +* Augment overview command to formally analyze diagrams (#388). +* Move functions related to `Either` type to dedicated module (#391). +* Move function related to JSON objects to dedicated module (#393). +* Move definitions related to `ExprPair` type to dedicated module (#395). +* Move functions related to Copilot specs to dedicated modules (#397). +* Rename module to more accurately reflect intent (#399). +* Move auxiliary function into new auxiliary module (#401). +* Split `Command.CommonDiagram` into smaller, more cohesive modules (#403). +* Simplify internal definition `showTransitions` (#405). +* Add diagram query functions to `Data.Diagram` (#407). +* Factorize translation of diagrams to Copilot into separate module (#409). +* Remove unnecessary arguments in code generated by diagram backend (#411). +* Move functions related to reading specs to dedicated module (#413). +* Make standalone, app backends support working directly with diagrams (#415). +* Add support for reading specs from YAML files (#417). +* Fix order of arguments in calls to internal function (#419). +* Adjust standalone, app backends to support multiple input specs (#421). +* Introduce report command (#423). + ## [1.13.0] - 2026-03-21 * Version bump (1.13.0) (#373). diff --git a/ogma-core.cabal b/ogma-core.cabal --- a/ogma-core.cabal +++ b/ogma-core.cabal @@ -19,7 +19,7 @@ build-type: Simple name: ogma-core -version: 1.13.0 +version: 1.14.0 homepage: https://github.com/nasa/ogma bug-reports: https://github.com/nasa/ogma/issues license: Apache-2.0 @@ -73,6 +73,7 @@ templates/fprime/Copilot.hpp templates/fprime/Dockerfile templates/fprime/instance-copilot + templates/report/Report.md templates/standalone/Copilot.hs data/formats/fcs_smv data/formats/fcs_lustre @@ -105,6 +106,7 @@ Command.Diagram Command.FPrimeApp Command.Overview + Command.Report Command.Result Command.ROSApp Command.Standalone @@ -114,6 +116,7 @@ Language.Trans.CStruct2CopilotStruct Language.Trans.CStructs2Copilot Language.Trans.CStructs2MsgHandlers + Language.Trans.Diagram2Copilot Language.Trans.Lustre2Copilot Language.Trans.Spec2Copilot Language.Trans.SMV2Copilot @@ -123,7 +126,20 @@ Command.Common Command.Errors Command.VariableDB - Language.Trans.SpecAnalysis + Copilot.Core.Analysis + Copilot.Language.Reify.Extra + Data.Aeson.Extra + Data.Diagram + Data.Diagram.Analysis + Data.Diagram.Parser + Data.Diagram.Parser.Dot + Data.Diagram.Parser.Mermaid + Data.Either.Extra + Data.ExprPair + Data.Spec.Analysis + Data.Spec.Extra + Data.Spec.Parser + Language.YAMLSpec.Parser autogen-modules: Paths_ogma_core @@ -133,28 +149,30 @@ , aeson >= 2.0.0.0 && < 2.3 , bytestring >= 0.10.8.2 && < 0.13 , containers >= 0.5 && < 0.8 - , copilot-core >= 4.6.1 && < 4.7 - , copilot-language >= 4.6.1 && < 4.7 - , copilot-theorem >= 4.6.1 && < 4.7 + , copilot-core >= 4.6.1 && < 4.8 + , copilot-language >= 4.6.1 && < 4.8 + , copilot-theorem >= 4.6.1 && < 4.8 , directory >= 1.3.1.5 && < 1.4 , filepath >= 1.4.2 && < 1.6 , graphviz >= 2999.20 && < 2999.21 , hint >= 0.9.0 && < 1.10 - , megaparsec >= 8.0.0 && < 9.10 + , megaparsec >= 8.0.0 && < 9.8 , mtl >= 2.2.2 && < 2.4 , process >= 1.6 && < 1.7 , text >= 1.2.3.1 && < 2.2 + , vector >= 0.12.0.1 && < 0.14 + , yaml >= 0.11.7.0 && < 0.12 - , ogma-extra >= 1.13.0 && < 1.14 - , ogma-language-c >= 1.13.0 && < 1.14 - , ogma-language-copilot >= 1.13.0 && < 1.14 - , ogma-language-csv >= 1.13.0 && < 1.14 - , ogma-language-jsonspec >= 1.13.0 && < 1.14 - , ogma-language-lustre >= 1.13.0 && < 1.14 - , ogma-language-smv >= 1.13.0 && < 1.14 - , ogma-language-xlsx >= 1.13.0 && < 1.14 - , ogma-language-xmlspec >= 1.13.0 && < 1.14 - , ogma-spec >= 1.13.0 && < 1.14 + , ogma-extra >= 1.14.0 && < 1.15 + , ogma-language-c >= 1.14.0 && < 1.15 + , ogma-language-copilot >= 1.14.0 && < 1.15 + , ogma-language-csv >= 1.14.0 && < 1.15 + , ogma-language-jsonspec >= 1.14.0 && < 1.15 + , ogma-language-lustre >= 1.14.0 && < 1.15 + , ogma-language-smv >= 1.14.0 && < 1.15 + , ogma-language-xlsx >= 1.14.0 && < 1.15 + , ogma-language-xmlspec >= 1.14.0 && < 1.15 + , ogma-spec >= 1.14.0 && < 1.15 hs-source-dirs: src @@ -176,7 +194,7 @@ base >= 4.11.0.0 && < 5 , directory >= 1.3.1.5 && < 1.4 , HUnit >= 1.2.0.0 && < 1.7 - , QuickCheck >= 2.8.2 && < 2.16 + , QuickCheck >= 2.8.2 && < 2.17 , test-framework >= 0.8.2 && < 0.9 , test-framework-hunit >= 0.2.0 && < 0.4 , test-framework-quickcheck2 >= 0.3.0.4 && < 0.4 diff --git a/src/Command/CFSApp.hs b/src/Command/CFSApp.hs --- a/src/Command/CFSApp.hs +++ b/src/Command/CFSApp.hs @@ -59,6 +59,10 @@ import Command.VariableDB (Connection (..), TopicDef (..), TypeDef (..), VariableDB, findConnection, findInput, findTopic, findType, findTypeByType) +import Data.Aeson.Extra (mergeObjects) +import Data.ExprPair (ExprPair(..), exprPair) +import Data.Location (Location (..)) +import Data.Spec.Parser (readInputExpr) -- | Generate a new CFS application connected to Copilot. command :: CommandOptions @@ -93,20 +97,24 @@ rs <- parseRequirementsListFile handlersFile varDB <- openVarDBFilesWithDefault varDBFile - specT <- maybe (return Nothing) (\e -> Just <$> parseInputExpr' e) cExpr - specF <- maybe (return Nothing) (\f -> Just <$> parseInputFile' f) fp + specT <- maybe (return Nothing) (\e -> Just . InputFileSpec <$> readInputExpr' e) cExpr + specF <- if null fpA + then return Nothing + else do + fpA' <- mapM readInputFile' fpA + let fpA'' = combineInputFiles fpA' + if length fpA'' > 1 + then liftEither $ Left commandMultipleInputTypes + else pure $ Just $ head fpA'' let spec = specT <|> specF liftEither $ checkArguments spec vs rs - copilotM <- sequenceA $ (\spec' -> processSpec spec' fp cExpr) <$> spec + copilotM <- sequenceA $ (\spec' -> processSpec spec' cExpr fpA) <$> spec - let varNames = fromMaybe (specExtractExternalVariables spec) vs - monitors = maybe - (specExtractHandlers spec) - (map (\x -> (x, Nothing))) - rs + let varNames = fromMaybe (defaultVarNames spec) vs + monitors = maybe (defaultMonitors spec) (map (\x -> (x, Nothing))) rs let appData = commandLogic varDB varNames monitors' copilotM monitors' = mapMaybe (monitorMap varDB) monitors @@ -116,7 +124,7 @@ where cExpr = commandConditionExpr options - fp = commandInputFile options + fpA = commandInputFiles options varNameFile = commandVariables options varDBFile = maybeToList $ commandVariableDB options handlersFile = commandHandlers options @@ -124,15 +132,26 @@ propFormatName = commandPropFormat options propVia = commandPropVia options - parseInputExpr' e = - parseInputExpr e propFormatName propVia exprT + readInputExpr' e = + readInputExpr e propFormatName propVia exprT - parseInputFile' f = + readInputFile' f = parseInputFile f formatName propFormatName propVia exprT processSpec spec' expr' fp' = Command.Standalone.commandLogic expr' fp' "copilot" [] exprT spec' + defaultVarNames spec = case spec of + Just (InputFileSpec spec') -> specExtractExternalVariables (Just spec') + Just (InputFileDiagram _) -> [] + Nothing -> specExtractExternalVariables Nothing + + + defaultMonitors spec = case spec of + Just (InputFileSpec spec') -> specExtractHandlers (Just spec') + Just (InputFileDiagram _) -> [ ("handler", Just "uint8_t" ) ] + Nothing -> specExtractHandlers Nothing + -- | Generate a variable substitution map for a cFS application. commandLogic :: VariableDB -> [String] @@ -158,7 +177,7 @@ -- applications. data CommandOptions = CommandOptions { commandConditionExpr :: Maybe String -- ^ Trigger condition. - , commandInputFile :: Maybe FilePath -- ^ Input specification file. + , commandInputFiles :: [FilePath] -- ^ Input specification files. , commandTargetDir :: FilePath -- ^ Target directory where the -- application should be created. , commandTemplateDir :: Maybe FilePath -- ^ Directory where the template is @@ -280,3 +299,15 @@ instance ToJSON AppData +-- | Error message associated to having multiple input files of incompatible +-- types. +commandMultipleInputTypes :: ErrorTriplet +commandMultipleInputTypes = + ErrorTriplet ecMultipleInputTypes msg LocationNothing + where + msg = + "Too many inputs provided. Provide one diagram or multiple specs." + +-- | Error: multiple inputs of incompatible types. +ecMultipleInputTypes :: ErrorCode +ecMultipleInputTypes = 1 diff --git a/src/Command/Common.hs b/src/Command/Common.hs --- a/src/Command/Common.hs +++ b/src/Command/Common.hs @@ -21,7 +21,8 @@ -- -- | Shared functions across multiple backends. module Command.Common - ( parseInputExpr + ( InputFile(..) + , combineInputFiles , parseInputFile , parseVariablesFile , parseRequirementsListFile @@ -31,13 +32,9 @@ , checkArguments , specExtractExternalVariables , specExtractHandlers - , ExprPair(..) - , ExprPairT(..) - , exprPair , processResult , cannotCopyTemplate , makeLeftE - , mergeObjects , locateTemplateDir ) where @@ -48,144 +45,100 @@ import Control.Monad.IO.Class (liftIO) import Data.Aeson (Value (Null, Object), eitherDecode, eitherDecodeFileStrict, object) -import Data.Aeson.KeyMap (union) -import qualified Data.ByteString.Lazy as L -import Data.List (isInfixOf, isPrefixOf) -import System.Directory (doesFileExist) import System.FilePath (()) -import System.Process (readProcess) -- External imports: auxiliary import Data.ByteString.Extra as B (safeReadFile) import Data.String.Extra (sanitizeLCIdentifier, sanitizeUCIdentifier) -- External imports: ogma -import Data.OgmaSpec (Requirement (..), Spec (..), - externalVariableName, externalVariables, - requirementName, requirementResultType, - requirements) -import Language.CSVSpec.Parser (parseCSVSpec) -import Language.JSONSpec.Parser (parseJSONSpec) -import Language.XLSXSpec.Parser (parseXLSXSpec) -import Language.XMLSpec.Parser (parseXMLSpec) - --- External imports: language ASTs, transformers -import qualified Language.Lustre.AbsLustre as Lustre -import qualified Language.Lustre.ParLustre as Lustre (myLexer, pBoolSpec) - -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.Lustre2Copilot as Lustre (boolSpec2Copilot, - boolSpecNames) -import Language.Trans.SMV2Copilot as SMV (boolSpec2Copilot, - boolSpecNames) +import Data.OgmaSpec (Requirement (..), Spec (..), externalVariableName, + externalVariables, requirementName, requirementResultType, + requirements) -- Internal imports: VariableDBs import Command.VariableDB (VariableDB, emptyVariableDB, mergeVariableDB) -- Internal imports: auxiliary -import Command.Errors (ErrorTriplet(..), ErrorCode) -import Command.Result (Result (..)) -import Data.Location (Location (..)) -import Paths_ogma_core (getDataDir) +import Command.Errors (ErrorTriplet(..), ErrorCode) +import Command.Result (Result (..)) +import Data.Diagram (Diagram) +import Data.Diagram.Parser (DiagramFormat (..), readDiagram) +import Data.Either.Extra (makeLeft) +import Data.ExprPair (ExprPair (..), ExprPairT (..)) +import Data.Location (Location (..)) +import Data.Spec.Parser (readInputFile) +import Paths_ogma_core (getDataDir) --- | Process input specification from a single expression and return its --- abstract representation. -parseInputExpr :: String - -> String - -> Maybe String - -> ExprPairT a - -> ExceptT ErrorTriplet IO (Spec a) -parseInputExpr expr propFormatName propVia exprT = - ExceptT $ do - let ExprPairT parse replace print ids def = exprT +-- | File containing information to be processed by Ogma (e.g., specification, +-- diagram). +data InputFile a = InputFileDiagram Diagram + | InputFileSpec (Spec a) - let wrapper = wrapVia propVia parse +-- | Merge a list of input files into a smaller list of input files. +-- +-- PRE: If there is more than one input file, all input files are specs. +combineInputFiles :: [InputFile a] -> [InputFile a] +combineInputFiles [] = [] +combineInputFiles [x] = [x] +combineInputFiles xs + | any isInputDiagram xs + = [] - result <- wrapper expr + | otherwise + = [ InputFileSpec $ foldr1 mergeSpecs $ map getSpec xs ] - let spec = do - expr' <- result - let req = Requirement "triggerCondition" expr' "" Nothing Nothing - return $ Spec [] [] [ req ] + where - case spec of - Left e -> return $ Left $ cannotReadConditionExpr expr e - Right s -> return $ Right s + -- True if the given argument is a diagram. + isInputDiagram :: InputFile a -> Bool + isInputDiagram (InputFileDiagram _) = True + isInputDiagram _ = False --- | Process input specification, if available, and return its abstract --- representation. + -- Merge two specifications. + mergeSpecs :: Spec a -> Spec a -> Spec a + mergeSpecs s1 s2 = Spec + { internalVariables = internalVariables s1 ++ internalVariables s2 + , externalVariables = externalVariables s2 ++ externalVariables s2 + , requirements = requirements s1 ++ requirements s2 + } + + -- Unsafely unwrap the spec in an input file. + -- + -- PRE: The argument input file contains a spec. + getSpec :: InputFile a -> Spec a + getSpec (InputFileSpec s) = s + getSpec _ = error "The input file provided is not a spec" + +-- | Process input file, it contains a valid diagram or specification, and +-- return its abstract representation. parseInputFile :: FilePath -> String -> String -> Maybe String -> ExprPairT a - -> ExceptT ErrorTriplet IO (Spec a) -parseInputFile fp formatName propFormatName propVia exprT = - ExceptT $ do - let ExprPairT parse replace print ids def = exprT + -> ExceptT ErrorTriplet IO (InputFile a) +parseInputFile fp formatName propFormatName propVia exprT + | isDiagramFormat formatName + = InputFileDiagram <$> + readDiagram fp diagramFormat (ExprPair exprT) - let wrapper = wrapVia propVia parse - -- Obtain format file. - -- - -- A format name that exists as a file in the disk always takes preference - -- over a file format included with Ogma. A file format with a forward - -- slash in the name is always assumed to be a user-provided filename. - -- Regardless of whether the file is user-provided or known to Ogma, we - -- check (again) whether the file exists, and print an error message if - -- not. - exists <- doesFileExist formatName - dataDir <- getDataDir - let formatFile - | isInfixOf "/" formatName || exists - = formatName - | otherwise - = dataDir "data" "formats" - (formatName ++ "_" ++ propFormatName) - formatMissing <- not <$> doesFileExist formatFile + | otherwise + = InputFileSpec <$> + readInputFile fp formatName propFormatName propVia exprT - if formatMissing - then return $ Left $ commandIncorrectFormatSpec formatFile - else do - res <- do - format <- readFile formatFile + where - -- 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. - if | isPrefixOf "XMLFormat" format - -> do let xmlFormat = read format - content <- readFile fp - parseXMLSpec - (wrapper) (def) xmlFormat content - -- (fmap (fmap print) . wrapper) (print def) xmlFormat content - | isPrefixOf "CSVFormat" format - -> do let csvFormat = read format - content <- readFile fp - parseCSVSpec wrapper def csvFormat content - | isPrefixOf "XLSXFormat" format - -> do let xlsxFormat = read format - content <- L.readFile fp - parseXLSXSpec wrapper def xlsxFormat content - | otherwise - -> do let jsonFormat = read format - content <- B.safeReadFile fp - case content of - Left e -> return $ Left e - Right b -> do case eitherDecode b of - Left e -> return $ Left e - Right v -> - parseJSONSpec - (wrapper) - jsonFormat - v - case res of - Left e -> return $ Left $ cannotOpenInputFile fp - Right x -> return $ Right x + isDiagramFormat :: String -> Bool + isDiagramFormat fName = fName `elem` [ "dot", "mermaid" ] + diagramFormat :: DiagramFormat + diagramFormat + | formatName == "dot" = Dot + | formatName == "mermaid" = Mermaid + | otherwise = error $ + "diagramFormat: Not a diagram format " ++ show formatName + -- | Process a variable selection file, if available, and return the variable -- names. parseVariablesFile :: Maybe FilePath @@ -224,7 +177,7 @@ -> ExceptT ErrorTriplet IO VariableDB parseVarDBFile Nothing = return emptyVariableDB parseVarDBFile (Just fn) = - ExceptT $ makeLeftE' (cannotOpenDB fn) <$> + ExceptT $ makeLeft (cannotOpenDB fn) <$> eitherDecodeFileStrict fn -- | Read a list of variable DBs, as well as the default variable DB. @@ -260,7 +213,7 @@ -- -- If an input file is not provided, then the user must provide BOTH a variable -- list, and a list of handlers. -checkArguments :: Maybe (Spec a) +checkArguments :: Maybe (InputFile a) -> Maybe [String] -> Maybe [String] -> Either ErrorTriplet () @@ -290,53 +243,6 @@ handlerNameF = ("handler" ++) . sanitizeUCIdentifier --- * Handler for boolean expressions - --- | Handler for boolean expressions that knows how to parse them, replace --- variables in them, and convert them to Copilot. --- --- It also contains a default value to be used whenever an expression cannot be --- found in the input file. -data ExprPair = forall a . ExprPair - { exprTPair :: ExprPairT a - } - -data ExprPairT a = ExprPairT - { exprTParse :: String -> Either String a - , exprTReplace :: [(String, String)] -> a -> a - , exprTPrint :: a -> String - , exprTIdents :: a -> [String] - , exprTUnknown :: a - } - - --- | Return a handler depending on whether it should be for Lustre boolean --- expressions or for SMV boolean expressions. We default to SMV if not format --- is given. -exprPair :: String -> ExprPair -exprPair "lustre" = ExprPair $ - ExprPairT - (Lustre.pBoolSpec . Lustre.myLexer) - (\_ -> id) - (Lustre.boolSpec2Copilot) - (Lustre.boolSpecNames) - (Lustre.BoolSpecSignal (Lustre.Ident "undefined")) -exprPair "literal" = ExprPair $ - ExprPairT - Right - (\_ -> id) - id - (const []) - "undefined" -exprPair "cocospec" = exprPair "lustre" -exprPair _ = ExprPair $ - ExprPairT - (SMV.pBoolSpec . SMV.myLexer) - (substituteBoolExpr) - (SMV.boolSpec2Copilot) - (SMV.boolSpecNames) - (SMV.BoolSpecSignal (SMV.Ident "undefined")) - -- * Errors -- | Process a computation that can fail with an error code, and turn it into a @@ -361,25 +267,6 @@ "the arguments provided are insufficient: you must provide an input " ++ "specification, or both a variables and a handlers file." --- | Exception handler to deal with the case in which the trigger expression --- cannot be understood. -cannotReadConditionExpr :: String -> String -> ErrorTriplet -cannotReadConditionExpr expr errorMsg = - ErrorTriplet ecCannotReadConditionExpr msg LocationNothing - where - msg = - "cannot parse condition or trigger expression " ++ show expr ++ ":" - ++ errorMsg - --- | Exception handler to deal with the case in which the input file cannot be --- opened. -cannotOpenInputFile :: FilePath -> ErrorTriplet -cannotOpenInputFile file = - ErrorTriplet ecCannotOpenInputFile msg (LocationFile file) - where - msg = - "cannot open input specification file " ++ file - -- | Exception handler to deal with the case in which the variable DB cannot be -- opened. cannotOpenDB :: FilePath -> ErrorTriplet @@ -407,15 +294,6 @@ msg = "cannot open handlers file " ++ file --- | Error message associated to the format file not being found. -commandIncorrectFormatSpec :: FilePath -> ErrorTriplet -commandIncorrectFormatSpec formatFile = - ErrorTriplet ecIncorrectFormatFile msg (LocationFile formatFile) - where - msg = - "The format specification " ++ formatFile ++ " does not exist or is not " - ++ "readable" - -- | Exception handler to deal with the case in which the template vars file -- cannot be opened. cannotOpenTemplateVars :: FilePath -> ErrorTriplet @@ -451,14 +329,6 @@ ecWrongArguments :: ErrorCode ecWrongArguments = 1 --- | Error: the trigger expression provided by the user cannot be parsed. -ecCannotReadConditionExpr :: ErrorCode -ecCannotReadConditionExpr = 1 - --- | Error: the input specification provided by the user cannot be opened. -ecCannotOpenInputFile :: ErrorCode -ecCannotOpenInputFile = 1 - -- | Error: the variable DB provided by the user cannot be opened. ecCannotOpenDBFile :: ErrorCode ecCannotOpenDBFile = 1 @@ -471,10 +341,6 @@ ecCannotOpenHandlersFile :: ErrorCode ecCannotOpenHandlersFile = 1 --- | Error: the format file cannot be opened. -ecIncorrectFormatFile :: ErrorCode -ecIncorrectFormatFile = 1 - -- | Error: the template vars file provided by the user cannot be opened. ecCannotOpenTemplateVarsFile :: ErrorCode ecCannotOpenTemplateVarsFile = 1 @@ -501,37 +367,6 @@ dataDir <- getDataDir return $ dataDir "templates" name --- | Parse a property using an auxiliary program to first translate it, if --- available. --- --- If a program is given, it is first called on the property, and then the --- result is parsed with the parser passed as an argument. If a program is not --- given, then the parser is applied to the given string. -wrapVia :: Maybe String -- ^ Auxiliary program to translate the - -- property. - -> (String -> Either String a) -- ^ Parser used on the result. - -> String -- ^ Property to parse. - -> IO (Either String a) -wrapVia Nothing parse s = return (parse s) -wrapVia (Just f) parse s = - E.handle (\(e :: E.IOException) -> return $ Left $ show e) $ do - out <- readProcess f [] s - return $ parse out - --- | Merge two JSON objects. --- --- Fails if the values are not objects or null. -mergeObjects :: Value -> Value -> Value -mergeObjects (Object m1) (Object m2) = Object (union m1 m2) -mergeObjects obj Null = obj -mergeObjects Null obj = obj -mergeObjects _ _ = error "The values passed are not objects" - -- | Replace the left Exception in an Either. makeLeftE :: c -> Either E.SomeException b -> Either c b -makeLeftE = makeLeftE' - --- | Replace the left value in an @Either@. -makeLeftE' :: c -> Either a b -> Either c b -makeLeftE' c (Left _) = Left c -makeLeftE' _ (Right x) = Right x +makeLeftE = makeLeft diff --git a/src/Command/Diagram.hs b/src/Command/Diagram.hs --- a/src/Command/Diagram.hs +++ b/src/Command/Diagram.hs @@ -30,61 +30,38 @@ where -- External imports -import Control.Exception as E -import Control.Monad (when, void) -import Data.Aeson (object, (.=)) -import Data.ByteString.Lazy (toStrict) -import qualified Data.ByteString.Lazy as B -import Data.Either (isLeft) -import Data.Foldable (for_) -import Data.Functor.Identity (Identity) -import Data.GraphViz (graphEdges) -import qualified Data.GraphViz as G -import qualified Data.GraphViz.Attributes.Complete as Attributes -import Data.GraphViz.Commands.IO (toUTF8) -import qualified Data.GraphViz.Parsing as G -import Data.GraphViz.PreProcessing (preProcess) -import qualified Data.GraphViz.Types.Generalised as Gs -import Data.List (intercalate, nub, sort) -import qualified Data.Set as Set -import Data.Text (Text) -import qualified Data.Text as T -import qualified Data.Text.Encoding as T -import Data.Text.Lazy (pack) -import qualified Data.Text.Lazy as LT -import Data.Void (Void) -import System.FilePath (()) -import Text.Megaparsec (ErrorFancy (ErrorFail), - ParsecT, choice, empty, - errorBundlePretty, - fancyFailure, many, - manyTill, noneOf, parse, - (<|>)) -import Text.Megaparsec.Char (alphaNumChar, char, - digitChar, newline, space1, - string) -import qualified Text.Megaparsec.Char.Lexer as L - +import Control.Exception as E +import Control.Monad.Except (runExceptT) +import Data.Aeson (object, (.=)) +import Data.Foldable (for_) +import Data.Text.Lazy (pack) +import System.FilePath (()) -- External imports: auxiliary -import Data.ByteString.Extra as B ( safeReadFile ) import System.Directory.Extra ( copyTemplate ) -- External imports: parsing expressions. +import qualified Language.Lustre.AbsLustre as Lustre import qualified Language.Lustre.ParLustre as Lustre (myLexer, pBoolSpec) +import qualified Language.SMV.AbsSMV as SMV import qualified Language.SMV.ParSMV as SMV (myLexer, pBoolSpec) -- Internal imports: auxiliary -import Command.Result (Result (..)) -import Data.Location (Location (..)) -import Paths_ogma_core (getDataDir) +import Command.Errors (ErrorTriplet (..)) +import Command.Result (Result (..)) +import Data.Diagram.Parser (DiagramFormat (..), readDiagram) +import Data.ExprPair (ExprPair (..), ExprPairT (..)) +import Data.Location (Location (..)) +import Paths_ogma_core (getDataDir) -- Internal imports: language ASTs, transformers -import Language.SMV.Substitution (substituteBoolExpr) -import qualified Language.Trans.Lustre2Copilot as Lustre (boolSpec2Copilot, - boolSpecNames) -import Language.Trans.SMV2Copilot as SMV (boolSpec2Copilot, - boolSpecNames) +import Language.SMV.Substitution (substituteBoolExpr) +import Language.Trans.Diagram2Copilot (DiagramMode (..), + diagram2CopilotSpec) +import qualified Language.Trans.Lustre2Copilot as Lustre (boolSpec2Copilot, + boolSpecNames) +import Language.Trans.SMV2Copilot as SMV (boolSpec2Copilot, + boolSpecNames) -- | Generate a new Copilot monitor that implements a state machine described -- in a diagram given as an input file. @@ -111,13 +88,13 @@ let (mOutput, result) = diagramResult fp copilotSpecElems -- If the result is success, expand the template. - for_ mOutput $ \(streamDefs, handlerInputs) -> do + for_ mOutput $ \(streamDefs, triggers) -> do let subst = object - [ "streamDefs" .= pack streamDefs - , "specName" .= pack (diagramFilename options) - , "input" .= pack (diagramInputVar options) - , "state" .= pack (diagramStateVar options) - , "handlerInputs" .= pack handlerInputs + [ "streamDefs" .= pack streamDefs + , "specName" .= pack (diagramFilename options) + , "input" .= pack (diagramInputVar options) + , "state" .= pack (diagramStateVar options) + , "triggers" .= pack triggers ] templateDir <- case diagramTemplateDir options of @@ -147,17 +124,11 @@ -> ExprPair -> IO (Either String (String, String)) diagram' fp options exprP = do - contentEither <- B.safeReadFile fp - return $ 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. - diagFileContent <- contentEither - - -- Abtract representation of a state machine diagram. - diagramR <- parseDiagram (diagramFormat options) diagFileContent exprP - - return $ diagramToCopilot diagramR (diagramMode options) + diagramE <- runExceptT $ readDiagram fp (diagramFormat options) exprP + case diagramE of + Left (ErrorTriplet _ec msg _loc) -> pure $ Left msg + Right diagramR -> + pure $ Right $ diagram2CopilotSpec diagramR (diagramMode options) -- | Options used to customize the conversion of diagrams to Copilot code. data DiagramOptions = DiagramOptions @@ -171,18 +142,6 @@ , diagramInputVar :: String } --- | Modes of operation. -data DiagramMode = CheckState -- ^ Check if given state matches expectation - | ComputeState -- ^ Compute expected state - | CheckMoves -- ^ Check if transitioning to a state would be - -- possible. - deriving (Eq, Show) - --- | Diagram formats supported. -data DiagramFormat = Mermaid - | Dot - deriving (Eq, Show) - -- | Property formats supported. data DiagramPropFormat = Lustre | Inputs @@ -232,300 +191,36 @@ -- * Handler for boolean expressions in edges or transitions between states. --- | Handler for boolean expressions that knows how to parse them, replace --- variables in them, and convert them to Copilot. -data ExprPair = forall a . ExprPair - { _exprParse :: String -> Either String a - , _exprReplace :: [(String, String)] -> a -> a - , _exprPrint :: a -> String - , _exprIdents :: a -> [String] - } - -- | Return a handler depending on the format used for edge or transition -- properties. exprPair :: DiagramPropFormat -> ExprPair -exprPair Lustre = ExprPair (Lustre.pBoolSpec . Lustre.myLexer) - (\_ -> id) - Lustre.boolSpec2Copilot - Lustre.boolSpecNames -exprPair Inputs = ExprPair ((Right . read) :: String -> Either String Int) - (\_ -> id) - (\x -> "input == " ++ show x) - (const []) -exprPair Literal = ExprPair Right - (\_ -> id) - id - (const []) -exprPair SMV = ExprPair (SMV.pBoolSpec . SMV.myLexer) - substituteBoolExpr - SMV.boolSpec2Copilot - SMV.boolSpecNames - --- | Parse and print a value using an auxiliary Expression Pair. --- --- Fails if the value has no valid parse. -exprPairShow :: ExprPair -> String -> String -exprPairShow (ExprPair parseProp _replace printProp _ids) = - printProp . fromRight' . parseProp - --- * Diagrams - --- | Internal representation for diagrams. -newtype Diagram = Diagram - { diagramTransitions :: [(Int, String, Int)] - } - deriving (Show, Eq) - --- * Diagram parsers - --- | Generic function to parse a diagram. -parseDiagram :: DiagramFormat -- ^ Format of the input file - -> B.ByteString -- ^ Contents of the diagram - -> ExprPair -- ^ Subparser for conditions or edge - -- expressions - -> Either String Diagram -parseDiagram Dot = parseDiagramDot -parseDiagram Mermaid = parseDiagramMermaid - --- ** Dot parser - --- | Parse a DOT / Graphviz diagram. -parseDiagramDot :: B.ByteString -> ExprPair -> Either String Diagram -parseDiagramDot contents exprP = do - let contentsUTF8 = toUTF8 contents - dg <- fst $ G.runParser G.parse $ preProcess contentsUTF8 - return $ makeDiagram dg - where - makeDiagram :: Gs.DotGraph LT.Text -> Diagram - makeDiagram g = Diagram links - where - links = map edgeToLink (graphEdges g) - - edgeToLink edge = - ( read (LT.unpack o) - , exprPairShow exprP (LT.unpack e) - , read (LT.unpack d) - ) - where - o = G.fromNode edge - d = G.toNode edge - e = getLabel (G.edgeAttributes edge) - - -- Extract the label from a list of attributes. If no label is - -- found, it's assumed that the condition is the literal true. - getLabel [] = "true" - getLabel ((Attributes.Label (Attributes.StrLabel l)) : _) = l - getLabel (_ : as) = getLabel as - --- ** Mermaid parser - --- | Parse a mermaid diagram. -parseDiagramMermaid :: B.ByteString -> ExprPair -> Either String Diagram -parseDiagramMermaid txtDia exprP = - case parsingResult of - Left e -> Left (errorBundlePretty e) - Right x -> Right x - where - txt = T.decodeUtf8 (toStrict txtDia) - parsingResult = parse (spaces *> pDiagram exprP) "" txt - --- | Type for parser for memaid diagrams. -type MermaidParser = ParsecT Void Text Identity - --- | Parser for mermaid diagrams. -pDiagram :: ExprPair -> MermaidParser Diagram -pDiagram exprP = - pGraphDiagram exprP - <|> pStateDiagram exprP - <|> pSequenceDiagram exprP - --- | Parser for a mermaid diagram. --- --- This parser depends on an auxiliary parser for the expressions associated to --- the edges or connections between states. -pGraphDiagram :: ExprPair -> MermaidParser Diagram -pGraphDiagram exprP = do - _ <- string "graph" <* spaces - _name <- T.pack <$> manyTill alphaNumChar (char ';') - _ <- newline - - transitions <- many (pGraphTransition exprP) - - pure $ Diagram transitions - --- | Parser for an edge in a state diagram. --- --- This parser depends on an auxiliary parser for the expressions associated to --- the edges or connections between states. -pGraphTransition :: ExprPair -> MermaidParser (Int, String, Int) -pGraphTransition ep@(ExprPair { _exprParse = parseProp }) = do - _ <- spaces - stateFrom <- many digitChar - _ <- string "-->|" - edge <- many (noneOf ("|" :: [Char])) - - let x = parseProp edge - when (isLeft x) $ fancyFailure $ Set.singleton $ - ErrorFail $ "Edge property has incorrect format: " ++ show edge - - _ <- char '|' - stateTo <- many digitChar - _ <- char ';' - _ <- newline - return (read stateFrom, exprPairShow ep edge, read stateTo) - --- | Parser for Mermaid diagrams of type stateDiagram-v2. -pStateDiagram :: ExprPair -> MermaidParser Diagram -pStateDiagram exprPair = do - _ <- string "stateDiagram-v2" <* spaces - - transitions <- many (pStateTransition exprPair) - - pure $ Diagram transitions - --- | Parser for transition label in stateDiagram-v2 mermaid diagram. -pStateTransition :: ExprPair -> MermaidParser (Int, String, Int) -pStateTransition ep@(ExprPair { _exprParse = parseProp }) = do - _ <- spaces - from <- read <$> many digitChar - _ <- spaces - string "-->" - _ <- spaces - to <- read <$> many digitChar - _ <- spaces - _ <- char ':' - _ <- spaces - edge <- many (noneOf ("\n" :: [Char])) - - let x = parseProp edge - when (isLeft x) $ fancyFailure $ Set.singleton $ - ErrorFail $ "Edge property has incorrect format: " ++ show edge - - _ <- newline - - pure $ (from, exprPairShow ep edge, to) - --- | Parser for Mermaid diagrams of type sequenceDiagram. -pSequenceDiagram :: ExprPair -> MermaidParser Diagram -pSequenceDiagram exprPair = do - spaces - _ <- string "sequenceDiagram" - spaces - - conditions <- many (pSequenceTransition exprPair) - let transitions = zipWith (\t idx -> (idx, t, idx + 1)) conditions [0..] - - pure $ Diagram transitions - --- | Parser for a connection, message or transition in a sequence diagram. --- --- This parser depends on an auxiliary parser for the expressions associated to --- the connections or messages between elements. -pSequenceTransition :: ExprPair -> MermaidParser String -pSequenceTransition ep@(ExprPair { _exprParse = parseProp }) = do - spaces - stateFrom <- many digitChar - spaces - pSequenceArrow - spaces - stateTo <- many digitChar - spaces - _ <- char ':' - spaces - edge <- many (noneOf ("\n" :: [Char])) - - let x = parseProp edge - when (isLeft x) $ fancyFailure $ Set.singleton $ - ErrorFail $ "Edge property has incorrect format: " ++ show edge - - _ <- newline - - pure (exprPairShow ep edge) - --- | Parser for arrow in sequence diagram. -pSequenceArrow :: MermaidParser () -pSequenceArrow = void $ choice - [ string "->>" - , string "-->>" - , string "-)" - ] - --- | Consume spaces -spaces :: MermaidParser () -spaces = L.space space1 empty empty +exprPair Lustre = ExprPair $ + ExprPairT + (Lustre.pBoolSpec . Lustre.myLexer) + (\_ -> id) + Lustre.boolSpec2Copilot + Lustre.boolSpecNames + (Lustre.BoolSpecSignal (Lustre.Ident "undefined")) +exprPair Inputs = ExprPair $ + ExprPairT + ((Right . read) :: String -> Either String Int) + (\_ -> id) + (\x -> "input == " ++ show x) + (const []) + (-1) +exprPair Literal = ExprPair $ + ExprPairT + Right + (\_ -> id) + id + (const []) + "undefined" +exprPair SMV = ExprPair $ + ExprPairT + (SMV.pBoolSpec . SMV.myLexer) + substituteBoolExpr + SMV.boolSpec2Copilot + SMV.boolSpecNames + (SMV.BoolSpecSignal (SMV.Ident "undefined")) -- * Backend - --- | Convert the diagram into a set of Copilot definitions, and a list of --- arguments for the top-level handler. -diagramToCopilot :: Diagram -> DiagramMode -> (String, String) -diagramToCopilot diag mode = (machine, arguments) - where - machine = unlines - [ "stateMachineProp :: Stream Bool" - , "stateMachineProp = " ++ propExpr - , "" - , "stateMachine1 :: Stream Word8" - , "stateMachine1 = stateMachineGF (initialState, finalState, noInput, " - ++ "transitions, badState)" - , "" - , "-- Check" - , "initialState :: Word8" - , "initialState = " ++ show initialState - , "" - , "-- Check" - , "finalState :: Word8" - , "finalState = " ++ show finalState - , "" - , "noInput :: Stream Bool" - , "noInput = false" - , "" - , "badState :: Word8" - , "badState = " ++ show badState - , "" - , "transitions = " ++ showTransitions - ] - - -- Elements of the spec. - propExpr = case mode of - CheckState -> "stateMachine1 /= externalState" - ComputeState -> "true" - CheckMoves -> "true" - initialState = minimum states - finalState = maximum states - badState = maximum states + 1 - - -- Arguments for the handler. - arguments = "[ " ++ intercalate ", " (map ("arg " ++) argExprs) ++ " ]" - - argExprs = case mode of - CheckState -> [ "stateMachine1", "externalState", "input" ] - ComputeState -> [ "stateMachine1", "externalState", "input" ] - CheckMoves -> map stateCheckExpr states - - stateCheckExpr stateId = - "(checkValidTransition transitions externalState " ++ show stateId ++ ")" - - -- States and transitions from the diagram. - transitions = diagramTransitions diag - states = nub $ sort $ concat [ [x, y] | (x, _, y) <- transitions ] - - showTransitions :: String - showTransitions = "[" ++ showTransitions' transitions - - showTransitions' :: [(Int, String, Int)] -> String - showTransitions' [] = "]" - showTransitions' (x1:x2:xs) = - showTransition x1 ++ ", " ++ showTransitions' (x2:xs) - showTransitions' (x2:[]) = showTransition x2 ++ "]" - - showTransition :: (Int, String, Int) -> String - showTransition (a, b, c) = - "(" ++ show a ++ ", " ++ b ++ ", " ++ show c ++ ")" - --- * Auxiliary functions - --- | Unsafe fromRight. Fails if the value is a 'Left'. -fromRight' :: Either a b -> b -fromRight' (Right v) = v -fromRight' _ = error "fromRight' applied to Left value." diff --git a/src/Command/FPrimeApp.hs b/src/Command/FPrimeApp.hs --- a/src/Command/FPrimeApp.hs +++ b/src/Command/FPrimeApp.hs @@ -53,6 +53,10 @@ import Command.Errors (ErrorCode, ErrorTriplet (..)) import Command.VariableDB (InputDef (..), TypeDef (..), VariableDB, findInput, findType, findTypeByType) +import Data.Aeson.Extra (mergeObjects) +import Data.ExprPair (ExprPair(..), exprPair) +import Data.Location (Location (..)) +import Data.Spec.Parser (readInputExpr) -- | Generate a new FPrime component connected to Copilot. command :: CommandOptions -- ^ Options to the ROS backend. @@ -87,20 +91,24 @@ rs <- parseRequirementsListFile handlersFile varDB <- openVarDBFilesWithDefault varDBFile - specT <- maybe (return Nothing) (\e -> Just <$> parseInputExpr' e) cExpr - specF <- maybe (return Nothing) (\f -> Just <$> parseInputFile' f) fp + specT <- maybe (return Nothing) (\e -> Just . InputFileSpec <$> readInputExpr' e) cExpr + specF <- if null fpA + then return Nothing + else do + fpA' <- mapM readInputFile' fpA + let fpA'' = combineInputFiles fpA' + if length fpA'' > 1 + then liftEither $ Left commandMultipleInputTypes + else pure $ Just $ head fpA'' let spec = specT <|> specF liftEither $ checkArguments spec vs rs - copilotM <- sequenceA $ (\spec' -> processSpec spec' fp cExpr) <$> spec + copilotM <- sequenceA $ (\spec' -> processSpec spec' cExpr fpA) <$> spec - let varNames = fromMaybe (specExtractExternalVariables spec) vs - monitors = maybe - (specExtractHandlers spec) - (map (\x -> (x, Nothing))) - rs + let varNames = fromMaybe (defaultVarNames spec) vs + monitors = maybe (defaultMonitors spec) (map (\x -> (x, Nothing))) rs let appData = AppData variables monitors' copilotM variables = mapMaybe (variableMap varDB) varNames @@ -111,7 +119,7 @@ where cExpr = commandConditionExpr options - fp = commandInputFile options + fpA = commandInputFiles options varNameFile = commandVariables options varDBFile = maybeToList $ commandVariableDB options handlersFile = commandHandlers options @@ -119,22 +127,33 @@ propFormatName = commandPropFormat options propVia = commandPropVia options - parseInputExpr' e = - parseInputExpr e propFormatName propVia exprT + readInputExpr' e = + readInputExpr e propFormatName propVia exprT - parseInputFile' f = + readInputFile' f = parseInputFile f formatName propFormatName propVia exprT processSpec spec' expr' fp' = Command.Standalone.commandLogic expr' fp' "copilot" [] exprT spec' + defaultVarNames spec = case spec of + Just (InputFileSpec spec') -> specExtractExternalVariables (Just spec') + Just (InputFileDiagram _) -> [] + Nothing -> specExtractExternalVariables Nothing + + + defaultMonitors spec = case spec of + Just (InputFileSpec spec') -> specExtractHandlers (Just spec') + Just (InputFileDiagram _) -> [ ("handler", Just "uint8_t" ) ] + Nothing -> specExtractHandlers Nothing + -- ** Argument processing -- | Options used to customize the conversion of specifications to F' -- applications. data CommandOptions = CommandOptions { commandConditionExpr :: Maybe String -- ^ Trigger condition. - , commandInputFile :: Maybe FilePath -- ^ Input specification file. + , commandInputFiles :: [FilePath] -- ^ Input specification files. , commandTargetDir :: FilePath -- ^ Target directory where the -- component should be created. , commandTemplateDir :: Maybe FilePath -- ^ Directory where the template is @@ -213,3 +232,16 @@ deriving (Generic) instance ToJSON AppData + +-- | Error message associated to having multiple input files of incompatible +-- types. +commandMultipleInputTypes :: ErrorTriplet +commandMultipleInputTypes = + ErrorTriplet ecMultipleInputTypes msg LocationNothing + where + msg = + "Too many inputs provided. Provide one diagram or multiple specs." + +-- | Error: multiple inputs of incompatible types. +ecMultipleInputTypes :: ErrorCode +ecMultipleInputTypes = 1 diff --git a/src/Command/Overview.hs b/src/Command/Overview.hs --- a/src/Command/Overview.hs +++ b/src/Command/Overview.hs @@ -31,20 +31,23 @@ -- External imports import Control.Monad.Except (runExceptT) import Data.Aeson (ToJSON (..)) -import Data.List (nub, (\\)) import GHC.Generics (Generic) -- External imports: Ogma -import Data.OgmaSpec (ExternalVariableDef (..), InternalVariableDef (..), - Requirement (..), Spec (..)) +import Data.OgmaSpec (Spec (..)) -- Internal imports -import Command.Common +import Command.Common (InputFile(..), parseInputFile) import Command.Errors (ErrorCode, ErrorTriplet (..)) import Command.Result (Result (..)) +import Data.Diagram.Analysis (AnalysisResult (..), + analyzeDiagram) +import Data.ExprPair (ExprPair(..), ExprPairT(..), + exprPair) import Data.Location (Location (..)) +import qualified Data.Spec.Analysis as SpecAnalysis +import Data.Spec.Extra (addMissingIdentifiers) import qualified Language.Trans.Spec2Copilot as Spec2Copilot -import qualified Language.Trans.SpecAnalysis as SpecAnalysis -- | Generate overview of a spec given in an input file. -- @@ -77,11 +80,19 @@ -> ExprPair -> IO (Either String CommandSummary) command' fp options (ExprPair exprT) = do - spec <- runExceptT $ parseInputFile' fp - case spec of - Left (ErrorTriplet _ec msg _loc) -> return $ Left msg + res <- runExceptT $ + parseInputFile fp formatName propFormatName propVia exprT + case res of + Left (ErrorTriplet _ s _) -> return $ Left s - Right spec' -> do + Right (InputFileDiagram diagramR) -> do + analysisResult <- analyzeDiagram diagramR + pure $ Right $ + CommandSummaryDiagram + (numStates analysisResult) + (deterministic analysisResult) + + Right (InputFileSpec spec') -> do let specCompleted = addMissingIdentifiers ids spec' specAnalyzed = Spec2Copilot.specAnalyze specCompleted @@ -97,26 +108,30 @@ consistent <- SpecAnalysis.consistent <$> specFormalAnalysis pure $ - CommandSummary + CommandSummaryRequirement numExterns numInternal numReqs numTrues numFalses consistent where - parseInputFile' f = parseInputFile f formatName propFormatName propVia exprT - formatName = commandFormat options - propFormatName = commandPropFormat options - propVia = commandPropVia options + formatName = commandFormat options + propFormatName = commandPropFormat options + propVia = commandPropVia options ExprPairT _parse replace printExpr ids _def = exprT -data CommandSummary = CommandSummary - { commandExternalVariables :: Int - , commandInternalVariables :: Int - , commandRequirements :: Int - , commandRequirementsTrue :: Int - , commandRequirementsFalse :: Int - , commandRequirementsConsistent :: Bool - } +data CommandSummary + = CommandSummaryRequirement + { commandExternalVariables :: Int + , commandInternalVariables :: Int + , commandRequirements :: Int + , commandRequirementsTrue :: Int + , commandRequirementsFalse :: Int + , commandRequirementsConsistent :: Bool + } + | CommandSummaryDiagram + { commandNumStates :: Int + , commandDeterministic :: Bool + } deriving (Generic, Show) instance ToJSON CommandSummary @@ -145,21 +160,3 @@ commandResult _options fp result = case result of Left msg -> (Nothing, Error ecOverviewError msg (LocationFile fp)) Right t -> (Just t, Success) - --- | 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 @@ -58,6 +58,10 @@ import Command.VariableDB (Connection (..), InputDef (..), TopicDef (..), TypeDef (..), VariableDB, findConnection, findInput, findTopic, findType, findTypeByType) +import Data.Aeson.Extra (mergeObjects) +import Data.ExprPair (ExprPair(..), exprPair) +import Data.Location (Location (..)) +import Data.Spec.Parser (readInputExpr) -- | Generate a new ROS application connected to Copilot. command :: CommandOptions -- ^ Options to the ROS backend. @@ -92,20 +96,24 @@ rs <- parseRequirementsListFile handlersFile varDB <- openVarDBFilesWithDefault varDBFile - specT <- maybe (return Nothing) (\e -> Just <$> parseInputExpr' e) cExpr - specF <- maybe (return Nothing) (\f -> Just <$> parseInputFile' f) fp + specT <- maybe (return Nothing) (\e -> Just . InputFileSpec <$> readInputExpr' e) cExpr + specF <- if null fpA + then return Nothing + else do + fpA' <- mapM readInputFile' fpA + let fpA'' = combineInputFiles fpA' + if length fpA'' > 1 + then liftEither $ Left commandMultipleInputTypes + else pure $ Just $ head fpA'' let spec = specT <|> specF liftEither $ checkArguments spec vs rs - copilotM <- sequenceA $ (\spec' -> processSpec spec' fp cExpr) <$> spec + copilotM <- sequenceA $ (\spec' -> processSpec spec' cExpr fpA) <$> spec - let varNames = fromMaybe (specExtractExternalVariables spec) vs - monitors = maybe - (specExtractHandlers spec) - (map (\x -> (x, Nothing))) - rs + let varNames = fromMaybe (defaultVarNames spec) vs + monitors = maybe (defaultMonitors spec) (map (\x -> (x, Nothing))) rs let appData = AppData variables monitors' copilotM testingAdditionalApps testingVars @@ -124,7 +132,7 @@ where cExpr = commandConditionExpr options - fp = commandInputFile options + fpA = commandInputFiles options varNameFile = commandVariables options varDBFile = maybeToList $ commandVariableDB options handlersFile = commandHandlers options @@ -132,15 +140,26 @@ propFormatName = commandPropFormat options propVia = commandPropVia options - parseInputExpr' e = - parseInputExpr e propFormatName propVia exprT + readInputExpr' e = + readInputExpr e propFormatName propVia exprT - parseInputFile' f = + readInputFile' f = parseInputFile f formatName propFormatName propVia exprT processSpec spec' expr' fp' = Command.Standalone.commandLogic expr' fp' "copilot" [] exprT spec' + defaultVarNames spec = case spec of + Just (InputFileSpec spec') -> specExtractExternalVariables (Just spec') + Just (InputFileDiagram _) -> [] + Nothing -> specExtractExternalVariables Nothing + + + defaultMonitors spec = case spec of + Just (InputFileSpec spec') -> specExtractHandlers (Just spec') + Just (InputFileDiagram _) -> [ ("handler", Just "uint8_t" ) ] + Nothing -> specExtractHandlers Nothing + testingAdditionalApps = commandTestingApps options testingLimitedVars = commandTestingVars options @@ -150,7 +169,7 @@ -- applications. data CommandOptions = CommandOptions { commandConditionExpr :: Maybe String -- ^ Trigger condition. - , commandInputFile :: Maybe FilePath -- ^ Input specification file. + , commandInputFiles :: [FilePath] -- ^ Input specification files. , commandTargetDir :: FilePath -- ^ Target directory where the -- application should be created. , commandTemplateDir :: Maybe FilePath -- ^ Directory where the template is @@ -269,3 +288,16 @@ "float" -> "randomFloat" "double" -> "randomFloat" def -> def + +-- | Error message associated to having multiple input files of incompatible +-- types. +commandMultipleInputTypes :: ErrorTriplet +commandMultipleInputTypes = + ErrorTriplet ecMultipleInputTypes msg LocationNothing + where + msg = + "Too many inputs provided. Provide one diagram or multiple specs." + +-- | Error: multiple inputs of incompatible types. +ecMultipleInputTypes :: ErrorCode +ecMultipleInputTypes = 1 diff --git a/src/Command/Report.hs b/src/Command/Report.hs new file mode 100644 --- /dev/null +++ b/src/Command/Report.hs @@ -0,0 +1,235 @@ +{-# LANGUAGE DeriveGeneric #-} +-- Copyright 2024 United States Government as represented by the Administrator +-- of the National Aeronautics and Space Administration. All Rights Reserved. +-- +-- Disclaimers +-- +-- Licensed under the Apache License, Version 2.0 (the "License"); you may +-- not use this file except in compliance with the License. You may obtain a +-- copy of the License at +-- +-- https://www.apache.org/licenses/LICENSE-2.0 +-- +-- Unless required by applicable law or agreed to in writing, software +-- distributed under the License is distributed on an "AS IS" BASIS, WITHOUT +-- WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the +-- License for the specific language governing permissions and limitations +-- under the License. +-- +-- | Produce a report of the diagrams and requirements in the input files. +module Command.Report + ( command + , CommandOptions(..) + , CommandSummary(..) + , ErrorCode + ) + where + +-- External imports +import qualified Control.Exception as E +import Control.Monad.Except (ExceptT (..), liftEither, withExceptT) +import Control.Monad.IO.Class (liftIO) +import Data.Aeson (ToJSON (..)) +import GHC.Generics (Generic) + +-- External imports: Ogma +import Data.OgmaSpec (Requirement (..), Spec (..)) +import Data.String.Extra (sanitizeUCIdentifier) +import System.Directory.Extra (copyTemplate) + +-- Internal imports +import Command.Common (InputFile (..), + cannotCopyTemplate, + locateTemplateDir, makeLeftE, + parseInputFile, processResult) +import Command.Errors (ErrorCode, ErrorTriplet (..)) +import Command.Result (Result (..)) +import Data.Diagram.Analysis (AnalysisResult (..), + analyzeDiagram) +import Data.ExprPair (ExprPair (..), ExprPairT (..), + exprPair) +import Data.Location (Location (..)) +import qualified Data.Spec.Analysis as SpecAnalysis +import Data.Spec.Extra (addMissingIdentifiers) +import qualified Language.Trans.Spec2Copilot as Spec2Copilot + +-- | Generate report of a spec or diagram given in an input file. +-- +-- PRE: The file given is readable, contains a valid file with recognizable +-- format, the formulas in the file do not use any identifiers that exist in +-- Copilot, or any of @prop@, @clock@, @ftp@, @notPreviousNot@. The template, +-- if provided, exists and uses the variables needed by the report application +-- generator. The target directory is writable and there's enough disk space to +-- copy the files over. +command :: CommandOptions -- ^ Customization options + -> IO (Result ErrorCode) +command options = processResult $ do + -- Obtain template dir + templateDir <- locateTemplateDir mTemplateDir "report" + + let functions = exprPair (commandPropFormat options) + + reportData <- command' options functions + + -- Expand template + ExceptT $ fmap (makeLeftE cannotCopyTemplate) $ E.try $ + copyTemplate templateDir (toJSON reportData) targetDir + + where + + targetDir = commandTargetDir options + mTemplateDir = commandTemplateDir options + +-- | Generate report of a spec or diagram given in an input file. +-- +-- PRE: The file given is readable, contains a valid file with recognizable +-- format, the formulas in the file do not use any identifiers that exist in +-- Copilot, or any of @prop@, @clock@, @ftp@, @notPreviousNot@. The template, +-- if provided, exists and uses the variables needed by the report application +-- generator. The target directory is writable and there's enough disk space to +-- copy the files over. +command' :: CommandOptions + -> ExprPair + -> ExceptT ErrorTriplet IO CommandSummary +command' options (ExprPair exprT) = do + res <- parseInputFile fp formatName propFormatName propVia exprT + case res of + InputFileDiagram diagramR -> do + analysisResult <- liftIO $ analyzeDiagram diagramR + let diagramDetails = DiagramDetails + (numStates analysisResult) + (deterministic analysisResult) + + pure $ CommandSummary + { commandExternalVariables = 0 + , commandInternalVariables = 0 + , commandRequirementsAny = False + , commandRequirements = 0 + , commandRequirementsTrue = 0 + , commandRequirementsFalse = 0 + , commandRequirementsConsistent = True + , commandRequirementList = [] + , commandDiagramsAny = True + , commandDiagrams = 1 + , commandDiagramList = [diagramDetails] + } + + InputFileSpec spec -> withExceptT commandCannotAnalyzeF $ do + let specCompleted = addMissingIdentifiers ids spec + specAnalyzed <- liftEither $ Spec2Copilot.specAnalyze specCompleted + + specFormalAnalysis <- ExceptT $ + SpecAnalysis.specAnalyze [] replace printExpr specCompleted + + let numExterns = length $ externalVariables specAnalyzed + numInternal = length $ internalVariables specAnalyzed + + numReqs = length reqList + reqList = requirements specAnalyzed + reqListDetails = map reqDetailsF reqList + reqDetailsF x = + RequirementDetails + (requirementName x) + (requirementDescription x) + (requirementNameAsProp (requirementName x) `elem` trueReqs) + (requirementNameAsProp (requirementName x) `elem` falseReqs) + + numTrues = SpecAnalysis.numAlwaysTrue specFormalAnalysis + numFalses = SpecAnalysis.numAlwaysFalse specFormalAnalysis + trueReqs = SpecAnalysis.alwaysTrueReq specFormalAnalysis + falseReqs = SpecAnalysis.alwaysFalseReq specFormalAnalysis + consistent = SpecAnalysis.consistent specFormalAnalysis + + pure $ CommandSummary + { commandExternalVariables = numExterns + , commandInternalVariables = numInternal + , commandRequirementsAny = numReqs > 0 + , commandRequirements = numReqs + , commandRequirementsTrue = numTrues + , commandRequirementsFalse = numFalses + , commandRequirementsConsistent = consistent + , commandRequirementList = reqListDetails + , commandDiagramsAny = False + , commandDiagrams = 0 + , commandDiagramList = [] + } + + where + + fp = commandInputFile options + formatName = commandFormat options + propFormatName = commandPropFormat options + propVia = commandPropVia options + + ExprPairT _parse replace printExpr ids _def = exprT + +-- | Options used to customize the interpretation of input specifications and +-- the resulting report. +data CommandOptions = CommandOptions + { commandTargetDir :: String + , commandTemplateDir :: Maybe String + , commandInputFile :: String + , commandFormat :: String + , commandPropFormat :: String + , commandPropVia :: Maybe String + } + +-- | Summary of the files read. +data CommandSummary = CommandSummary + { commandExternalVariables :: Int + , commandInternalVariables :: Int + , commandRequirementsAny :: Bool + , commandRequirements :: Int + , commandRequirementsTrue :: Int + , commandRequirementsFalse :: Int + , commandRequirementsConsistent :: Bool + , commandRequirementList :: [RequirementDetails] + , commandDiagramsAny :: Bool + , commandDiagrams :: Int + , commandDiagramList :: [DiagramDetails] + } + deriving (Generic, Show) + +instance ToJSON CommandSummary + +-- | Information to include in a report about a requirement. +data RequirementDetails = RequirementDetails + { summaryRequirementName :: String + , summaryRequirementDesc :: String + , summaryRequirementTrue :: Bool + , summaryRequirementFalse :: Bool + } + deriving (Generic, Show) + +instance ToJSON RequirementDetails + +-- | Information to include in a report about a diagram. +data DiagramDetails = DiagramDetails + { summaryDiagramNumStates :: Int + , summaryDiagramDeterministic :: Bool + } + deriving (Generic, Show) + +instance ToJSON DiagramDetails + +-- * Errors + +-- | Error message associated to not being able to formalize the input spec. +commandCannotAnalyzeF :: String -> ErrorTriplet +commandCannotAnalyzeF e = + ErrorTriplet ecCannotAnalyzeError msg LocationNothing + where + msg = "The input specification(s) cannot be analyzed: " ++ e + +-- ** Error codes + +-- | Error: the input file cannot be analyzed. +ecCannotAnalyzeError :: ErrorCode +ecCannotAnalyzeError = 1 + +-- * Auxiliary functions + +-- | Name of a requirement when used as a property or handler in a +-- Copilot specification. +requirementNameAsProp :: String -> String +requirementNameAsProp x = "prop" ++ sanitizeUCIdentifier x diff --git a/src/Command/Standalone.hs b/src/Command/Standalone.hs --- a/src/Command/Standalone.hs +++ b/src/Command/Standalone.hs @@ -35,22 +35,24 @@ import Control.Exception as E import Control.Monad.Except (ExceptT (..), liftEither) import Data.Aeson (ToJSON (..)) -import Data.List (nub, (\\)) import Data.Maybe (fromMaybe) import GHC.Generics (Generic) -- External imports: Ogma -import Data.OgmaSpec (ExternalVariableDef (..), - InternalVariableDef (..), Requirement (..), - Spec (..)) import System.Directory.Extra (copyTemplate) -- Internal imports import Command.Common -import Command.Errors (ErrorCode, ErrorTriplet(..)) -import Command.Result (Result (..)) -import Data.Location (Location (..)) -import Language.Trans.Spec2Copilot (spec2Copilot, specAnalyze) +import Command.Errors (ErrorCode, ErrorTriplet(..)) +import Command.Result (Result (..)) +import Data.Aeson.Extra (mergeObjects) +import Data.Either.Extra (mapLeft) +import Data.ExprPair (ExprPair(..), ExprPairT(..), exprPair) +import Data.Location (Location (..)) +import Data.Spec.Extra (addMissingIdentifiers) +import Data.Spec.Parser (readInputExpr) +import Language.Trans.Diagram2Copilot (DiagramMode (..), diagram2CopilotSpec) +import Language.Trans.Spec2Copilot (spec2Copilot, specAnalyze) -- | Generate a new standalone Copilot monitor that implements the spec in an -- input file. @@ -100,40 +102,53 @@ -- Read spec and complement the specification with any missing/implicit -- definitions. - specT <- maybe (return Nothing) (\e -> Just <$> parseInputExpr' e) triggerExprM - specF <- maybe (return Nothing) (\f -> Just <$> parseInputFile' f) fpM + specT <- maybe (return Nothing) (\e -> Just . InputFileSpec <$> readInputExpr' e) triggerExprM + specF <- if null fpA + then return Nothing + else do + fpA' <- mapM readInputFile' fpA + let fpA'' = combineInputFiles fpA' + if length fpA'' > 1 + then liftEither $ Left commandMultipleInputTypes + else pure $ Just $ head fpA'' + let spec = specT <|> specF case spec of Nothing -> liftEither $ Left $ commandMissingSpec - Just spec' -> commandLogic triggerExprM fpM name typeMaps exprT spec' + Just spec' -> commandLogic triggerExprM fpA name typeMaps exprT spec' where triggerExprM = commandConditionExpr options - fpM = commandInputFile options + fpA = commandInputFiles options name = commandFilename options typeMaps = typeToCopilotTypeMapping (commandTypeMapping options) formatName = commandFormat options propFormatName = commandPropFormat options propVia = commandPropVia options - parseInputExpr' e = - parseInputExpr e propFormatName propVia exprT + readInputExpr' e = + readInputExpr e propFormatName propVia exprT - parseInputFile' f = + readInputFile' f = parseInputFile f formatName propFormatName propVia exprT -- | Generate the data of a new standalone Copilot monitor that implements the -- spec, using a subexpression handler. commandLogic :: Maybe String - -> Maybe FilePath + -> [FilePath] -> String -> [(String, String)] -> ExprPairT a - -> Spec a + -> InputFile a -> ExceptT ErrorTriplet IO AppData -commandLogic expr fp name typeMaps exprT input = do +commandLogic expr fps name typeMaps exprT (InputFileDiagram d) = + return $ AppData [] int [] trigs name + where + (int, trigs) = diagram2CopilotSpec d ComputeState + +commandLogic expr fps name typeMaps exprT (InputFileSpec input) = do let spec = addMissingIdentifiers ids input -- Analyze the spec for incorrect identifiers and convert it to Copilot. -- If there is an error, we change the error to a message we control. @@ -150,10 +165,10 @@ where - commandIncorrectSpec' = case (expr, fp) of - (Nothing, Just fp') -> commandIncorrectSpecF fp' - (Just expr', _) -> commandIncorrectSpecE expr' - (_, _) -> error "Both expression and file are missing" + commandIncorrectSpec' = case (expr, fps) of + (Nothing, []) -> error "Both expression and file are missing" + (Nothing, fps') -> commandIncorrectSpecF + (Just expr', _) -> commandIncorrectSpecE expr' ExprPairT parse replace print ids def = exprT @@ -163,7 +178,7 @@ -- code. data CommandOptions = CommandOptions { commandConditionExpr :: Maybe String - , commandInputFile :: Maybe FilePath -- ^ Input specification file. + , commandInputFiles :: [FilePath] -- ^ Input specification file(s). , commandTargetDir :: FilePath -- ^ Target directory where the -- application should be created. , commandTemplateDir :: Maybe FilePath -- ^ Directory where the template @@ -214,13 +229,22 @@ msg = "No input specification has been provided." +-- | Error message associated to having multiple input files of incompatible +-- types. +commandMultipleInputTypes :: ErrorTriplet +commandMultipleInputTypes = + ErrorTriplet ecMultipleInputTypes msg LocationNothing + where + msg = + "Too many inputs provided. Provide one diagram or multiple specs." + -- | Error message associated to not being able to formalize the input spec. -commandIncorrectSpecF :: String -> String -> ErrorTriplet -commandIncorrectSpecF file e = - ErrorTriplet ecIncorrectSpec msg (LocationFile file) +commandIncorrectSpecF :: String -> ErrorTriplet +commandIncorrectSpecF e = + ErrorTriplet ecIncorrectSpec msg LocationNothing where msg = - "The input specification " ++ file ++ " canbot be formalized: " ++ e + "The input specification(s) canbot be formalized: " ++ e -- | Error message associated to not being able to formalize the input spec. commandIncorrectSpecE :: String -> String -> ErrorTriplet @@ -236,28 +260,10 @@ ecMissingSpec :: ErrorCode ecMissingSpec = 1 +-- | Error: multiple inputs of incompatible types. +ecMultipleInputTypes :: ErrorCode +ecMultipleInputTypes = 1 + -- | Error: the input specification cannot be formalized. ecIncorrectSpec :: ErrorCode ecIncorrectSpec = 1 - --- | 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) - -mapLeft :: (a -> c) -> Either a b -> Either c b -mapLeft f (Left x) = Left (f x) -mapLeft _ (Right x) = Right x diff --git a/src/Copilot/Core/Analysis.hs b/src/Copilot/Core/Analysis.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Core/Analysis.hs @@ -0,0 +1,59 @@ +-- Copyright 2024 United States Government as represented by the Administrator +-- of the National Aeronautics and Space Administration. All Rights Reserved. +-- +-- Disclaimers +-- +-- Licensed under the Apache License, Version 2.0 (the "License"); you may +-- not use this file except in compliance with the License. You may obtain a +-- copy of the License at +-- +-- https://www.apache.org/licenses/LICENSE-2.0 +-- +-- Unless required by applicable law or agreed to in writing, software +-- distributed under the License is distributed on an "AS IS" BASIS, WITHOUT +-- WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the +-- License for the specific language governing permissions and limitations +-- under the License. + +-- | Formally analyze Copilot Core specifications. +module Copilot.Core.Analysis + ( exprIsConstant ) + where + +-- External imports +import qualified Copilot.Core as Core +import Copilot.Theorem.What4 (SatResult (..), Solver (Z3), prove) +import Data.List (lookup) + +-- | Determine if a boolean expression is always 'True' or always 'False'. +-- +-- The first boolean in the result is 'True' if the expression can be proven +-- always 'True'. The second boolean in the expression is 'True' is the +-- expression can be proven always 'False'. +-- +-- They values in the tuple cannot both 'True' at the same time. +exprIsConstant :: Core.Spec + -> Core.Name + -> Core.Expr Bool + -> IO (Bool, Bool) +exprIsConstant spec name expr = do + r1 <- propIsValid spec name (Core.Forall expr) + r2 <- propIsValid spec name (Core.Forall (Core.Op1 Core.Not expr)) + pure (r1, r2) + +-- | 'True' if the Copilot 'Prop' with the given name and expression is +-- constantly 'True', or valid, and 'False' otherwise (not always 'True' or +-- unknown). +propIsValid :: Core.Spec + -> Core.Name + -> Core.Prop + -> IO Bool +propIsValid spec name expr = + maybe False isValid . lookup name <$> prove Z3 spec' + where + spec' = spec { Core.specProperties = prop' : Core.specProperties spec } + prop' = Core.Property name expr + + isValid :: SatResult -> Bool + isValid Valid = True + isValid _ = False diff --git a/src/Copilot/Language/Reify/Extra.hs b/src/Copilot/Language/Reify/Extra.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Language/Reify/Extra.hs @@ -0,0 +1,43 @@ +-- Copyright 2024 United States Government as represented by the Administrator +-- of the National Aeronautics and Space Administration. All Rights Reserved. +-- +-- Disclaimers +-- +-- Licensed under the Apache License, Version 2.0 (the "License"); you may +-- not use this file except in compliance with the License. You may obtain a +-- copy of the License at +-- +-- https://www.apache.org/licenses/LICENSE-2.0 +-- +-- Unless required by applicable law or agreed to in writing, software +-- distributed under the License is distributed on an "AS IS" BASIS, WITHOUT +-- WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the +-- License for the specific language governing permissions and limitations +-- under the License. + +-- | Typechecking of Copilot specs. +module Copilot.Language.Reify.Extra + ( reifySpec ) + where + +-- External imports +import qualified Copilot.Core as Core +import qualified Copilot.Language as Copilot +import qualified Copilot.Language.Reify as Copilot +import qualified Language.Haskell.Interpreter as HI + +-- | Read a specification from a 'String' and reify it. +-- +-- This function receives a list of possibly qualified imports. +reifySpec :: [(String, Maybe String)] -> String -> IO Core.Spec +reifySpec imports specText = do + coreSpecE <- HI.runInterpreter $ do + HI.setImportsQ imports + copilotSpec <- HI.interpret specText (HI.as :: Copilot.Spec) + HI.liftIO $ Copilot.reify copilotSpec + + case coreSpecE of + Left err -> do putStrLn $ "Error: " ++ show err + error $ show err + + Right coreSpec -> return coreSpec diff --git a/src/Data/Aeson/Extra.hs b/src/Data/Aeson/Extra.hs new file mode 100644 --- /dev/null +++ b/src/Data/Aeson/Extra.hs @@ -0,0 +1,34 @@ +-- Copyright 2022 United States Government as represented by the Administrator +-- of the National Aeronautics and Space Administration. All Rights Reserved. +-- +-- Disclaimers +-- +-- Licensed under the Apache License, Version 2.0 (the "License"); you may +-- not use this file except in compliance with the License. You may obtain a +-- copy of the License at +-- +-- https://www.apache.org/licenses/LICENSE-2.0 +-- +-- Unless required by applicable law or agreed to in writing, software +-- distributed under the License is distributed on an "AS IS" BASIS, WITHOUT +-- WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the +-- License for the specific language governing permissions and limitations +-- under the License. +-- +-- | Auxiliary functions for working with JSON values. +module Data.Aeson.Extra + ( mergeObjects ) + where + +-- External imports +import Data.Aeson (Value (Null, Object)) +import Data.Aeson.KeyMap (union) + +-- | Merge two JSON values. +-- +-- Fails if the values are not objects or null. +mergeObjects :: Value -> Value -> Value +mergeObjects (Object m1) (Object m2) = Object (union m1 m2) +mergeObjects obj Null = obj +mergeObjects Null obj = obj +mergeObjects _ _ = error "The values passed are not objects" diff --git a/src/Data/Diagram.hs b/src/Data/Diagram.hs new file mode 100644 --- /dev/null +++ b/src/Data/Diagram.hs @@ -0,0 +1,59 @@ +-- Copyright 2024 United States Government as represented by the Administrator +-- of the National Aeronautics and Space Administration. All Rights Reserved. +-- +-- Disclaimers +-- +-- Licensed under the Apache License, Version 2.0 (the "License"); you may +-- not use this file except in compliance with the License. You may obtain a +-- copy of the License at +-- +-- https://www.apache.org/licenses/LICENSE-2.0 +-- +-- Unless required by applicable law or agreed to in writing, software +-- distributed under the License is distributed on an "AS IS" BASIS, WITHOUT +-- WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the +-- License for the specific language governing permissions and limitations +-- under the License. +-- +-- | Diagrams. +module Data.Diagram + ( Diagram(..) + , diagramStates + , diagramNumStates + , diagramInitialState + , diagramFinalState + , diagramBadState + ) + where + +-- External imports +import Data.List (nub, sort) + +-- | Internal representation for diagrams. +newtype Diagram = Diagram + { diagramTransitions :: [(Int, String, Int)] + } + deriving (Show, Eq) + +-- | States in a diagram. +diagramStates :: Diagram -> [Int] +diagramStates diagram = nub $ sort $ concat + [ [s, d] | (s, _, d) <- diagramTransitions diagram ] + +-- | Number of states in a diagram. +diagramNumStates :: Diagram -> Int +diagramNumStates = length . diagramStates + +-- | Initial state of a diagram. +diagramInitialState :: Diagram -> Int +diagramInitialState = minimum . diagramStates + +-- | Final state of a diagram. +-- +-- PRE: The diagram obtains one and only one final state. +diagramFinalState :: Diagram -> Int +diagramFinalState = maximum . diagramStates + +-- | Return a state value that does not represent any state in the diagram. +diagramBadState :: Diagram -> Int +diagramBadState diag = maximum (diagramStates diag) + 1 diff --git a/src/Data/Diagram/Analysis.hs b/src/Data/Diagram/Analysis.hs new file mode 100644 --- /dev/null +++ b/src/Data/Diagram/Analysis.hs @@ -0,0 +1,153 @@ +-- Copyright 2024 United States Government as represented by the Administrator +-- of the National Aeronautics and Space Administration. All Rights Reserved. +-- +-- Disclaimers +-- +-- Licensed under the Apache License, Version 2.0 (the "License"); you may +-- not use this file except in compliance with the License. You may obtain a +-- copy of the License at +-- +-- https://www.apache.org/licenses/LICENSE-2.0 +-- +-- Unless required by applicable law or agreed to in writing, software +-- distributed under the License is distributed on an "AS IS" BASIS, WITHOUT +-- WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the +-- License for the specific language governing permissions and limitations +-- under the License. +-- +-- | Formal analysis of diagrams. +module Data.Diagram.Analysis + ( analyzeDiagram + , AnalysisResult(..) + ) + where + +-- External imports +import qualified Copilot.Core as Core + +-- Internal imports: auxiliary +import Copilot.Core.Analysis (exprIsConstant) +import Copilot.Language.Reify.Extra (reifySpec) +import Data.Diagram (Diagram (..), + diagramNumStates) +import Language.Trans.Diagram2Copilot (diagram2Copilot) + +-- * Analysis of Specs + +-- | Result of analyzing a diagram. +data AnalysisResult = AnalysisResult + { numStates :: Int -- ^ Number of states in the diagram. + , deterministic :: Bool -- ^ True if the diagram is deterministic. + } + +-- | Formally analyze a diagram. +analyzeDiagram :: Diagram -> IO AnalysisResult +analyzeDiagram diagram = do + + let nStates = diagramNumStates diagram + + coreSpec <- reifySpec defaultSpecImports $ showDiagram diagram + + let properties = zip ["deterministic"] propertyGuards + propertyGuards = map Core.triggerGuard $ Core.specTriggers coreSpec + + constantProperties <- mapM (uncurry $ exprIsConstant coreSpec) properties + + let numTrue = length $ filter fst constantProperties + + let diagramDeterministic = numTrue > 0 + + return $ AnalysisResult nStates diagramDeterministic + +-- | Default imports for a 'Spec' that was converted into a 'Copilot.Spec'. +defaultSpecImports :: [(String, Maybe String)] +defaultSpecImports = + [ ("Control.Monad.Writer", Nothing) + , ("Copilot.Language", Nothing) + , ("Copilot.Language.Spec", Nothing) + , ("Data.Functor.Identity", Nothing) + , ("Data.List", Just "L") + , ("Prelude", Just "P") + ] + +-- | Render a 'Diagram' as a Haskell definition of a 'Copilot.Spec'. +-- +-- The shown 'Copilot.Spec' has a top-level triggers for the properties we are +-- interested in, as well as several auxiliary definitions. +showDiagram :: Diagram -> String +showDiagram diagram = unlines $ + [ "do let" ] + ++ map (" " ++) (lines auxiliaryDefinitions) + ++ map (" " ++) (lines input) + ++ map (" " ++) (lines diagramDefinitions) + ++ [ " trigger \"deterministic\" (isDeterministic stateMachine1) []" ] + + where + + input = unlines + [ "input :: Stream Word8" + , "input = extern \"input\" Nothing" + ] + + diagramDefinitions = diagram2Copilot diagram + +-- | Auxiliary definitions needed in the spec. +auxiliaryDefinitions :: String +auxiliaryDefinitions = unlines + [ "stateMachine :: (Eq a, Typed a)" + , " => (a, a, Stream Bool, [(a, Stream Bool, a)], a)" + , " -> Stream a" + , "stateMachine (initial, final, noInputData, transitions, bad) =" + , " state" + , " where" + , " state = ifThenElses transitions" + , " previousState = [initial] ++ state" + , "" + , " -- ifThenElses :: [(a, Stream Bool, a)] -> Stream a" + , " ifThenElses [] =" + , " ifThenElse" + , " (previousState == constant final && noInputData)" + , " (constant final)" + , " (constant bad)" + , "" + , " ifThenElses ((s1, i, s2):ss) =" + , " ifThenElse" + , " (previousState == constant s1 && i)" + , " (constant s2)" + , " (ifThenElses ss)" + , "" + , "isDeterministic :: (Ord a, Eq a, Typed a)" + , " => (a, a, Stream Bool, [(a, Stream Bool, a)], a)" + , " -> Stream Bool" + , "isDeterministic (_, _, _, ts, _) = all $" + , " map" + , " (\\s -> all (map not $ pairwise $ transitionsFrom s))" + , " states" + , " where" + , " states = L.nub $ L.sort $ concat $" + , " map (\\(s1, _, s2) -> [s1, s2]) ts" + , "" + , " transitionsFrom s = [ t | (s1, t, _) <- ts, s P.== s1 ]" + , "" + , "completeMachine :: (Ord a, Eq a, Typed a)" + , " => (a, a, Stream Bool, [(a, Stream Bool, a)], a)" + , " -> Stream Bool" + , "completeMachine (_, _, _, ts, _) = all $" + , " map (\\s -> or $ transitionsFrom s) states" + , " where" + , " states = L.nub $ L.sort $ concat $" + , " map (\\(s1, _, s2) -> [s1, s2]) ts" + , " transitionsFrom s = [ t | (s1, t, _) <- ts, s P.== s1 ]" + , "" + , "all [] = true" + , "all (x:xs) = x && all xs" + , "" + , "or [] = false" + , "or (x:xs) = x || or xs" + , "" + , "pairwise :: [ Stream Bool ] -> [ Stream Bool ]" + , "pairwise [] = []" + , "pairwise (x:[]) = []" + , "pairwise (x1:xs) =" + , " (map (\\x2 -> (x1 && x2)) xs) P.++ pairwise xs" + ] diff --git a/src/Data/Diagram/Parser.hs b/src/Data/Diagram/Parser.hs new file mode 100644 --- /dev/null +++ b/src/Data/Diagram/Parser.hs @@ -0,0 +1,81 @@ +-- Copyright 2024 United States Government as represented by the Administrator +-- of the National Aeronautics and Space Administration. All Rights Reserved. +-- +-- Disclaimers +-- +-- Licensed under the Apache License, Version 2.0 (the "License"); you may +-- not use this file except in compliance with the License. You may obtain a +-- copy of the License at +-- +-- https://www.apache.org/licenses/LICENSE-2.0 +-- +-- Unless required by applicable law or agreed to in writing, software +-- distributed under the License is distributed on an "AS IS" BASIS, WITHOUT +-- WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the +-- License for the specific language governing permissions and limitations +-- under the License. +-- +-- | Parsing of diagrams. +module Data.Diagram.Parser + ( DiagramFormat(..) + , readDiagram + ) + where + +-- External imports +import Control.Monad.Except (ExceptT (..)) +import qualified Data.ByteString.Lazy as B + +-- External imports: auxiliary +import Data.ByteString.Extra as B (safeReadFile) + +-- Internal imports: auxiliary +import Command.Errors (ErrorCode, ErrorTriplet (..)) +import Data.Diagram (Diagram) +import Data.Diagram.Parser.Dot (parseDiagramDot) +import Data.Diagram.Parser.Mermaid (parseDiagramMermaid) +import Data.Either.Extra (mapLeft) +import Data.ExprPair (ExprPair) +import Data.Location (Location (..)) + +-- | Diagram formats supported. +data DiagramFormat = Mermaid + | Dot + deriving (Eq, Show) + +-- | Read a diagram from a file. +readDiagram :: FilePath -- ^ File containing diagram + -> DiagramFormat -- ^ Format of the input file + -> ExprPair -- ^ Subparser for conditions + -- or edge expressions + -> ExceptT ErrorTriplet IO Diagram +readDiagram fp format exprP = ExceptT $ do + contentEither <- B.safeReadFile fp + let diagramE = do + -- The following functions use Either to return errors. The use of + -- (>>=) to chain functions makes the program stop at the earliest + -- error. + diagFileContent <- contentEither + + -- Abtract representation of a state machine diagram. + parseDiagram format diagFileContent exprP + + pure $ mapLeft + (\msg -> ErrorTriplet ecCannotReadDiagram msg (LocationFile fp)) + diagramE + +--- | Generic function to parse a diagram. +parseDiagram :: DiagramFormat -- ^ Format of the input file + -> B.ByteString -- ^ Contents of the diagram + -> ExprPair -- ^ Subparser for conditions or edge + -- expressions + -> Either String Diagram +parseDiagram Dot = parseDiagramDot +parseDiagram Mermaid = parseDiagramMermaid + +-- ** Error codes + +-- | Error: the diagram cannot be read due to an error opening the file or +-- parsing the file. +ecCannotReadDiagram :: ErrorCode +ecCannotReadDiagram = 1 diff --git a/src/Data/Diagram/Parser/Dot.hs b/src/Data/Diagram/Parser/Dot.hs new file mode 100644 --- /dev/null +++ b/src/Data/Diagram/Parser/Dot.hs @@ -0,0 +1,66 @@ +{-# LANGUAGE OverloadedStrings #-} +-- Copyright 2024 United States Government as represented by the Administrator +-- of the National Aeronautics and Space Administration. All Rights Reserved. +-- +-- Disclaimers +-- +-- Licensed under the Apache License, Version 2.0 (the "License"); you may +-- not use this file except in compliance with the License. You may obtain a +-- copy of the License at +-- +-- https://www.apache.org/licenses/LICENSE-2.0 +-- +-- Unless required by applicable law or agreed to in writing, software +-- distributed under the License is distributed on an "AS IS" BASIS, WITHOUT +-- WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the +-- License for the specific language governing permissions and limitations +-- under the License. +-- +-- | Parsing of diagrams from Dot files. +module Data.Diagram.Parser.Dot + ( parseDiagramDot + ) + where + +-- External imports +import qualified Data.ByteString.Lazy as B +import Data.GraphViz (graphEdges) +import qualified Data.GraphViz as G +import qualified Data.GraphViz.Attributes.Complete as Attributes +import Data.GraphViz.Commands.IO (toUTF8) +import qualified Data.GraphViz.Parsing as G +import Data.GraphViz.PreProcessing (preProcess) +import qualified Data.GraphViz.Types.Generalised as Gs +import qualified Data.Text.Lazy as LT + +-- Internal imports: auxiliary +import Data.Diagram (Diagram (..)) +import Data.ExprPair (ExprPair, exprPairShow) + +-- | Parse a DOT / Graphviz diagram. +parseDiagramDot :: B.ByteString -> ExprPair -> Either String Diagram +parseDiagramDot contents exprP = do + let contentsUTF8 = toUTF8 contents + dg <- fst $ G.runParser G.parse $ preProcess contentsUTF8 + return $ makeDiagram dg + where + makeDiagram :: Gs.DotGraph LT.Text -> Diagram + makeDiagram g = Diagram links + where + links = map edgeToLink (graphEdges g) + + edgeToLink edge = + ( read (LT.unpack o) + , exprPairShow exprP (LT.unpack e) + , read (LT.unpack d) + ) + where + o = G.fromNode edge + d = G.toNode edge + e = getLabel (G.edgeAttributes edge) + + -- Extract the label from a list of attributes. If no label is + -- found, it's assumed that the condition is the literal true. + getLabel [] = "true" + getLabel ((Attributes.Label (Attributes.StrLabel l)) : _) = l + getLabel (_ : as) = getLabel as diff --git a/src/Data/Diagram/Parser/Mermaid.hs b/src/Data/Diagram/Parser/Mermaid.hs new file mode 100644 --- /dev/null +++ b/src/Data/Diagram/Parser/Mermaid.hs @@ -0,0 +1,181 @@ +{-# LANGUAGE OverloadedStrings #-} +-- Copyright 2024 United States Government as represented by the Administrator +-- of the National Aeronautics and Space Administration. All Rights Reserved. +-- +-- Disclaimers +-- +-- Licensed under the Apache License, Version 2.0 (the "License"); you may +-- not use this file except in compliance with the License. You may obtain a +-- copy of the License at +-- +-- https://www.apache.org/licenses/LICENSE-2.0 +-- +-- Unless required by applicable law or agreed to in writing, software +-- distributed under the License is distributed on an "AS IS" BASIS, WITHOUT +-- WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the +-- License for the specific language governing permissions and limitations +-- under the License. +-- +-- | Parsing of diagrams from Mermaid files. +module Data.Diagram.Parser.Mermaid + ( parseDiagramMermaid + ) + where + +-- External imports +import Control.Monad (void, when) +import Data.ByteString.Lazy (toStrict) +import qualified Data.ByteString.Lazy as B +import Data.Either (isLeft) +import Data.Functor.Identity (Identity) +import qualified Data.Set as Set +import Data.Text (Text) +import qualified Data.Text as T +import qualified Data.Text.Encoding as T +import Data.Void (Void) +import Text.Megaparsec (ErrorFancy (ErrorFail), ParsecT, + choice, empty, errorBundlePretty, + fancyFailure, many, manyTill, + noneOf, parse, (<|>)) +import Text.Megaparsec.Char (alphaNumChar, char, digitChar, + newline, space1, string) +import qualified Text.Megaparsec.Char.Lexer as L + +-- Internal imports: auxiliary +import Data.Diagram (Diagram (..)) +import Data.ExprPair (ExprPair (..), ExprPairT (..), exprPairShow) + +-- | Parse a mermaid diagram. +parseDiagramMermaid :: B.ByteString -> ExprPair -> Either String Diagram +parseDiagramMermaid txtDia exprP = + case parsingResult of + Left e -> Left (errorBundlePretty e) + Right x -> Right x + where + txt = T.decodeUtf8 (toStrict txtDia) + parsingResult = parse (spaces *> pDiagram exprP) "" txt + +-- | Type for parser for memaid diagrams. +type MermaidParser = ParsecT Void Text Identity + +-- | Parser for mermaid diagrams. +pDiagram :: ExprPair -> MermaidParser Diagram +pDiagram exprP = + pGraphDiagram exprP + <|> pStateDiagram exprP + <|> pSequenceDiagram exprP + +-- | Parser for a mermaid diagram. +-- +-- This parser depends on an auxiliary parser for the expressions associated to +-- the edges or connections between states. +pGraphDiagram :: ExprPair -> MermaidParser Diagram +pGraphDiagram exprP = do + _ <- string "graph" <* spaces + _name <- T.pack <$> manyTill alphaNumChar (char ';') + _ <- newline + + transitions <- many (pGraphTransition exprP) + + pure $ Diagram transitions + +-- | Parser for an edge in a state diagram. +-- +-- This parser depends on an auxiliary parser for the expressions associated to +-- the edges or connections between states. +pGraphTransition :: ExprPair -> MermaidParser (Int, String, Int) +pGraphTransition ep@(ExprPair (ExprPairT { exprTParse = parseProp })) = do + _ <- spaces + stateFrom <- many digitChar + _ <- string "-->|" + edge <- many (noneOf ("|" :: [Char])) + + let x = parseProp edge + when (isLeft x) $ fancyFailure $ Set.singleton $ + ErrorFail $ "Edge property has incorrect format: " ++ show edge + + _ <- char '|' + stateTo <- many digitChar + _ <- char ';' + _ <- newline + return (read stateFrom, exprPairShow ep edge, read stateTo) + +-- | Parser for Mermaid diagrams of type stateDiagram-v2. +pStateDiagram :: ExprPair -> MermaidParser Diagram +pStateDiagram exprPair = do + _ <- string "stateDiagram-v2" <* spaces + + transitions <- many (pStateTransition exprPair) + + pure $ Diagram transitions + +-- | Parser for transition label in stateDiagram-v2 mermaid diagram. +pStateTransition :: ExprPair -> MermaidParser (Int, String, Int) +pStateTransition ep@(ExprPair (ExprPairT { exprTParse = parseProp })) = do + _ <- spaces + from <- read <$> many digitChar + _ <- spaces + string "-->" + _ <- spaces + to <- read <$> many digitChar + _ <- spaces + _ <- char ':' + _ <- spaces + edge <- many (noneOf ("\n" :: [Char])) + + let x = parseProp edge + when (isLeft x) $ fancyFailure $ Set.singleton $ + ErrorFail $ "Edge property has incorrect format: " ++ show edge + + _ <- newline + + pure $ (from, exprPairShow ep edge, to) + +-- | Parser for Mermaid diagrams of type sequenceDiagram. +pSequenceDiagram :: ExprPair -> MermaidParser Diagram +pSequenceDiagram exprPair = do + spaces + _ <- string "sequenceDiagram" + spaces + + conditions <- many (pSequenceTransition exprPair) + let transitions = zipWith (\t idx -> (idx, t, idx + 1)) conditions [0..] + + pure $ Diagram transitions + +-- | Parser for a connection, message or transition in a sequence diagram. +-- +-- This parser depends on an auxiliary parser for the expressions associated to +-- the connections or messages between elements. +pSequenceTransition :: ExprPair -> MermaidParser String +pSequenceTransition ep@(ExprPair (ExprPairT { exprTParse = parseProp })) = do + spaces + stateFrom <- many digitChar + spaces + pSequenceArrow + spaces + stateTo <- many digitChar + spaces + _ <- char ':' + spaces + edge <- many (noneOf ("\n" :: [Char])) + + let x = parseProp edge + when (isLeft x) $ fancyFailure $ Set.singleton $ + ErrorFail $ "Edge property has incorrect format: " ++ show edge + + _ <- newline + + pure (exprPairShow ep edge) + +-- | Parser for arrow in sequence diagram. +pSequenceArrow :: MermaidParser () +pSequenceArrow = void $ choice + [ string "->>" + , string "-->>" + , string "-)" + ] + +-- | Consume spaces +spaces :: MermaidParser () +spaces = L.space space1 empty empty diff --git a/src/Data/Either/Extra.hs b/src/Data/Either/Extra.hs new file mode 100644 --- /dev/null +++ b/src/Data/Either/Extra.hs @@ -0,0 +1,35 @@ +-- Copyright 2022 United States Government as represented by the Administrator +-- of the National Aeronautics and Space Administration. All Rights Reserved. +-- +-- Disclaimers +-- +-- Licensed under the Apache License, Version 2.0 (the "License"); you may +-- not use this file except in compliance with the License. You may obtain a +-- copy of the License at +-- +-- https://www.apache.org/licenses/LICENSE-2.0 +-- +-- Unless required by applicable law or agreed to in writing, software +-- distributed under the License is distributed on an "AS IS" BASIS, WITHOUT +-- WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the +-- License for the specific language governing permissions and limitations +-- under the License. +-- +-- | Auxiliary functions for working with values of type 'Either'. +module Data.Either.Extra + ( makeLeft + , mapLeft + ) + where + +-- | Replace the left value in an @Either@. +makeLeft :: c -> Either a b -> Either c b +makeLeft c (Left _) = Left c +makeLeft _ (Right x) = Right x + +-- | Apply a transformation only to the 'Left' values of an 'Either'. +-- +-- Left counterpart of 'fmap'. +mapLeft :: (a -> c) -> Either a b -> Either c b +mapLeft f (Left x) = Left (f x) +mapLeft _ (Right x) = Right x diff --git a/src/Data/ExprPair.hs b/src/Data/ExprPair.hs new file mode 100644 --- /dev/null +++ b/src/Data/ExprPair.hs @@ -0,0 +1,106 @@ +{-# LANGUAGE ExistentialQuantification #-} +-- Copyright 2022 United States Government as represented by the Administrator +-- of the National Aeronautics and Space Administration. All Rights Reserved. +-- +-- Disclaimers +-- +-- Licensed under the Apache License, Version 2.0 (the "License"); you may +-- not use this file except in compliance with the License. You may obtain a +-- copy of the License at +-- +-- https://www.apache.org/licenses/LICENSE-2.0 +-- +-- Unless required by applicable law or agreed to in writing, software +-- distributed under the License is distributed on an "AS IS" BASIS, WITHOUT +-- WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the +-- License for the specific language governing permissions and limitations +-- under the License. +-- +-- | Abstraction for expressions used in specifications. +module Data.ExprPair + ( ExprPair(..) + , ExprPairT(..) + , exprPair + , exprPairShow + ) + where + +-- External imports +import qualified Language.Lustre.AbsLustre as Lustre +import qualified Language.Lustre.ParLustre as Lustre (myLexer, pBoolSpec) +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.Lustre2Copilot as Lustre (boolSpec2Copilot, + boolSpecNames) +import Language.Trans.SMV2Copilot as SMV (boolSpec2Copilot, + boolSpecNames) + +-- | Existential wrapper over abstraction to handle expressions used in +-- specifications. +-- +-- The abstraction provides mechanisms to parse expressions, replace variables +-- in them, render them in a known format or notation, and find identifiers in +-- them, and it provides a default value to use when an expression is needed. +data ExprPair = forall a . ExprPair + { exprTPair :: ExprPairT a + } + +-- | Abstraction to handle expressions used in specifications. +-- +-- The abstraction provides mechanisms to parse expressions, replace variables +-- in them, render them in a known format or notation, and find identifiers in +-- them, and it provides a default value to use when an expression is needed. +data ExprPairT a = ExprPairT + { exprTParse :: String -> Either String a + , exprTReplace :: [(String, String)] -> a -> a + , exprTPrint :: a -> String + , exprTIdents :: a -> [String] + , exprTUnknown :: a + } + +-- | Return 'ExprPair' for a given language (e.g., Lustre, SMV). +-- +-- The language name must be lowercase. +-- +-- We default to SMV if no format is given. +-- +-- The format literal returns an ExprPair that uses Strings as the base type +-- and keeps them unchanged. +exprPair :: String -> ExprPair +exprPair "lustre" = ExprPair $ + ExprPairT + (Lustre.pBoolSpec . Lustre.myLexer) + (\_ -> id) + (Lustre.boolSpec2Copilot) + (Lustre.boolSpecNames) + (Lustre.BoolSpecSignal (Lustre.Ident "undefined")) +exprPair "literal" = ExprPair $ + ExprPairT + Right + (\_ -> id) + id + (const []) + "undefined" +exprPair "cocospec" = exprPair "lustre" +exprPair _ = ExprPair $ + ExprPairT + (SMV.pBoolSpec . SMV.myLexer) + (substituteBoolExpr) + (SMV.boolSpec2Copilot) + (SMV.boolSpecNames) + (SMV.BoolSpecSignal (SMV.Ident "undefined")) + +-- | Parse and print a value using an auxiliary Expression Pair. +-- +-- Fails if the value has no valid parse. +exprPairShow :: ExprPair -> String -> String +exprPairShow (ExprPair exprP) = + printProp . fromRight' . parseProp + where + ExprPairT parseProp _replace printProp _ids _unknown = exprP + + -- | Unsafe fromRight. Fails if the value is a 'Left'. + fromRight' :: Either a b -> b + fromRight' (Right v) = v + fromRight' _ = error "fromRight' applied to Left value." diff --git a/src/Data/Spec/Analysis.hs b/src/Data/Spec/Analysis.hs new file mode 100644 --- /dev/null +++ b/src/Data/Spec/Analysis.hs @@ -0,0 +1,267 @@ +-- Copyright 2024 United States Government as represented by the Administrator +-- of the National Aeronautics and Space Administration. All Rights Reserved. +-- +-- Disclaimers +-- +-- Licensed under the Apache License, Version 2.0 (the "License"); you may +-- not use this file except in compliance with the License. You may obtain a +-- copy of the License at +-- +-- https://www.apache.org/licenses/LICENSE-2.0 +-- +-- Unless required by applicable law or agreed to in writing, software +-- distributed under the License is distributed on an "AS IS" BASIS, WITHOUT +-- WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the +-- License for the specific language governing permissions and limitations +-- under the License. + +-- | Formally analyze specifications and provide information about them. +module Data.Spec.Analysis + ( AnalysisResult(..) + , specAnalyze + ) + where + +-- External imports +import qualified Copilot.Core as Core +import Data.List (intercalate, lookup) +import Data.Maybe (fromMaybe) + +-- External imports: auxiliary +import Data.String.Extra (sanitizeLCIdentifier, sanitizeUCIdentifier) + +-- External imports: ogma-spec +import Data.OgmaSpec (ExternalVariableDef (..), InternalVariableDef (..), + Requirement (..), Spec (..)) + +-- Internal imports +import Copilot.Core.Analysis (exprIsConstant) +import Copilot.Language.Reify.Extra (reifySpec) + +-- * Analysis of Specs + +-- | Result of analyzing a specification. +data AnalysisResult = AnalysisResult + { numAlwaysTrue :: Int -- ^ Number of always true requirements. + , numAlwaysFalse :: Int -- ^ Number of always false requirements. + , alwaysTrueReq :: [String] -- ^ List of always true requirements. + , alwaysFalseReq :: [String] -- ^ List of always false requirements. + , consistent :: Bool -- ^ Whether requirements are mutually + -- consistent. + } + +-- | Formally analyze a specification for redundancies, conflicts, etc. +specAnalyze :: [(String, String)] -- Type substitution table + -> ([(String, String)] -> a -> a) -- Expr substitution function + -> (a -> String) -- Expr show function + -> Spec a -- Specification + -> IO (Either String AnalysisResult) +specAnalyze typeMaps exprTransform showExpr spec = do + let structuredSpec = + spec2Copilot typeMaps exprTransform showExpr spec + + coreSpec <- reifySpec defaultSpecImports $ showSpec structuredSpec + + let properties = zip propertyNames propertyGuards + propertyNames = map (\(_, p, _, _, _) -> p) + $ copilotProperties structuredSpec + propertyGuards = map Core.triggerGuard $ Core.specTriggers coreSpec + + constantProperties <- mapM (uncurry $ exprIsConstant coreSpec) properties + + let constantProperties' = zip propertyNames constantProperties + + let numTrue = length $ filter fst constantProperties + numFalse = length $ filter snd constantProperties + + trueReqs = map fst $ filter (fst . snd) constantProperties' + falseReqs = map fst $ filter (snd . snd) constantProperties' + + let negatedConjunction = Core.Op1 Core.Not + $ foldr (Core.Op2 Core.And) true propertyGuards + true = Core.Const Core.Bool True + + provedNegatedConjunction <- + exprIsConstant coreSpec "ogma_inc" negatedConjunction + + -- The requirements are considered consistent if it was *not* possible to + -- prove that their conjunction is always false. + let consistent = not $ fst provedNegatedConjunction + + return $ Right $ + AnalysisResult numTrue numFalse trueReqs falseReqs consistent + +-- * Auxiliary + +-- ** Structured Copilot specifications + +-- | A structured Copilot specification. +data CopilotSpec = CopilotSpec + { copilotProperties :: [(String, String, String, String, String)] + -- ^ Requirement name, property name, handler name, + -- implementation and arguments. + + , copilotAuxDefs :: [(String, String, String)] + -- ^ Name, type, implementation + } + +-- | Given a 'Spec', return a structured version the corresponding Copilot spec +-- that differentiates between the auxiliary definitions (inputs, outputs) and +-- the properties or requirements to check. +-- +-- 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, String)] -- Type substitution table + -> ([(String, String)] -> a -> a) -- Expr substitution function + -> (a -> String) -- Expr show function + -> Spec a -- Specification + -> CopilotSpec +spec2Copilot typeMaps exprTransform showExpr spec = CopilotSpec reqs auxDefs + where + -- Encoding of requirements as boolean streams + reqs :: [(String, String, String, String, String)] + reqs = map reqToDecl (requirements spec) + where + reqToDecl i = + ( reqName + , propName + , handlerName + , reqBody nameSubstitutions + , handlerArg + ) + where + reqName = requirementName i + + propName = safeMap nameSubstitutions (requirementName i) + + handlerName = "handler" ++ sanitizeUCIdentifier (requirementName i) + + -- Definition implementation. We use an auxiliary function to + -- transform the implementation into Copilot, applying a + -- substitution. + reqBody subs = showExpr (exprTransform subs (requirementExpr i)) + + handlerArg = + case (requirementResultType i, requirementResultExpr i) of + (Just _, Just ex) -> "[ arg (" ++ showExpr ex ++ " ) ]" + _ -> "[]" + + auxDefs :: [(String, String, String)] + auxDefs = externs ++ internals + + externs :: [(String, String, String)] + externs = map externVarToDecl (externalVariables spec) + where + externVarToDecl i = (propName, streamType, implementation) + where + propName = safeMap nameSubstitutions (externalVariableName i) + + streamType = "Stream " ++ "(" ++ valueType ++ ")" + valueType = safeMap typeMaps (externalVariableType i) + + implementation = "extern" ++ " " ++ show (externalVariableName i) + ++ " " ++ "Nothing" + + -- Internal stream definitions + internals :: [(String, String, String)] + internals = map internalVarToDecl (internalVariables spec) + where + internalVarToDecl i = (propName, streamType, implementation) + where + propName = safeMap nameSubstitutions (internalVariableName i) + + streamType = "Stream " ++ "(" ++ valueType ++ ")" + valueType = safeMap typeMaps (internalVariableType i) + + implementation = internalVariableExpr i + + nameSubstitutions = internalVariableMap + ++ externalVariableMap + ++ 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 input spec. + internalVariableNames = map internalVariableName + $ internalVariables spec + + externalVariableNames = map externalVariableName + $ externalVariables spec + + requirementNames = map requirementName + $ requirements spec + +-- | Render a 'CopilotSpec' as a Haskell definition of a 'Copilot.Spec', +-- listing the elements in the spec with the necessary indentation. +-- +-- The shown 'Copilot.Spec' has a list of top-level triggers, as well as +-- several auxiliary definitions. +showSpec :: CopilotSpec -> String +showSpec spec = template ++ "\n" ++ extra ++ "\n" ++ triggers + where + -- Initial template used for analysis purposes. + template :: String + template = unlines + [ "do let" + , "" + , " clock :: Stream Int64" + , " clock = [0] ++ (clock + 1)" + , "" + , " ftp :: Stream Bool" + , " ftp = [True] ++ false" + , "" + , " pre :: Stream Bool -> Stream Bool" + , " pre = ([False] ++)" + , "" + , " tpre :: Stream Bool -> Stream Bool" + , " tpre = ([True] ++)" + , "" + , " notPreviousNot :: Stream Bool -> Stream Bool" + , " notPreviousNot = not . PTLTL.previous . not" + ] + + extra = unlines + $ intercalate [""] + $ map formatDef + $ copilotAuxDefs spec + + triggers = unlines + $ intercalate [""] + $ map formatTrigger + $ copilotProperties spec + + formatDef (n, t, i) = + map (" " ++) [ n ++ " :: " ++ t, n ++ " = " ++ i ] + + formatTrigger (_, _, h, g, a) = + map (" " ++) [ "trigger " ++ show h ++ " (" ++ g ++ ") " ++ a ] + +-- | Default imports for a 'Spec' that was converted into a 'Copilot.Spec'. +defaultSpecImports :: [(String, Maybe String)] +defaultSpecImports = + [ ("Control.Monad.Writer", Nothing) + , ("Copilot.Language", Nothing) + , ("Copilot.Language.Spec", Nothing) + , ("Data.Functor.Identity", Nothing) + , ("Language.Copilot", Nothing) + , ("Copilot.Library.PTLTL", Just "PTLTL") + , ("Prelude", Just "P") + ] + +-- ** Auxiliary list functions + +-- | Substitute a key based on a given substitution table from key to +-- alternative key. +-- +-- They key is left unchanged if it cannot be found in the substitution table. +safeMap :: Eq k => [(k, k)] -> k -> k +safeMap ls k = fromMaybe k $ lookup k ls diff --git a/src/Data/Spec/Extra.hs b/src/Data/Spec/Extra.hs new file mode 100644 --- /dev/null +++ b/src/Data/Spec/Extra.hs @@ -0,0 +1,46 @@ +-- Copyright 2022 United States Government as represented by the Administrator +-- of the National Aeronautics and Space Administration. All Rights Reserved. +-- +-- Disclaimers +-- +-- Licensed under the Apache License, Version 2.0 (the "License"); you may +-- not use this file except in compliance with the License. You may obtain a +-- copy of the License at +-- +-- https://www.apache.org/licenses/LICENSE-2.0 +-- +-- Unless required by applicable law or agreed to in writing, software +-- distributed under the License is distributed on an "AS IS" BASIS, WITHOUT +-- WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the +-- License for the specific language governing permissions and limitations +-- under the License. +-- +-- | Auxiliary functions for working with values of type 'Spec'. +module Data.Spec.Extra + ( addMissingIdentifiers ) + where + +-- External imports +import Data.List (nub, (\\)) + +-- External imports: ogma +import Data.OgmaSpec (ExternalVariableDef (..), InternalVariableDef (..), + Requirement (..), Spec (..)) + +-- | 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/Data/Spec/Parser.hs b/src/Data/Spec/Parser.hs new file mode 100644 --- /dev/null +++ b/src/Data/Spec/Parser.hs @@ -0,0 +1,218 @@ +{-# LANGUAGE MultiWayIf #-} +{-# LANGUAGE ScopedTypeVariables #-} +-- Copyright 2022 United States Government as represented by the Administrator +-- of the National Aeronautics and Space Administration. All Rights Reserved. +-- +-- Disclaimers +-- +-- Licensed under the Apache License, Version 2.0 (the "License"); you may +-- not use this file except in compliance with the License. You may obtain a +-- copy of the License at +-- +-- https://www.apache.org/licenses/LICENSE-2.0 +-- +-- Unless required by applicable law or agreed to in writing, software +-- distributed under the License is distributed on an "AS IS" BASIS, WITHOUT +-- WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the +-- License for the specific language governing permissions and limitations +-- under the License. +-- +-- | Parsing of specs. +module Data.Spec.Parser + ( readInputExpr + , readInputFile + ) + where + +-- External imports +import qualified Control.Exception as E +import Control.Monad.Except (ExceptT (..)) +import Data.Aeson (eitherDecode) +import qualified Data.ByteString.Lazy as L +import Data.List (isInfixOf, isPrefixOf, nub, (\\)) +import System.Directory (doesFileExist) +import System.FilePath (()) +import System.Process (readProcess) + +-- External imports: auxiliary +import Data.ByteString.Extra as B (safeReadFile) +import Data.String.Extra (sanitizeLCIdentifier, sanitizeUCIdentifier) + +-- External imports: ogma +import Data.OgmaSpec (ExternalVariableDef (..), + InternalVariableDef (..), Requirement (..), + Spec (..)) +import Language.CSVSpec.Parser (parseCSVSpec) +import Language.JSONSpec.Parser (parseJSONSpec) +import Language.XLSXSpec.Parser (parseXLSXSpec) +import Language.XMLSpec.Parser (parseXMLSpec) +import Language.YAMLSpec.Parser (parseYAMLSpec) + +-- Internal imports: auxiliary +import Command.Errors (ErrorTriplet(..), ErrorCode) +import Data.Diagram (Diagram) +import Data.Either.Extra (mapLeft) +import Data.ExprPair (ExprPairT(..)) +import Data.Location (Location (..)) +import Paths_ogma_core (getDataDir) + +-- | Process input specification from a single expression and return its +-- abstract representation. +readInputExpr :: String + -> String + -> Maybe String + -> ExprPairT a + -> ExceptT ErrorTriplet IO (Spec a) +readInputExpr expr propFormatName propVia exprT = + ExceptT $ do + let ExprPairT parse replace print ids def = exprT + + let wrapper = wrapVia propVia parse + + result <- wrapper expr + + let spec = do + expr' <- result + let req = Requirement "triggerCondition" expr' "" Nothing Nothing + return $ Spec [] [] [ req ] + + -- Return the spec, transforming the error message if applicable. + pure $ mapLeft (cannotReadConditionExpr expr) spec + +--- | Process input specification, if available, and return its abstract +--- representation. +readInputFile :: FilePath + -> String + -> String + -> Maybe String + -> ExprPairT a + -> ExceptT ErrorTriplet IO (Spec a) +readInputFile fp formatName propFormatName propVia exprT = + ExceptT $ do + let ExprPairT parse replace print ids def = exprT + + let wrapper = wrapVia propVia parse + -- Obtain format file. + -- + -- A format name that exists as a file in the disk always takes preference + -- over a file format included with Ogma. A file format with a forward + -- slash in the name is always assumed to be a user-provided filename. + -- Regardless of whether the file is user-provided or known to Ogma, we + -- check (again) whether the file exists, and print an error message if + -- not. + exists <- doesFileExist formatName + dataDir <- getDataDir + let formatFile + | isInfixOf "/" formatName || exists + = formatName + | otherwise + = dataDir "data" "formats" + (formatName ++ "_" ++ propFormatName) + formatMissing <- not <$> doesFileExist formatFile + + if formatMissing + then return $ Left $ commandIncorrectFormatSpec formatFile + else do + res <- do + format <- readFile formatFile + + -- 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. + if | isPrefixOf "XMLFormat" format + -> do let xmlFormat = read format + content <- readFile fp + parseXMLSpec + (wrapper) (def) xmlFormat content + -- (fmap (fmap print) . wrapper) (print def) xmlFormat content + | isPrefixOf "CSVFormat" format + -> do let csvFormat = read format + content <- readFile fp + parseCSVSpec wrapper def csvFormat content + | isPrefixOf "XLSXFormat" format + -> do let xlsxFormat = read format + content <- L.readFile fp + parseXLSXSpec wrapper def xlsxFormat content + | isPrefixOf "YAMLFormat" format + -> do let yamlFormat = read format + content <- B.safeReadFile fp + case content of + Left e -> return $ Left e + Right b -> parseYAMLSpec wrapper yamlFormat (L.toStrict b) + | otherwise + -> do let jsonFormat = read format + content <- B.safeReadFile fp + case content of + Left e -> return $ Left e + Right b -> do case eitherDecode b of + Left e -> return $ Left e + Right v -> + parseJSONSpec + (wrapper) + jsonFormat + v + case res of + Left e -> return $ Left $ cannotOpenInputFile fp + Right x -> return $ Right x + + + +-- | Exception handler to deal with the case in which the trigger expression +-- cannot be understood. +cannotReadConditionExpr :: String -> String -> ErrorTriplet +cannotReadConditionExpr expr errorMsg = + ErrorTriplet ecCannotReadConditionExpr msg LocationNothing + where + msg = + "cannot parse condition or trigger expression " ++ show expr ++ ":" + ++ errorMsg + +-- | Exception handler to deal with the case in which the input file cannot be +-- opened. +cannotOpenInputFile :: FilePath -> ErrorTriplet +cannotOpenInputFile file = + ErrorTriplet ecCannotOpenInputFile msg (LocationFile file) + where + msg = + "cannot open input specification file " ++ file + +-- | Error message associated to the format file not being found. +commandIncorrectFormatSpec :: FilePath -> ErrorTriplet +commandIncorrectFormatSpec formatFile = + ErrorTriplet ecIncorrectFormatFile msg (LocationFile formatFile) + where + msg = + "The format specification " ++ formatFile ++ " does not exist or is not " + ++ "readable" + +-- ** Error codes + +-- | Error: the trigger expression provided by the user cannot be parsed. +ecCannotReadConditionExpr :: ErrorCode +ecCannotReadConditionExpr = 1 + +-- | Error: the input specification provided by the user cannot be opened. +ecCannotOpenInputFile :: ErrorCode +ecCannotOpenInputFile = 1 + +-- | Error: the format file cannot be opened. +ecIncorrectFormatFile :: ErrorCode +ecIncorrectFormatFile = 1 + +-- | Parse a property using an auxiliary program to first translate it, if +-- available. +-- +-- If a program is given, it is first called on the property, and then the +-- result is parsed with the parser passed as an argument. If a program is not +-- given, then the parser is applied to the given string. +wrapVia :: Maybe String -- ^ Auxiliary program to translate the + -- property. + -> (String -> Either String a) -- ^ Parser used on the result. + -> String -- ^ Property to parse. + -> IO (Either String a) +wrapVia Nothing parse s = return (parse s) +wrapVia (Just f) parse s = + E.handle (\(e :: E.IOException) -> return $ Left $ show e) $ do + out <- readProcess f [] s + return $ parse out diff --git a/src/Language/Trans/Diagram2Copilot.hs b/src/Language/Trans/Diagram2Copilot.hs new file mode 100644 --- /dev/null +++ b/src/Language/Trans/Diagram2Copilot.hs @@ -0,0 +1,121 @@ +-- Copyright 2024 United States Government as represented by the Administrator +-- of the National Aeronautics and Space Administration. All Rights Reserved. +-- +-- Disclaimers +-- +-- Licensed under the Apache License, Version 2.0 (the "License"); you may +-- not use this file except in compliance with the License. You may obtain a +-- copy of the License at +-- +-- https://www.apache.org/licenses/LICENSE-2.0 +-- +-- Unless required by applicable law or agreed to in writing, software +-- distributed under the License is distributed on an "AS IS" BASIS, WITHOUT +-- WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the +-- License for the specific language governing permissions and limitations +-- under the License. +-- +-- | Transform a state diagram into a Copilot specification. +module Language.Trans.Diagram2Copilot + ( DiagramMode(..) + , diagram2CopilotSpec + , diagram2Copilot + ) + where + +-- External imports +import Data.List (intercalate, nub, sort) + +-- Internal imports: auxiliary +import Data.Diagram (Diagram (..), diagramBadState, diagramFinalState, + diagramInitialState) + +-- | Modes of operation. +data DiagramMode = CheckState -- ^ Check if given state matches expectation + | ComputeState -- ^ Compute expected state + | CheckMoves -- ^ Check if transitioning to a state would be + -- possible. + deriving (Eq, Show) + +-- | Convert the diagram into a set of Copilot definitions, and a list of +-- indented trigger definitions to include in the Copilot spec. +diagram2CopilotSpec :: Diagram -> DiagramMode -> (String, String) +diagram2CopilotSpec diag mode = (machine, triggers) + where + machine = unlines + [ "stateMachineS :: Stream Word8" + , "stateMachineS = stateMachineGF stateMachine1" + , "" + , "stateMachineProp :: Stream Bool" + , "stateMachineProp = " ++ propExpr + , "" + ] + ++ diagram2Copilot diag + + -- Elements of the spec. + propExpr = case mode of + CheckState -> "stateMachineS /= externalState" + ComputeState -> "true" + CheckMoves -> "true" + + triggers = " trigger \"handler\" stateMachineProp " ++ arguments + + -- Arguments for the handler. + arguments = "[ " ++ intercalate ", " (map ("arg " ++) argExprs) ++ " ]" + + argExprs = case mode of + CheckState -> [ "stateMachineS" ] + ComputeState -> [ "stateMachineS" ] + CheckMoves -> map stateCheckExpr states + + stateCheckExpr stateId = + "(checkValidTransition transitions externalState " ++ show stateId ++ ")" + + -- States and transitions from the diagram. + transitions = diagramTransitions diag + states = nub $ sort $ concat [ [x, y] | (x, _, y) <- transitions ] + +-- | Convert the diagram into a set of Copilot definitions. +diagram2Copilot :: Diagram -> String +diagram2Copilot diag = unlines + [ "stateMachine1 :: ( Word8" + , " , Word8" + , " , Stream Bool" + , " , [(Word8, Stream Bool, Word8)]" + , " , Word8" + , " )" + , "stateMachine1 =" + , " (initialState, finalState, noInput, transitions, badState)" + , "" + , "-- Check" + , "initialState :: Word8" + , "initialState = " ++ show initialState + , "" + , "-- Check" + , "finalState :: Word8" + , "finalState = " ++ show finalState + , "" + , "noInput :: Stream Bool" + , "noInput = false" + , "" + , "badState :: Word8" + , "badState = " ++ show badState + , "" + , "transitions = " ++ showTransitions + ] + + where + + initialState = diagramInitialState diag + finalState = diagramFinalState diag + badState = diagramBadState diag + + transitions = diagramTransitions diag + + showTransitions :: String + showTransitions = + "[" ++ intercalate ", " (map showTransition transitions) ++ "]" + + showTransition :: (Int, String, Int) -> String + showTransition (a, b, c) = + "(" ++ show a ++ ", " ++ b ++ ", " ++ show c ++ ")" diff --git a/src/Language/Trans/SpecAnalysis.hs b/src/Language/Trans/SpecAnalysis.hs deleted file mode 100644 --- a/src/Language/Trans/SpecAnalysis.hs +++ /dev/null @@ -1,312 +0,0 @@ --- Copyright 2024 United States Government as represented by the Administrator --- of the National Aeronautics and Space Administration. All Rights Reserved. --- --- Disclaimers --- --- Licensed under the Apache License, Version 2.0 (the "License"); you may --- not use this file except in compliance with the License. You may obtain a --- copy of the License at --- --- https://www.apache.org/licenses/LICENSE-2.0 --- --- Unless required by applicable law or agreed to in writing, software --- distributed under the License is distributed on an "AS IS" BASIS, WITHOUT --- WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the --- License for the specific language governing permissions and limitations --- under the License. - --- | Formally analyze specifications and provide information about them. -module Language.Trans.SpecAnalysis - ( AnalysisResult(..) - , specAnalyze - ) - where - --- External imports -import qualified Copilot.Core as Core -import qualified Copilot.Language as Copilot -import qualified Copilot.Language.Reify as Copilot -import Copilot.Theorem.What4 (SatResult (..), Solver (Z3), - prove) -import Data.List (intercalate, lookup) -import Data.Maybe (fromMaybe) -import qualified Language.Haskell.Interpreter as HI - --- External imports: auxiliary -import Data.String.Extra (sanitizeLCIdentifier, sanitizeUCIdentifier) - --- External imports: ogma-spec -import Data.OgmaSpec (ExternalVariableDef (..), InternalVariableDef (..), - Requirement (..), Spec (..)) - --- * Analysis of Specs - --- | Result of analyzing a specification. -data AnalysisResult = AnalysisResult - { numAlwaysTrue :: Int -- ^ Number of always true requirements. - , numAlwaysFalse :: Int -- ^ Number of always false requirements. - , consistent :: Bool -- ^ Whether requirements are mutually consistent. - } - --- | Formally analyze a specification for redundancies, conflicts, etc. -specAnalyze :: [(String, String)] -- Type substitution table - -> ([(String, String)] -> a -> a) -- Expr substitution function - -> (a -> String) -- Expr show function - -> Spec a -- Specification - -> IO (Either String AnalysisResult) -specAnalyze typeMaps exprTransform showExpr spec = do - let structuredSpec = - spec2Copilot typeMaps exprTransform showExpr spec - - coreSpec <- reifySpec defaultSpecImports $ showSpec structuredSpec - - let properties = zip propertyNames propertyGuards - propertyNames = map (\(_, p, _, _, _) -> p) - $ copilotProperties structuredSpec - propertyGuards = map Core.triggerGuard $ Core.specTriggers coreSpec - - constantProperties <- mapM (uncurry $ exprIsConstant coreSpec) properties - - let numTrue = length $ filter fst constantProperties - numFalse = length $ filter snd constantProperties - - let negatedConjunction = Core.Op1 Core.Not - $ foldr (Core.Op2 Core.And) true propertyGuards - true = Core.Const Core.Bool True - - provedNegatedConjunction <- - exprIsConstant coreSpec "ogma_inc" negatedConjunction - - -- The requirements are considered consistent if it was *not* possible to - -- prove that their conjunction is always false. - let consistent = not $ fst provedNegatedConjunction - - return $ Right $ AnalysisResult numTrue numFalse consistent - --- * Auxiliary - --- ** Structured Copilot specifications - --- | A structured Copilot specification. -data CopilotSpec = CopilotSpec - { copilotProperties :: [(String, String, String, String, String)] - -- ^ Requirement name, property name, handler name, - -- implementation and arguments. - - , copilotAuxDefs :: [(String, String, String)] - -- ^ Name, type, implementation - } - --- | Given a 'Spec', return a structured version the corresponding Copilot spec --- that differentiates between the auxiliary definitions (inputs, outputs) and --- the properties or requirements to check. --- --- 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, String)] -- Type substitution table - -> ([(String, String)] -> a -> a) -- Expr substitution function - -> (a -> String) -- Expr show function - -> Spec a -- Specification - -> CopilotSpec -spec2Copilot typeMaps exprTransform showExpr spec = CopilotSpec reqs auxDefs - where - -- Encoding of requirements as boolean streams - reqs :: [(String, String, String, String, String)] - reqs = map reqToDecl (requirements spec) - where - reqToDecl i = - ( reqName - , propName - , handlerName - , reqBody nameSubstitutions - , handlerArg - ) - where - reqName = requirementName i - - propName = safeMap nameSubstitutions (requirementName i) - - handlerName = "handler" ++ sanitizeUCIdentifier (requirementName i) - - -- Definition implementation. We use an auxiliary function to - -- transform the implementation into Copilot, applying a - -- substitution. - reqBody subs = showExpr (exprTransform subs (requirementExpr i)) - - handlerArg = - case (requirementResultType i, requirementResultExpr i) of - (Just _, Just ex) -> "[ arg (" ++ showExpr ex ++ " ) ]" - _ -> "[]" - - auxDefs :: [(String, String, String)] - auxDefs = externs ++ internals - - externs :: [(String, String, String)] - externs = map externVarToDecl (externalVariables spec) - where - externVarToDecl i = (propName, streamType, implementation) - where - propName = safeMap nameSubstitutions (externalVariableName i) - - streamType = "Stream " ++ "(" ++ valueType ++ ")" - valueType = safeMap typeMaps (externalVariableType i) - - implementation = "extern" ++ " " ++ show (externalVariableName i) - ++ " " ++ "Nothing" - - -- Internal stream definitions - internals :: [(String, String, String)] - internals = map internalVarToDecl (internalVariables spec) - where - internalVarToDecl i = (propName, streamType, implementation) - where - propName = safeMap nameSubstitutions (internalVariableName i) - - streamType = "Stream " ++ "(" ++ valueType ++ ")" - valueType = safeMap typeMaps (internalVariableType i) - - implementation = internalVariableExpr i - - nameSubstitutions = internalVariableMap - ++ externalVariableMap - ++ 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 input spec. - internalVariableNames = map internalVariableName - $ internalVariables spec - - externalVariableNames = map externalVariableName - $ externalVariables spec - - requirementNames = map requirementName - $ requirements spec - --- | Render a 'CopilotSpec' as a Haskell definition of a 'Copilot.Spec', --- listing the elements in the spec with the necessary indentation. --- --- The shown 'Copilot.Spec' has a list of top-level triggers, as well as --- several auxiliary definitions. -showSpec :: CopilotSpec -> String -showSpec spec = template ++ "\n" ++ extra ++ "\n" ++ triggers - where - -- Initial template used for analysis purposes. - template :: String - template = unlines - [ "do let" - , "" - , " clock :: Stream Int64" - , " clock = [0] ++ (clock + 1)" - , "" - , " ftp :: Stream Bool" - , " ftp = [True] ++ false" - , "" - , " pre :: Stream Bool -> Stream Bool" - , " pre = ([False] ++)" - , "" - , " tpre :: Stream Bool -> Stream Bool" - , " tpre = ([True] ++)" - , "" - , " notPreviousNot :: Stream Bool -> Stream Bool" - , " notPreviousNot = not . PTLTL.previous . not" - ] - - extra = unlines - $ intercalate [""] - $ map formatDef - $ copilotAuxDefs spec - - triggers = unlines - $ intercalate [""] - $ map formatTrigger - $ copilotProperties spec - - formatDef (n, t, i) = - map (" " ++) [ n ++ " :: " ++ t, n ++ " = " ++ i ] - - formatTrigger (_, _, h, g, a) = - map (" " ++) [ "trigger " ++ show h ++ " (" ++ g ++ ") " ++ a ] - --- | Default imports for a 'Spec' that was converted into a 'Copilot.Spec'. -defaultSpecImports :: [(String, Maybe String)] -defaultSpecImports = - [ ("Control.Monad.Writer", Nothing) - , ("Copilot.Language", Nothing) - , ("Copilot.Language.Spec", Nothing) - , ("Data.Functor.Identity", Nothing) - , ("Language.Copilot", Nothing) - , ("Copilot.Library.PTLTL", Just "PTLTL") - , ("Prelude", Just "P") - ] - --- ** Typechecking of Copilot specs - --- | Read a specification from a 'String' and reify it. --- --- This function receives a list of possibly qualified imports. -reifySpec :: [(String, Maybe String)] -> String -> IO Core.Spec -reifySpec imports specText = do - coreSpecE <- HI.runInterpreter $ do - HI.setImportsQ imports - copilotSpec <- HI.interpret specText (HI.as :: Copilot.Spec) - HI.liftIO $ Copilot.reify copilotSpec - - case coreSpecE of - Left err -> do putStrLn $ "Error: " ++ show err - error $ show err - - Right coreSpec -> return coreSpec - --- ** Analysis of Copilot specs - --- | Determine if a boolean expression is always 'True' or always 'False'. --- --- The first boolean in the result is 'True' if the expression can be proven --- always 'True'. The second boolean in the expression is 'True' is the --- expression can be proven always 'False'. --- --- They values in the tuple cannot both 'True' at the same time. -exprIsConstant :: Core.Spec - -> Core.Name - -> Core.Expr Bool - -> IO (Bool, Bool) -exprIsConstant spec name expr = do - r1 <- propIsValid spec name (Core.Forall expr) - r2 <- propIsValid spec name (Core.Forall (Core.Op1 Core.Not expr)) - pure (r1, r2) - --- | 'True' if the Copilot 'Prop' with the given name and expression is --- constantly 'True', or valid, and 'False' otherwise (not always 'True' or --- unknown). -propIsValid :: Core.Spec - -> Core.Name - -> Core.Prop - -> IO Bool -propIsValid spec name expr = - maybe False isValid . lookup name <$> prove Z3 spec' - where - spec' = spec { Core.specProperties = prop' : Core.specProperties spec } - prop' = Core.Property name expr - - isValid :: SatResult -> Bool - isValid Valid = True - isValid _ = False - --- ** Auxiliary list functions - --- | Substitute a key based on a given substitution table from key to --- alternative key. --- --- They key is left unchanged if it cannot be found in the substitution table. -safeMap :: Eq k => [(k, k)] -> k -> k -safeMap ls k = fromMaybe k $ lookup k ls diff --git a/src/Language/YAMLSpec/Parser.hs b/src/Language/YAMLSpec/Parser.hs new file mode 100644 --- /dev/null +++ b/src/Language/YAMLSpec/Parser.hs @@ -0,0 +1,215 @@ +{-# LANGUAGE ScopedTypeVariables #-} +-- Copyright 2024 United States Government as represented by the Administrator +-- of the National Aeronautics and Space Administration. All Rights Reserved. +-- +-- Disclaimers +-- +-- Licensed under the Apache License, Version 2.0 (the "License"); you may +-- not use this file except in compliance with the License. You may obtain a +-- copy of the License at +-- +-- https://www.apache.org/licenses/LICENSE-2.0 +-- +-- Unless required by applicable law or agreed to in writing, software +-- distributed under the License is distributed on an "AS IS" BASIS, WITHOUT +-- WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the +-- License for the specific language governing permissions and limitations +-- under the License. + +-- | Parser for Ogma specs stored in YAML files. +module Language.YAMLSpec.Parser where + +-- External imports +import Control.Monad.Except (ExceptT (..), runExceptT) +import Control.Monad.IO.Class (liftIO) +import Data.Aeson (Value (..)) +import Data.Aeson.Key (fromString) +import qualified Data.Aeson.KeyMap as M +import qualified Data.ByteString as BS +import Data.Char (isSpace) +import Data.List (intercalate) +import Data.Text (unpack) +import qualified Data.Vector as V +import qualified Data.Yaml as Y + +-- External imports: ogma-spec +import Data.Either.Extra (mapLeft) +import Data.OgmaSpec (ExternalVariableDef (..), InternalVariableDef (..), + Requirement (..), Spec (..)) + +-- | Field names of a spec listed in a YAML file. +data YAMLFormat = YAMLFormat + { specInternalVars :: Maybe String + , specInternalVarId :: String + , specInternalVarExpr :: String + , specInternalVarType :: Maybe String + , specExternalVars :: Maybe String + , specExternalVarId :: String + , specExternalVarType :: Maybe String + , specRequirements :: Maybe String + , specRequirementId :: Maybe String + , specRequirementDesc :: Maybe String + , specRequirementExpr :: String + , specRequirementResultType :: Maybe String + , specRequirementResultExpr :: Maybe String + } + deriving (Read) + +-- | Parse a spec from a YAML file. +parseYAMLSpec :: forall a + . (String -> IO (Either String a)) + -> YAMLFormat + -> BS.ByteString + -> IO (Either String (Spec a)) +parseYAMLSpec parseExpr yamlFormat bs = runExceptT $ do + value <- except $ mapLeft Y.prettyPrintParseException $ Y.decodeEither' bs + + let values :: [Value] + values = maybe [] (objectFieldValueList value) (specInternalVars yamlFormat) + + internalVarDef :: Value -> Either String InternalVariableDef + internalVarDef value = do + let msg = "internal variable name" + varId <- valueToString msg =<< listToEither msg (objectFieldValues (specInternalVarId yamlFormat) value) + + let msg = "internal variable type" + varType <- maybe (Right "") (\e -> valueToString msg =<< (listToEither msg (objectFieldValues e value))) (specInternalVarType yamlFormat) + + let msg = "internal variable expr" + varExpr <- valueToString msg =<< listToEither msg (objectFieldValues (specInternalVarExpr yamlFormat) value) + + return $ InternalVariableDef + { internalVariableName = varId + , internalVariableType = varType + , internalVariableExpr = varExpr + } + + internalVariableDefs <- except $ mapM internalVarDef values + + let values :: [Value] + values = maybe [] (objectFieldValueList value) (specExternalVars yamlFormat) + + externalVarDef :: Value -> Either String ExternalVariableDef + externalVarDef value = do + + let msg = "external variable name" + varId <- valueToString msg + =<< listToEither msg (objectFieldValues (specExternalVarId yamlFormat) value) + + let msg = "external variable type" + varType <- maybe (Right "") (\e -> valueToString msg =<< (listToEither msg (objectFieldValues e value))) (specExternalVarType yamlFormat) + + return $ ExternalVariableDef + { externalVariableName = varId + , externalVariableType = varType + } + + externalVariableDefs <- except $ mapM externalVarDef values + + let values :: [Value] + values = maybe [value] (objectFieldValueList value) (specRequirements yamlFormat) + + requirementDef value = do + let msg = "Requirement name" + reqId <- except $ maybe (Right "") (\e -> valueToString msg =<< (listToEither msg (objectFieldValues e value))) (specRequirementId yamlFormat) + + let msg = "Requirement expression" + reqExpr <- except $ valueToString msg =<< listToEither msg (objectFieldValues (specRequirementExpr yamlFormat) value) + reqExpr' <- ExceptT $ parseExpr reqExpr + + let msg = "Requirement description" + reqDesc <- except $ maybe (Right "") (\e -> valueToString msg =<< (listToEither msg (objectFieldValues e value))) (specRequirementDesc yamlFormat) + let reqDesc' = cleanString reqDesc + + let msg = "Requirement result type" + ty :: Maybe (Either String String) + ty = (\e -> valueToString msg =<< (listToEither msg (objectFieldValues e value))) <$> (specRequirementResultType yamlFormat) + reqResType <- except $ maybeEither ty + + let msg = "Requirement result expression" + resultExpr :: Maybe (Either String String) + resultExpr = (\e -> valueToString msg =<< (listToEither msg (objectFieldValues e value))) <$> (specRequirementResultExpr yamlFormat) + + reqResExpr <- except $ maybeEither resultExpr + reqResExpr' <- ExceptT $ case reqResExpr of + Nothing -> return $ Right Nothing + Just x -> fmap Just <$> parseExpr x + + return $ Requirement + { requirementName = reqId + , requirementExpr = reqExpr' + , requirementDescription = reqDesc' + , requirementResultType = reqResType + , requirementResultExpr = reqResExpr' + } + + requirements <- mapM requirementDef values + + return $ Spec internalVariableDefs externalVariableDefs requirements + +-- * Auxiliary functions + +-- ** JSON functions + +-- | Convert a string JSON value into a 'String'. +valueToString :: String -> Value -> Either String String +valueToString msg (String x) = Right $ unpack x +valueToString msg _ = Left $ "The YAML value provided for " ++ msg ++ " does not contain a string" + +-- | Object the values associated to a key of an object. +-- +-- If the values are an array, it returns the values in the array directly. +objectFieldValueList :: Value -> String -> [Value] +objectFieldValueList (Object o) key = + case M.lookup (fromString key) o of + Just (Array arr) -> V.toList arr + Just v -> [v] + Nothing -> [] +objectFieldValueList _ _ = [] + +-- | Object the values associated to a key of an object. +-- +-- If the values are an array, it returns the values in the array directly. +objectFieldValues :: String -> Value -> [Value] +objectFieldValues key (Object o) = maybe [] (:[]) $ M.lookup (fromString key) o +objectFieldValues _ _ = [] + +-- ** Either-related auxiliary functions + +-- | Convert a string into an Either value. +-- +-- Fails if there more or less than one value in the list. +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 + +-- | Wrap an 'Either' value in an @ExceptT m@ monad. +except :: Monad m => Either e a -> ExceptT e m a +except = ExceptT . return + +-- | Swap the order in a Maybe and an Either monad. +maybeEither :: Maybe (Either a b) -> Either a (Maybe b) +maybeEither Nothing = Right Nothing +maybeEither (Just e) = fmap Just e + +-- ** String-related auxiliary functions + +-- | Remove trailing spaces and lines from a multi-line string. +cleanString :: String -> String +cleanString = + unlines' + . dropWhile null + . dropWhileEnd null + . map strip + . lines + where + strip = dropWhile isSpace . dropWhileEnd isSpace + dropWhileEnd x = reverse . dropWhile x . reverse + +-- | Concatenate a list of strings into one string, separated by a line ending. +-- +-- This variant of 'unlines' does not add a line break at the end of the last +-- line. +unlines' :: [String] -> String +unlines' = intercalate "\n" diff --git a/templates/cfs/copilot/fsw/src/Properties.hs b/templates/cfs/copilot/fsw/src/Properties.hs --- a/templates/cfs/copilot/fsw/src/Properties.hs +++ b/templates/cfs/copilot/fsw/src/Properties.hs @@ -34,6 +34,31 @@ notPreviousNot :: Stream Bool -> Stream Bool notPreviousNot = not . PTLTL.previous . not +-- Initial state, final state, no transition signal, transitions, bad state +type StateMachineGF a = (a, a, Stream Bool, [(a, Stream Bool, a)], a) + +stateMachineGF :: (Eq a, Typed a) + => StateMachineGF a + -> Stream a +stateMachineGF (initial, final, noInputData, transitions, bad) = + state + where + state = ifThenElses transitions + previousState = [initial] ++ state + + -- ifThenElses :: [(a, Stream Bool, a)] -> Stream a + ifThenElses [] = + ifThenElse + (previousState == constant final && noInputData) + (constant final) + (constant bad) + + ifThenElses ((s1, i, s2):ss) = + ifThenElse + (previousState == constant s1 && i) + (constant s2) + (ifThenElses ss) + -- | Complete specification. Calls C handler functions when properties are -- violated. spec :: Spec diff --git a/templates/diagram/Copilot.hs b/templates/diagram/Copilot.hs --- a/templates/diagram/Copilot.hs +++ b/templates/diagram/Copilot.hs @@ -24,7 +24,7 @@ -- violated. spec :: Spec spec = do - trigger "handler" stateMachineProp {{{handlerInputs}}} +{{{triggers}}} main :: IO () main = reify spec >>= compile "{{{specName}}}" diff --git a/templates/report/Report.md b/templates/report/Report.md new file mode 100644 --- /dev/null +++ b/templates/report/Report.md @@ -0,0 +1,67 @@ +{{#commandDiagramsAny}} +# Diagrams + +{{#commandDiagramList}} +## Diagram + +The diagram: + - Has {{summaryDiagramNumStates}} states. +{{#summaryDiagramDeterministic}} + - Is deterministic. +{{/summaryDiagramDeterministic}} +{{^summaryDiagramDeterministic}} + - Is not deterministic. +{{/summaryDiagramDeterministic}} + +{{/commandDiagramList}} +{{/commandDiagramsAny}} +{{#commandRequirementsAny}} +# Requirements + +## Summary + +The project has {{commandRequirements}} requirements in total. + +Of these requirements: + +- {{commandRequirementsTrue}} requirements are constantly or always true. + +- {{commandRequirementsFalse}} requirements are constantly or always false. + +{{#commandRequirementsConsistent}} +No inconsistencies detected in the requirements. +{{/commandRequirementsConsistent}} +{{^commandRequirementsConsistent}} +The requirements are not mutually consistent: there is no way for all +requirements to be true at the same time. +{{/commandRequirementsConsistent}} + +The requirements mention: + +- {{commandExternalVariables}} external variables. + +- {{commandInternalVariables}} internal variables. + +## Detailed list + +{{#commandRequirementList}} +### {{summaryRequirementName}} + +**Description:** {{summaryRequirementDesc}} + +**Properties:** + +{{#summaryRequirementTrue}} +- The requirement is always true or vacuously true. +{{/summaryRequirementTrue}} +{{#summaryRequirementFalse}} +- The requirement is always false or vacuously false. +{{/summaryRequirementFalse}} +{{^summaryRequirementTrue}} +{{^summaryRequirementFalse}} +- None. +{{/summaryRequirementFalse}} +{{/summaryRequirementTrue}} + +{{/commandRequirementList}} +{{/commandRequirementsAny}} diff --git a/templates/ros/copilot/src/Copilot.hs b/templates/ros/copilot/src/Copilot.hs --- a/templates/ros/copilot/src/Copilot.hs +++ b/templates/ros/copilot/src/Copilot.hs @@ -34,6 +34,31 @@ notPreviousNot :: Stream Bool -> Stream Bool notPreviousNot = not . PTLTL.previous . not +-- Initial state, final state, no transition signal, transitions, bad state +type StateMachineGF a = (a, a, Stream Bool, [(a, Stream Bool, a)], a) + +stateMachineGF :: (Eq a, Typed a) + => StateMachineGF a + -> Stream a +stateMachineGF (initial, final, noInputData, transitions, bad) = + state + where + state = ifThenElses transitions + previousState = [initial] ++ state + + -- ifThenElses :: [(a, Stream Bool, a)] -> Stream a + ifThenElses [] = + ifThenElse + (previousState == constant final && noInputData) + (constant final) + (constant bad) + + ifThenElses ((s1, i, s2):ss) = + ifThenElse + (previousState == constant s1 && i) + (constant s2) + (ifThenElses ss) + -- | Complete specification. Calls C handler functions when properties are -- violated. spec :: Spec diff --git a/templates/standalone/Copilot.hs b/templates/standalone/Copilot.hs --- a/templates/standalone/Copilot.hs +++ b/templates/standalone/Copilot.hs @@ -33,6 +33,31 @@ notPreviousNot :: Stream Bool -> Stream Bool notPreviousNot = not . PTLTL.previous . not +-- Initial state, final state, no transition signal, transitions, bad state +type StateMachineGF a = (a, a, Stream Bool, [(a, Stream Bool, a)], a) + +stateMachineGF :: (Eq a, Typed a) + => StateMachineGF a + -> Stream a +stateMachineGF (initial, final, noInputData, transitions, bad) = + state + where + state = ifThenElses transitions + previousState = [initial] ++ state + + -- ifThenElses :: [(a, Stream Bool, a)] -> Stream a + ifThenElses [] = + ifThenElse + (previousState == constant final && noInputData) + (constant final) + (constant bad) + + ifThenElses ((s1, i, s2):ss) = + ifThenElse + (previousState == constant s1 && i) + (constant s2) + (ifThenElses ss) + -- | Complete specification. Calls C handler functions when properties are -- violated. spec :: Spec diff --git a/tests/Main.hs b/tests/Main.hs --- a/tests/Main.hs +++ b/tests/Main.hs @@ -104,7 +104,7 @@ targetDir <- getTemporaryDirectory let opts = CommandOptions { commandConditionExpr = Nothing - , commandInputFile = Just file + , commandInputFiles = [ file ] , commandFormat = "fcs" , commandPropFormat = "smv" , commandTypeMapping = [("int", "Int64"), ("real", "Float")] @@ -142,7 +142,7 @@ targetDir <- getTemporaryDirectory let opts = CommandOptions { commandConditionExpr = Nothing - , commandInputFile = Just file + , commandInputFiles = [ file ] , commandFormat = "fdb" , commandPropFormat = "lustre" , commandTypeMapping = []