ogma-core 1.13.0 → 1.14.0

raw patch · 32 files changed

+2484/−1062 lines, 32 filesdep +vectordep +yamldep ~QuickCheckdep ~copilot-coredep ~copilot-languagePVP ok

version bump matches the API change (PVP)

Dependencies added: vector, yaml

Dependency ranges changed: QuickCheck, copilot-core, copilot-language, copilot-theorem, megaparsec, ogma-extra, ogma-language-c, ogma-language-copilot, ogma-language-csv, ogma-language-jsonspec, ogma-language-lustre, ogma-language-smv, ogma-language-xlsx, ogma-language-xmlspec, ogma-spec

API changes (from Hackage documentation)

Files

• CHANGELOG.md +27/−0
• ogma-core.cabal +35/−17
• src/Command/CFSApp.hs +44/−13
• src/Command/Common.hs +72/−237
• src/Command/Diagram.hs +60/−365
• src/Command/FPrimeApp.hs +45/−13
• src/Command/Overview.hs +37/−40
• src/Command/ROSApp.hs +45/−13
• src/Command/Report.hs +235/−0
• src/Command/Standalone.hs +55/−49
• src/Copilot/Core/Analysis.hs +59/−0
• src/Copilot/Language/Reify/Extra.hs +43/−0
• src/Data/Aeson/Extra.hs +34/−0
• src/Data/Diagram.hs +59/−0
• src/Data/Diagram/Analysis.hs +153/−0
• src/Data/Diagram/Parser.hs +81/−0
• src/Data/Diagram/Parser/Dot.hs +66/−0
• src/Data/Diagram/Parser/Mermaid.hs +181/−0
• src/Data/Either/Extra.hs +35/−0
• src/Data/ExprPair.hs +106/−0
• src/Data/Spec/Analysis.hs +267/−0
• src/Data/Spec/Extra.hs +46/−0
• src/Data/Spec/Parser.hs +218/−0
• src/Language/Trans/Diagram2Copilot.hs +121/−0
• src/Language/Trans/SpecAnalysis.hs +0/−312
• src/Language/YAMLSpec/Parser.hs +215/−0
• templates/cfs/copilot/fsw/src/Properties.hs +25/−0
• templates/diagram/Copilot.hs +1/−1
• templates/report/Report.md +67/−0
• templates/ros/copilot/src/Copilot.hs +25/−0
• templates/standalone/Copilot.hs +25/−0
• tests/Main.hs +2/−2

@@ -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).

@@ -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

@@ -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

@@ -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

@@ -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) "<input>" 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."

@@ -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

@@ -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)

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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"

@@ -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

@@ -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"+  ]

@@ -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

@@ -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

@@ -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) "<input>" 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

@@ -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

@@ -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."

@@ -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

@@ -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)

@@ -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

@@ -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 ++ ")"

@@ -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

@@ -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"

@@ -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

@@ -24,7 +24,7 @@ -- violated. spec :: Spec spec = do-  trigger "handler" stateMachineProp {{{handlerInputs}}}+{{{triggers}}}  main :: IO () main = reify spec >>= compile "{{{specName}}}"

@@ -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}}

@@ -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

@@ -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

@@ -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 = []