ogma-core 1.0.7 → 1.0.8
raw patch · 10 files changed
+831/−10 lines, 10 filesdep ~ogma-extradep ~ogma-language-cdep ~ogma-language-cocospec
Dependency ranges changed: ogma-extra, ogma-language-c, ogma-language-cocospec, ogma-language-copilot, ogma-language-fret-cs, ogma-language-fret-reqs, ogma-language-smv
Files
- CHANGELOG.md +7/−0
- ogma-core.cabal +20/−8
- src/Command/FPrimeApp.hs +739/−0
- src/Language/Trans/CoCoSpec2Copilot.hs +1/−0
- src/Language/Trans/FRETComponentSpec2Copilot.hs +1/−1
- src/Language/Trans/FRETReqsDB2Copilot.hs +1/−1
- src/Language/Trans/SMV2Copilot.hs +1/−0
- templates/fprime/CMakeLists.txt +9/−0
- templates/fprime/Dockerfile +49/−0
- templates/fprime/instance-copilot +3/−0
CHANGELOG.md view
@@ -1,5 +1,12 @@ # Revision history for ogma-core +## [1.0.8] - 2023-03-21++* Version bump 1.0.8 (#81).+* Support inequality operator in SMV and CoCoSpec (#71).+* Introduce new F' (FPrime) backend (#77).+* Mark package as uncurated (#74).+ ## [1.0.7] - 2023-01-21 * Version bump 1.0.7 (#69). * Introduce new ROS2 backend (#56).
ogma-core.cabal view
@@ -32,7 +32,7 @@ build-type: Simple name: ogma-core-version: 1.0.7+version: 1.0.8 homepage: http://nasa.gov license: OtherLicense license-file: LICENSE.pdf@@ -63,12 +63,24 @@ templates/ros/CMakeLists.txt templates/ros/src/.keep templates/ros/package.xml+ templates/fprime/CMakeLists.txt+ templates/fprime/Dockerfile+ templates/fprime/instance-copilot++-- Ogma packages should be uncurated so that only the official maintainers make+-- changes.+--+-- Because this is a NASA project, we want to make sure that users obtain+-- exactly what we publish, unmodified by anyone external to our project.+x-curation: uncurated+ library exposed-modules: Command.CFSApp Command.CStructs2Copilot Command.CStructs2MsgHandlers+ Command.FPrimeApp Command.FRETComponentSpec2Copilot Command.FRETReqsDB2Copilot Command.Result@@ -97,13 +109,13 @@ , IfElse , mtl - , ogma-extra >= 1.0.0 && < 1.1- , ogma-language-c >= 1.0.0 && < 1.1- , ogma-language-cocospec >= 1.0.0 && < 1.1- , ogma-language-copilot >= 1.0.0 && < 1.1- , ogma-language-fret-cs >= 1.0.0 && < 1.1- , ogma-language-fret-reqs >= 1.0.0 && < 1.1- , ogma-language-smv >= 1.0.0 && < 1.1+ , ogma-extra >= 1.0.8 && < 1.1+ , ogma-language-c >= 1.0.8 && < 1.1+ , ogma-language-cocospec >= 1.0.8 && < 1.1+ , ogma-language-copilot >= 1.0.8 && < 1.1+ , ogma-language-fret-cs >= 1.0.8 && < 1.1+ , ogma-language-fret-reqs >= 1.0.8 && < 1.1+ , ogma-language-smv >= 1.0.8 && < 1.1 hs-source-dirs: src
+ src/Command/FPrimeApp.hs view
@@ -0,0 +1,739 @@+-- Copyright 2022 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.+--+-- | Create <https://github.com/nasa/fprime FPrime> components that subscribe+-- to obtain data and call Copilot when new values arrive.++{- HLINT ignore "Functor law" -}+module Command.FPrimeApp+ ( fprimeApp+ , ErrorCode+ )+ where++-- External imports+import qualified Control.Exception as E+import Control.Monad.Except ( ExceptT, liftEither, liftIO, runExceptT,+ throwError )+import Data.Aeson ( eitherDecode )+import Data.Char ( toUpper )+import Data.List ( find, intercalate, nub, sort )+import Data.Maybe ( fromMaybe )+import System.FilePath ( (</>) )++-- External imports: auxiliary+import Data.ByteString.Extra as B ( safeReadFile )+import Data.String.Extra ( sanitizeLCIdentifier, sanitizeUCIdentifier )+import System.Directory.Extra ( copyDirectoryRecursive )++-- Internal imports: auxiliary+import Command.Result ( Result (..) )+import Data.Location ( Location (..) )+import Language.FRETComponentSpec.AST ( FRETComponentSpec,+ fretExternalVariableName,+ fretExternalVariables,+ fretRequirementName, fretRequirements )++-- Internal imports+import Paths_ogma_core ( getDataDir )++-- * 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.+ -> IO (Result ErrorCode)+fprimeApp targetDir fretCSFile varNameFile varDBFile handlersFile =+ processResult $ do+ cs <- parseOptionalFRETCS fretCSFile+ vs <- parseOptionalVariablesFile varNameFile+ rs <- parseOptionalRequirementsListFile handlersFile+ varDB <- parseOptionalVarDBFile varDBFile++ liftEither $ checkArguments cs vs rs++ let varNames = fromMaybe (fretCSExtractExternalVariables cs) vs+ monitors = fromMaybe (fretCSExtractHandlers cs) rs++ e <- liftIO $ fprimeApp' targetDir varNames varDB monitors+ liftEither e++-- | 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.+ -> [String] -- ^ List of variable names (data sources).+ -> [(String, String)] -- ^ List of variables with their types, and+ -- the message IDs (topics) they can be+ -- obtained from.+ -> [String] -- ^ List of handlers associated to the+ -- monitors (or requirements monitored).+ -> IO (Either ErrorTriplet ())+fprimeApp' targetDir varNames varDB monitors =+ E.handle (return . Left . cannotCopyTemplate) $ do+ -- Obtain template dir+ dataDir <- getDataDir+ let templateDir = dataDir </> "templates" </> "fprime"++ -- Expand template+ copyDirectoryRecursive templateDir targetDir++ let f n o@(oVars) =+ case variableMap varDB n of+ Nothing -> o+ Just vars -> (vars : oVars)++ -- This is a Data.List.unzip4+ let vars = foldr f [] varNames++ let fprimeFileName =+ targetDir </> "Copilot.fpp"+ fprimeFileContents =+ unlines $+ componentInterface vars monitors++ writeFile fprimeFileName fprimeFileContents++ let fprimeFileName =+ targetDir </> "Copilot.hpp"+ fprimeFileContents =+ unlines $+ componentHeader vars monitors++ writeFile fprimeFileName fprimeFileContents++ let fprimeFileName =+ targetDir </> "Copilot.cpp"+ fprimeFileContents =+ unlines $+ componentImpl vars monitors++ writeFile fprimeFileName fprimeFileContents++ return $ Right ()++-- ** Argument processing++-- | Process FRET component spec, if available, and return its abstract+-- representation.+parseOptionalFRETCS :: Maybe FilePath+ -> ExceptT ErrorTriplet IO (Maybe FRETComponentSpec)+parseOptionalFRETCS Nothing = return Nothing+parseOptionalFRETCS (Just fp) = do+ -- Throws an exception if the file cannot be read.+ content <- liftIO $ B.safeReadFile fp++ let fretCS :: Either String FRETComponentSpec+ fretCS = eitherDecode =<< content++ case fretCS of+ Left e -> throwError $ cannotOpenFRETFile fp e+ Right cs -> return $ Just cs++-- | Process a variable selection file, if available, and return the variable+-- names.+parseOptionalVariablesFile :: Maybe FilePath+ -> ExceptT ErrorTriplet IO (Maybe [String])+parseOptionalVariablesFile Nothing = return Nothing+parseOptionalVariablesFile (Just fp) = do+ -- Fail if the file cannot be opened.+ varNamesE <- liftIO $ E.try $ lines <$> readFile fp+ case varNamesE of+ Left e -> throwError $ cannotOpenVarFile fp e+ Right varNames -> return $ Just varNames++-- | Process a requirements / handlers list file, if available, and return the+-- handler names.+parseOptionalRequirementsListFile :: Maybe FilePath+ -> ExceptT ErrorTriplet IO (Maybe [String])+parseOptionalRequirementsListFile Nothing = return Nothing+parseOptionalRequirementsListFile (Just fp) = do+ -- Fail if the file cannot be opened.+ handlerNamesE <- liftIO $ E.try $ lines <$> readFile fp+ case handlerNamesE of+ Left e -> throwError $ cannotOpenHandlersFile fp e+ Right monitors -> return $ Just monitors++-- | Process a variable database file, if available, and return the rows in it.+parseOptionalVarDBFile :: Maybe FilePath+ -> ExceptT ErrorTriplet+ IO+ [(String, String)]+parseOptionalVarDBFile Nothing = return []+parseOptionalVarDBFile (Just fp) = do+ -- We first try to open the files we need to fill in details in the FPrime+ -- component template.+ --+ -- The variable DB is optional, so this check only fails if the filename+ -- provided does not exist or if the file cannot be opened or parsed (wrong+ -- format).+ varDBE <- liftIO $ E.try $ fmap read <$> lines <$> readFile fp+ case varDBE of+ Left e -> throwError $ cannotOpenDB fp e+ Right varDB -> return varDB++-- | Check that the arguments provided are sufficient to operate.+--+-- 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.+--+-- If a FRET file is not provided, then the user must provide BOTH a variable+-- list, and a list of handlers.+checkArguments :: Maybe FRETComponentSpec+ -> Maybe [String]+ -> Maybe [String]+ -> Either ErrorTriplet ()+checkArguments Nothing Nothing Nothing = Left wrongArguments+checkArguments Nothing Nothing _ = Left wrongArguments+checkArguments Nothing _ Nothing = Left wrongArguments+checkArguments _ (Just []) _ = Left wrongArguments+checkArguments _ _ (Just []) = Left wrongArguments+checkArguments _ _ _ = Right ()++-- | Extract the variables from a FRET component specification, and sanitize+-- them to be used in FPrime.+fretCSExtractExternalVariables :: Maybe FRETComponentSpec -> [String]+fretCSExtractExternalVariables Nothing = []+fretCSExtractExternalVariables (Just cs) = map sanitizeLCIdentifier+ $ map fretExternalVariableName+ $ fretExternalVariables cs++-- | Extract the requirements from a FRET component specification, and sanitize+-- them to match the names of the handlers used by Copilot.+fretCSExtractHandlers :: Maybe FRETComponentSpec -> [String]+fretCSExtractHandlers Nothing = []+fretCSExtractHandlers (Just cs) = map handlerNameF+ $ map fretRequirementName+ $ fretRequirements cs+ where+ handlerNameF = ("handlerprop" ++) . sanitizeUCIdentifier++-- | Return the variable information needed to generate declarations+-- and subscriptions for a given variable name and variable database.+variableMap :: [(String, String)]+ -> String+ -> Maybe VarDecl+variableMap varDB varName =+ csvToVarMap <$> find (sameName varName) varDB++ where++ -- True if the given variable and db entry have the same name+ sameName :: String+ -> (String, String)+ -> Bool+ sameName n (vn, _) = n == vn++ -- Convert a DB row into Variable info needed to generate the FPrime file+ csvToVarMap :: (String, String)+ -> (VarDecl)+ csvToVarMap (nm, ty) = (VarDecl nm ty)++-- | The declaration of a variable in C, with a given type and name.+data VarDecl = VarDecl+ { varDeclName :: String+ , varDeclType :: String+ }++-- * FPrime component content++-- | Return the contents of the FPrime component interface (.fpp) specification.+componentInterface :: [VarDecl]+ -> [String] -- Monitors+ -> [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"+ , ""+ , " }"+ , ""+ , "}"+ ]+ where++ typePorts = nub $ sort $ map toTypePort variables+ toTypePort varDecl = " port "+ ++ fprimeVarDeclType varDecl+ ++ "Value(value: "+ ++ fprimeVarDeclType varDecl+ ++ ")"++ inputPorts = map toInputPortDecl variables+ toInputPortDecl varDecl = " async input port "+ ++ varDeclName varDecl+ ++ "In : " ++ fprimeVarDeclType varDecl+ ++ "Value"++ fprimeVarDeclType varDecl = case varDeclType varDecl of+ "uint8_t" -> "U8"+ "uint16_t" -> "U16"+ "uint32_t" -> "U32"+ "uint64_t" -> "U64"+ "int8_t" -> "I8"+ "int16_t" -> "I16"+ "int32_t" -> "I32"+ "int64_t" -> "I64"+ "float" -> "F32"+ "double" -> "F64"+ def -> def++ violationEvents = intercalate [""]+ $ map violationEvent monitors+ violationEvent monitor =+ [ " @ " ++ monitor ++ " violation"+ , " event " ++ ucMonitor ++ "_VIOLATION("+ , " " ++ replicate (length ucMonitor) ' ' ++ " ) \\"+ , " severity activity high \\"+ , " id 0 \\"+ , " format \"" ++ monitor ++ " violation\""+ ]+ where+ ucMonitor = map toUpper monitor++-- | 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"+ ]+ where+ handlers = intercalate [""]+ $ map toInputHandler variables+ toInputHandler nm =+ [ " //! Handler implementation for " ++ varDeclName nm ++ "In"+ , " //!"+ , " void " ++ varDeclName nm ++ "In_handler("+ , " const NATIVE_INT_TYPE portNum, /*!< The port number*/"+ , " " ++ portTy ++ " value"+ , " );"+ ]+ where+ portTy = varDeclType nm+++-- | Return the contents of the main FPrime component.+componentImpl :: [VarDecl]+ -> [String] -- Monitors+ -> [String]+componentImpl variables monitors =+ [ "// ======================================================================"+ , "// \\title Copilot.cpp"+ , "// \\author Ogma"+ , "// \\brief cpp file for Copilot component implementation class"+ , "// ======================================================================"+ , ""+ , ""+ , "#include <Ref/Copilot/Copilot.hpp>"+ , "#include \"Fw/Types/BasicTypes.hpp\""+ , ""+ , "#ifdef __cplusplus"+ , "extern \"C\" {"+ , "#endif"+ , ""+ , "#include \"copilot.h\""+ , "#include \"copilot_types.h\""+ , ""+ , "#ifdef __cplusplus"+ , "}"+ , "#endif"+ , ""+ ]+ ++ inputs+ ++ monitorResults +++ [ ""+ , "namespace Ref {"+ , ""+ , " // ----------------------------------------------------------------------"+ , " // Construction, initialization, and destruction"+ , " // ----------------------------------------------------------------------"+ , ""+ , " Copilot ::"+ , " Copilot("+ , " const char *const compName"+ , " ) : CopilotComponentBase(compName)"+ , " {"+ , ""+ , " }"+ , ""+ , " void Copilot ::"+ , " init("+ , " const NATIVE_INT_TYPE queueDepth,"+ , " const NATIVE_INT_TYPE instance"+ , " )"+ , " {"+ , " CopilotComponentBase::init(queueDepth, instance);"+ , " }"+ , ""+ , " Copilot ::"+ , " ~Copilot()"+ , " {"+ , ""+ , " }"+ , ""+ , " // ----------------------------------------------------------------------"+ , " // Handler implementations for user-defined typed input ports"+ , " // ----------------------------------------------------------------------"+ , ""+ ]+ ++ inputHandlers +++ [ ""+ , " // ----------------------------------------------------------------------"+ , " // Command handler implementations"+ , " // ----------------------------------------------------------------------"+ , ""+ , " void Copilot ::"+ , " CHECK_MONITORS_cmdHandler("+ , " const FwOpcodeType opCode,"+ , " const U32 cmdSeq"+ , " )"+ , " {"+ ]+ ++ triggerResultReset +++ [ " step();"+ , " this->cmdResponse_out(opCode,cmdSeq,Fw::CmdResponse::OK);"+ ]+ ++ triggerChecks +++ [ " }"+ , ""+ , "} // end namespace Ref"+ , ""+ ]+ ++ triggers++ where++ inputs = variablesS++ monitorResults = intercalate [""]+ $ map monitorResult monitors+ monitorResult monitor =+ [ "bool " ++ monitor ++ "_result;"+ ]++ inputHandlers = intercalate [""]+ $ map toInputHandler variables+ toInputHandler nm =+ [ " void Copilot :: "+ , " " ++ varDeclName nm ++ "In_handler("+ , " const NATIVE_INT_TYPE portNum,"+ , " " ++ portTy ++ " value"+ , " )"+ , " {"+ , " " ++ varDeclName nm ++ " = (" ++ ty ++ ") value;"+ , " }"+ ]+ where+ portTy = varDeclType nm+ ty = varDeclType nm++ triggerResultReset = intercalate [""]+ $ map monitorResultReset monitors+ monitorResultReset monitor =+ [ " " ++ monitor ++ "_result = false;"+ ]++ triggerChecks = intercalate [""]+ $ map triggerCheck monitors+ triggerCheck monitor =+ [ " if (" ++ monitor ++ "_result) {"+ , " this->log_ACTIVITY_HI_" ++ ucMonitor ++ "_VIOLATION();"+ , " }"+ ]+ where+ ucMonitor = map toUpper monitor++ triggers :: [String]+ triggers = intercalate [""]+ $ map triggerImpl monitors+ triggerImpl monitor =+ [ "void " ++ monitor ++ "() {"+ , " " ++ monitor ++ "_result = true;"+ , "}"+ ]++ variablesS :: [String]+ variablesS = map toVarDecl variables+ toVarDecl varDecl =+ varDeclType varDecl ++ " " ++ varDeclName varDecl ++ ";"++-- * Exception handlers++-- | Exception handler to deal with the case in which the arguments+-- provided are incorrect.+wrongArguments :: ErrorTriplet+wrongArguments =+ 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."++-- | Exception handler to deal with the case in which the FRET CS cannot be+-- opened.+cannotOpenFRETFile :: FilePath -> String -> ErrorTriplet+cannotOpenFRETFile file _e =+ ErrorTriplet ecCannotOpenFRETFile msg (LocationFile file)+ where+ msg =+ "cannot open FRET component specification file " ++ file++-- | Exception handler to deal with the case in which the variable DB cannot be+-- opened.+cannotOpenDB :: FilePath -> E.SomeException -> ErrorTriplet+cannotOpenDB file _e =+ ErrorTriplet ecCannotOpenDBUser msg (LocationFile file)+ where+ msg =+ "cannot open variable DB file " ++ file++-- | Exception handler to deal with the case in which the variable file+-- provided by the user cannot be opened.+cannotOpenVarFile :: FilePath -> E.SomeException -> ErrorTriplet+cannotOpenVarFile file _e =+ ErrorTriplet ecCannotOpenVarFile msg (LocationFile file)+ where+ msg =+ "cannot open variable list file " ++ file++-- | Exception handler to deal with the case in which the handlers file+-- provided by the user cannot be opened.+cannotOpenHandlersFile :: FilePath -> E.SomeException -> ErrorTriplet+cannotOpenHandlersFile file _e =+ ErrorTriplet ecCannotOpenHandlersFile msg (LocationFile file)+ where+ msg =+ "cannot open handler list file " ++ file++-- | Exception handler to deal with the case of files that cannot be+-- copied/generated due lack of space or permissions or some I/O error.+cannotCopyTemplate :: E.SomeException -> ErrorTriplet+cannotCopyTemplate e =+ ErrorTriplet ecCannotCopyTemplate msg LocationNothing+ where+ msg =+ "FPrime component 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 e++-- | A triplet containing error information.+data ErrorTriplet = ErrorTriplet ErrorCode String Location++-- | Process a computation that can fail with an error code, and turn it into a+-- computation that returns a 'Result'.+processResult :: Monad m => ExceptT ErrorTriplet m a -> m (Result ErrorCode)+processResult m = do+ r <- runExceptT m+ case r of+ Left (ErrorTriplet errorCode msg location)+ -> return $ Error errorCode msg location+ _ -> return Success++-- * Error codes++-- | Encoding of reasons why the command can fail.+--+-- The error codes used are 1 for user error, and 2 for internal bug.+type ErrorCode = Int++-- | Error: wrong arguments provided.+ecWrongArguments :: ErrorCode+ecWrongArguments = 1++-- | Error: the FRET component specification provided by the user cannot be+-- opened.+ecCannotOpenFRETFile :: ErrorCode+ecCannotOpenFRETFile = 1++-- | Error: the variable DB provided by the user cannot be opened.+ecCannotOpenDBUser :: ErrorCode+ecCannotOpenDBUser = 1++-- | Error: the variable file provided by the user cannot be opened.+ecCannotOpenVarFile :: ErrorCode+ecCannotOpenVarFile = 1++-- | Error: the handlers file provided by the user cannot be opened.+ecCannotOpenHandlersFile :: ErrorCode+ecCannotOpenHandlersFile = 1++-- | Error: the files cannot be copied/generated due lack of space or+-- permissions or some I/O error.+ecCannotCopyTemplate :: ErrorCode+ecCannotCopyTemplate = 1
src/Language/Trans/CoCoSpec2Copilot.hs view
@@ -113,6 +113,7 @@ -- operator. opTwoNum2Copilot :: BoolNumOp -> String opTwoNum2Copilot BoolNumOp2Eq = "=="+opTwoNum2Copilot BoolNumOp2Ne = "/=" opTwoNum2Copilot BoolNumOp2Le = "<=" opTwoNum2Copilot BoolNumOp2Lt = "<" opTwoNum2Copilot BoolNumOp2Gt = ">="
src/Language/Trans/FRETComponentSpec2Copilot.hs view
@@ -107,7 +107,7 @@ , "import qualified Copilot.Library.MTL as MTL" , "import Language.Copilot (reify)" , "import Prelude hiding ((&&), (||), (++),"- ++ " (<=), (>=), (<), (>), (==), not)"+ ++ " (<=), (>=), (<), (>), (==), (/=), not)" , "" ]
src/Language/Trans/FRETReqsDB2Copilot.hs view
@@ -111,7 +111,7 @@ , "import qualified Copilot.Library.PTLTL as PTLTL" , "import Language.Copilot (reify)" , "import Prelude hiding ((&&), (||), (++), (<=), (>=),"- ++ " (<), (>), (==), not)"+ ++ " (<), (>), (==), (/=), not)" , "" ]
src/Language/Trans/SMV2Copilot.hs view
@@ -134,6 +134,7 @@ ordOp2Copilot OrdOpLT = "<" ordOp2Copilot OrdOpLE = "<=" ordOp2Copilot OrdOpEQ = "=="+ordOp2Copilot OrdOpNE = "/=" ordOp2Copilot OrdOpGT = ">" ordOp2Copilot OrdOpGE = ">="
+ templates/fprime/CMakeLists.txt view
@@ -0,0 +1,9 @@+# Register the standard build+set(SOURCE_FILES+ "${CMAKE_CURRENT_LIST_DIR}/copilot.c"+ "${CMAKE_CURRENT_LIST_DIR}/copilot.h"+ "${CMAKE_CURRENT_LIST_DIR}/copilot_types.h"+ "${CMAKE_CURRENT_LIST_DIR}/Copilot.cpp"+ "${CMAKE_CURRENT_LIST_DIR}/Copilot.fpp"+)+register_fprime_module()
+ templates/fprime/Dockerfile view
@@ -0,0 +1,49 @@+# This dockerfile compiles a monitoring application inside FPrime's Reference+# Application.+FROM ubuntu:focal++# Avoid questions during package installation.+ENV DEBIAN_FRONTEND=noninteractive++# Install FPrime dependencies and clone fprime from the repo.+RUN apt-get update+RUN apt-get install -y git cmake gcc python3 pip++RUN git clone https://github.com/nasa/fprime+RUN pip install -r fprime/requirements.txt++WORKDIR fprime/Ref++# Add all the monitoring app files.+RUN mkdir Copilot+ADD CMakeLists.txt Copilot/+ADD Copilot.fpp Copilot/+ADD Copilot.cpp Copilot/+ADD Copilot.hpp Copilot/+ADD copilot.c Copilot/+ADD copilot.h Copilot/+ADD copilot_types.h Copilot/++# Enable Copilot app (add it after SignalGen).+RUN sed -i -e '/^add_fprime_subdirectory.*SignalGen.*/a add_fprime_subdirectory("${CMAKE_CURRENT_LIST_DIR}\/Copilot\/")' CMakeLists.txt++RUN fprime-util generate++# Update Ref deployment.++## Define Component Instance.+##+## This command adds the contents of the given instance-copilot at the end of+## Queued component instances section, which is right before the Passive+## components section.+ADD instance-copilot .+RUN line=$(grep -n 'Passive component instances' Top/instances.fpp | tail -n1 | cut -d: -f1); line=$(($line - 2)); sed -i -e "${line}r instance-copilot" Top/instances.fpp+RUN rm instance-copilot++## Update topology.+##+## This command adds the copilot monitoring node right after linuxTime in the+## topology.+RUN sed -i -e '/^ \+instance linuxTime/a\ \ \ \ instance copilotMonitor' Top/topology.fpp++RUN fprime-util build --jobs "$(nproc || printf '%s\n' 1)"
+ templates/fprime/instance-copilot view
@@ -0,0 +1,3 @@+ instance copilotMonitor: Ref.Copilot base id 0x2700 \+ queue size Default.queueSize+