ogma-core 1.5.0 → 1.6.0
raw patch · 18 files changed
+1643/−625 lines, 18 filesdep +containersdep +directorydep +graphvizdep ~HUnitdep ~QuickCheckdep ~base
Dependencies added: containers, directory, graphviz, megaparsec, ogma-language-xmlspec, process
Dependency ranges changed: HUnit, QuickCheck, base, bytestring, filepath, mtl, ogma-extra, ogma-language-c, ogma-language-cocospec, ogma-language-copilot, ogma-language-jsonspec, ogma-language-smv, ogma-spec, test-framework, test-framework-hunit, test-framework-quickcheck2
Files
- CHANGELOG.md +14/−0
- data/formats/xml-md_cocospec +13/−0
- data/formats/xml-md_smv +13/−0
- data/formats/xml-reqif_cocospec +13/−0
- data/formats/xml-reqif_smv +13/−0
- ogma-core.cabal +40/−17
- src/Command/Diagram.hs +462/−0
- src/Command/FPrimeApp.hs +301/−350
- src/Command/ROSApp.hs +228/−84
- src/Command/Standalone.hs +145/−34
- src/Language/Trans/Spec2Copilot.hs +27/−105
- templates/diagram/Copilot.hs +77/−0
- templates/fprime/Copilot.cpp +78/−0
- templates/fprime/Copilot.fpp +71/−0
- templates/fprime/Copilot.hpp +66/−0
- templates/fprime/instance-copilot +1/−1
- templates/standalone/Copilot.hs +40/−0
- tests/Main.hs +41/−34
CHANGELOG.md view
@@ -1,5 +1,19 @@ # Revision history for ogma-core +## [1.6.0] - 2025-01-21++* Version bump 1.6.0 (#208).+* Replace queueSize with QUEUE_SIZE in FPP file (#186).+* Use template expansion system to generate F' monitoring component (#185).+* Use template expansion system to generate standalone Copilot monitor (#189).+* Add repository information to cabal package (#148).+* Add version bounds to all dependencies (#119).+* Add command to transform state diagrams into monitors (#194).+* Extend standalone command to use external process to parse properties (#197).+* Enable using user-provided file as format definition spec (#200).+* Add support for XML files to standalone backend (#202).+* Extend support for file, property formats across backends (#204).+ ## [1.5.0] - 2024-11-21 * Version bump 1.5.0 (#178).
+ data/formats/xml-md_cocospec view
@@ -0,0 +1,13 @@+XMLFormat+ { XML.specInternalVars = Nothing+ , XML.specInternalVarId = ("//*", Nothing)+ , XML.specInternalVarExpr = ("//*", Nothing)+ , XML.specInternalVarType = Nothing+ , XML.specExternalVars = Nothing+ , XML.specExternalVarId = ("//*", Nothing)+ , XML.specExternalVarType = Nothing+ , XML.specRequirements = ("//sysml:Requirement", Nothing)+ , XML.specRequirementId = ("//sysml:Requirement/@Id/text()", Nothing)+ , XML.specRequirementDesc = Just ("//sysml:Requirement/@Id/text()", Nothing)+ , XML.specRequirementExpr = ("//sysml:Requirement/@Text/text()", Nothing)+ }
+ data/formats/xml-md_smv view
@@ -0,0 +1,13 @@+XMLFormat+ { XML.specInternalVars = Nothing+ , XML.specInternalVarId = ("//*", Nothing)+ , XML.specInternalVarExpr = ("//*", Nothing)+ , XML.specInternalVarType = Nothing+ , XML.specExternalVars = Nothing+ , XML.specExternalVarId = ("//*", Nothing)+ , XML.specExternalVarType = Nothing+ , XML.specRequirements = ("//sysml:Requirement", Nothing)+ , XML.specRequirementId = ("//sysml:Requirement/@Id/text()", Nothing)+ , XML.specRequirementDesc = Just ("//sysml:Requirement/@Id/text()", Nothing)+ , XML.specRequirementExpr = ("//sysml:Requirement/@Text/text()", Nothing)+ }
+ data/formats/xml-reqif_cocospec view
@@ -0,0 +1,13 @@+XMLFormat+ { specInternalVars = Nothing+ , specInternalVarId = ("//*", Nothing)+ , specInternalVarExpr = ("//*", Nothing)+ , specInternalVarType = Nothing+ , specExternalVars = Nothing+ , specExternalVarId = ("//*", Nothing)+ , specExternalVarType = Nothing+ , specRequirements = ("//SPEC-OBJECTS/SPEC-OBJECT/TYPE/SPEC-OBJECT-TYPE-REF[contains(text(),\"KEY\")]/../..", Just ("KEY", "//SPEC-OBJECT-TYPE[contains(@LONG-NAME, \"Requirement\")]/@IDENTIFIER/text()"))+ , specRequirementId = ("//SPEC-OBJECT/@IDENTIFIER/text()", Nothing)+ , specRequirementDesc = Just ("//ATTRIBUTE-VALUE-XHTML/DEFINITION/ATTRIBUTE-DEFINITION-XHTML-REF[contains(text(),'KEY')]/../../THE-VALUE/div/*", Just ("KEY", "//ATTRIBUTE-DEFINITION-XHTML[contains(@LONG-NAME, \"ReqIF.Name\")]/@IDENTIFIER/text()"))+ , specRequirementExpr = ("//ATTRIBUTE-VALUE-XHTML/DEFINITION/ATTRIBUTE-DEFINITION-XHTML-REF[contains(text(),'KEY')]/../../THE-VALUE/div/*", Just ("KEY", "//ATTRIBUTE-DEFINITION-XHTML[contains(@LONG-NAME, \"ReqIF.Text\")]/@IDENTIFIER/text()"))+ }
+ data/formats/xml-reqif_smv view
@@ -0,0 +1,13 @@+XMLFormat+ { specInternalVars = Nothing+ , specInternalVarId = ("//*", Nothing)+ , specInternalVarExpr = ("//*", Nothing)+ , specInternalVarType = Nothing+ , specExternalVars = Nothing+ , specExternalVarId = ("//*", Nothing)+ , specExternalVarType = Nothing+ , specRequirements = ("//SPEC-OBJECTS/SPEC-OBJECT/TYPE/SPEC-OBJECT-TYPE-REF[contains(text(),\"KEY\")]/../..", Just ("KEY", "//SPEC-OBJECT-TYPE[contains(@LONG-NAME, \"Requirement\")]/@IDENTIFIER/text()"))+ , specRequirementId = ("//SPEC-OBJECT/@IDENTIFIER/text()", Nothing)+ , specRequirementDesc = Just ("//ATTRIBUTE-VALUE-XHTML/DEFINITION/ATTRIBUTE-DEFINITION-XHTML-REF[contains(text(),'KEY')]/../../THE-VALUE/div/*", Just ("KEY", "//ATTRIBUTE-DEFINITION-XHTML[contains(@LONG-NAME, \"ReqIF.Name\")]/@IDENTIFIER/text()"))+ , specRequirementExpr = ("//ATTRIBUTE-VALUE-XHTML/DEFINITION/ATTRIBUTE-DEFINITION-XHTML-REF[contains(text(),'KEY')]/../../THE-VALUE/div/*", Just ("KEY", "//ATTRIBUTE-DEFINITION-XHTML[contains(@LONG-NAME, \"ReqIF.Text\")]/@IDENTIFIER/text()"))+ }
ogma-core.cabal view
@@ -32,8 +32,9 @@ build-type: Simple name: ogma-core-version: 1.5.0+version: 1.6.0 homepage: https://github.com/nasa/ogma+bug-reports: https://github.com/nasa/ogma/issues license: OtherLicense license-file: LICENSE.pdf author: Ivan Perez, Alwyn Goodloe@@ -65,13 +66,22 @@ templates/ros/copilot/src/copilot_logger.cpp templates/ros/copilot/src/copilot_monitor.cpp templates/ros/copilot/package.xml+ templates/diagram/Copilot.hs templates/fprime/CMakeLists.txt+ templates/fprime/Copilot.cpp+ templates/fprime/Copilot.fpp+ templates/fprime/Copilot.hpp templates/fprime/Dockerfile templates/fprime/instance-copilot+ templates/standalone/Copilot.hs data/formats/fcs_smv data/formats/fcs_cocospec data/formats/fdb_smv data/formats/fdb_cocospec+ data/formats/xml-md_cocospec+ data/formats/xml-md_smv+ data/formats/xml-reqif_cocospec+ data/formats/xml-reqif_smv -- Ogma packages should be uncurated so that only the official maintainers make -- changes.@@ -80,12 +90,18 @@ -- exactly what we publish, unmodified by anyone external to our project. x-curation: uncurated +source-repository head+ type: git+ location: git@github.com:nasa/ogma.git+ subdir: ogma-core+ library exposed-modules: Command.CFSApp Command.CStructs2Copilot Command.CStructs2MsgHandlers+ Command.Diagram Command.FPrimeApp Command.Result Command.ROSApp@@ -109,18 +125,24 @@ build-depends: base >= 4.11.0.0 && < 5 , aeson >= 2.0.0.0 && < 2.2- , bytestring- , filepath- , mtl+ , bytestring >= 0.10.8.2 && < 0.13+ , containers >= 0.5 && < 0.8+ , directory >= 1.3.1.5 && < 1.4+ , filepath >= 1.4.2 && < 1.6+ , graphviz >= 2999.20 && < 2999.21+ , megaparsec >= 8.0.0 && < 9.10+ , mtl >= 2.2.2 && < 2.4+ , process >= 1.6 && < 1.7 , text >= 1.2.3.1 && < 2.1 - , ogma-extra >= 1.5.0 && < 1.6- , ogma-language-c >= 1.5.0 && < 1.6- , ogma-language-cocospec >= 1.5.0 && < 1.6- , ogma-language-copilot >= 1.5.0 && < 1.6- , ogma-language-jsonspec >= 1.5.0 && < 1.6- , ogma-language-smv >= 1.5.0 && < 1.6- , ogma-spec >= 1.5.0 && < 1.6+ , ogma-extra >= 1.6.0 && < 1.7+ , ogma-language-c >= 1.6.0 && < 1.7+ , ogma-language-cocospec >= 1.6.0 && < 1.7+ , ogma-language-copilot >= 1.6.0 && < 1.7+ , ogma-language-jsonspec >= 1.6.0 && < 1.7+ , ogma-language-smv >= 1.6.0 && < 1.7+ , ogma-language-xmlspec >= 1.6.0 && < 1.7+ , ogma-spec >= 1.6.0 && < 1.7 hs-source-dirs: src@@ -139,12 +161,13 @@ Main.hs build-depends:- base- , HUnit- , QuickCheck- , test-framework- , test-framework-hunit- , test-framework-quickcheck2+ 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+ , test-framework >= 0.8.2 && < 0.9+ , test-framework-hunit >= 0.2.0 && < 0.4+ , test-framework-quickcheck2 >= 0.3.0.4 && < 0.4 , ogma-core
+ src/Command/Diagram.hs view
@@ -0,0 +1,462 @@+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE OverloadedStrings #-}+-- Copyright 2024 United States Government as represented by the Administrator+-- of the National Aeronautics and Space Administration. All Rights Reserved.+--+-- Disclaimers+--+-- No Warranty: THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY+-- OF ANY KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT+-- LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO+-- SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR A+-- PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT THE+-- SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT DOCUMENTATION, IF+-- PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE. THIS AGREEMENT DOES NOT, IN+-- ANY MANNER, CONSTITUTE AN ENDORSEMENT BY GOVERNMENT AGENCY OR ANY PRIOR+-- RECIPIENT OF ANY RESULTS, RESULTING DESIGNS, HARDWARE, SOFTWARE PRODUCTS OR+-- ANY OTHER APPLICATIONS RESULTING FROM USE OF THE SUBJECT SOFTWARE. FURTHER,+-- GOVERNMENT AGENCY DISCLAIMS ALL WARRANTIES AND LIABILITIES REGARDING+-- THIRD-PARTY SOFTWARE, IF PRESENT IN THE ORIGINAL SOFTWARE, AND DISTRIBUTES+-- IT "AS IS."+--+-- Waiver and Indemnity: RECIPIENT AGREES TO WAIVE ANY AND ALL CLAIMS AGAINST+-- THE UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS, AS WELL AS+-- ANY PRIOR RECIPIENT. IF RECIPIENT'S USE OF THE SUBJECT SOFTWARE RESULTS IN+-- ANY LIABILITIES, DEMANDS, DAMAGES, EXPENSES OR LOSSES ARISING FROM SUCH USE,+-- INCLUDING ANY DAMAGES FROM PRODUCTS BASED ON, OR RESULTING FROM, RECIPIENT'S+-- USE OF THE SUBJECT SOFTWARE, RECIPIENT SHALL INDEMNIFY AND HOLD HARMLESS THE+-- UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS, AS WELL AS ANY+-- PRIOR RECIPIENT, TO THE EXTENT PERMITTED BY LAW. RECIPIENT'S SOLE REMEDY+-- FOR ANY SUCH MATTER SHALL BE THE IMMEDIATE, UNILATERAL TERMINATION OF THIS+-- AGREEMENT.+--+-- | Transform a state diagram into a Copilot specification.+module Command.Diagram+ ( diagram+ , DiagramOptions(..)+ , DiagramFormat(..)+ , DiagramMode(..)+ , DiagramPropFormat(..)+ , ErrorCode+ )+ where++-- External imports+import Control.Exception as E+import Control.Monad (when)+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, 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+++-- External imports: auxiliary+import Data.ByteString.Extra as B ( safeReadFile )+import System.Directory.Extra ( copyTemplate )++-- External imports: parsing expressions.+import qualified Language.CoCoSpec.ParCoCoSpec as CoCoSpec (myLexer, pBoolSpec)+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)++-- Internal imports: language ASTs, transformers+import Language.SMV.Substitution (substituteBoolExpr)+import qualified Language.Trans.CoCoSpec2Copilot as CoCoSpec (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.+--+-- 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 @stateMachine@, @externalState@, @noneOf@,+-- @checkValidTransitions@, @main@, @spec@, @stateMachine1@, @clock@, @ftp@,+-- @notPreviousNot@. All identifiers used are valid C99 identifiers. The+-- template, if provided, exists and uses the variables needed by the diagram+-- application generator. The target directory is writable and there's enough+-- disk space to copy the files over.+diagram :: FilePath -- ^ Path to a file containing a diagram+ -> DiagramOptions -- ^ Customization options+ -> IO (Result ErrorCode)+diagram fp options = do+ E.handle (return . diagramTemplateError fp) $ do+ -- Sub-parser for edge expressions.+ let functions = exprPair (diagramPropFormat options)++ -- Convert the diagram into elements in a Copilot spec.+ copilotSpecElems <- diagram' fp options functions++ -- Convert the elements into a success or error result.+ let (mOutput, result) = diagramResult fp copilotSpecElems++ -- If the result is success, expand the template.+ for_ mOutput $ \(streamDefs, handlerInputs) -> do+ let subst = object+ [ "streamDefs" .= pack streamDefs+ , "specName" .= pack (diagramFilename options)+ , "input" .= pack (diagramInputVar options)+ , "state" .= pack (diagramStateVar options)+ , "handlerInputs" .= pack handlerInputs+ ]++ templateDir <- case diagramTemplateDir options of+ Just x -> return x+ Nothing -> do+ dataDir <- getDataDir+ return $ dataDir </> "templates" </> "diagram"++ let targetDir = diagramTargetDir options++ copyTemplate templateDir subst targetDir++ return result++-- | Generate a new Copilot monitor that implements a state machine described+-- in a diagram given as an input file, using a subexpression handler.+--+-- 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 @stateMachine@, @externalState@, @noneOf@,+-- @checkValidTransitions@, @main@, @spec@, @stateMachine1@, @clock@, @ftp@,+-- @notPreviousNot@. All identifiers used are valid C99 identifiers. The+-- template, if provided, exists and uses the variables needed by the diagram+-- application generator. The target directory is writable and there's enough+-- disk space to copy the files over.+diagram' :: FilePath+ -> DiagramOptions+ -> 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)++-- | Options used to customize the conversion of diagrams to Copilot code.+data DiagramOptions = DiagramOptions+ { diagramTargetDir :: FilePath+ , diagramTemplateDir :: Maybe FilePath+ , diagramFormat :: DiagramFormat+ , diagramPropFormat :: DiagramPropFormat+ , diagramFilename :: String+ , diagramMode :: DiagramMode+ , diagramStateVar :: String+ , 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 = CoCoSpec+ | Inputs+ | Literal+ | SMV+ deriving (Eq, Show)++-- * Error codes++-- | Encoding of reasons why the command can fail.+--+-- The error code used is 1 for user error.+type ErrorCode = Int++-- | Error: the input file cannot be read due to it being unreadable or the+-- format being incorrect.+ecDiagramError :: ErrorCode+ecDiagramError = 1++-- | Error: diagram component generation failed during the copy/write+-- process.+ecDiagramTemplateError :: ErrorCode+ecDiagramTemplateError = 2++-- * Result++-- | Process the result of the transformation function.+diagramResult :: FilePath+ -> Either String a+ -> (Maybe a, Result ErrorCode)+diagramResult fp result = case result of+ Left msg -> (Nothing, Error ecDiagramError msg (LocationFile fp))+ Right t -> (Just t, Success)++-- | Report an error when trying to open or copy the template.+diagramTemplateError :: FilePath+ -> E.SomeException+ -> Result ErrorCode+diagramTemplateError fp exception =+ Error ecDiagramTemplateError msg (LocationFile fp)+ where+ msg =+ "Diagram monitor generation failed during copy/write operation. Check"+ ++ " that there's free space in the disk and that you have the necessary"+ ++ " permissions to write in the destination directory. "+ ++ show exception++-- * 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 CoCoSpec = ExprPair (CoCoSpec.pBoolSpec . CoCoSpec.myLexer)+ (\_ -> id)+ CoCoSpec.boolSpec2Copilot+ CoCoSpec.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 a mermaid diagram.+--+-- This parser depends on an auxiliary parser for the expressions associated to+-- the edges or connections between states.+pDiagram :: ExprPair -> MermaidParser Diagram+pDiagram exprP = do+ _ <- string "graph" <* spaces+ _name <- T.pack <$> manyTill alphaNumChar (char ';')+ _ <- newline++ transitions <- many (pTransition 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.+pTransition :: ExprPair -> MermaidParser (Int, String, Int)+pTransition 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)++-- | Consume spaces+spaces :: MermaidParser ()+spaces = L.space space1 empty empty++-- * 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."
src/Command/FPrimeApp.hs view
@@ -1,3 +1,7 @@+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE MultiWayIf #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE ScopedTypeVariables #-} -- Copyright 2022 United States Government as represented by the Administrator -- of the National Aeronautics and Space Administration. All Rights Reserved. --@@ -35,70 +39,90 @@ module Command.FPrimeApp ( fprimeApp , ErrorCode+ , FPrimeAppOptions(..) ) where -- External imports import qualified Control.Exception as E-import Control.Monad.Except ( ExceptT, liftEither, liftIO, runExceptT,- throwError )-import Data.Aeson ( eitherDecode )+import Control.Monad.Except ( ExceptT(..), liftEither, liftIO,+ runExceptT, throwError )+import Data.Aeson ( eitherDecode, object, (.=) ) import Data.Char ( toUpper )-import Data.List ( find, intercalate, nub, sort )+import Data.List ( isInfixOf, isPrefixOf, find,+ intercalate, nub, sort ) import Data.Maybe ( fromMaybe )+import Data.Text.Lazy ( pack )+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 )-import System.Directory.Extra ( copyDirectoryRecursive )+import System.Directory.Extra ( copyTemplate ) -- External imports: ogma import Data.OgmaSpec (Spec, externalVariableName, externalVariables, requirementName, requirements) import Language.JSONSpec.Parser (JSONFormat (..), parseJSONSpec)+import Language.XMLSpec.Parser (parseXMLSpec) -- Internal imports: auxiliary import Command.Result ( Result (..) ) import Data.Location ( Location (..) ) +-- Internal imports: language ASTs, transformers+import qualified Language.CoCoSpec.AbsCoCoSpec as CoCoSpec+import qualified Language.CoCoSpec.ParCoCoSpec as CoCoSpec ( 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.CoCoSpec2Copilot as CoCoSpec (boolSpec2Copilot,+ boolSpecNames)+import Language.Trans.SMV2Copilot as SMV (boolSpec2Copilot,+ boolSpecNames)+ -- Internal imports import Paths_ogma_core ( getDataDir ) -- * FPrime component generation -- | Generate a new FPrime component connected to Copilot.-fprimeApp :: FilePath -- ^ Target directory where the component- -- should be created.- -> Maybe FilePath -- ^ FRET Component specification file.- -> Maybe FilePath -- ^ File containing a list of variables to make- -- available to Copilot.- -> Maybe FilePath -- ^ File containing a list of known variables- -- with their types and the message IDs they- -- can be obtained from.- -> Maybe FilePath -- ^ File containing a list of handlers used in the- -- Copilot specification. The handlers are assumed- -- to receive no arguments.+fprimeApp :: Maybe FilePath -- ^ Input specification file.+ -> FPrimeAppOptions -- ^ Options to the ROS backend. -> IO (Result ErrorCode)-fprimeApp targetDir fretCSFile varNameFile varDBFile handlersFile =- processResult $ do- cs <- parseOptionalFRETCS fretCSFile- vs <- parseOptionalVariablesFile varNameFile- rs <- parseOptionalRequirementsListFile handlersFile- varDB <- parseOptionalVarDBFile varDBFile+fprimeApp fp options =+ processResult $ do+ spec <- parseOptionalInputFile fp options functions+ vs <- parseOptionalVariablesFile varNameFile+ rs <- parseOptionalRequirementsListFile handlersFile+ varDB <- parseOptionalVarDBFile varDBFile - liftEither $ checkArguments cs vs rs+ liftEither $ checkArguments spec vs rs - let varNames = fromMaybe (fretCSExtractExternalVariables cs) vs- monitors = fromMaybe (fretCSExtractHandlers cs) rs+ let varNames = fromMaybe (specExtractExternalVariables spec) vs+ monitors = fromMaybe (specExtractHandlers spec) rs - e <- liftIO $ fprimeApp' targetDir varNames varDB monitors- liftEither e+ e <- liftIO $ fprimeApp' targetDir mTemplateDir varNames varDB monitors+ liftEither e+ where+ targetDir = fprimeAppTargetDir options+ mTemplateDir = fprimeAppTemplateDir options+ varNameFile = fprimeAppVarNames options+ varDBFile = fprimeAppVariableDB options+ handlersFile = fprimeAppHandlers options+ functions = exprPair (fprimeAppPropFormat options) -- | Generate a new FPrime component connected to Copilot, by copying the -- template and filling additional necessary files. fprimeApp' :: FilePath -- ^ Target directory where the component -- should be created.+ -> Maybe FilePath -- ^ Directory where the template is to be+ -- found. -> [String] -- ^ List of variable names (data sources). -> [(String, String)] -- ^ List of variables with their types, and -- the message IDs (topics) they can be@@ -106,14 +130,14 @@ -> [String] -- ^ List of handlers associated to the -- monitors (or requirements monitored). -> IO (Either ErrorTriplet ())-fprimeApp' targetDir varNames varDB monitors =+fprimeApp' targetDir mTemplateDir varNames varDB monitors = E.handle (return . Left . cannotCopyTemplate) $ do -- Obtain template dir- dataDir <- getDataDir- let templateDir = dataDir </> "templates" </> "fprime"-- -- Expand template- copyDirectoryRecursive templateDir targetDir+ templateDir <- case mTemplateDir of+ Just x -> return x+ Nothing -> do+ dataDir <- getDataDir+ return $ dataDir </> "templates" </> "fprime" let f n o@(oVars) = case variableMap varDB n of@@ -123,49 +147,126 @@ -- This is a Data.List.unzip4 let vars = foldr f [] varNames - let fprimeFileName =- targetDir </> "Copilot.fpp"- fprimeFileContents =- unlines $- componentInterface vars monitors-- writeFile fprimeFileName fprimeFileContents+ -- Copilot.fpp+ (ifaceTypePorts, ifaceInputPorts, ifaceViolationEvents) =+ componentInterface vars monitors - let fprimeFileName =- targetDir </> "Copilot.hpp"- fprimeFileContents =- unlines $- componentHeader vars monitors+ -- Copilot.hpp+ hdrHandlers = componentHeader vars monitors - writeFile fprimeFileName fprimeFileContents+ -- Copilot.cpp+ (implInputs, implMonitorResults, implInputHandlers,+ implTriggerResultReset, implTriggerChecks, implTriggers) =+ componentImpl vars monitors - let fprimeFileName =- targetDir </> "Copilot.cpp"- fprimeFileContents =- unlines $- componentImpl vars monitors+ subst = object $+ [ "ifaceTypePorts" .= pack ifaceTypePorts+ , "ifaceInputPorts" .= pack ifaceInputPorts+ , "ifaceViolationEvents" .= pack ifaceViolationEvents+ , "hdrHandlers" .= pack hdrHandlers+ , "implInputs" .= pack implInputs+ , "implMonitorResults" .= pack implMonitorResults+ , "implInputHandlers" .= pack implInputHandlers+ , "implTriggerResultReset" .= pack implTriggerResultReset+ , "implTriggerChecks" .= pack implTriggerChecks+ , "implTriggers" .= pack implTriggers+ ] - writeFile fprimeFileName fprimeFileContents+ copyTemplate templateDir subst targetDir return $ Right () -- ** Argument processing --- | Process FRET component spec, if available, and return its abstract+-- | Options used to customize the conversion of specifications to F'+-- applications.+data FPrimeAppOptions = FPrimeAppOptions+ { fprimeAppTargetDir :: FilePath -- ^ Target directory where the+ -- component should be created.+ , fprimeAppTemplateDir :: Maybe FilePath -- ^ Directory where the template is+ -- to be found.+ , fprimeAppVarNames :: Maybe FilePath -- ^ File containing a list of+ -- variables to make available to+ -- Copilot.+ , fprimeAppVariableDB :: Maybe FilePath -- ^ File containing a list of known+ -- variables with their types and+ -- the message IDs they can be+ -- obtained from.+ , fprimeAppHandlers :: Maybe FilePath -- ^ File containing a list of+ -- handlers used in the Copilot+ -- specification. The handlers are+ -- assumed to receive no arguments.+ , fprimeAppFormat :: String -- ^ Format of the input file.+ , fprimeAppPropFormat :: String -- ^ Format used for input+ -- properties.+ , fprimeAppPropVia :: Maybe String -- ^ Use external command to+ -- pre-process system properties.+ }++-- | Process input specification, if available, and return its abstract -- representation.-parseOptionalFRETCS :: Maybe FilePath- -> ExceptT ErrorTriplet IO (Maybe (Spec String))-parseOptionalFRETCS Nothing = return Nothing-parseOptionalFRETCS (Just fp) = do- -- Throws an exception if the file cannot be read.- content <- liftIO $ B.safeReadFile fp- let fretCS :: Either String (Spec String)- fretCS = parseJSONSpec return fretFormat =<< eitherDecode =<< content+parseOptionalInputFile :: Maybe FilePath+ -> FPrimeAppOptions+ -> ExprPair+ -> ExceptT ErrorTriplet IO (Maybe (Spec String))+parseOptionalInputFile Nothing _ _ =+ return Nothing+parseOptionalInputFile (Just fp) opts (ExprPair parse replace print ids def) =+ ExceptT $ do+ let wrapper = wrapVia (fprimeAppPropVia opts) 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.+ let formatName = fprimeAppFormat opts+ exists <- doesFileExist formatName+ dataDir <- getDataDir+ let formatFile+ | isInfixOf "/" formatName || exists+ = formatName+ | otherwise+ = dataDir </> "data" </> "formats" </>+ (formatName ++ "_" ++ fprimeAppPropFormat opts)+ formatMissing <- not <$> doesFileExist formatFile - case fretCS of- Left e -> throwError $ cannotOpenFRETFile fp e- Right cs -> return $ Just cs+ if formatMissing+ then return $ Left $ fprimeAppIncorrectFormatSpec 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+ (fmap (fmap print) . wrapper)+ (print def)+ xmlFormat+ 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+ (fmap (fmap print) . wrapper)+ jsonFormat+ v+ case res of+ Left e -> return $ Left $ cannotOpenInputFile fp e+ Right x -> return $ Right $ Just x+ -- | Process a variable selection file, if available, and return the variable -- names. parseOptionalVariablesFile :: Maybe FilePath@@ -213,11 +314,11 @@ -- The FPrime backend provides several modes of operation, which are selected -- by providing different arguments to the `ros` command. ----- When a FRET component specification file is provided, the variables and--- requirements defined in it are used unless variables or handlers files are--- provided, in which case the latter take priority.+-- When an input specification file is provided, the variables and requirements+-- defined in it are used unless variables or handlers files are provided, in+-- which case the latter take priority. ----- If a FRET file is not provided, then the user must provide BOTH a variable+-- 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) -> Maybe [String]@@ -230,21 +331,21 @@ checkArguments _ _ (Just []) = Left wrongArguments checkArguments _ _ _ = Right () --- | Extract the variables from a FRET component specification, and sanitize--- them to be used in FPrime.-fretCSExtractExternalVariables :: Maybe (Spec a) -> [String]-fretCSExtractExternalVariables Nothing = []-fretCSExtractExternalVariables (Just cs) = map sanitizeLCIdentifier- $ map externalVariableName- $ externalVariables cs+-- | Extract the variables from a specification, and sanitize them to be used+-- in FPrime.+specExtractExternalVariables :: Maybe (Spec a) -> [String]+specExtractExternalVariables Nothing = []+specExtractExternalVariables (Just cs) = map sanitizeLCIdentifier+ $ map externalVariableName+ $ externalVariables cs --- | Extract the requirements from a FRET component specification, and sanitize--- them to match the names of the handlers used by Copilot.-fretCSExtractHandlers :: Maybe (Spec a) -> [String]-fretCSExtractHandlers Nothing = []-fretCSExtractHandlers (Just cs) = map handlerNameF- $ map requirementName- $ requirements cs+-- | Extract the requirements from a specification, and sanitize them to match+-- the names of the handlers used by Copilot.+specExtractHandlers :: Maybe (Spec a) -> [String]+specExtractHandlers Nothing = []+specExtractHandlers (Just cs) = map handlerNameF+ $ map requirementName+ $ requirements cs where handlerNameF = ("handler" ++) . sanitizeUCIdentifier @@ -275,98 +376,82 @@ , varDeclType :: String } +-- * 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+ { exprParse :: String -> Either String a+ , exprReplace :: [(String, String)] -> a -> a+ , exprPrint :: a -> String+ , exprIdents :: a -> [String]+ , exprUnknown :: a+ }++-- | Return a handler depending on whether it should be for CoCoSpec boolean+-- expressions or for SMV boolean expressions. We default to SMV if not format+-- is given.+exprPair :: String -> ExprPair+exprPair "cocospec" =+ ExprPair+ (CoCoSpec.pBoolSpec . CoCoSpec.myLexer)+ (\_ -> id)+ (CoCoSpec.boolSpec2Copilot)+ (CoCoSpec.boolSpecNames)+ (CoCoSpec.BoolSpecSignal (CoCoSpec.Ident "undefined"))+exprPair "literal" =+ ExprPair+ Right+ (\_ -> id)+ id+ (const [])+ "undefined"+exprPair _ =+ ExprPair+ (SMV.pBoolSpec . SMV.myLexer)+ (substituteBoolExpr)+ (SMV.boolSpec2Copilot)+ (SMV.boolSpecNames)+ (SMV.BoolSpecSignal (SMV.Ident "undefined"))++-- | 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+ -- * FPrime component content -- | Return the contents of the FPrime component interface (.fpp) specification. componentInterface :: [VarDecl] -> [String] -- Monitors- -> [String]+ -> (String, String, String) componentInterface variables monitors =- [ "module Ref {"- , ""- ]- ++ typePorts ++- [ ""- , " @ Monitoring component"- , " queued component Copilot {"- , ""- , " # ----------------------------------------------------------------------"- , " # General ports"- , " # ----------------------------------------------------------------------"- , ""- ]- ++ inputPorts ++- [ ""- , " # ----------------------------------------------------------------------"- , " # Special ports"- , " # ----------------------------------------------------------------------"- , ""- , " @ Command receive"- , " command recv port cmdIn"- , ""- , " @ Command registration"- , " command reg port cmdRegOut"- , ""- , " @ Command response"- , " command resp port cmdResponseOut"- , ""- , " @ Event"- , " event port eventOut"- , ""- , " @ Parameter get"- , " param get port prmGetOut"- , ""- , " @ Parameter set"- , " param set port prmSetOut"- , ""- , " @ Telemetry"- , " telemetry port tlmOut"- , ""- , " @ Text event"- , " text event port textEventOut"- , ""- , " @ Time get"- , " time get port timeGetOut"- , ""- , " # ----------------------------------------------------------------------"- , " # Parameters"- , " # ----------------------------------------------------------------------"- , ""- , " # This section intentionally left blank"- , ""- , " # ----------------------------------------------------------------------"- , " # Events"- , " # ----------------------------------------------------------------------"- , ""- ]- ++ violationEvents ++- [ ""- , " # ----------------------------------------------------------------------"- , " # Commands"- , " # ----------------------------------------------------------------------"- , ""- , " sync command CHECK_MONITORS()"- , ""- , " # ----------------------------------------------------------------------"- , " # Telemetry"- , " # ----------------------------------------------------------------------"- , ""- , " # This section intentionally left blank"- , ""- , " }"- , ""- , "}"- ]+ (typePorts, inputPorts, violationEvents) where - typePorts = nub $ sort $ map toTypePort variables+ typePorts = unlines' $ nub $ sort $ map toTypePort variables toTypePort varDecl = " port " ++ fprimeVarDeclType varDecl ++ "Value(value: " ++ fprimeVarDeclType varDecl ++ ")" - inputPorts = map toInputPortDecl variables+ inputPorts = unlines' $ map toInputPortDecl variables toInputPortDecl varDecl = " async input port " ++ varDeclName varDecl ++ "In : " ++ fprimeVarDeclType varDecl@@ -385,7 +470,8 @@ "double" -> "F64" def -> def - violationEvents = intercalate [""]+ violationEvents = unlines'+ $ intercalate [""] $ map violationEvent monitors violationEvent monitor = [ " @ " ++ monitor ++ " violation"@@ -401,78 +487,11 @@ -- | Return the contents of the FPrime component header file. componentHeader :: [VarDecl] -> [String] -- Monitors- -> [String]-componentHeader variables _monitors =- [ "// ======================================================================"- , "// \\title Copilot.hpp"- , "// \\author root"- , "// \\brief hpp file for Copilot component implementation class"- , "// ======================================================================"- , ""- , "#ifndef Copilot_HPP"- , "#define Copilot_HPP"- , ""- , "#include \"Ref/Copilot/CopilotComponentAc.hpp\""- , ""- , "namespace Ref {"- , ""- , " class Copilot :"- , " public CopilotComponentBase"- , " {"- , ""- , " public:"- , ""- , " // ----------------------------------------------------------------------"- , " // Construction, initialization, and destruction"- , " // ----------------------------------------------------------------------"- , ""- , " //! Construct object Copilot"- , " //!"- , " Copilot("- , " const char *const compName /*!< The component name*/"- , " );"- , ""- , " //! Initialize object Copilot"- , " //!"- , " void init("- , " const NATIVE_INT_TYPE queueDepth, /*!< The queue depth*/"- , " const NATIVE_INT_TYPE instance = 0 /*!< The instance number*/"- , " );"- , ""- , " //! Destroy object Copilot"- , " //!"- , " ~Copilot();"- , ""- , " PRIVATE:"- , ""- , " // ----------------------------------------------------------------------"- , " // Handler implementations for user-defined typed input ports"- , " // ----------------------------------------------------------------------"- , ""- ]- ++ handlers ++- [ ""- , " PRIVATE:"- , ""- , " // ----------------------------------------------------------------------"- , " // Command handler implementations"- , " // ----------------------------------------------------------------------"- , ""- , " //! Implementation for CHECK_MONITORS command handler"- , " //! "- , " void CHECK_MONITORS_cmdHandler("- , " const FwOpcodeType opCode, /*!< The opcode*/"- , " const U32 cmdSeq /*!< The command sequence number*/"- , " );"- , ""- , " };"- , ""- , "} // end namespace Ref"- , ""- , "#endif"- ]+ -> String+componentHeader variables _monitors = handlers where- handlers = intercalate [""]+ handlers = unlines'+ $ intercalate [""] $ map toInputHandler variables toInputHandler nm = [ " //! Handler implementation for " ++ varDeclName nm ++ "In"@@ -489,103 +508,29 @@ -- | Return the contents of the main FPrime component. componentImpl :: [VarDecl] -> [String] -- Monitors- -> [String]+ -> (String, String, String, String, String, String) componentImpl variables monitors =- [ "// ======================================================================"- , "// \\title Copilot.cpp"- , "// \\author Ogma"- , "// \\brief cpp file for Copilot component implementation class"- , "// ======================================================================"- , ""- , ""- , "#include <Ref/Copilot/Copilot.hpp>"- , "#include \"Fw/Types/BasicTypes.hpp\""- , ""- , "#ifdef __cplusplus"- , "extern \"C\" {"- , "#endif"- , ""- , "#include \"copilot.h\""- , "#include \"copilot_types.h\""- , ""- , "#ifdef __cplusplus"- , "}"- , "#endif"- , ""- ]- ++ inputs- ++ monitorResults ++- [ ""- , "namespace Ref {"- , ""- , " // ----------------------------------------------------------------------"- , " // Construction, initialization, and destruction"- , " // ----------------------------------------------------------------------"- , ""- , " Copilot ::"- , " Copilot("- , " const char *const compName"- , " ) : CopilotComponentBase(compName)"- , " {"- , ""- , " }"- , ""- , " void Copilot ::"- , " init("- , " const NATIVE_INT_TYPE queueDepth,"- , " const NATIVE_INT_TYPE instance"- , " )"- , " {"- , " CopilotComponentBase::init(queueDepth, instance);"- , " }"- , ""- , " Copilot ::"- , " ~Copilot()"- , " {"- , ""- , " }"- , ""- , " // ----------------------------------------------------------------------"- , " // Handler implementations for user-defined typed input ports"- , " // ----------------------------------------------------------------------"- , ""- ]- ++ inputHandlers ++- [ ""- , " // ----------------------------------------------------------------------"- , " // Command handler implementations"- , " // ----------------------------------------------------------------------"- , ""- , " void Copilot ::"- , " CHECK_MONITORS_cmdHandler("- , " const FwOpcodeType opCode,"- , " const U32 cmdSeq"- , " )"- , " {"- ]- ++ triggerResultReset ++- [ " step();"- , " this->cmdResponse_out(opCode,cmdSeq,Fw::CmdResponse::OK);"- ]- ++ triggerChecks ++- [ " }"- , ""- , "} // end namespace Ref"- , ""- ]- ++ triggers+ ( inputs+ , monitorResults+ , inputHandlers+ , triggerResultReset+ , triggerChecks+ , triggers+ ) where - inputs = variablesS+ inputs = unlines' variablesS - monitorResults = intercalate [""]+ monitorResults = unlines'+ $ intercalate [""] $ map monitorResult monitors monitorResult monitor = [ "bool " ++ monitor ++ "_result;" ] - inputHandlers = intercalate [""]+ inputHandlers = unlines'+ $ intercalate [""] $ map toInputHandler variables toInputHandler nm = [ " void Copilot :: "@@ -601,13 +546,15 @@ portTy = varDeclType nm ty = varDeclType nm - triggerResultReset = intercalate [""]+ triggerResultReset = unlines'+ $ intercalate [""] $ map monitorResultReset monitors monitorResultReset monitor = [ " " ++ monitor ++ "_result = false;" ] - triggerChecks = intercalate [""]+ triggerChecks = unlines'+ $ intercalate [""] $ map triggerCheck monitors triggerCheck monitor = [ " if (" ++ monitor ++ "_result) {"@@ -617,8 +564,9 @@ where ucMonitor = map toUpper monitor - triggers :: [String]- triggers = intercalate [""]+ triggers :: String+ triggers = unlines'+ $ intercalate [""] $ map triggerImpl monitors triggerImpl monitor = [ "void " ++ monitor ++ "() {"@@ -640,18 +588,17 @@ ErrorTriplet ecWrongArguments msg LocationNothing where msg =- "the arguments provided are insufficient: you must provide a FRET "- ++ "component specification file, or both a variables and a handlers "- ++ "file."+ "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 FRET CS cannot be+-- | Exception handler to deal with the case in which the input file cannot be -- opened.-cannotOpenFRETFile :: FilePath -> String -> ErrorTriplet-cannotOpenFRETFile file _e =- ErrorTriplet ecCannotOpenFRETFile msg (LocationFile file)+cannotOpenInputFile :: FilePath -> String -> ErrorTriplet+cannotOpenInputFile file _e =+ ErrorTriplet ecCannotOpenInputFile msg (LocationFile file) where msg =- "cannot open FRET component specification file " ++ file+ "cannot open input specification file " ++ file -- | Exception handler to deal with the case in which the variable DB cannot be -- opened.@@ -692,6 +639,15 @@ ++ " permissions to write in the destination directory." ++ show e +-- | Error messages associated to the format file not being found.+fprimeAppIncorrectFormatSpec :: String -> ErrorTriplet+fprimeAppIncorrectFormatSpec formatFile =+ ErrorTriplet ecIncorrectFormatFile msg LocationNothing+ where+ msg =+ "The format specification " ++ formatFile ++ " does not exist or is not "+ ++ "readable"+ -- | A triplet containing error information. data ErrorTriplet = ErrorTriplet ErrorCode String Location @@ -716,10 +672,9 @@ ecWrongArguments :: ErrorCode ecWrongArguments = 1 --- | Error: the FRET component specification provided by the user cannot be--- opened.-ecCannotOpenFRETFile :: ErrorCode-ecCannotOpenFRETFile = 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. ecCannotOpenDBUser :: ErrorCode@@ -738,18 +693,14 @@ ecCannotCopyTemplate :: ErrorCode ecCannotCopyTemplate = 1 --- | JSONPath selectors for a FRET file-fretFormat :: JSONFormat-fretFormat = JSONFormat- { specInternalVars = Just "..Internal_variables[*]"- , specInternalVarId = ".name"- , specInternalVarExpr = ".assignmentCopilot"- , specInternalVarType = Just ".type"- , specExternalVars = Just "..Other_variables[*]"- , specExternalVarId = ".name"- , specExternalVarType = Just ".type"- , specRequirements = "..Requirements[*]"- , specRequirementId = ".name"- , specRequirementDesc = Just ".fretish"- , specRequirementExpr = ".ptLTL"- }+-- | Error: the format file cannot be opened.+ecIncorrectFormatFile :: ErrorCode+ecIncorrectFormatFile = 1++-- * Auxliary functions++-- | Create a string from a list of strings, inserting new line characters+-- between them. Unlike 'Prelude.unlines', this function does not insert+-- an end of line character at the end of the last string.+unlines' :: [String] -> String+unlines' = intercalate "\n"
src/Command/ROSApp.hs view
@@ -1,4 +1,7 @@-{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE MultiWayIf #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE ScopedTypeVariables #-} -- Copyright 2022 United States Government as represented by the Administrator -- of the National Aeronautics and Space Administration. All Rights Reserved. --@@ -40,18 +43,21 @@ module Command.ROSApp ( rosApp , ErrorCode+ , ROSAppOptions(..) ) where -- External imports import qualified Control.Exception as E-import Control.Monad.Except (ExceptT, liftEither, liftIO, runExceptT,- throwError)+import Control.Monad.Except (ExceptT(..), liftEither, liftIO,+ runExceptT, throwError) import Data.Aeson (eitherDecode, object, (.=))-import Data.List (find, intersperse)+import Data.List (isInfixOf, isPrefixOf, find, intersperse) import Data.Maybe (fromMaybe) import Data.Text.Lazy (pack)+import System.Directory (doesFileExist) import System.FilePath ((</>))+import System.Process (readProcess) -- External imports: auxiliary import Data.ByteString.Extra as B (safeReadFile)@@ -62,44 +68,59 @@ import Data.OgmaSpec (Spec, externalVariableName, externalVariables, requirementName, requirements) import Language.JSONSpec.Parser (JSONFormat (..), parseJSONSpec)+import Language.XMLSpec.Parser (parseXMLSpec) -- Internal imports: auxiliary import Command.Result (Result (..)) import Data.Location (Location (..)) +-- Internal imports: language ASTs, transformers+import qualified Language.CoCoSpec.AbsCoCoSpec as CoCoSpec+import qualified Language.CoCoSpec.ParCoCoSpec as CoCoSpec ( 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.CoCoSpec2Copilot as CoCoSpec (boolSpec2Copilot,+ boolSpecNames)+import Language.Trans.SMV2Copilot as SMV (boolSpec2Copilot,+ boolSpecNames)+ -- Internal imports import Paths_ogma_core ( getDataDir ) -- * ROS app generation -- | Generate a new ROS application connected to Copilot.-rosApp :: FilePath -- ^ Target directory where the application- -- should be created.- -> Maybe FilePath -- ^ Directory where the template is to be found.- -> Maybe FilePath -- ^ FRET Component specification file.- -> Maybe FilePath -- ^ File containing a list of variables to make- -- available to Copilot.- -> Maybe FilePath -- ^ File containing a list of known variables- -- with their types and the message IDs they- -- can be obtained from.- -> Maybe FilePath -- ^ File containing a list of handlers used in the- -- Copilot specification. The handlers are assumed- -- to receive no arguments.+rosApp :: Maybe FilePath -- ^ Input specification file.+ -> ROSAppOptions -- ^ Options to the ROS backend. -> IO (Result ErrorCode)-rosApp targetDir mTemplateDir fretCSFile varNameFile varDBFile handlersFile =- processResult $ do- cs <- parseOptionalFRETCS fretCSFile- vs <- parseOptionalVariablesFile varNameFile- rs <- parseOptionalRequirementsListFile handlersFile- varDB <- parseOptionalVarDBFile varDBFile+rosApp fp options =+ processResult $ do+ spec <- parseOptionalInputFile+ fp+ options+ (exprPair (rosAppPropFormat options))+ vs <- parseOptionalVariablesFile varNameFile+ rs <- parseOptionalRequirementsListFile handlersFile+ varDB <- parseOptionalVarDBFile varDBFile - liftEither $ checkArguments cs vs rs+ liftEither $ checkArguments spec vs rs - let varNames = fromMaybe (fretCSExtractExternalVariables cs) vs- monitors = fromMaybe (fretCSExtractHandlers cs) rs+ let varNames = fromMaybe (specExtractExternalVariables spec) vs+ monitors = fromMaybe (specExtractHandlers spec) rs - e <- liftIO $ rosApp' targetDir mTemplateDir varNames varDB monitors- liftEither e+ e <- liftIO $+ rosApp' targetDir mTemplateDir varNames varDB monitors+ liftEither e+ where+ targetDir = rosAppTargetDir options+ mTemplateDir = rosAppTemplateDir options+ varNameFile = rosAppVariables options+ varDBFile = rosAppVariableDB options+ handlersFile = rosAppHandlers options -- | Generate a new ROS application connected to Copilot, by copying the -- template and filling additional necessary files.@@ -168,21 +189,91 @@ -- ** Argument processing --- | Process FRET component spec, if available, and return its abstract+-- | Options used to customize the conversion of specifications to ROS+-- applications.+data ROSAppOptions = ROSAppOptions+ { rosAppTargetDir :: FilePath -- ^ Target directory where the+ -- application should be created.+ , rosAppTemplateDir :: Maybe FilePath -- ^ Directory where the template is+ -- to be found.+ , rosAppVariables :: Maybe FilePath -- ^ File containing a list of+ -- variables to make available to+ -- Copilot.+ , rosAppVariableDB :: Maybe FilePath -- ^ File containing a list of known+ -- variables with their types and the+ -- message IDs they can be obtained+ -- from.+ , rosAppHandlers :: Maybe FilePath -- ^ File containing a list of+ -- handlers used in the Copilot+ -- specification. The handlers are+ -- assumed to receive no arguments.+ , rosAppFormat :: String -- ^ Format of the input file.+ , rosAppPropFormat :: String -- ^ Format used for input properties.+ , rosAppPropVia :: Maybe String -- ^ Use external command to+ -- pre-process system properties.+ }++-- | Process input specification, if available, and return its abstract -- representation.-parseOptionalFRETCS :: Maybe FilePath- -> ExceptT ErrorTriplet IO (Maybe (Spec String))-parseOptionalFRETCS Nothing = return Nothing-parseOptionalFRETCS (Just fp) = do- -- Throws an exception if the file cannot be read.- content <- liftIO $ B.safeReadFile fp- let fretCS :: Either String (Spec String)- fretCS = parseJSONSpec return fretFormat =<< eitherDecode =<< content+parseOptionalInputFile :: Maybe FilePath+ -> ROSAppOptions+ -> ExprPair+ -> ExceptT ErrorTriplet IO (Maybe (Spec String))+parseOptionalInputFile Nothing _ _ =+ return Nothing+parseOptionalInputFile (Just fp) opts (ExprPair parse replace print ids def) =+ ExceptT $ do+ let wrapper = wrapVia (rosAppPropVia opts) 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.+ let formatName = rosAppFormat opts+ exists <- doesFileExist formatName+ dataDir <- getDataDir+ let formatFile+ | isInfixOf "/" formatName || exists+ = formatName+ | otherwise+ = dataDir </> "data" </> "formats" </>+ (formatName ++ "_" ++ rosAppPropFormat opts)+ formatMissing <- not <$> doesFileExist formatFile - case fretCS of- Left e -> throwError $ cannotOpenFRETFile fp e- Right cs -> return $ Just cs+ if formatMissing+ then return $ Left $ rosAppIncorrectFormatSpec 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+ (fmap (fmap print) . wrapper) (print def) xmlFormat 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+ (fmap (fmap print) . wrapper)+ jsonFormat+ v+ case res of+ Left e -> return $ Left $ cannotOpenInputFile fp e+ Right x -> return $ Right $ Just x+ -- | Process a variable selection file, if available, and return the variable -- names. parseOptionalVariablesFile :: Maybe FilePath@@ -230,11 +321,11 @@ -- The ROS backend provides several modes of operation, which are selected -- by providing different arguments to the `ros` command. ----- When a FRET component specification file is provided, the variables and--- requirements defined in it are used unless variables or handlers files are--- provided, in which case the latter take priority.+-- When an input specification file is provided, the variables and requirements+-- defined in it are used unless variables or handlers files are provided, in+-- which case the latter take priority. ----- If a FRET file is not provided, then the user must provide BOTH a variable+-- If an input file is not provided, then the user must provide BOTH a variable -- list, and a list of handlers. checkArguments :: Maybe (Spec String) -> Maybe [String]@@ -247,21 +338,21 @@ checkArguments _ _ (Just []) = Left wrongArguments checkArguments _ _ _ = Right () --- | Extract the variables from a FRET component specification, and sanitize--- them to be used in ROS.-fretCSExtractExternalVariables :: Maybe (Spec String) -> [String]-fretCSExtractExternalVariables Nothing = []-fretCSExtractExternalVariables (Just cs) = map sanitizeLCIdentifier- $ map externalVariableName- $ externalVariables cs+-- | Extract the variables from a specification, and sanitize them to be used+-- in ROS.+specExtractExternalVariables :: Maybe (Spec String) -> [String]+specExtractExternalVariables Nothing = []+specExtractExternalVariables (Just cs) = map sanitizeLCIdentifier+ $ map externalVariableName+ $ externalVariables cs --- | Extract the requirements from a FRET component specification, and sanitize--- them to match the names of the handlers used by Copilot.-fretCSExtractHandlers :: Maybe (Spec String) -> [String]-fretCSExtractHandlers Nothing = []-fretCSExtractHandlers (Just cs) = map handlerNameF- $ map requirementName- $ requirements cs+-- | Extract the requirements from a specification, and sanitize them to match+-- the names of the handlers used by Copilot.+specExtractHandlers :: Maybe (Spec String) -> [String]+specExtractHandlers Nothing = []+specExtractHandlers (Just cs) = map handlerNameF+ $ map requirementName+ $ requirements cs where handlerNameF = ("handler" ++) . sanitizeUCIdentifier @@ -311,6 +402,64 @@ , msgDataVarType :: String } +-- * 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+ { exprParse :: String -> Either String a+ , exprReplace :: [(String, String)] -> a -> a+ , exprPrint :: a -> String+ , exprIdents :: a -> [String]+ , exprUnknown :: a+ }++-- | Return a handler depending on whether it should be for CoCoSpec boolean+-- expressions or for SMV boolean expressions. We default to SMV if not format+-- is given.+exprPair :: String -> ExprPair+exprPair "cocospec" =+ ExprPair+ (CoCoSpec.pBoolSpec . CoCoSpec.myLexer)+ (\_ -> id)+ (CoCoSpec.boolSpec2Copilot)+ (CoCoSpec.boolSpecNames)+ (CoCoSpec.BoolSpecSignal (CoCoSpec.Ident "undefined"))+exprPair "literal" =+ ExprPair+ Right+ (\_ -> id)+ id+ (const [])+ "undefined"+exprPair _ =+ ExprPair+ (SMV.pBoolSpec . SMV.myLexer)+ (substituteBoolExpr)+ (SMV.boolSpec2Copilot)+ (SMV.boolSpecNames)+ (SMV.BoolSpecSignal (SMV.Ident "undefined"))++-- | 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+ -- * ROS apps content -- | Return the contents of the main ROS application.@@ -547,18 +696,17 @@ ErrorTriplet ecWrongArguments msg LocationNothing where msg =- "the arguments provided are insufficient: you must provide a FRET "- ++ "component specification file, or both a variables and a handlers "- ++ "file."+ "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 FRET CS cannot be+-- | Exception handler to deal with the case in which the input file cannot be -- opened.-cannotOpenFRETFile :: FilePath -> String -> ErrorTriplet-cannotOpenFRETFile file _e =- ErrorTriplet ecCannotOpenFRETFile msg (LocationFile file)+cannotOpenInputFile :: FilePath -> String -> ErrorTriplet+cannotOpenInputFile file _e =+ ErrorTriplet ecCannotOpenInputFile msg (LocationFile file) where msg =- "cannot open FRET component specification file " ++ file+ "cannot open input specification file " ++ file -- | Exception handler to deal with the case in which the variable DB cannot be -- opened.@@ -599,6 +747,15 @@ ++ " permissions to write in the destination directory." ++ show e +-- | Error messages associated to the format file not being found.+rosAppIncorrectFormatSpec :: String -> ErrorTriplet+rosAppIncorrectFormatSpec formatFile =+ ErrorTriplet ecIncorrectFormatFile msg LocationNothing+ where+ msg =+ "The format specification " ++ formatFile ++ " does not exist or is not "+ ++ "readable"+ -- | A triplet containing error information. data ErrorTriplet = ErrorTriplet ErrorCode String Location @@ -623,10 +780,9 @@ ecWrongArguments :: ErrorCode ecWrongArguments = 1 --- | Error: the FRET component specification provided by the user cannot be--- opened.-ecCannotOpenFRETFile :: ErrorCode-ecCannotOpenFRETFile = 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. ecCannotOpenDBUser :: ErrorCode@@ -645,18 +801,6 @@ ecCannotCopyTemplate :: ErrorCode ecCannotCopyTemplate = 1 --- | JSONPath selectors for a FRET file-fretFormat :: JSONFormat-fretFormat = JSONFormat- { specInternalVars = Just "..Internal_variables[*]"- , specInternalVarId = ".name"- , specInternalVarExpr = ".assignmentCopilot"- , specInternalVarType = Just ".type"- , specExternalVars = Just "..Other_variables[*]"- , specExternalVarId = ".name"- , specExternalVarType = Just ".type"- , specRequirements = "..Requirements[*]"- , specRequirementId = ".name"- , specRequirementDesc = Just ".fretish"- , specRequirementExpr = ".ptLTL"- }+-- | Error: the format file cannot be opened.+ecIncorrectFormatFile :: ErrorCode+ecIncorrectFormatFile = 1
src/Command/Standalone.hs view
@@ -1,4 +1,7 @@ {-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE MultiWayIf #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE ScopedTypeVariables #-} -- Copyright 2020 United States Government as represented by the Administrator -- of the National Aeronautics and Space Administration. All Rights Reserved. --@@ -38,15 +41,20 @@ where -- External imports-import Data.Aeson (decode, eitherDecode)-import Data.ByteString.Lazy (fromStrict, pack)+import Control.Exception as E+import Data.Aeson (decode, eitherDecode, object, (.=))+import Data.ByteString.Lazy (fromStrict) import Data.Foldable (for_)-import Data.List (nub, (\\))+import Data.List (isInfixOf, isPrefixOf, nub, (\\)) import Data.Maybe (fromMaybe)+import System.Directory (doesFileExist)+import System.Process (readProcess) import System.FilePath ((</>))+import Data.Text.Lazy (pack) -- External imports: auxiliary-import Data.ByteString.Extra as B ( safeReadFile )+import Data.ByteString.Extra as B ( safeReadFile )+import System.Directory.Extra ( copyTemplate ) -- Internal imports: auxiliary import Command.Result (Result (..))@@ -57,6 +65,7 @@ import Data.OgmaSpec (ExternalVariableDef (..), InternalVariableDef (..), Requirement (..), Spec (..)) import Language.JSONSpec.Parser (JSONFormat (..), parseJSONSpec)+import Language.XMLSpec.Parser (parseXMLSpec) -- Internal imports: language ASTs, transformers import qualified Language.CoCoSpec.AbsCoCoSpec as CoCoSpec@@ -73,72 +82,138 @@ boolSpecNames) import Language.Trans.Spec2Copilot (spec2Copilot, specAnalyze) --- | Print the contents of a Copilot module that implements the spec in an+-- | Generate a new standalone Copilot monitor that implements the spec 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@. All identifiers--- used are valid C99 identifiers.+-- used are valid C99 identifiers. The template, if provided, exists and uses+-- the variables needed by the standalone application generator. The target+-- directory is writable and there's enough disk space to copy the files over. standalone :: FilePath -- ^ Path to a file containing a specification -> StandaloneOptions -- ^ Customization options -> IO (Result ErrorCode) standalone fp options = do+ E.handle (return . standaloneTemplateError options fp) $ do+ -- Obtain template dir+ templateDir <- case standaloneTemplateDir options of+ Just x -> return x+ Nothing -> do+ dataDir <- getDataDir+ return $ dataDir </> "templates" </> "standalone" - let functions = exprPair (standalonePropFormat options)+ let functions = exprPair (standalonePropFormat options) - copilot <- standalone' fp options functions+ copilot <- standalone' fp options functions - let (mOutput, result) = standaloneResult options fp copilot+ let (mOutput, result) = standaloneResult options fp copilot - for_ mOutput putStrLn- return result+ for_ mOutput $ \(externs, internals, reqs, triggers, specName) -> do+ let subst = object $+ [ "externs" .= pack externs+ , "internals" .= pack internals+ , "reqs" .= pack reqs+ , "triggers" .= pack triggers+ , "specName" .= pack specName+ ] --- | Print the contents of a Copilot module that implements the spec in an+ let targetDir = standaloneTargetDir options++ copyTemplate templateDir subst targetDir++ return result++-- | Generate a new standalone Copilot monitor that implements the spec in an -- input file, using a subexpression handler. -- -- 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@. All identifiers--- used are valid C99 identifiers.+-- used are valid C99 identifiers. The template, if provided, exists and uses+-- the variables needed by the standalone application generator. The target+-- directory is writable and there's enough disk space to copy the files over. standalone' :: FilePath -> StandaloneOptions -> ExprPair- -> IO (Either String String)-standalone' fp options (ExprPair parse replace print ids) = do+ -> IO (Either String (String, String, String, String, String))+standalone' fp options (ExprPair parse replace print ids def) = do let name = standaloneFilename options typeMaps = typeToCopilotTypeMapping options - -- Obtain format file+ -- 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.+ let formatName = standaloneFormat options+ exists <- doesFileExist formatName dataDir <- getDataDir- let formatFile =- dataDir </> "data" </> "formats" </>- (standaloneFormat options ++ "_" ++ standalonePropFormat options)+ let formatFile+ | isInfixOf "/" formatName || exists+ = formatName+ | otherwise+ = dataDir </> "data" </> "formats" </>+ (standaloneFormat options ++ "_" ++ standalonePropFormat options)+ formatMissing <- not <$> doesFileExist formatFile - format <- read <$> readFile formatFile+ if formatMissing+ then return $ Left $ standaloneIncorrectFormatSpec formatFile+ else 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.- content <- B.safeReadFile fp- res <- case content of- Left s -> return $ Left s- Right b -> return $ parseJSONSpec parse format =<< eitherDecode b+ let wrapper = wrapVia (standalonePropVia options) parse+ -- 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.+ res <-+ if | isPrefixOf "XMLFormat" format+ -> do let xmlFormat = read format+ content <- readFile fp+ parseXMLSpec wrapper def xmlFormat content+ | otherwise+ -> do let jsonFormat = read format+ content <- B.safeReadFile fp+ case content of+ Left s -> return $ Left s+ Right b -> do case eitherDecode b of+ Left e -> return $ Left e+ Right v -> parseJSONSpec wrapper jsonFormat v - -- Complement the specification with any missing/implicit definitions- let res' = fmap (addMissingIdentifiers ids) res+ -- Complement the specification with any missing/implicit definitions+ let res' = fmap (addMissingIdentifiers ids) res - let copilot = spec2Copilot name typeMaps replace print =<< specAnalyze =<< res'+ return $ spec2Copilot name typeMaps replace print =<< specAnalyze =<< res' - return copilot+-- | 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 :: IOException) -> return $ Left $ show e) $ do+ out <- readProcess f [] s+ return $ parse out -- | Options used to customize the conversion of specifications to Copilot -- code. data StandaloneOptions = StandaloneOptions- { standaloneFormat :: String+ { standaloneTargetDir :: FilePath+ , standaloneTemplateDir :: Maybe FilePath+ , standaloneFormat :: String , standalonePropFormat :: String , standaloneTypeMapping :: [(String, String)] , standaloneFilename :: String+ , standalonePropVia :: Maybe String } -- * Error codes@@ -153,17 +228,42 @@ ecStandaloneError :: ErrorCode ecStandaloneError = 1 +-- | Error: standalone component generation failed during the copy/write+-- process.+ecStandaloneTemplateError :: ErrorCode+ecStandaloneTemplateError = 2+ -- * Result -- | Process the result of the transformation function. standaloneResult :: StandaloneOptions -> FilePath- -> Either String String- -> (Maybe String, Result ErrorCode)+ -> Either String a+ -> (Maybe a, Result ErrorCode) standaloneResult options fp result = case result of Left msg -> (Nothing, Error ecStandaloneError msg (LocationFile fp)) Right t -> (Just t, Success) +-- | Report an error when trying to open or copy the template+standaloneTemplateError :: StandaloneOptions+ -> FilePath+ -> E.SomeException+ -> Result ErrorCode+standaloneTemplateError options fp exception =+ Error ecStandaloneTemplateError msg (LocationFile fp)+ where+ msg =+ "Standlone monitor generation failed during copy/write operation. Check"+ ++ " that there's free space in the disk and that you have the necessary"+ ++ " permissions to write in the destination directory. "+ ++ show exception++-- | Error message associated to the format file not being found.+standaloneIncorrectFormatSpec :: String -> String+standaloneIncorrectFormatSpec formatFile =+ "The format specification " ++ formatFile ++ " does not exist or is not "+ ++ "readable"+ -- * Mapping of types from input format to Copilot typeToCopilotTypeMapping :: StandaloneOptions -> [(String, String)] typeToCopilotTypeMapping options =@@ -184,11 +284,15 @@ -- | 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 { exprParse :: String -> Either String a , exprReplace :: [(String, String)] -> a -> a , exprPrint :: a -> String , exprIdents :: a -> [String]+ , exprUnknown :: a } -- | Return a handler depending on whether it should be for CoCoSpec boolean@@ -199,10 +303,17 @@ (\_ -> id) (CoCoSpec.boolSpec2Copilot) (CoCoSpec.boolSpecNames)+ (CoCoSpec.BoolSpecSignal (CoCoSpec.Ident "undefined"))+exprPair "literal" = ExprPair Right+ (\_ -> id)+ id+ (const [])+ "undefined" exprPair _ = ExprPair (SMV.pBoolSpec . SMV.myLexer) (substituteBoolExpr) (SMV.boolSpec2Copilot) (SMV.boolSpecNames)+ (SMV.BoolSpecSignal (SMV.Ident "undefined")) -- | Add to a spec external variables for all identifiers mentioned in -- expressions that are not defined anywhere.
src/Language/Trans/Spec2Copilot.hs view
@@ -1,4 +1,5 @@ -- Copyright 2024 United States Government as represented by the Administrator+-- Copyright 2024 United States Government as represented by the Administrator -- of the National Aeronautics and Space Administration. All Rights Reserved. -- -- Disclaimers@@ -36,7 +37,7 @@ module Language.Trans.Spec2Copilot where -- External imports-import Data.List ( intersect, lookup, union )+import Data.List ( intercalate, intersect, lookup, union ) import Data.Maybe ( fromMaybe ) -- External imports: auxiliary@@ -56,46 +57,17 @@ -> ([(String, String)] -> a -> a) -- Expr subsitution function -> (a -> String) -- Expr show function -> Spec a -- Specification- -> Either String String+ -> Either String (String, String, String, String, String) spec2Copilot specName typeMaps exprTransform showExpr spec =- pure $ unlines $ concat- [ imports- , externs- , internals- , reqs- , clock- , ftp- , pre- , tpre- , notPreviousNot- , copilotSpec- , main'- ]+ pure (externs, internals, reqs, triggers, specName) where - -- Import header block- imports :: [String]- imports =- [ "import Copilot.Compile.C99"- , "import Copilot.Language hiding (prop)"- , "import Copilot.Language.Prelude"- , "import Copilot.Library.LTL (next)"- , "import Copilot.Library.MTL hiding (since,"- ++ " alwaysBeen, trigger)"- , "import Copilot.Library.PTLTL (since, previous,"- ++ " alwaysBeen)"- , "import qualified Copilot.Library.PTLTL as PTLTL"- , "import qualified Copilot.Library.MTL as MTL"- , "import Language.Copilot (reify)"- , "import Prelude hiding ((&&), (||), (++),"- ++ " (<=), (>=), (<), (>), (==), (/=), not)"- , ""- ]- -- Extern streams- externs = concatMap externVarToDecl- (externalVariables spec)+ externs = unlines'+ $ intercalate [""]+ $ map externVarToDecl+ (externalVariables spec) where externVarToDecl i = [ propName ++ " :: Stream "@@ -110,14 +82,15 @@ ++ show (externalVariableName i) ++ " " ++ "Nothing"- , "" ] where propName = safeMap nameSubstitutions (externalVariableName i) -- Internal stream definitions- internals = concatMap internalVarToDecl- (internalVariables spec)+ internals = unlines'+ $ intercalate [""]+ $ map internalVarToDecl+ (internalVariables spec) where internalVarToDecl i = (\implem -> [ propName@@ -129,20 +102,19 @@ , propName ++ " = " ++ implem-- , "" ]) implementation where propName = safeMap nameSubstitutions (internalVariableName i) implementation = (internalVariableExpr i) -- Encoding of requirements as boolean streams- reqs :: [String]- reqs = concatMap reqToDecl (requirements spec)+ reqs :: String+ reqs = unlines'+ $ intercalate [""]+ $ map reqToDecl (requirements spec) where reqToDecl i = [ reqComment, reqSignature , reqBody nameSubstitutions- , "" ] where reqName = safeMap nameSubstitutions (requirementName i)@@ -165,58 +137,10 @@ (showExpr (exprTransform subs (requirementExpr i))) - -- Auxiliary streams: clock- clock :: [String]- clock = [ ""- , "-- | Clock that increases in one-unit steps."- , "clock :: Stream Int64"- , "clock = [0] ++ (clock + 1)"- , ""- ]-- -- Auxiliary streams: first time point- ftp :: [String]- ftp = [ ""- , "-- | First Time Point"- , "ftp :: Stream Bool"- , "ftp = [True] ++ false"- , ""- ]-- -- Auxiliary streams: pre- pre = [ ""- , "pre :: Stream Bool -> Stream Bool"- , "pre = ([False] ++)"- ]-- -- Auxiliary streams: tpre- tpre = [ ""- , "tpre :: Stream Bool -> Stream Bool"- , "tpre = ([True] ++)"- ]-- -- Auxiliary streams: notPreviousNot- notPreviousNot :: [String]- notPreviousNot = [ ""- , "notPreviousNot :: Stream Bool -> Stream Bool"- , "notPreviousNot = not . PTLTL.previous . not"- ]-- -- Main specification- copilotSpec :: [String]- copilotSpec = [ ""- , "-- | Complete specification. Calls C handler functions"- ++ " when"- , "-- properties are violated."- , "spec :: Spec"- , "spec = do"- ]- ++ triggers- ++ [ "" ]+ -- Main specification triggers+ triggers :: String+ triggers = unlines' $ fmap reqTrigger (requirements spec) where- triggers :: [String]- triggers = fmap reqTrigger (requirements spec)- reqTrigger :: Requirement a -> String reqTrigger r = " trigger " ++ show handlerName ++ " (not " ++ propName ++ ") " ++ "[]"@@ -224,14 +148,6 @@ handlerName = "handler" ++ sanitizeUCIdentifier (requirementName r) propName = safeMap nameSubstitutions (requirementName r) - -- Main program that compiles specification to C in two files (code and- -- header).- main' :: [String]- main' = [ ""- , "main :: IO ()"- , "main = reify spec >>= compile \"" ++ specName ++ "\""- ]- -- Map from a variable name to its desired identifier in the code -- generated. internalVariableMap =@@ -247,7 +163,7 @@ ++ externalVariableMap ++ requirementNameMap - -- Variable/requirement names used in the component spec.+ -- Variable/requirement names used in the input spec. internalVariableNames = map internalVariableName $ internalVariables spec @@ -300,7 +216,7 @@ requirementNameMap = map (\x -> (x, "prop" ++ sanitizeUCIdentifier x)) requirementNames - -- Variable/requirement names used in the component spec.+ -- Variable/requirement names used in the input spec. internalVariableNames = map internalVariableName $ internalVariables spec @@ -318,3 +234,9 @@ -- substitution table. safeMap :: [(String, String)] -> String -> String safeMap ls k = fromMaybe k $ lookup k ls++-- | Create a string from a list of strings, inserting new line characters+-- between them. Unlike 'Prelude.unlines', this function does not insert+-- an end of line character at the end of the last string.+unlines' :: [String] -> String+unlines' = intercalate "\n"
+ templates/diagram/Copilot.hs view
@@ -0,0 +1,77 @@+import Copilot.Compile.C99+import Copilot.Language hiding (max, min, prop)+import Copilot.Language.Prelude+import Copilot.Library.LTL (next)+import Copilot.Library.MTL hiding (alwaysBeen, since, trigger)+import qualified Copilot.Library.MTL as MTL+import Copilot.Library.PTLTL (alwaysBeen, previous, since)+import qualified Copilot.Library.PTLTL as PTLTL+import Language.Copilot (reify)+import Language.Copilot hiding (max, min)+import Prelude hiding (max, min, mod, not, until,+ (&&), (++), (/=), (<), (<=), (==),+ (>), (>=), (||))++externalState :: Stream Word8+externalState = extern "{{{state}}}" Nothing++input :: Stream Word8+input = extern "{{{input}}}" Nothing++{{{streamDefs}}}++-- | Complete specification. Calls C handler functions when properties are+-- violated.+spec :: Spec+spec = do+ trigger "handler" stateMachineProp {{{handlerInputs}}}++main :: IO ()+main = reify spec >>= compile "{{{specName}}}"++-- Initial state, final state, no transition signal, transitions, bad state+type StateMachineGF = ( Word8, Word8, Stream Bool, [(Word8, Stream Bool, Word8)], Word8)++stateMachineGF :: StateMachineGF -> Stream Word8+stateMachineGF (initialState, finalState, noInputData, transitions, badState) = state+ where+ state = [initialState] ++ ifThenElses transitions++ ifThenElses :: [(Word8, Stream Bool, Word8)] -> Stream Word8+ ifThenElses [] =+ ifThenElse (state == constant finalState && noInputData)+ (constant finalState)+ (constant badState)++ ifThenElses ((s1,i,s2):ss) =+ ifThenElse (state == constant s1 && i) (constant s2) (ifThenElses ss)++-- | True when the given input stream does hold any of the values in the given+-- list.+noneOf :: [Stream Bool] -> Stream Bool+noneOf [] = true+noneOf (x:xs) = not x && noneOf xs++-- | Given a list of transitions, and a current state, and a list of possible+-- destination states, produce a list of booleans indicating if a transition to+-- each of the destination states would be valid.+checkValidTransitions :: [(Word8, Stream Bool, Word8)]+ -> Stream Word8+ -> [Word8]+ -> [Stream Bool]+checkValidTransitions transitions curState destinations =+ map (checkValidTransition transitions curState) destinations++-- | Given a list of transitions, and a current state, and destination states,+-- produce a list of booleans indicating if a transition to each of the+-- destination states would be valid.+checkValidTransition :: [(Word8, Stream Bool, Word8)]+ -> Stream Word8+ -> Word8+ -> Stream Bool+checkValidTransition [] _ _ = true+checkValidTransition ((so1, c, sd1):sx) so2 sd2 =+ ifThenElse+ ((constant so1 == so2) && (constant sd1 == constant sd2))+ c+ (checkValidTransition sx so2 sd2)
+ templates/fprime/Copilot.cpp view
@@ -0,0 +1,78 @@+// ======================================================================+// \title Copilot.cpp+// \author Ogma+// \brief cpp file for Copilot component implementation class+// ======================================================================+++#include <Ref/Copilot/Copilot.hpp>+#include "Fw/Types/BasicTypes.hpp"++#ifdef __cplusplus+extern "C" {+#endif++#include "copilot.h"+#include "copilot_types.h"++#ifdef __cplusplus+}+#endif++{{{implInputs}}}+{{{implMonitorResults}}}++namespace Ref {++ // ----------------------------------------------------------------------+ // Construction, initialization, and destruction+ // ----------------------------------------------------------------------++ Copilot ::+ Copilot(+ const char *const compName+ ) : CopilotComponentBase(compName)+ {++ }++ void Copilot ::+ init(+ const NATIVE_INT_TYPE queueDepth,+ const NATIVE_INT_TYPE instance+ )+ {+ CopilotComponentBase::init(queueDepth, instance);+ }++ Copilot ::+ ~Copilot()+ {++ }++ // ----------------------------------------------------------------------+ // Handler implementations for user-defined typed input ports+ // ----------------------------------------------------------------------++{{{implInputHandlers}}}++ // ----------------------------------------------------------------------+ // Command handler implementations+ // ----------------------------------------------------------------------++ void Copilot ::+ CHECK_MONITORS_cmdHandler(+ const FwOpcodeType opCode,+ const U32 cmdSeq+ )+ {+{{{implTriggerResultReset}}}+ step();+ this->cmdResponse_out(opCode,cmdSeq,Fw::CmdResponse::OK);+{{{implTriggerChecks}}}+ }++} // end namespace Ref++{{{implTriggers}}}
+ templates/fprime/Copilot.fpp view
@@ -0,0 +1,71 @@+module Ref {++{{{ifaceTypePorts}}}++ @ Monitoring component+ queued component Copilot {++ # ----------------------------------------------------------------------+ # General ports+ # ----------------------------------------------------------------------++{{{ifaceInputPorts}}}++ # ----------------------------------------------------------------------+ # Special ports+ # ----------------------------------------------------------------------++ @ Command receive+ command recv port cmdIn++ @ Command registration+ command reg port cmdRegOut++ @ Command response+ command resp port cmdResponseOut++ @ Event+ event port eventOut++ @ Parameter get+ param get port prmGetOut++ @ Parameter set+ param set port prmSetOut++ @ Telemetry+ telemetry port tlmOut++ @ Text event+ text event port textEventOut++ @ Time get+ time get port timeGetOut++ # ----------------------------------------------------------------------+ # Parameters+ # ----------------------------------------------------------------------++ # This section intentionally left blank++ # ----------------------------------------------------------------------+ # Events+ # ----------------------------------------------------------------------++{{{ifaceViolationEvents}}}++ # ----------------------------------------------------------------------+ # Commands+ # ----------------------------------------------------------------------++ sync command CHECK_MONITORS()++ # ----------------------------------------------------------------------+ # Telemetry+ # ----------------------------------------------------------------------++ # This section intentionally left blank++ }++}
+ templates/fprime/Copilot.hpp view
@@ -0,0 +1,66 @@+// ======================================================================+// \title Copilot.hpp+// \author root+// \brief hpp file for Copilot component implementation class+// ======================================================================++#ifndef Copilot_HPP+#define Copilot_HPP++#include "Ref/Copilot/CopilotComponentAc.hpp"++namespace Ref {++ class Copilot :+ public CopilotComponentBase+ {++ public:++ // ----------------------------------------------------------------------+ // Construction, initialization, and destruction+ // ----------------------------------------------------------------------++ //! Construct object Copilot+ //!+ Copilot(+ const char *const compName /*!< The component name*/+ );++ //! Initialize object Copilot+ //!+ void init(+ const NATIVE_INT_TYPE queueDepth, /*!< The queue depth*/+ const NATIVE_INT_TYPE instance = 0 /*!< The instance number*/+ );++ //! Destroy object Copilot+ //!+ ~Copilot();++ PRIVATE:++ // ----------------------------------------------------------------------+ // Handler implementations for user-defined typed input ports+ // ----------------------------------------------------------------------++{{{hdrHandlers}}}++ PRIVATE:++ // ----------------------------------------------------------------------+ // Command handler implementations+ // ----------------------------------------------------------------------++ //! Implementation for CHECK_MONITORS command handler+ //! + void CHECK_MONITORS_cmdHandler(+ const FwOpcodeType opCode, /*!< The opcode*/+ const U32 cmdSeq /*!< The command sequence number*/+ );++ };++} // end namespace Ref++#endif
templates/fprime/instance-copilot view
@@ -1,3 +1,3 @@ instance copilotMonitor: Ref.Copilot base id 0x2700 \- queue size Default.queueSize+ queue size Default.QUEUE_SIZE
+ templates/standalone/Copilot.hs view
@@ -0,0 +1,40 @@+import Copilot.Compile.C99+import Copilot.Language hiding (prop)+import Copilot.Language.Prelude+import Copilot.Library.LTL (next)+import Copilot.Library.MTL hiding (since, alwaysBeen, trigger)+import Copilot.Library.PTLTL (since, previous, alwaysBeen)+import qualified Copilot.Library.PTLTL as PTLTL+import qualified Copilot.Library.MTL as MTL+import Language.Copilot (reify)+import Prelude hiding ((&&), (||), (++), (<=), (>=), (<), (>), (==), (/=), not)++{{{externs}}}+{{{internals}}}+{{{reqs}}}++-- | Clock that increases in one-unit steps.+clock :: Stream Int64+clock = [0] ++ (clock + 1)++-- | First Time Point+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++-- | Complete specification. Calls C handler functions when properties are+-- violated.+spec :: Spec+spec = do+{{{triggers}}}++main :: IO ()+main = reify spec >>= compile "{{{specName}}}"
tests/Main.hs view
@@ -5,6 +5,7 @@ import Test.Framework ( Test, defaultMainWithOpts ) import Test.Framework.Providers.HUnit ( testCase ) import Test.HUnit ( assertBool )+import System.Directory ( getTemporaryDirectory ) -- Internal imports import Command.CStructs2Copilot (cstructs2Copilot)@@ -20,37 +21,37 @@ tests :: [Test.Framework.Test] tests = [- testCase "fret-cmd-fret-cs-ok"- (testFretComponentSpec2Copilot "tests/fret_good.json" True)+ testCase "standalone-cmd-fcs-ok"+ (testStandaloneFCS "tests/fcs_good.json" True) -- Should pass - , testCase "fret-cmd-fret-file-not-found"- (testFretComponentSpec2Copilot "tests/file-invalid.json" False)+ , testCase "standalone-cmd-fsc-file-not-found"+ (testStandaloneFCS "tests/file-invalid.json" False) -- Should fail because the file does not exist - , testCase "fret-cmd-fret-parse-fail-1"- (testFretComponentSpec2Copilot- "tests/commands-fret-error-parsing-failed-1.json"+ , testCase "standalone-cmd-fcs-parse-fail-1"+ (testStandaloneFCS+ "tests/commands-fcs-error-parsing-failed-1.json" False ) -- Should fail because the opening bracket is [ and not { - , testCase "fret-cmd-fret-parse-fail-2"- (testFretComponentSpec2Copilot- "tests/commands-fret-error-parsing-failed-2.json"+ , testCase "standalone-cmd-fcs-parse-fail-2"+ (testStandaloneFCS+ "tests/commands-fcs-error-parsing-failed-2.json" False ) -- Should fail because a field is missing in an external variable - , testCase "fret-cmd-fret-parse-fail-3"- (testFretComponentSpec2Copilot- "tests/commands-fret-error-parsing-failed-3.json"+ , testCase "standalone-cmd-fcs-parse-fail-3"+ (testStandaloneFCS+ "tests/commands-fcs-error-parsing-failed-3.json" False ) -- Should fail because a field is missing in an internal variable - , testCase "fret-reqs-db-cocospec"- (testFretReqsDBCoCoSpec2Copilot "tests/fret-example1.json" True)+ , testCase "standalone-reqs-db-cocospec"+ (testStandaloneFDB "tests/fdb-example1.json" True) -- Should pass , testCase "structs-parse-ok"@@ -88,24 +89,27 @@ errorMsg = "The result of the transformation of the C header file " ++ file ++ " to Copilot struct declarations was unexpected." --- | Test FRET Component Spec 2 Copilot transformation.+-- | Test standalone backend. ----- This test uses the Copilot backend for FRET files, so it generates a Copilot--- file.+-- This test uses the standalone, so it generates a Copilot file. -- -- This IO action fails if any of the following are true: -- * The given file is not found or accessible. -- * The format in the given file is incorrect. -- * Ogma fails due to an internal error or bug.-testFretComponentSpec2Copilot :: FilePath -- ^ Path to a FRET/JSON requirements file- -> Bool- -> IO ()-testFretComponentSpec2Copilot file success = do+testStandaloneFCS :: FilePath -- ^ Path to a input file+ -> Bool+ -> IO ()+testStandaloneFCS file success = do+ targetDir <- getTemporaryDirectory let opts = StandaloneOptions { standaloneFormat = "fcs" , standalonePropFormat = "smv" , standaloneTypeMapping = [("int", "Int64"), ("real", "Float")]- , standaloneFilename = "fret"+ , standaloneFilename = "monitor"+ , standaloneTargetDir = targetDir+ , standaloneTemplateDir = Nothing+ , standalonePropVia = Nothing } result <- standalone file opts @@ -115,29 +119,32 @@ assertBool errorMsg testPass where- errorMsg = "The result of the transformation of FRET CS file "+ errorMsg = "The result of the transformation of input file " ++ file ++ " to Copilot was unexpected." --- | Test FRET Component Spec 2 Copilot transformation.+-- | Test standalone backend with FDB format. ----- This test uses the Copilot backend for FRET files with the CoCoSpec--- frontend.+-- This test uses the standalone backend with the FDB format and the CoCoSpec+-- property format. -- -- This IO action fails if any of the following are true: -- * The given file is not found or accessible. -- * The format in the given file is incorrect. -- * Ogma fails due to an internal error or bug. ---testFretReqsDBCoCoSpec2Copilot :: FilePath -- ^ Path to a FRET/JSON- -- requirements file- -> Bool- -> IO ()-testFretReqsDBCoCoSpec2Copilot file success = do+testStandaloneFDB :: FilePath -- ^ Path to input file+ -> Bool+ -> IO ()+testStandaloneFDB file success = do+ targetDir <- getTemporaryDirectory let opts = StandaloneOptions { standaloneFormat = "fdb" , standalonePropFormat = "cocospec" , standaloneTypeMapping = []- , standaloneFilename = "fret"+ , standaloneFilename = "monitor"+ , standaloneTargetDir = targetDir+ , standaloneTemplateDir = Nothing+ , standalonePropVia = Nothing } result <- standalone file opts @@ -147,5 +154,5 @@ assertBool errorMsg testPass where- errorMsg = "The result of the transformation of FRET CS file "+ errorMsg = "The result of the transformation of input file " ++ file ++ " to Copilot was unexpected."