diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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). diff --git a/data/formats/xml-md_cocospec b/data/formats/xml-md_cocospec new file mode 100644 --- /dev/null +++ b/data/formats/xml-md_cocospec @@ -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) + } diff --git a/data/formats/xml-md_smv b/data/formats/xml-md_smv new file mode 100644 --- /dev/null +++ b/data/formats/xml-md_smv @@ -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) + } diff --git a/data/formats/xml-reqif_cocospec b/data/formats/xml-reqif_cocospec new file mode 100644 --- /dev/null +++ b/data/formats/xml-reqif_cocospec @@ -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()")) + } diff --git a/data/formats/xml-reqif_smv b/data/formats/xml-reqif_smv new file mode 100644 --- /dev/null +++ b/data/formats/xml-reqif_smv @@ -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()")) + } diff --git a/ogma-core.cabal b/ogma-core.cabal --- a/ogma-core.cabal +++ b/ogma-core.cabal @@ -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 diff --git a/src/Command/Diagram.hs b/src/Command/Diagram.hs new file mode 100644 --- /dev/null +++ b/src/Command/Diagram.hs @@ -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) "" 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." diff --git a/src/Command/FPrimeApp.hs b/src/Command/FPrimeApp.hs --- a/src/Command/FPrimeApp.hs +++ b/src/Command/FPrimeApp.hs @@ -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 " - , "#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" diff --git a/src/Command/ROSApp.hs b/src/Command/ROSApp.hs --- a/src/Command/ROSApp.hs +++ b/src/Command/ROSApp.hs @@ -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 diff --git a/src/Command/Standalone.hs b/src/Command/Standalone.hs --- a/src/Command/Standalone.hs +++ b/src/Command/Standalone.hs @@ -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. diff --git a/src/Language/Trans/Spec2Copilot.hs b/src/Language/Trans/Spec2Copilot.hs --- a/src/Language/Trans/Spec2Copilot.hs +++ b/src/Language/Trans/Spec2Copilot.hs @@ -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" diff --git a/templates/diagram/Copilot.hs b/templates/diagram/Copilot.hs new file mode 100644 --- /dev/null +++ b/templates/diagram/Copilot.hs @@ -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) diff --git a/templates/fprime/Copilot.cpp b/templates/fprime/Copilot.cpp new file mode 100644 --- /dev/null +++ b/templates/fprime/Copilot.cpp @@ -0,0 +1,78 @@ +// ====================================================================== +// \title Copilot.cpp +// \author Ogma +// \brief cpp file for Copilot component implementation class +// ====================================================================== + + +#include +#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}}} diff --git a/templates/fprime/Copilot.fpp b/templates/fprime/Copilot.fpp new file mode 100644 --- /dev/null +++ b/templates/fprime/Copilot.fpp @@ -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 + + } + +} diff --git a/templates/fprime/Copilot.hpp b/templates/fprime/Copilot.hpp new file mode 100644 --- /dev/null +++ b/templates/fprime/Copilot.hpp @@ -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 diff --git a/templates/fprime/instance-copilot b/templates/fprime/instance-copilot --- a/templates/fprime/instance-copilot +++ b/templates/fprime/instance-copilot @@ -1,3 +1,3 @@ instance copilotMonitor: Ref.Copilot base id 0x2700 \ - queue size Default.queueSize + queue size Default.QUEUE_SIZE diff --git a/templates/standalone/Copilot.hs b/templates/standalone/Copilot.hs new file mode 100644 --- /dev/null +++ b/templates/standalone/Copilot.hs @@ -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}}}" diff --git a/tests/Main.hs b/tests/Main.hs --- a/tests/Main.hs +++ b/tests/Main.hs @@ -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."