packages feed

ogma-core 1.4.1 → 1.5.0

raw patch · 19 files changed

+516/−772 lines, 19 filesdep +textdep ~ogma-extradep ~ogma-language-cdep ~ogma-language-cocospec

Dependencies added: text

Dependency ranges changed: ogma-extra, ogma-language-c, ogma-language-cocospec, ogma-language-copilot, ogma-language-jsonspec, ogma-language-smv, ogma-spec

Files

CHANGELOG.md view
@@ -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).
+ data/formats/fcs_cocospec view
@@ -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"+  }
+ data/formats/fcs_smv view
@@ -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"+  }
+ data/formats/fdb_cocospec view
@@ -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"+  }
+ data/formats/fdb_smv view
@@ -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"+  }
ogma-core.cabal view
@@ -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
src/Command/CFSApp.hs view
@@ -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
− src/Command/FRETComponentSpec2Copilot.hs 
@@ -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)
− src/Command/FRETReqsDB2Copilot.hs 
@@ -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)
src/Command/ROSApp.hs view
@@ -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 <functional>"-    , "#include <memory>"-    , ""-    , "#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<CopilotRV>());"-    , "  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 <cstdint>"-      ]--    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 <functional>"-      , "#include <memory>"-      , ""-      , "#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<CopilotLogger>());"-      , "  rclcpp::shutdown();"-      , "  return 0;"-      , "}"-      ]--    typeIncludes = unlines-      [ "#include \"std_msgs/msg/empty.hpp\""-      ]      msgSubscriptionS     = unlines                          $ concat
+ src/Command/Standalone.hs view
@@ -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)
src/Language/Trans/SMV2Copilot.hs view
@@ -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
src/Language/Trans/Spec2Copilot.hs view
@@ -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"                   ]
templates/copilot-cfs/fsw/src/copilot_cfs.c view
@@ -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.
templates/ros/Dockerfile view
@@ -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
− templates/ros/copilot/src/.keep 
+ templates/ros/copilot/src/copilot_logger.cpp view
@@ -0,0 +1,27 @@+#include <functional>+#include <memory>++#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<CopilotLogger>());+  rclcpp::shutdown();+  return 0;+}++
+ templates/ros/copilot/src/copilot_monitor.cpp view
@@ -0,0 +1,52 @@+#include <functional>+#include <memory>++#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 <cstdint>+#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<CopilotRV>());+  rclcpp::shutdown();+  return 0;+}+
tests/Main.hs view
@@ -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.