diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,16 @@ # Revision history for ogma-core +## [1.5.0] - 2024-11-21 + +* Version bump 1.5.0 (#178). +* Fix incorrect path when using Space ROS humble-2024.10.0 (#158). +* Use template expansion system to generate cFS monitoring application (#157). +* Use template expansion system to generate ROS monitoring application (#162). +* Fix comment in generated Copilot spec (#164). +* Add missing notPreviousNot to generated spec (#168). +* Introduce new standalone command (#170). +* Correct name in documentation (#176). + ## [1.4.1] - 2024-09-21 * Version bump 1.4.1 (#155). diff --git a/data/formats/fcs_cocospec b/data/formats/fcs_cocospec new file mode 100644 --- /dev/null +++ b/data/formats/fcs_cocospec @@ -0,0 +1,13 @@ +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 = ".CoCoSpecCode" + } diff --git a/data/formats/fcs_smv b/data/formats/fcs_smv new file mode 100644 --- /dev/null +++ b/data/formats/fcs_smv @@ -0,0 +1,13 @@ +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" + } diff --git a/data/formats/fdb_cocospec b/data/formats/fdb_cocospec new file mode 100644 --- /dev/null +++ b/data/formats/fdb_cocospec @@ -0,0 +1,13 @@ +JSONFormat + { specInternalVars = Nothing + , specInternalVarId = "" + , specInternalVarExpr = "" + , specInternalVarType = Nothing + , specExternalVars = Just ".semantics.variables..*.*" + , specExternalVarId = "" + , specExternalVarType = Nothing + , specRequirements = "$[:]" + , specRequirementId = ".reqid" + , specRequirementDesc = Just ".fulltext" + , specRequirementExpr = ".semantics.CoCoSpecCode" + } diff --git a/data/formats/fdb_smv b/data/formats/fdb_smv new file mode 100644 --- /dev/null +++ b/data/formats/fdb_smv @@ -0,0 +1,13 @@ +JSONFormat + { specInternalVars = Nothing + , specInternalVarId = "" + , specInternalVarExpr = "" + , specInternalVarType = Nothing + , specExternalVars = Just ".semantics.variables..*.*" + , specExternalVarId = "" + , specExternalVarType = Nothing + , specRequirements = "$[:]" + , specRequirementId = ".reqid" + , specRequirementDesc = Just ".fulltext" + , specRequirementExpr = ".semantics.ptExpanded" + } diff --git a/ogma-core.cabal b/ogma-core.cabal --- a/ogma-core.cabal +++ b/ogma-core.cabal @@ -32,7 +32,7 @@ build-type: Simple name: ogma-core -version: 1.4.1 +version: 1.5.0 homepage: https://github.com/nasa/ogma license: OtherLicense license-file: LICENSE.pdf @@ -62,11 +62,16 @@ templates/copilot-cfs/fsw/src/copilot_cfs_events.h templates/ros/Dockerfile templates/ros/copilot/CMakeLists.txt - templates/ros/copilot/src/.keep + templates/ros/copilot/src/copilot_logger.cpp + templates/ros/copilot/src/copilot_monitor.cpp templates/ros/copilot/package.xml templates/fprime/CMakeLists.txt templates/fprime/Dockerfile templates/fprime/instance-copilot + data/formats/fcs_smv + data/formats/fcs_cocospec + data/formats/fdb_smv + data/formats/fdb_cocospec -- Ogma packages should be uncurated so that only the official maintainers make -- changes. @@ -82,10 +87,9 @@ Command.CStructs2Copilot Command.CStructs2MsgHandlers Command.FPrimeApp - Command.FRETComponentSpec2Copilot - Command.FRETReqsDB2Copilot Command.Result Command.ROSApp + Command.Standalone Data.Location @@ -108,14 +112,15 @@ , bytestring , filepath , mtl + , text >= 1.2.3.1 && < 2.1 - , ogma-extra >= 1.4.1 && < 1.5 - , ogma-language-c >= 1.4.1 && < 1.5 - , ogma-language-cocospec >= 1.4.1 && < 1.5 - , ogma-language-copilot >= 1.4.1 && < 1.5 - , ogma-language-jsonspec >= 1.4.1 && < 1.5 - , ogma-language-smv >= 1.4.1 && < 1.5 - , ogma-spec >= 1.4.1 && < 1.5 + , 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 hs-source-dirs: src diff --git a/src/Command/CFSApp.hs b/src/Command/CFSApp.hs --- a/src/Command/CFSApp.hs +++ b/src/Command/CFSApp.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE OverloadedStrings #-} -- Copyright 2020 United States Government as represented by the Administrator -- of the National Aeronautics and Space Administration. All Rights Reserved. -- @@ -45,16 +46,17 @@ where -- External imports -import qualified Control.Exception as E -import Data.List ( find ) -import System.FilePath ( () ) - --- External imports: auxiliary -import System.Directory.Extra ( copyDirectoryRecursive ) +import qualified Control.Exception as E +import Data.Aeson (decode, object, (.=)) +import Data.List (find) +import Data.Text (Text) +import Data.Text.Lazy (pack, unpack) +import System.FilePath ( () ) -- Internal imports: auxiliary -import Command.Result ( Result (..) ) -import Data.Location ( Location (..) ) +import Command.Result ( Result (..) ) +import Data.Location ( Location (..) ) +import System.Directory.Extra ( copyTemplate ) -- Internal imports import Paths_ogma_core ( getDataDir ) @@ -62,13 +64,14 @@ -- | Generate a new CFS application connected to Copilot. cFSApp :: FilePath -- ^ Target directory where the application -- should be created. + -> Maybe FilePath -- ^ Directory where the template is to be found. -> 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. -> IO (Result ErrorCode) -cFSApp targetDir varNameFile varDBFile = do +cFSApp targetDir mTemplateDir varNameFile varDBFile = do -- We first try to open the two files we need to fill in details in the CFS -- app template. @@ -97,12 +100,13 @@ Right varNames -> do -- Obtain template dir - dataDir <- getDataDir - let templateDir = dataDir "templates" "copilot-cfs" + templateDir <- case mTemplateDir of + Just x -> return x + Nothing -> do + dataDir <- getDataDir + return $ dataDir "templates" "copilot-cfs" E.handle (return . cannotCopyTemplate) $ do - -- Expand template - copyDirectoryRecursive templateDir targetDir let f n o@(oVars, oIds, oInfos, oDatas) = case variableMap varDB n of @@ -113,10 +117,18 @@ -- This is a Data.List.unzip4 let (vars, ids, infos, datas) = foldr f ([], [], [], []) varNames - let cfsFileName = targetDir "fsw" "src" "copilot_cfs.c" - cfsFileContents = unlines $ fileContents vars ids infos datas + let (variablesS, msgSubscriptionS, msgCasesS, msgHandlerS) = + appComponents vars ids infos datas + subst = object $ + [ "variablesS" .= pack variablesS + , "msgSubscriptionsS" .= pack msgSubscriptionS + , "msgCasesS" .= pack msgCasesS + , "msgHandlerS" .= pack msgHandlerS + ] - writeFile cfsFileName cfsFileContents + -- Expand template + copyTemplate templateDir subst targetDir + return Success -- | Predefined list of Icarous variables that are known to Ogma @@ -170,9 +182,10 @@ , msgDataVarType :: String } --- | Return the contents of the main CFS application. -fileContents :: [VarDecl] -> [MsgInfoId] -> [MsgInfo] -> [MsgData] -> [String] -fileContents variables msgIds msgNames msgDatas = cfsFileContents +-- | Return the components that are customized in a cFS application. +appComponents :: [VarDecl] -> [MsgInfoId] -> [MsgInfo] -> [MsgData] + -> (String, String, String, String) +appComponents variables msgIds msgNames msgDatas = cfsFileContents where variablesS = unlines $ map toVarDecl variables toVarDecl varDecl = varDeclType varDecl ++ " " ++ varDeclName varDecl ++ ";" @@ -205,157 +218,11 @@ ] cfsFileContents = - [ "/********************************************************************" - , "** File: copilot_cfs.c" - , "**" - , "** Purpose:" - , "** This file contains the source code for the Copilot App." - , "**" - , "*********************************************************************/" - , "" - , "/*" - , "** Include Files:" - , "*/" - , "" - , "#include \"copilot_cfs.h\"" - , "#include \"copilot_cfs_perfids.h\"" - , "#include \"copilot_cfs_msgids.h\"" - , "#include \"copilot_cfs_msg.h\"" - , "#include \"copilot_cfs_events.h\"" - , "#include \"copilot_cfs_version.h\"" - , "#include \"Icarous_msgids.h\"" - , "#include \"Icarous_msg.h\"" - , "" - , variablesS - , "void split(void);" - , "void step(void);" - , "" - , "/*" - , "** global data" - , "*/" - , "" - , "copilot_hk_tlm_t COPILOT_HkTelemetryPkt;" - , "CFE_SB_PipeId_t COPILOT_CommandPipe;" - , "CFE_SB_MsgPtr_t COPILOTMsgPtr;" - , "" - , "static CFE_EVS_BinFilter_t COPILOT_EventFilters[] =" - , " { /* Event ID mask */" - , " {COPILOT_STARTUP_INF_EID, 0x0000}," - , " {COPILOT_COMMAND_ERR_EID, 0x0000}," - , " {COPILOT_COMMANDCPVIOL_INF_EID, 0x0000}," - , " };" - , "" - , "/* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */" - , "/* COPILOT_AppMain() -- App entry point and main process loop */" - , "/* */" - , "/* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */" - , "void COPILOT_AppMain( void )" - , "{" - , " int32 status;" - , " uint32 RunStatus = CFE_ES_APP_RUN;" - , "" - , " CFE_ES_PerfLogEntry(COPILOT_CFS_PERF_ID);" - , "" - , " COPILOT_AppInit();" - , "" - , " /*" - , " ** COPILOT Runloop" - , " */" - , " while (CFE_ES_RunLoop(&RunStatus) == TRUE)" - , " {" - , " CFE_ES_PerfLogExit(COPILOT_CFS_PERF_ID);" - , "" - , " // Pend on receipt of command packet" - , " // (timeout set to 500 millisecs)" - , " status = CFE_SB_RcvMsg (&COPILOTMsgPtr," - , " COPILOT_CommandPipe," - , " 500);" - , " " - , " CFE_ES_PerfLogEntry(COPILOT_CFS_PERF_ID);" - , "" - , " if (status == CFE_SUCCESS)" - , " {" - , " COPILOT_ProcessCommandPacket();" - , " }" - , "" - , " }" - , "" - , " CFE_ES_ExitApp(RunStatus);" - , "" - , "} /* End of COPILOT_AppMain() */" - , "" - , "/* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */" - , "/* */" - , "/* COPILOT_AppInit() -- initialization */" - , "/* */" - , "/* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */" - , "void COPILOT_AppInit(void)" - , "{" - , " // Register the app with Executive services" - , " CFE_ES_RegisterApp();" - , "" - , " // Register the events" - , " CFE_EVS_Register(COPILOT_EventFilters," - , " sizeof(COPILOT_EventFilters) / " - ++ "sizeof(CFE_EVS_BinFilter_t)," - , " CFE_EVS_BINARY_FILTER);" - , "" - , " // Create the Software Bus command pipe and subscribe to " - , " // housekeeping messages" - , " CFE_SB_CreatePipe(&COPILOT_CommandPipe, COPILOT_PIPE_DEPTH," - ++ "\"COPILOT_CMD_PIPE\");" + ( variablesS , msgSubscriptionS - , "" - , " CFE_EVS_SendEvent (COPILOT_STARTUP_INF_EID," - , " CFE_EVS_INFORMATION," - , " \"COPILOT App Initialized. Ver %d.%d.%d.%d\"," - , " COPILOT_CFS_MAJOR_VERSION," - , " COPILOT_CFS_MINOR_VERSION, " - , " COPILOT_CFS_REVISION, " - , " COPILOT_CFS_MISSION_REV);" - , "" - , "} /* End of COPILOT_AppInit() */" - , "" - , "/* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */" - , "/* Name: COPILOT_ProcessCommandPacket */" - , "/* */" - , "/* Purpose: */" - , "/* This routine will process any packet that is received */" - , "/* on the COPILOT command pipe. */" - , "/* */" - , "/* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */" - , "void COPILOT_ProcessCommandPacket(void)" - , "{" - , " CFE_SB_MsgId_t MsgId;" - , "" - , " MsgId = CFE_SB_GetMsgId(COPILOTMsgPtr);" - , "" - , " switch (MsgId)" - , " {" , msgCasesS - , " default:" - , " COPILOT_HkTelemetryPkt.copilot_command_error_count++;" - , " CFE_EVS_SendEvent(COPILOT_COMMAND_ERR_EID,CFE_EVS_ERROR," - , " " - ++ "\"COPILOT: invalid command packet,MID = 0x%x\"," - , " MsgId);" - , " break;" - , " }" - , "" - , " return;" - , "" - , "} /* End COPILOT_ProcessCommandPacket */" - , "" , msgHandlerS - , "" - , "/**" - , " * Report copilot property violations." - , " */" - , "void split(void) {" - , " CFE_EVS_SendEvent(COPILOT_COMMANDCPVIOL_INF_EID, CFE_EVS_ERROR," - , " \"COPILOT: violation\");" - , "}" - ] + ) -- * Exception handlers diff --git a/src/Command/FRETComponentSpec2Copilot.hs b/src/Command/FRETComponentSpec2Copilot.hs deleted file mode 100644 --- a/src/Command/FRETComponentSpec2Copilot.hs +++ /dev/null @@ -1,204 +0,0 @@ -{-# LANGUAGE ExistentialQuantification #-} --- Copyright 2020 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 FRET component specification into a Copilot specification. --- --- This module makes use of --- "Language.Trans.FRETComponentSpec2Copilot", which does most of the work. -module Command.FRETComponentSpec2Copilot - ( fretComponentSpec2Copilot - , FRETComponentSpec2CopilotOptions(..) - , ErrorCode - ) - where - --- External imports -import Data.Aeson ( eitherDecode, decode ) -import Data.ByteString.Lazy (fromStrict) -import Data.Foldable (for_) - --- External imports: auxiliary -import Data.ByteString.Extra as B ( safeReadFile ) - --- Internal imports: auxiliary -import Command.Result ( Result (..) ) -import Data.Location ( Location (..) ) - --- Internal imports: language ASTs, transformers -import Data.OgmaSpec (Spec) - -import qualified Language.CoCoSpec.AbsCoCoSpec as CoCoSpec -import qualified Language.CoCoSpec.ParCoCoSpec as CoCoSpec ( myLexer, - pBoolSpec ) - -import Language.JSONSpec.Parser (JSONFormat (..), parseJSONSpec) - -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) -import Language.Trans.SMV2Copilot as SMV (boolSpec2Copilot) -import Language.Trans.Spec2Copilot (spec2Copilot, specAnalyze) - --- | Print the contents of a Copilot module that implements the Past-time TL --- formula in a FRET file. --- --- PRE: The file given is readable, contains a valid FRET file with a PT --- formula in the @ptExpanded@ key, the formula does not use any identifiers --- that exist in Copilot, or any of @prop@, @clock@, @ftp@. All identifiers --- used are valid C99 identifiers. -fretComponentSpec2Copilot :: FilePath -- ^ Path to a file containing a FRET - -- Component Specification - -> FRETComponentSpec2CopilotOptions - -- ^ Customization options - -- formula - -> IO (Result ErrorCode) -fretComponentSpec2Copilot fp options = do - - let functions = fretExprPair (fretCS2CopilotUseCoCoSpec options) - - copilot <- fretComponentSpec2Copilot' fp options functions - - let (mOutput, result) = - fretComponentSpec2CopilotResult options fp copilot - - for_ mOutput putStrLn - return result - --- | Print the contents of a Copilot module that implements the Past-time TL --- formula in a FRET file, using a subexpression handler. --- --- PRE: The file given is readable, contains a valid FRET file with a PT --- formula in the @ptExpanded@ key, the formula does not use any identifiers --- that exist in Copilot, or any of @prop@, @clock@, @ftp@. All identifiers --- used are valid C99 identifiers. -fretComponentSpec2Copilot' :: FilePath - -> FRETComponentSpec2CopilotOptions - -> FRETExprPair - -> IO (Either String String) -fretComponentSpec2Copilot' fp options (FRETExprPair parse replace print) = do - let name = fretCS2CopilotFilename options - useCoCoSpec = fretCS2CopilotUseCoCoSpec options - typeMaps = fretTypeToCopilotTypeMapping options - - -- 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 (fretFormat useCoCoSpec) =<< eitherDecode b - - let copilot = spec2Copilot name typeMaps replace print =<< specAnalyze =<< res - - return copilot - --- | Options used to customize the conversion of FRET Component Specifications --- to Copilot code. -data FRETComponentSpec2CopilotOptions = FRETComponentSpec2CopilotOptions - { fretCS2CopilotUseCoCoSpec :: Bool - , fretCS2CopilotIntType :: String - , fretCS2CopilotRealType :: String - , fretCS2CopilotFilename :: String - } - --- * Error codes - --- | Encoding of reasons why the command can fail. --- --- The error code used is 1 for user error. -type ErrorCode = Int - --- | Error: the FRET Component Spec file cannot be read due to the file being --- unreadable or the format being incorrect. -ecFretCSError :: ErrorCode -ecFretCSError = 1 - --- * Result - --- | Process the result of the transformation function. -fretComponentSpec2CopilotResult :: FRETComponentSpec2CopilotOptions - -> FilePath - -> Either String String - -> (Maybe String, Result ErrorCode) -fretComponentSpec2CopilotResult options fp result = case result of - Left msg -> (Nothing, Error ecFretCSError msg (LocationFile fp)) - Right t -> (Just t, Success) - --- * Parser - --- | JSONPath selectors for a FRET file -fretFormat :: Bool -> JSONFormat -fretFormat useCoCoSpec = 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 = if useCoCoSpec then ".CoCoSpecCode" else ".ptLTL" - } - --- * Mapping of types from FRET to Copilot -fretTypeToCopilotTypeMapping :: FRETComponentSpec2CopilotOptions - -> [(String, String)] -fretTypeToCopilotTypeMapping options = - [ ("bool", "Bool") - , ("int", fretCS2CopilotIntType options) - , ("integer", fretCS2CopilotIntType options) - , ("real", fretCS2CopilotRealType options) - , ("string", "String") - ] - --- * Handler for boolean expressions - --- | Handler for boolean expressions that knows how to parse them, replace --- variables in them, and convert them to Copilot. -data FRETExprPair = forall a . FRETExprPair - { exprParse :: String -> Either String a - , exprReplace :: [(String, String)] -> a -> a - , exprPrint :: a -> String - } - --- | Return a handler depending on whether it should be for CoCoSpec boolean --- expressions or for SMV boolean expressions. -fretExprPair :: Bool -> FRETExprPair -fretExprPair True = FRETExprPair (CoCoSpec.pBoolSpec . CoCoSpec.myLexer) - (\_ -> id) - (CoCoSpec.boolSpec2Copilot) -fretExprPair False = FRETExprPair (SMV.pBoolSpec . SMV.myLexer) - (substituteBoolExpr) - (SMV.boolSpec2Copilot) diff --git a/src/Command/FRETReqsDB2Copilot.hs b/src/Command/FRETReqsDB2Copilot.hs deleted file mode 100644 --- a/src/Command/FRETReqsDB2Copilot.hs +++ /dev/null @@ -1,213 +0,0 @@ -{-# LANGUAGE ExistentialQuantification #-} --- Copyright 2020 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 FRET requirements database containing a temporal logic --- specification into a Copilot specification. -module Command.FRETReqsDB2Copilot - ( fretReqsDB2Copilot - , FRETReqsDB2CopilotOptions(..) - , ErrorCode - ) - where - --- External imports -import Data.Aeson (eitherDecode) -import Data.Foldable (for_) -import Data.List (nub, (\\)) - --- External imports: auxiliary -import Data.ByteString.Extra as B ( safeReadFile ) - --- Internal imports: auxiliary -import Command.Result ( Result (..) ) -import Data.Location ( Location (..) ) - --- Internal imports: Generic specification, parser. -import Data.OgmaSpec (ExternalVariableDef (..), - InternalVariableDef (..), Requirement (..), - Spec (..)) -import Language.JSONSpec.Parser (JSONFormat (..), parseJSONSpec) - --- Internal imports: language ASTs, transformers -import qualified Language.CoCoSpec.ParCoCoSpec as CoCoSpec (myLexer, pBoolSpec) -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) -import Language.Trans.Spec2Copilot (spec2Copilot, specAnalyze) - --- | Print the contents of a Copilot module that implements the Past-time TL --- formula in a FRET file. --- --- PRE: The file given is readable, contains a valid FRET file with a PT --- formula in the @ptExpanded@ key, the formula does not use any identifiers --- that exist in Copilot, or any of @prop@, @clock@, @ftp@. All identifiers --- used are valid C99 identifiers. -fretReqsDB2Copilot :: FilePath -- ^ Path to a file containing a FRET - -- Requirements Database - -> FRETReqsDB2CopilotOptions - -- ^ Customization options formula - -> IO (Result ErrorCode) -fretReqsDB2Copilot fp options = do - - let functions = fretExprPair (fretReqsDB2CopilotUseCoCoSpec options) - - copilot <- fretReqsDB2Copilot' fp options functions - - let (mOutput, result) = - fretReqsDB2CopilotResult options fp copilot - - for_ mOutput putStrLn - return result - --- | Print the contents of a Copilot module that implements the Past-time TL --- formula in a FRET file, using a subexpression handler. --- --- PRE: The file given is readable, contains a valid FRET file with a PT --- formula in the @ptExpanded@ key, the formula does not use any identifiers --- that exist in Copilot, or any of @prop@, @clock@, @ftp@. All identifiers --- used are valid C99 identifiers. -fretReqsDB2Copilot' :: FilePath - -> FRETReqsDB2CopilotOptions - -> FRETExprPair - -> IO (Either String String) -fretReqsDB2Copilot' fp options (FRETExprPair parse replace showExpr ids) = do - let name = fretReqsDB2CopilotFilename options - useCoCoSpec = fretReqsDB2CopilotUseCoCoSpec options - typeMaps = [("", "_")] - - -- 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 (fretFormat useCoCoSpec) =<< eitherDecode b - - -- Complement the specification with any missing/implicit definitions - let res' = fmap (addMissingIdentifiers ids) res - - let copilot = - spec2Copilot name typeMaps replace showExpr =<< specAnalyze =<< res' - - return copilot - --- | Options used to customize the conversion of FRET Requirements Database --- to Copilot code. -data FRETReqsDB2CopilotOptions = FRETReqsDB2CopilotOptions - { fretReqsDB2CopilotUseCoCoSpec :: Bool - , fretReqsDB2CopilotFilename :: String - } - --- * Error codes - --- | Encoding of reasons why the command can fail. --- --- The error code used is 1 for user error. -type ErrorCode = Int - --- | Error: the FRET Requirements DB file cannot be read due to the file being --- unreadable or the format being incorrect. -ecFretReqsDBError :: ErrorCode -ecFretReqsDBError = 1 - --- * Result - --- | Process the result of the transformation function. -fretReqsDB2CopilotResult :: FRETReqsDB2CopilotOptions - -> FilePath - -> Either String String - -> (Maybe String, Result ErrorCode) -fretReqsDB2CopilotResult _options fp result = case result of - Left msg -> (Nothing, Error ecFretReqsDBError msg (LocationFile fp)) - Right t -> (Just t, Success) - --- * Parser - --- | JSONPath selectors for a FRET file -fretFormat :: Bool -> JSONFormat -fretFormat useCoCoSpec = JSONFormat - { specInternalVars = Nothing - , specInternalVarId = "" - , specInternalVarExpr = "" - , specInternalVarType = Nothing - , specExternalVars = Just ".semantics.variables..*.*" - , specExternalVarId = "" - , specExternalVarType = Nothing - , specRequirements = "$[:]" - , specRequirementId = ".reqid" - , specRequirementDesc = Just ".fulltext" - , specRequirementExpr = if useCoCoSpec then ".semantics.CoCoSpecCode" else ".semantics.ptExpanded" - } - --- * Handler for boolean expressions - --- | Handler for boolean expressions that knows how to parse them, replace --- variables in them, and convert them to Copilot. -data FRETExprPair = forall a . FRETExprPair - { exprParse :: String -> Either String a - , exprReplace :: [(String, String)] -> a -> a - , exprPrint :: a -> String - , exprIdents :: a -> [String] - } - --- | Return a handler depending on whether it should be for CoCoSpec boolean --- expressions or for SMV boolean expressions. -fretExprPair :: Bool -> FRETExprPair -fretExprPair True = FRETExprPair (CoCoSpec.pBoolSpec . CoCoSpec.myLexer) - (\_ -> id) - (CoCoSpec.boolSpec2Copilot) - (CoCoSpec.boolSpecNames) -fretExprPair False = FRETExprPair (SMV.pBoolSpec . SMV.myLexer) - (substituteBoolExpr) - (SMV.boolSpec2Copilot) - (SMV.boolSpecNames) - --- | Add to a spec external variables for all identifiers mentioned in --- expressions that are not defined anywhere. -addMissingIdentifiers :: (a -> [String]) -> Spec a -> Spec a -addMissingIdentifiers f s = s { externalVariables = vars' } - where - vars' = externalVariables s ++ newVars - newVars = map (\n -> ExternalVariableDef n "") newVarNames - - -- Names that are not defined anywhere - newVarNames = identifiers \\ existingNames - - -- Identifiers being mentioned in the requirements. - identifiers = nub $ concatMap (f . requirementExpr) (requirements s) - - -- Names that are defined in variables. - existingNames = map externalVariableName (externalVariables s) - ++ map internalVariableName (internalVariables s) diff --git a/src/Command/ROSApp.hs b/src/Command/ROSApp.hs --- a/src/Command/ROSApp.hs +++ b/src/Command/ROSApp.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE OverloadedStrings #-} -- Copyright 2022 United States Government as represented by the Administrator -- of the National Aeronautics and Space Administration. All Rights Reserved. -- @@ -46,15 +47,16 @@ import qualified Control.Exception as E import Control.Monad.Except (ExceptT, liftEither, liftIO, runExceptT, throwError) -import Data.Aeson (eitherDecode) +import Data.Aeson (eitherDecode, object, (.=)) import Data.List (find, intersperse) import Data.Maybe (fromMaybe) +import Data.Text.Lazy (pack) import System.FilePath (()) -- 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, @@ -73,6 +75,7 @@ -- | 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. @@ -83,7 +86,7 @@ -- Copilot specification. The handlers are assumed -- to receive no arguments. -> IO (Result ErrorCode) -rosApp targetDir fretCSFile varNameFile varDBFile handlersFile = +rosApp targetDir mTemplateDir fretCSFile varNameFile varDBFile handlersFile = processResult $ do cs <- parseOptionalFRETCS fretCSFile vs <- parseOptionalVariablesFile varNameFile @@ -95,13 +98,15 @@ let varNames = fromMaybe (fretCSExtractExternalVariables cs) vs monitors = fromMaybe (fretCSExtractHandlers cs) rs - e <- liftIO $ rosApp' targetDir varNames varDB monitors + e <- liftIO $ rosApp' targetDir mTemplateDir varNames varDB monitors liftEither e -- | Generate a new ROS application connected to Copilot, by copying the -- template and filling additional necessary files. rosApp' :: FilePath -- ^ Target directory where the -- application should be created. + -> Maybe FilePath -- ^ Directory where the template + -- is to be found. -> [String] -- ^ List of variable names -- (data sources). -> [(String, String, String, String)] -- ^ List of variables with their @@ -112,14 +117,14 @@ -- to the monitors (or -- requirements monitored). -> IO (Either ErrorTriplet ()) -rosApp' targetDir varNames varDB monitors = +rosApp' targetDir mTemplateDir varNames varDB monitors = E.handle (return . Left . cannotCopyTemplate) $ do -- Obtain template dir - dataDir <- getDataDir - let templateDir = dataDir "templates" "ros" - - -- Expand template - copyDirectoryRecursive templateDir targetDir + templateDir <- case mTemplateDir of + Just x -> return x + Nothing -> do + dataDir <- getDataDir + return $ dataDir "templates" "ros" let f n o@(oVars, oIds, oInfos, oDatas) = case variableMap varDB n of @@ -135,21 +140,29 @@ let (vars, ids, infos, datas) = foldr f ([], [], [], []) varNames - let rosFileName = - targetDir "copilot" "src" "copilot_monitor.cpp" - rosFileContents = - unlines $ - rosMonitorContents varNames vars ids infos datas monitors + let (variablesS, msgSubscriptionS, msgPublisherS, + msgHandlerInClassS, msgCallbacks, msgSubscriptionDeclrs, + msgPublisherDeclrs, msgHandlerGlobalS) = + rosMonitorComponents varNames vars ids infos datas monitors - writeFile rosFileName rosFileContents + (logMsgSubscriptionS, logMsgCallbacks, logMsgSubscriptionDeclrs) = + rosLoggerComponents varNames vars ids infos datas monitors - let rosFileName = - targetDir "copilot" "src" "copilot_logger.cpp" - rosFileContents = - unlines $ - rosLoggerContents varNames vars ids infos datas monitors + subst = object $ + [ "variablesS" .= pack variablesS + , "msgSubscriptionS" .= pack msgSubscriptionS + , "msgPublisherS" .= pack msgPublisherS + , "msgHandlerInClassS" .= pack msgHandlerInClassS + , "msgCallbacks" .= pack msgCallbacks + , "msgSubscriptionDeclrs" .= pack msgSubscriptionDeclrs + , "msgPublisherDeclrs" .= pack msgPublisherDeclrs + , "msgHandlerGlobalS" .= pack msgHandlerGlobalS + , "logMsgSubscriptionS" .= pack logMsgSubscriptionS + , "logMsgCallbacks" .= pack logMsgCallbacks + , "logMsgSubscriptionDeclrs" .= pack logMsgSubscriptionDeclrs + ] - writeFile rosFileName rosFileContents + copyTemplate templateDir subst targetDir return $ Right () @@ -301,52 +314,24 @@ -- * ROS apps content -- | Return the contents of the main ROS application. -rosMonitorContents :: [String] -- Variables - -> [VarDecl] - -> [MsgInfoId] - -> [MsgInfo] - -> [MsgData] - -> [String] -- Monitors - -> [String] -rosMonitorContents varNames variables msgIds msgNames msgDatas monitors = - [ "#include " - , "#include " - , "" - , "#include \"rclcpp/rclcpp.hpp\"" - , "" - , typeIncludes - , copilotIncludes - , "using std::placeholders::_1;" - , "" - , variablesS - , "class CopilotRV : public rclcpp::Node {" - , " public:" - , " CopilotRV() : Node(\"copilotrv\") {" +rosMonitorComponents + :: [String] -- Variables + -> [VarDecl] + -> [MsgInfoId] + -> [MsgInfo] + -> [MsgData] + -> [String] -- Monitors + -> (String, String, String, String, String, String, String, String) +rosMonitorComponents varNames variables msgIds msgNames msgDatas monitors = + ( variablesS , msgSubscriptionS , msgPublisherS - , " }" - , "" , msgHandlerInClassS - , " // Needed so we can report messages to the log." - , " static CopilotRV& getInstance() {" - , " static CopilotRV instance;" - , " return instance;" - , " }" - , "" - , " private:" , msgCallbacks , msgSubscriptionDeclrs , msgPublisherDeclrs - , "};" - , "" , msgHandlerGlobalS - , "int main(int argc, char* argv[]) {" - , " rclcpp::init(argc, argv);" - , " rclcpp::spin(std::make_shared());" - , " rclcpp::shutdown();" - , " return 0;" - , "}" - ] + ) where @@ -369,27 +354,6 @@ publisher = monitor ++ "_publisher_" - typeIncludes = unlines - [ "#include \"std_msgs/msg/bool.hpp\"" - , "#include \"std_msgs/msg/empty.hpp\"" - , "#include \"std_msgs/msg/u_int8.hpp\"" - , "#include \"std_msgs/msg/u_int16.hpp\"" - , "#include \"std_msgs/msg/u_int32.hpp\"" - , "#include \"std_msgs/msg/u_int64.hpp\"" - , "#include \"std_msgs/msg/int8.hpp\"" - , "#include \"std_msgs/msg/int16.hpp\"" - , "#include \"std_msgs/msg/int32.hpp\"" - , "#include \"std_msgs/msg/int64.hpp\"" - , "#include \"std_msgs/msg/float32.hpp\"" - , "#include \"std_msgs/msg/float64.hpp\"" - , "#include " - ] - - copilotIncludes = unlines - [ "#include \"monitor.h\"" - , "#include \"monitor.c\"" - ] - variablesS = unlines $ map toVarDecl variables toVarDecl varDecl = varDeclType' varDecl ++ " " ++ varDeclName varDecl ++ ";" @@ -515,49 +479,17 @@ publisher = nm ++ "_publisher_" -- | Return the contents of the logger ROS application. -rosLoggerContents :: [String] -- Variables - -> [VarDecl] - -> [MsgInfoId] - -> [MsgInfo] - -> [MsgData] - -> [String] -- Monitors - -> [String] -rosLoggerContents varNames variables msgIds msgNames msgDatas monitors = - rosFileContents +rosLoggerComponents :: [String] -- Variables + -> [VarDecl] + -> [MsgInfoId] + -> [MsgInfo] + -> [MsgData] + -> [String] -- Monitors + -> (String, String, String) +rosLoggerComponents varNames variables msgIds msgNames msgDatas monitors = + (msgSubscriptionS, msgCallbacks, msgSubscriptionDeclrs) where - - rosFileContents = - [ "#include " - , "#include " - , "" - , "#include \"rclcpp/rclcpp.hpp\"" - , "" - , typeIncludes - , "using std::placeholders::_1;" - , "" - , "class CopilotLogger : public rclcpp::Node {" - , " public:" - , " CopilotLogger() : Node(\"copilotlogger\") {" - , msgSubscriptionS - , " }" - , "" - , " private:" - , msgCallbacks - , msgSubscriptionDeclrs - , "};" - , "" - , "int main(int argc, char* argv[]) {" - , " rclcpp::init(argc, argv);" - , " rclcpp::spin(std::make_shared());" - , " rclcpp::shutdown();" - , " return 0;" - , "}" - ] - - typeIncludes = unlines - [ "#include \"std_msgs/msg/empty.hpp\"" - ] msgSubscriptionS = unlines $ concat diff --git a/src/Command/Standalone.hs b/src/Command/Standalone.hs new file mode 100644 --- /dev/null +++ b/src/Command/Standalone.hs @@ -0,0 +1,223 @@ +{-# LANGUAGE ExistentialQuantification #-} +-- Copyright 2020 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 specification into a standalone Copilot specification. +module Command.Standalone + ( standalone + , StandaloneOptions(..) + , ErrorCode + ) + where + +-- External imports +import Data.Aeson (decode, eitherDecode) +import Data.ByteString.Lazy (fromStrict, pack) +import Data.Foldable (for_) +import Data.List (nub, (\\)) +import Data.Maybe (fromMaybe) +import System.FilePath (()) + +-- External imports: auxiliary +import Data.ByteString.Extra as B ( safeReadFile ) + +-- Internal imports: auxiliary +import Command.Result (Result (..)) +import Data.Location (Location (..)) +import Paths_ogma_core (getDataDir) + +-- Internal imports: language ASTs, transformers +import Data.OgmaSpec (ExternalVariableDef (..), InternalVariableDef (..), + Requirement (..), Spec (..)) +import Language.JSONSpec.Parser (JSONFormat (..), parseJSONSpec) + +-- 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) +import Language.Trans.Spec2Copilot (spec2Copilot, specAnalyze) + +-- | Print the contents of a Copilot module 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. +standalone :: FilePath -- ^ Path to a file containing a specification + -> StandaloneOptions -- ^ Customization options + -> IO (Result ErrorCode) +standalone fp options = do + + let functions = exprPair (standalonePropFormat options) + + copilot <- standalone' fp options functions + + let (mOutput, result) = standaloneResult options fp copilot + + for_ mOutput putStrLn + return result + +-- | Print the contents of a Copilot module 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. +standalone' :: FilePath + -> StandaloneOptions + -> ExprPair + -> IO (Either String String) +standalone' fp options (ExprPair parse replace print ids) = do + let name = standaloneFilename options + typeMaps = typeToCopilotTypeMapping options + + -- Obtain format file + dataDir <- getDataDir + let formatFile = + dataDir "data" "formats" + (standaloneFormat options ++ "_" ++ standalonePropFormat options) + + format <- read <$> 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 + + -- Complement the specification with any missing/implicit definitions + let res' = fmap (addMissingIdentifiers ids) res + + let copilot = spec2Copilot name typeMaps replace print =<< specAnalyze =<< res' + + return copilot + +-- | Options used to customize the conversion of specifications to Copilot +-- code. +data StandaloneOptions = StandaloneOptions + { standaloneFormat :: String + , standalonePropFormat :: String + , standaloneTypeMapping :: [(String, String)] + , standaloneFilename :: String + } + +-- * 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. +ecStandaloneError :: ErrorCode +ecStandaloneError = 1 + +-- * Result + +-- | Process the result of the transformation function. +standaloneResult :: StandaloneOptions + -> FilePath + -> Either String String + -> (Maybe String, Result ErrorCode) +standaloneResult options fp result = case result of + Left msg -> (Nothing, Error ecStandaloneError msg (LocationFile fp)) + Right t -> (Just t, Success) + +-- * Mapping of types from input format to Copilot +typeToCopilotTypeMapping :: StandaloneOptions -> [(String, String)] +typeToCopilotTypeMapping options = + [ ("bool", "Bool") + , ("int", intType) + , ("integer", intType) + , ("real", realType) + , ("string", "String") + , ("", "_") + ] + where + intType = fromMaybe "Int64" $ lookup "int" types + realType = fromMaybe "Float" $ lookup "real" types + + types = standaloneTypeMapping options + +-- * Handler for boolean expressions + +-- | 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 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) +exprPair _ = ExprPair (SMV.pBoolSpec . SMV.myLexer) + (substituteBoolExpr) + (SMV.boolSpec2Copilot) + (SMV.boolSpecNames) + +-- | Add to a spec external variables for all identifiers mentioned in +-- expressions that are not defined anywhere. +addMissingIdentifiers :: (a -> [String]) -> Spec a -> Spec a +addMissingIdentifiers f s = s { externalVariables = vars' } + where + vars' = externalVariables s ++ newVars + newVars = map (\n -> ExternalVariableDef n "") newVarNames + + -- Names that are not defined anywhere + newVarNames = identifiers \\ existingNames + + -- Identifiers being mentioned in the requirements. + identifiers = nub $ concatMap (f . requirementExpr) (requirements s) + + -- Names that are defined in variables. + existingNames = map externalVariableName (externalVariables s) + ++ map internalVariableName (internalVariables s) diff --git a/src/Language/Trans/SMV2Copilot.hs b/src/Language/Trans/SMV2Copilot.hs --- a/src/Language/Trans/SMV2Copilot.hs +++ b/src/Language/Trans/SMV2Copilot.hs @@ -29,7 +29,7 @@ -- AGREEMENT. -- --- | Transform a FRET TL specification into a Copilot specification. +-- | Transform an SMV TL specification into a Copilot specification. -- -- Normally, this module would be implemented as a conversion between ASTs, -- but we want to add comments to the generated code, which are not @@ -40,7 +40,7 @@ Ident (..), MultOp (..), NumExpr (..), Number (..), Op1Name (..), OpOne (..), OpTwo (..), OrdOp (..)) --- | Return the Copilot representation of a FRET BoolSpec. +-- | Return the Copilot representation of an SMV BoolSpec. -- -- This function returns the temporal property only. The string does not -- contain any top-level names, any imports, or auxiliary definitions that may @@ -96,7 +96,7 @@ ++ " " ++ boolSpec2Copilot spec2 ++ ")" --- | Return the Copilot representation of a FRET boolean constant. +-- | Return the Copilot representation of an SMV boolean constant. const2Copilot :: BoolConst -> String const2Copilot BoolConstTrue = "true" const2Copilot BoolConstFalse = "false" @@ -119,17 +119,17 @@ ++ numExpr2Copilot y ++ ")" --- | Return the Copilot representation of a FRET additive operator. +-- | Return the Copilot representation of an SMV additive operator. additiveOp2Copilot :: AdditiveOp -> String additiveOp2Copilot OpPlus = "+" additiveOp2Copilot OpMinus = "-" --- | Return the Copilot representation of a FRET multiplicative operator. +-- | Return the Copilot representation of an SMV multiplicative operator. multOp2Copilot :: MultOp -> String multOp2Copilot OpTimes = "*" multOp2Copilot OpDiv = "/" --- | Return the Copilot representation of a FRET comparison operator. +-- | Return the Copilot representation of an SMV comparison operator. ordOp2Copilot :: OrdOp -> String ordOp2Copilot OrdOpLT = "<" ordOp2Copilot OrdOpLE = "<=" @@ -138,13 +138,13 @@ ordOp2Copilot OrdOpGT = ">" ordOp2Copilot OrdOpGE = ">=" --- | Return the Copilot representation of a unary logical FRET operator. +-- | Return the Copilot representation of a unary logical SMV operator. opOne2Copilot :: OpOne -> String opOne2Copilot (Op1Alone x) = opOneAlone2Copilot x opOne2Copilot (Op1MTL x op v) = opOneMTL2Copilot x op v opOne2Copilot (Op1MTLRange op mn mx) = opOneMTLRange2Copilot op mn mx --- | Return the Copilot representation of a unary logical non-MTL FRET +-- | Return the Copilot representation of a unary logical non-MTL SMV -- operator. opOneAlone2Copilot :: Op1Name -> String opOneAlone2Copilot Op1Pre = "pre" @@ -156,7 +156,7 @@ opOneAlone2Copilot Op1Hist = "PTLTL.alwaysBeen" opOneAlone2Copilot Op1O = "PTLTL.eventuallyPrev" --- | Return the Copilot representation of a unary logical MTL FRET operator. +-- | Return the Copilot representation of a unary logical MTL SMV operator. opOneMTL2Copilot :: Op1Name -> OrdOp -> Number -> String opOneMTL2Copilot operator _comparison number = opOneMTL2Copilot' operator ++ " " ++ show (0 :: Int) @@ -164,7 +164,7 @@ ++ " " ++ "clock" ++ " " ++ show (1 :: Int) --- | Return the Copilot representation of a unary logical MTL FRET operator +-- | Return the Copilot representation of a unary logical MTL SMV operator -- that uses an explicit range. opOneMTLRange2Copilot :: Op1Name -> Number -> Number -> String opOneMTLRange2Copilot operator mn mx = @@ -173,7 +173,7 @@ ++ " " ++ "clock" ++ " " ++ show (1 :: Int) --- | Return the Copilot representation of a unary logical possibly MTL FRET +-- | Return the Copilot representation of a unary logical possibly MTL SMV -- operator. opOneMTL2Copilot' :: Op1Name -> String opOneMTL2Copilot' Op1Pre = "pre" @@ -185,11 +185,11 @@ opOneMTL2Copilot' Op1Hist = "MTL.alwaysBeen" opOneMTL2Copilot' Op1O = "MTL.eventuallyPrev" --- | Return the Copilot representation of a FRET number. +-- | Return the Copilot representation of an SMV number. number2Copilot :: Number -> String number2Copilot (NumberInt n) = show n --- | Return the Copilot representation of a binary logical non-MTL FRET +-- | Return the Copilot representation of a binary logical non-MTL SMV -- operator. opTwo2Copilot :: OpTwo -> String opTwo2Copilot Op2S = "`since`" @@ -197,7 +197,7 @@ opTwo2Copilot Op2V = "`releases`" opTwo2Copilot Op2U = "`until`" --- | Return the Copilot representation of a FRET identifier. +-- | Return the Copilot representation of an SMV identifier. ident2Copilot :: Ident -> String ident2Copilot (Ident i) = i 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 @@ -67,6 +67,7 @@ , ftp , pre , tpre + , notPreviousNot , copilotSpec , main' ] @@ -194,12 +195,19 @@ , "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 the C function void " - ++ " handler(); when" - , "-- the property is violated." + , "-- | Complete specification. Calls C handler functions" + ++ " when" + , "-- properties are violated." , "spec :: Spec" , "spec = do" ] diff --git a/templates/copilot-cfs/fsw/src/copilot_cfs.c b/templates/copilot-cfs/fsw/src/copilot_cfs.c --- a/templates/copilot-cfs/fsw/src/copilot_cfs.c +++ b/templates/copilot-cfs/fsw/src/copilot_cfs.c @@ -19,7 +19,7 @@ #include "Icarous_msgids.h" #include "Icarous_msg.h" -position_t my_position; +{{variablesS}} void split(void); void step(void); @@ -98,7 +98,7 @@ ** messages */ CFE_SB_CreatePipe(&COPILOT_CommandPipe, COPILOT_PIPE_DEPTH,"COPILOT_CMD_PIPE"); - CFE_SB_Subscribe(ICAROUS_POSITION_MID, COPILOT_CommandPipe); +{{msgSubscriptionsS}} CFE_EVS_SendEvent (COPILOT_STARTUP_INF_EID, CFE_EVS_INFORMATION, "COPILOT App Initialized. Version %d.%d.%d.%d", @@ -125,9 +125,7 @@ switch (MsgId) { - case ICAROUS_POSITION_MID: - COPILOT_ProcessIcarousPosition(); - break; +{{ msgCasesS }} default: COPILOT_HkTelemetryPkt.copilot_command_error_count++; CFE_EVS_SendEvent(COPILOT_COMMAND_ERR_EID,CFE_EVS_ERROR, @@ -139,18 +137,7 @@ } /* End COPILOT_ProcessCommandPacket */ -/** - * Make ICAROUS data available to Copilot and run monitors. - */ -void COPILOT_ProcessIcarousPosition(void) -{ - position_t* msg; - msg = (position_t*) COPILOTMsgPtr; - my_position = *msg; - - // Run all copilot monitors. - step(); -} +{{msgHandlerS}} /** * Report copilot property violations. diff --git a/templates/ros/Dockerfile b/templates/ros/Dockerfile --- a/templates/ros/Dockerfile +++ b/templates/ros/Dockerfile @@ -1,4 +1,4 @@ -FROM osrf/space-ros:latest +FROM osrf/space-ros:humble-2024.10.0 ARG USER=spaceros-user ARG PACKAGE_PATH=/home/${USER}/monitors @@ -12,5 +12,5 @@ SHELL ["/bin/bash", "-c"] WORKDIR ${PACKAGE_PATH} -RUN source ${ROS_PATH}/install/setup.bash && \ +RUN source /opt/spaceros/install/setup.bash && \ colcon build diff --git a/templates/ros/copilot/src/.keep b/templates/ros/copilot/src/.keep deleted file mode 100644 --- a/templates/ros/copilot/src/.keep +++ /dev/null diff --git a/templates/ros/copilot/src/copilot_logger.cpp b/templates/ros/copilot/src/copilot_logger.cpp new file mode 100644 --- /dev/null +++ b/templates/ros/copilot/src/copilot_logger.cpp @@ -0,0 +1,27 @@ +#include +#include + +#include "rclcpp/rclcpp.hpp" + +#include "std_msgs/msg/empty.hpp" +using std::placeholders::_1; + +class CopilotLogger : public rclcpp::Node { + public: + CopilotLogger() : Node("copilotlogger") { +{{{logMsgSubscriptionS}}} + } + + private: +{{{logMsgCallbacks}}} +{{{logMsgSubscriptionDeclrs}}} +}; + +int main(int argc, char* argv[]) { + rclcpp::init(argc, argv); + rclcpp::spin(std::make_shared()); + rclcpp::shutdown(); + return 0; +} + + diff --git a/templates/ros/copilot/src/copilot_monitor.cpp b/templates/ros/copilot/src/copilot_monitor.cpp new file mode 100644 --- /dev/null +++ b/templates/ros/copilot/src/copilot_monitor.cpp @@ -0,0 +1,52 @@ +#include +#include + +#include "rclcpp/rclcpp.hpp" + +#include "std_msgs/msg/bool.hpp" +#include "std_msgs/msg/empty.hpp" +#include "std_msgs/msg/u_int8.hpp" +#include "std_msgs/msg/u_int16.hpp" +#include "std_msgs/msg/u_int32.hpp" +#include "std_msgs/msg/u_int64.hpp" +#include "std_msgs/msg/int8.hpp" +#include "std_msgs/msg/int16.hpp" +#include "std_msgs/msg/int32.hpp" +#include "std_msgs/msg/int64.hpp" +#include "std_msgs/msg/float32.hpp" +#include "std_msgs/msg/float64.hpp" +#include +#include "monitor.h" +#include "monitor.c" + +using std::placeholders::_1; + +{{{variablesS}}} +class CopilotRV : public rclcpp::Node { + public: + CopilotRV() : Node("copilotrv") { +{{{msgSubscriptionS}}} +{{{msgPublisherS}}} + } + +{{{msgHandlerInClassS}}} + // Needed so we can report messages to the log. + static CopilotRV& getInstance() { + static CopilotRV instance; + return instance; + } + + private: +{{{msgCallbacks}}} +{{{msgSubscriptionDeclrs}}} +{{{msgPublisherDeclrs}}} +}; + +{{{msgHandlerGlobalS}}} +int main(int argc, char* argv[]) { + rclcpp::init(argc, argv); + rclcpp::spin(std::make_shared()); + rclcpp::shutdown(); + return 0; +} + diff --git a/tests/Main.hs b/tests/Main.hs --- a/tests/Main.hs +++ b/tests/Main.hs @@ -7,14 +7,9 @@ import Test.HUnit ( assertBool ) -- Internal imports -import Command.CStructs2Copilot ( cstructs2Copilot ) -import Command.FRETComponentSpec2Copilot ( FRETComponentSpec2CopilotOptions (..) - , fretComponentSpec2Copilot - ) -import Command.FRETReqsDB2Copilot ( FRETReqsDB2CopilotOptions (..) - , fretReqsDB2Copilot - ) -import Command.Result ( isSuccess ) +import Command.CStructs2Copilot (cstructs2Copilot) +import Command.Result (isSuccess) +import Command.Standalone (StandaloneOptions (..), standalone) -- | Run all unit tests on ogma-core. main :: IO () @@ -106,13 +101,13 @@ -> Bool -> IO () testFretComponentSpec2Copilot file success = do - let opts = FRETComponentSpec2CopilotOptions - { fretCS2CopilotUseCoCoSpec = False - , fretCS2CopilotIntType = "Int64" - , fretCS2CopilotRealType = "Float" - , fretCS2CopilotFilename = "fret" + let opts = StandaloneOptions + { standaloneFormat = "fcs" + , standalonePropFormat = "smv" + , standaloneTypeMapping = [("int", "Int64"), ("real", "Float")] + , standaloneFilename = "fret" } - result <- fretComponentSpec2Copilot file opts + result <- standalone file opts -- True if success is expected and detected, or niether expected nor -- detected. @@ -138,11 +133,13 @@ -> Bool -> IO () testFretReqsDBCoCoSpec2Copilot file success = do - let opts = FRETReqsDB2CopilotOptions - { fretReqsDB2CopilotUseCoCoSpec = True - , fretReqsDB2CopilotFilename = "fret" + let opts = StandaloneOptions + { standaloneFormat = "fdb" + , standalonePropFormat = "cocospec" + , standaloneTypeMapping = [] + , standaloneFilename = "fret" } - result <- fretReqsDB2Copilot file opts + result <- standalone file opts -- True if success is expected and detected, or niether expected nor -- detected.