packages feed

ogma-core (empty) → 1.0.6

raw patch · 29 files changed

+3274/−0 lines, 29 filesdep +HUnitdep +IfElsedep +QuickChecksetup-changedbinary-added

Dependencies added: HUnit, IfElse, QuickCheck, aeson, base, filepath, ogma-core, ogma-extra, ogma-language-c, ogma-language-cocospec, ogma-language-copilot, ogma-language-fret-cs, ogma-language-fret-reqs, ogma-language-smv, test-framework, test-framework-hunit, test-framework-quickcheck2

Files

+ CHANGELOG.md view
@@ -0,0 +1,39 @@+# Revision history for ogma-core++## [1.0.6] - 2022-11-21++* Version bump 1.0.6 (#64).+* Update license in cabal file to OtherLicense (#62).++## [1.0.5] - 2022-09-21++* Version bump 1.0.5 (#60).+* Bump version bounds of Aeson (#55).+* Support floating point numbers in SMV expressions (#58).++## [1.0.4] - 2022-07-21++* Version bump 1.0.4 (#53).+* Address all hlint suggestions (#51).++## [1.0.3] - 2022-05-21++* Version bump 1.0.3 (#49).+* Conformance with style guide (partial) (#45).++## [1.0.2] - 2022-03-21++* Version bump 1.0.2 (#43).+* Fix compilation error in unit tests (#42).+* Remove reduntant parenthesis (#40).++## [1.0.1] - 2022-01-21++* Version bump 1.0.1 (#39).+* Align definitions consistently (#35).+* Indent ogma-core:Language.Trans.CStruct2CopilotStruct.buildCField (#36).+* Indent ogma-core:Command.Result module declaration (#37).++## [1.0.0] - 2021-11-22++* Initial release.
+ LICENSE.pdf view

binary file changed (absent → 117991 bytes)

+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ ogma-core.cabal view
@@ -0,0 +1,137 @@+-- 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.++cabal-version:       2.0+build-type:          Simple++name:                ogma-core+version:             1.0.6+homepage:            http://nasa.gov+license:             OtherLicense+license-file:        LICENSE.pdf+author:              Ivan Perez, Alwyn Goodloe+maintainer:          ivan.perezdominguez@nasa.gov+category:            Aerospace+extra-source-files:  CHANGELOG.md++synopsis:            Ogma: Helper tool to interoperate between Copilot and other languages.++description:         Ogma is a tool to facilitate the integration of safe runtime monitors into+                     other systems. Ogma extends+                     <https://github.com/Copilot-Language/copilot Copilot>, a high-level runtime+                     verification framework that generates hard real-time C99 code.+                     .+                     This package implements the internal commands of ogma.++data-files:          templates/copilot-cfs/CMakeLists.txt+                     templates/copilot-cfs/fsw/for_build/Makefile+                     templates/copilot-cfs/fsw/mission_inc/copilot_cfs_perfids.h+                     templates/copilot-cfs/fsw/platform_inc/copilot_cfs_msgids.h+                     templates/copilot-cfs/fsw/src/Properties.hs+                     templates/copilot-cfs/fsw/src/copilot_cfs_msg.h+                     templates/copilot-cfs/fsw/src/copilot_cfs.c+                     templates/copilot-cfs/fsw/src/copilot_cfs_version.h+                     templates/copilot-cfs/fsw/src/copilot_cfs.h+                     templates/copilot-cfs/fsw/src/copilot_cfs_events.h++library++  exposed-modules:+    Command.CFSApp+    Command.CStructs2Copilot+    Command.CStructs2MsgHandlers+    Command.FRETComponentSpec2Copilot+    Command.FRETReqsDB2Copilot+    Command.Result++    Data.Location++    Language.Trans.CoCoSpec2Copilot+    Language.Trans.CStruct2CopilotStruct+    Language.Trans.CStructs2Copilot+    Language.Trans.CStructs2MsgHandlers+    Language.Trans.FRETComponentSpec2Copilot+    Language.Trans.FRETReqsDB2Copilot+    Language.Trans.SMV2Copilot++  other-modules:+    Paths_ogma_core++  autogen-modules:+    Paths_ogma_core++  build-depends:+      base                    >= 4.11.0.0 && < 5+    , aeson                   >= 2.0.0.0  && < 2.2+    , filepath+    , IfElse++    , ogma-extra              >= 1.0.0 && < 1.1+    , ogma-language-c         >= 1.0.0 && < 1.1+    , ogma-language-cocospec  >= 1.0.0 && < 1.1+    , ogma-language-copilot   >= 1.0.0 && < 1.1+    , ogma-language-fret-cs   >= 1.0.0 && < 1.1+    , ogma-language-fret-reqs >= 1.0.0 && < 1.1+    , ogma-language-smv       >= 1.0.0 && < 1.1++  hs-source-dirs:+    src++  default-language:+    Haskell2010++  ghc-options:+    -Wall++test-suite unit-tests+  type:+    exitcode-stdio-1.0++  main-is:+    Main.hs++  build-depends:+      base+    , HUnit+    , QuickCheck+    , test-framework+    , test-framework-hunit+    , test-framework-quickcheck2++    , ogma-core++  hs-source-dirs:+    tests++  default-language:+    Haskell2010++  ghc-options:+    -Wall
+ src/Command/CFSApp.hs view
@@ -0,0 +1,431 @@+-- 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.+--+-- | Create <https://cfs.gsfc.nasa.gov/ NASA Core Flight System> (CFS)+-- applications that subscribe to the communication bus and call Copilot when+-- new messages arrive.+--+-- The applications are created ready to be extracted in the application+-- directory in CFS, and they subscribe to a generic monitor. It is the user's+-- responsibility to modify the generated Copilot and C code to deal with the+-- monitors they'd like to implement, and the data they must manipulate.++{- HLINT ignore "Functor law" -}+module Command.CFSApp+    ( cFSApp+    , ErrorCode+    )+  where++-- External imports+import qualified Control.Exception as E+import           Data.List         ( find )+import           System.FilePath   ( (</>) )++-- External imports: auxiliary+import System.Directory.Extra ( copyDirectoryRecursive )++-- Internal imports: auxiliary+import Command.Result ( Result (..) )+import Data.Location  ( Location (..) )++-- Internal imports+import Paths_ogma_core ( getDataDir )++-- | Generate a new CFS application connected to Copilot.+cFSApp :: FilePath       -- ^ Target directory where the application+                         --   should be created.+       -> 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++  -- We first try to open the two files we need to fill in details in the CFS+  -- app template.+  --+  -- The variable DB is optional, so this check only fails if the filename+  -- provided does not exist or if the file cannot be opened or parsed (wrong+  -- format).+  varDBE <- E.try $+                case varDBFile of+                  Nothing -> return knownVars+                  Just fn -> fmap read <$> lines <$> readFile fn++  case varDBE of+    Left  e     -> return $ cannotOpenDB varDBFile e+    Right varDB -> do++      -- The variable list is mandatory. This check fails if the filename+      -- provided does not exist or if the file cannot be opened. The condition+      -- on the result also checks that the list of variables in the file is+      -- not empty (otherwise, we do not know when to call Copilot).+      varNamesE <- E.try $ lines <$> readFile varNameFile++      case varNamesE of+        Left e         -> return $ cannotOpenVarFile varNameFile e+        Right []       -> return $ cannotEmptyVarList varNameFile+        Right varNames -> do++          -- Obtain template dir+          dataDir <- getDataDir+          let templateDir = 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+                    Nothing -> o+                    Just (vars, ids, infos, datas) ->+                      (vars : oVars, ids : oIds, infos : oInfos, datas : oDatas)++            -- 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++            writeFile cfsFileName cfsFileContents+            return Success++-- | Predefined list of Icarous variables that are known to Ogma+knownVars :: [(String, String, String, String)]+knownVars =+  [ ("position", "position_t", "ICAROUS_POSITION_MID", "IcarousPosition") ]++-- | Return the variable information needed to generate declarations+-- and subscriptions for a given variable name and variable database.+variableMap :: [(String, String, String, String)]+            -> String+            -> Maybe (VarDecl, MsgInfoId, MsgInfo, MsgData)+variableMap varDB varName =+    csvToVarMap <$> find (sameName varName) varDB++  where++    -- True if the given variable and db entry have the same name+    sameName :: String+             -> (String, String, String, String)+             -> Bool+    sameName n (vn, _, _, _) = n == vn++    -- Convert a DB row into Variable info needed to generate the CFS file+    csvToVarMap :: (String, String, String, String)+                -> (VarDecl, String, MsgInfo, MsgData)+    csvToVarMap (nm, ty, mid, mn) =+      (VarDecl nm ty, mid, MsgInfo mid mn, MsgData mn nm ty)++-- | The declaration of a variable in C, with a given type and name.+data VarDecl = VarDecl+  { varDeclName :: String+  , varDeclType :: String+  }++-- | The message ID to subscribe to.+type MsgInfoId = String++-- | A message ID to subscribe to and the name associated to it. The name is+-- used to generate a suitable name for the message handler.+data MsgInfo = MsgInfo+  { msgInfoId   :: MsgInfoId+  , msgInfoDesc :: String+  }++-- | Information on the data provided by a message with a given description,+-- and the type of the data it carries.+data MsgData = MsgData+  { msgDataDesc    :: String+  , msgDataVarName :: String+  , msgDataVarType :: String+  }++-- | Return the contents of the main CFS application.+fileContents :: [VarDecl] -> [MsgInfoId] -> [MsgInfo] -> [MsgData] -> [String]+fileContents variables msgIds msgNames msgDatas = cfsFileContents+  where+    variablesS = unlines $ map toVarDecl variables+    toVarDecl varDecl = varDeclType varDecl ++ " " ++ varDeclName varDecl ++ ";"++    msgSubscriptionS     = unlines $ map toMsgSubscription msgIds+    toMsgSubscription nm =+      "    CFE_SB_Subscribe(" ++ nm ++ ", COPILOT_CommandPipe);"++    msgCasesS = unlines $ map toMsgCase msgNames+    toMsgCase msgInfo = unlines+      [ "        case " ++ msgInfoId msgInfo ++ ":"+      , "            COPILOT_Process" ++ msgInfoDesc msgInfo ++ "();"+      , "            break;"+      ]++    msgHandlerS = unlines $ map toMsgHandler msgDatas+    toMsgHandler msgData =+      unlines [ "/**"+              , "* Make ICAROUS data available to Copilot and run monitors."+              , "*/"+              , "void COPILOT_Process" ++ msgDataDesc msgData ++ "(void)"+              , "{"+              , "    " ++ msgDataVarType msgData ++ "* msg;"+              , "    msg = (" ++ msgDataVarType msgData ++ "*) COPILOTMsgPtr;"+              , "    " ++ msgDataVarName msgData ++ " = *msg;"+              , ""+              , "    // Run all copilot monitors."+              , "    step();"+              , "}"+              ]++    cfsFileContents =+      [ "/********************************************************************"+      , "** File: copilot_cfs.c"+      , "**"+      , "** Purpose:"+      , "**   This file contains the source code for the Sample 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\");"+      , 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++-- | Exception handler to deal with the case in which the variable DB cannot be+-- opened.+cannotOpenDB :: Maybe FilePath -> E.SomeException -> Result ErrorCode+cannotOpenDB Nothing _e =+    Error ecCannotOpenDBCritical msg LocationNothing+  where+    msg =+      "cannotOpenDB: this is a bug. Please notify the developers"+cannotOpenDB (Just file) _e =+    Error ecCannotOpenDBUser msg (LocationFile file)+  where+    msg =+      "cannot open variable DB file " ++ file++-- | Exception handler to deal with the case in which the variable file+-- provided by the user cannot be opened.+cannotOpenVarFile :: FilePath -> E.SomeException -> Result ErrorCode+cannotOpenVarFile file _e =+    Error ecCannotOpenVarFile  msg (LocationFile file)+  where+    msg =+      "cannot open variable list file " ++ file++-- | Exception handler to deal with the case of the variable file provided+-- containing an empty list.+cannotEmptyVarList :: FilePath -> Result ErrorCode+cannotEmptyVarList file =+    Error ecCannotEmptyVarList msg (LocationFile file)+  where+    msg =+      "variable list in file " ++ file ++ " is empty"++-- | Exception handler to deal with the case of files that cannot be+-- copied/generated due lack of space or permissions or some I/O error.+cannotCopyTemplate :: E.SomeException -> Result ErrorCode+cannotCopyTemplate _e =+    Error ecCannotCopyTemplate msg LocationNothing+  where+    msg =+      "CFS app generation failed during copy/write operation. Check that"+      ++ " there's free space in the disk and that you have the necessary"+      ++ " permissions to write in the destination directory."++-- * Error codes++-- | Encoding of reasons why the command can fail.+--+-- The error codes used are 1 for user error, and 2 for internal bug.+type ErrorCode = Int++-- | Internal error: Variable DB cannot be opened.+ecCannotOpenDBCritical :: ErrorCode+ecCannotOpenDBCritical = 2++-- | Error: the variable DB provided by the user cannot be opened.+ecCannotOpenDBUser :: ErrorCode+ecCannotOpenDBUser = 1++-- | Error: the variable file provided by the user cannot be opened.+ecCannotOpenVarFile :: ErrorCode+ecCannotOpenVarFile = 1++-- | Error: the variable file provided contains an empty list.+ecCannotEmptyVarList :: ErrorCode+ecCannotEmptyVarList = 1++-- | Error: the files cannot be copied/generated due lack of space or+-- permissions or some I/O error.+ecCannotCopyTemplate :: ErrorCode+ecCannotCopyTemplate = 1
+ src/Command/CStructs2Copilot.hs view
@@ -0,0 +1,98 @@+-- 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.+--+-- | Generate Copilot struct definitions and instances from structs defined in+-- a C header file.+--+-- Working with Copilot structs requires three definitions: the datatype, a+-- @Struct@ instance, and a @Typed@ instance.+--+-- This module converts the C structs into 'Language.Copilot.CStruct.CStruct's,+-- and then converts those 'Language.Copilot.CStruct.CStruct's into Copilot+-- (i.e., Haskell) data type declarations and instance declarations. The result+-- is then printed to a file. This module makes use of+-- "Language.Trans.CStructs2Copilot", which does most of the work.+module Command.CStructs2Copilot+    ( cstructs2Copilot+    , ErrorCode+    )+  where++-- External imports: auxiliary+import Data.String.Extra as S ( safeReadFile )++-- Internal imports: auxiliary+import Command.Result ( Result (..) )+import Data.Location  ( Location (..) )++-- Internal imports: C parsing and AST+import qualified Language.C.AbsC as C ( TranslationUnit )+import qualified Language.C.ParC as C ( myLexer, pTranslationUnit )++-- Internal imports: transformation of C structs to Copilot structs+import Language.Trans.CStructs2Copilot ( cstructs2CopilotDecls )++-- | Generate Copilot struct definitions and instances from structs defined in+-- a C header file.+cstructs2Copilot :: FilePath -- ^ Path to a readable, valid C header file+                             -- containing struct definitions.+                 -> IO (Result ErrorCode)+cstructs2Copilot fp = do+    source <- parseCFile fp++    case cstructs2CopilotDecls =<< source of+      Right decls -> printDecls decls >> return Success+      Left msg    -> return $ Error ecCStructError msg (LocationFile fp)++  where++    -- Parse a C file, returning 'Left' with some message when there is a parse+    -- error.+    --+    parseCFile :: FilePath -> IO (Either String C.TranslationUnit)+    parseCFile fp' = do+      content <- S.safeReadFile fp'+      return $ C.pTranslationUnit . C.myLexer =<< content++    -- Print several Haskell declarations to standard output.+    printDecls :: [ String ] -> IO ()+    printDecls = putStrLn . unlines++-- * Error codes++-- | Encoding of reasons why the command can fail.+--+-- The error code used is 1 for user error.+type ErrorCode = Int++-- | Error: the C header file cannot be read due to the file being unreadable+-- or the format being incorrect.+ecCStructError :: ErrorCode+ecCStructError = 1
+ src/Command/CStructs2MsgHandlers.hs view
@@ -0,0 +1,88 @@+-- 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.+--+-- | Generate C methods that process NASA Core Flight System messages dealing+-- with the structs defined in a header file.+--+-- This module makes use of "Language.Trans.CStructs2MsgHandlers", which does+-- most of the work.+module Command.CStructs2MsgHandlers+    ( cstructs2MsgHandlers+    , ErrorCode+    )+  where++-- External imports: auxiliary+import Data.String.Extra as S ( safeReadFile )++-- Internal imports: auxiliary+import Command.Result ( Result (..) )+import Data.Location  ( Location (..) )++-- Internal imports: C parsing and AST+import qualified Language.C.AbsC as C ( TranslationUnit )+import qualified Language.C.ParC as C ( myLexer, pTranslationUnit )++-- Internal imports: transformation of C structs to handling methods.+import qualified Language.Trans.CStructs2MsgHandlers as T ( cstructs2MsgHandlers )++-- | Print message handlers that copy data and make it available to Copilot.+cstructs2MsgHandlers :: FilePath -- ^ Path to a readable, valid C header file+                                 -- containing struct definitions.+                     -> IO (Result ErrorCode)+cstructs2MsgHandlers fp = do+    result <- parseCFile fp++    case T.cstructs2MsgHandlers =<< result of+      Right content -> putStrLn content >> return Success++      Left msg -> return $ Error ecCStructError msg (LocationFile fp)++  where++    -- Parse a C file, returning 'Left' with some message when there is a parse+    -- error.+    --+    parseCFile :: FilePath -> IO (Either String C.TranslationUnit)+    parseCFile fp' = do+      content <- S.safeReadFile fp'+      return $ C.pTranslationUnit . C.myLexer =<< content++-- * Error codes++-- | Encoding of reasons why the command can fail.+--+-- The error code used is 1 for user error.+type ErrorCode = Int++-- | Error: the C header file cannot be read due to the file being unreadable+-- or the format being incorrect.+ecCStructError :: ErrorCode+ecCStructError = 1
+ src/Command/FRETComponentSpec2Copilot.hs view
@@ -0,0 +1,143 @@+-- 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 Control.Monad.IfElse ( awhen )+import Data.Aeson           ( eitherDecode )++-- External imports: auxiliary+import Data.ByteString.Extra as B ( safeReadFile )++-- Internal imports: auxiliary+import Command.Result ( Result (..) )+import Data.Location  ( Location (..) )++-- Internal imports+import           Language.FRETComponentSpec.AST           ( FRETComponentSpec )+import qualified Language.Trans.FRETComponentSpec2Copilot as T+  ( fretComponentSpec2Copilot+  , FRETComponentSpec2CopilotOptions(FRETComponentSpec2CopilotOptions)+  )++-- | 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++  -- 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.+  fret <- parseFretComponentSpec fp++  -- Extract internal command options from external command options+  let internalOptions = fretComponentSpec2CopilotOptions options++  let copilot = T.fretComponentSpec2Copilot internalOptions =<< fret++  let (mOutput, result) =+        fretComponentSpec2CopilotResult options fp copilot++  awhen mOutput putStrLn+  return result++-- | Options used to customize the conversion of FRET Component Specifications+-- to Copilot code.+data FRETComponentSpec2CopilotOptions = FRETComponentSpec2CopilotOptions+  { fretCS2CopilotUseCoCoSpec :: Bool+  , fretCS2CopilotIntType     :: String+  , fretCS2CopilotRealType    :: String+  }++-- | Parse a JSON file containing a FRET component specification.+--+-- Returns a 'Left' with an error message if the file does not have the correct+-- format.+--+-- Throws an exception if the file cannot be read.+parseFretComponentSpec :: FilePath -> IO (Either String FRETComponentSpec)+parseFretComponentSpec fp = do+  content <- B.safeReadFile fp+  return $ eitherDecode =<< content++-- * 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++-- * Input arguments++-- | Convert command input argument options to internal transformation function+-- input arguments.+fretComponentSpec2CopilotOptions :: FRETComponentSpec2CopilotOptions+                                 -> T.FRETComponentSpec2CopilotOptions+fretComponentSpec2CopilotOptions options =+  T.FRETComponentSpec2CopilotOptions+      (fretCS2CopilotUseCoCoSpec options)+      (fretCS2CopilotIntType options)+      (fretCS2CopilotRealType options)++-- * 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)
+ src/Command/FRETReqsDB2Copilot.hs view
@@ -0,0 +1,140 @@+-- 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.+--+-- This module makes use of+-- "Language.Trans.FRETReqsDB2Copilot", which does most of the work.+module Command.FRETReqsDB2Copilot+    ( fretReqsDB2Copilot+    , FRETReqsDB2CopilotOptions(..)+    , ErrorCode+    )+  where++-- External imports+import Control.Monad.IfElse ( awhen )+import Data.Aeson           ( eitherDecode )++-- External imports: auxiliary+import Data.ByteString.Extra as B ( safeReadFile )+import Data.List.Extra       ( headEither )++-- Internal imports: auxiliary+import Command.Result ( Result (..) )+import Data.Location  ( Location (..) )++-- Internal imports: FRET files and conversion to Copilot+import qualified Language.FRETReqsDB.AST           as FRET ( FRETReqsDB )+import qualified Language.Trans.FRETReqsDB2Copilot as T+  ( fret2CopilotModule+  , FRETReqsDB2CopilotOptions(FRETReqsDB2CopilotOptions)+  )++-- | 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 useCoCoSpec = do++  -- All of the following operations use Either to return error messages. The+  -- use of the monadic bind to pass arguments from one function to the next+  -- will cause the program to stop at the earliest error.+  fret <- parseFret fp++  -- Extract internal command options from external command options+  let internalOptions = fretReqsDB2CopilotOptions useCoCoSpec++  let copilot = T.fret2CopilotModule internalOptions =<< headEither =<< fret++  let (mOutput, result) =+        fretReqsDB2CopilotResult useCoCoSpec fp copilot++  awhen mOutput putStrLn+  return result++-- | Options used to customize the conversion of FRET Requirements Database+-- to Copilot code.+data FRETReqsDB2CopilotOptions = FRETReqsDB2CopilotOptions+  { fretReqsDB2CopilotUseCoCoSpec :: Bool+  }++-- | Parse a JSON file containing a FRET requirement database.+--+-- Returns a 'Left' with an error message if the file does not have the correct+-- format.+--+-- Throws an exception if the file cannot be read.+parseFret :: FilePath -> IO (Either String [FRET.FRETReqsDB])+parseFret fp = do+  content <- B.safeReadFile fp+  return $ eitherDecode =<< content++-- * 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++-- * Input arguments++-- | Convert command input argument options to internal transformation function+-- input arguments.+fretReqsDB2CopilotOptions :: FRETReqsDB2CopilotOptions+                          -> T.FRETReqsDB2CopilotOptions+fretReqsDB2CopilotOptions options =+  T.FRETReqsDB2CopilotOptions+      (fretReqsDB2CopilotUseCoCoSpec options)++-- * 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)
+ src/Command/Result.hs view
@@ -0,0 +1,53 @@+-- 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.+--+-- | A datatype representing the type of the results of processing input files.+module Command.Result+    ( Result (Success, Error)+    , isSuccess+    , isError+    )+  where++-- Internal imports+import Data.Location ( Location )++-- | Result of the global process+data Result a = Success+              | Error a String Location++-- | 'True' if the result is a success, 'False' otherwise.+isSuccess :: Result a -> Bool+isSuccess Success = True+isSuccess _       = False++-- | 'True' if the result is an error, 'False' otherwise.+isError :: Result a -> Bool+isError = not . isSuccess
+ src/Data/Location.hs view
@@ -0,0 +1,42 @@+-- 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.+--+-- | Locations where conditions take place (within a file, or outside).+module Data.Location+    ( Location(..)+    )+  where++-- | Locations where conditions take place (within a file, or outside).+data Location = LocationNothing                 -- ^ No location info.+              | LocationFile     String         -- ^ Within a file.+              | LocationFileLine String Int     -- ^ On a line within a file.+              | LocationFileLC   String Int Int -- ^ On a line and column+                                                --   within a file.
+ src/Language/Trans/CStruct2CopilotStruct.hs view
@@ -0,0 +1,166 @@+-- 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.+--+-- | Copilot's struct representation of C Structs and creation from C's AST.+module Language.Trans.CStruct2CopilotStruct+    (+      -- * Constructors+      mkCStruct++      -- * Convert C type names to valid Copilot names+    , camelCaseTypeName+    )+  where++-- External imports+import Data.Char ( toUpper )++-- External imports: Copilot C Struct representation+import Language.Copilot.CStruct ( CField (CArray, CPlain), CStruct(..) )++-- Internal imports+import qualified Language.C.AbsC as C++-- | Convert a top-level struct declaration into a CStruct+mkCStruct :: C.ExternalDeclaration -> Either String CStruct+mkCStruct (C.MkExternalDeclarationFunctionDefinition _) = Left "C files must contain struct definitions only."+mkCStruct (C.MkExternalDeclarationDeclaration (C.MkDeclaration specifiers initDecl)) =+  case specifiers of+    C.DeclarationSpecifiers (C.MkDeclarationSpecifierStorageClass C.MkStorageClassSpecifierTypedef) s ->+      let [C.MkDeclarationSpecifierTypeSpecifier (C.MkTypeSpecifierStructOrUnion (C.MkStructOrUnionSpecifierWithFields C.MkStructOrUnionStruct _structName u))] = s+          (C.MkInitDeclarationListOptJust [C.MkInitDeclaratorUninitialized (C.MkDeclarator C.MkPointerOptNothing (C.MkDirectDeclaratorIdentifier (C.Identifier t)))]) = initDecl+          name = Right t+          fields = mapM buildCField u+      in CStruct <$> name <*> fields+    _ -> Left "C files must contain struct definitions only."++-- -- | Convert a declaration within a struct into a field declaration.+buildCField :: C.StructDeclaration -> Either String CField+buildCField (C.MkStructDeclaration field name)+    | fieldLength > 0 = CArray <$> fieldType <*> fieldName <*> pure fieldLength+    | otherwise       = CPlain <$> fieldType <*> fieldName+  where+    fieldType   = extractFieldType (head field)+    fieldName   = extractFieldName (head name)+    fieldLength = extractFieldLength (head name)++-- | Extract the type of a field from a type specification.+extractFieldType :: C.SpecifierQualifier -> Either String String+extractFieldType (C.MkSpecifierQualifierTypeSpecifier t) = Right $ showTypeSpecifier t+extractFieldType (C.MkSpecifierQualifierTypeQualifier _) = Left "type qualifiers."++-- | String representing a known type.+showTypeSpecifier :: C.TypeSpecifier -> String+showTypeSpecifier C.MkTypeSpecifierFloat  = "float"+showTypeSpecifier C.MkTypeSpecifierDouble = "double"+showTypeSpecifier C.MkTypeSpecifierUInt8  = "uint8_t"+showTypeSpecifier C.MkTypeSpecifierUInt16 = "uint16_t"+showTypeSpecifier C.MkTypeSpecifierUInt32 = "uint32_t"+showTypeSpecifier C.MkTypeSpecifierUInt64 = "uint64_t"+showTypeSpecifier C.MkTypeSpecifierInt8   = "int8_t"+showTypeSpecifier C.MkTypeSpecifierInt16  = "int16_t"+showTypeSpecifier C.MkTypeSpecifierInt32  = "int32_t"+showTypeSpecifier C.MkTypeSpecifierInt64  = "int64_t"+showTypeSpecifier C.MkTypeSpecifierInt    = "int"++-- -- | Extract the name of a field from a struct declarator.+extractFieldName :: Read n => C.StructDeclarator -> Either String n+extractFieldName (C.MkStructDeclaratorDeclarator (C.MkDeclarator C.MkPointerOptNothing (C.MkDirectDeclaratorIdentifier (C.Identifier d)))) = Right $ read $ show d+extractFieldName (C.MkStructDeclaratorDeclarator+                    (C.MkDeclarator+                      C.MkPointerOptNothing+                      (C.MkDirectDeclaratorConstantExpressionOpt+                         (C.MkDirectDeclaratorIdentifier (C.Identifier i))+                         _arrayLength+                      )+                    )+                  ) = Right $ read $ show i+extractFieldName _ = Left $ "only struct declarations that are IDs without a"+                        ++  " pointer, or plain arrays without a pointer, are"+                        ++  " supported."+--+-- -- | Extract the length of an array field from a struct declarator.+extractFieldLength :: C.StructDeclarator -> Integer+extractFieldLength (C.MkStructDeclaratorDeclarator+                     (C.MkDeclarator+                       C.MkPointerOptNothing+                       (C.MkDirectDeclaratorConstantExpressionOpt+                          _varIdent+                          (C.MkConditionalExpressionJust+                            (C.MkConstantExpression+                              (C.Expression12+                                (C.MkCastExpression1+                                   (C.MkUnaryExpressionPostfix+                                      (C.MkPostfixExpression1+                                         (C.MkPrimaryExpressionIdentifier (C.Identifier _n))+                                      )+                                   )+                                )+                              )+                            )+                          )+                       )+                     ) ) = 99+extractFieldLength (C.MkStructDeclaratorDeclarator+                     (C.MkDeclarator+                       C.MkPointerOptNothing+                       (C.MkDirectDeclaratorConstantExpressionOpt+                         _varIdent+                         (C.MkConditionalExpressionJust+                           (C.MkConstantExpression+                             (C.Expression12+                               (C.MkCastExpression1+                                  (C.MkUnaryExpressionPostfix+                                     (C.MkPostfixExpression1+                                       (C.MkPrimaryExpressionConstant (C.MkConstantInteger (C.IntegerConstant i))+                                     )+                                   )+                                 )+                               )+                             )+                           )+                         )+                       )+                     )+                   ) = read i+extractFieldLength _ = 0++--+-- | Convert a 'String' to camel case, also eliminating the @_t@ at the end if+-- present.+camelCaseTypeName :: String -> String+camelCaseTypeName []     = []+camelCaseTypeName (x:xs) = toUpper x : camelCaseTypeName' xs+  where+    camelCaseTypeName' :: String -> String+    camelCaseTypeName' []   = []+    camelCaseTypeName' "_t" = []+    camelCaseTypeName' ('_':y:ys) = toUpper y : camelCaseTypeName' ys+    camelCaseTypeName' (y:ys) = y : camelCaseTypeName' ys
+ src/Language/Trans/CStructs2Copilot.hs view
@@ -0,0 +1,267 @@+-- 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.+--+-- | Generate Copilot struct definitions and instances from structs defined in+-- a C header file.+--+-- Working with Copilot structs requires three definitions: the datatype,+-- a @Struct@ instance, and a @Typed@ instance.+--+-- This module converts the C structs into 'CStruct's, and then converts+-- those 'CStruct's into Copilot (i.e., Haskell) data type declarations and+-- instance declarations represented as strings.+module Language.Trans.CStructs2Copilot where++-- External imports+import Data.Char ( isUpper, toLower )+import Data.List ( intercalate )++-- External imports: auxiliary+import Data.List.Extra ( toHead, toTail )++-- Internal imports: C AST+import qualified Language.C.AbsC          as C+import           Language.Copilot.CStruct ( CField (CArray, CPlain),+                                            CStruct (..) )++-- Internal imports: Copilot's representation of C structs+import Language.Trans.CStruct2CopilotStruct ( camelCaseTypeName, mkCStruct )++-- | Convert all the 'CStruct's in a header file into the declarations needed+-- in Copilot to use it.+cstructs2CopilotDecls :: C.TranslationUnit -> Either String [ String ]+cstructs2CopilotDecls (C.MkTranslationUnit gs) =+  concat <$> mapM (fmap cstruct2CopilotDecls  . mkCStruct) gs++-- | Convert a 'CStruct' into the declarations needed in Copilot to use it.+cstruct2CopilotDecls :: CStruct -> [ String ]+cstruct2CopilotDecls cstruct = [ cStructToCopilotStruct cstruct+                               , structInstance         cstruct+                               , typedInstance          cstruct+                               ]++-- ** Individual conversions++-- | Convert a 'CStruct' definition into a Copilot Struct declaration.+--+-- For example, given the struct generated by the following definition:+--+-- @+--   struct {+--     uint8_t f1;+--   } a_struct_t;+-- @+--+-- the corresponding Haskell definition would be:+--+-- @+-- data AStruct = AStruct+--   { aSF1 :: Word8 }+-- @+cStructToCopilotStruct :: CStruct -> String+cStructToCopilotStruct cstruct =+    "data "+    ++ datatype+    ++ " = "+    ++ constructor+  where++    -- The name of the type (e.g., @AStruct@).+    datatype = cStructName2Haskell (cStructName cstruct)++    -- The name of the constructor (e.g., @AStruct@).+    constructor = cStructName2Haskell (cStructName cstruct) ++ "\n" ++ fields++    -- The fields in the struct (e.g., @aSF1 :: Word 8@), formated as record+    -- fields: separated by commas, enclosed in curly brackets, and indented.+    fields = unlines $ map ("  " ++)+                     $ (++ ["}"])+                     $ toTail (", " ++)+                     $ toHead ("{ " ++)+                     $ map (toField cstruct) (cStructFields cstruct)++    -- Convert a 'CStruct' field into a Copilot record field declaration.+    --+    -- The second case (@CArray@) uses depedent types to promote the length of+    -- the array to type level.+    toField :: CStruct -> CField -> String+    toField cstruct' (CPlain t n) = name ++ " :: " ++ ty+      where+        name = fieldName cstruct' n+        ty   = "Field" ++ " " ++ show n+                       ++ " " ++ cTypeName2HaskellType t++    toField cstruct' (CArray t n l) = name ++ " :: " ++ ty+      where+        name = fieldName cstruct' n+        ty   = "Field" ++ " " ++ show n+                       ++ " (" ++ "Array"+                       ++ " " ++ show l+                       ++ " " ++ cTypeName2HaskellType t+                       ++ ")"++-- | Convert a 'CStruct' definition into a Copilot @Struct@ instance+-- declaration. For example, for the struct:+--+-- @+--   struct {+--     uint8_t f1;+--   } a_struct_t;+-- @+--+-- the corresponding @Struct@ instance would be:+--+-- @+--   instance Struct AStruct where+--     typename _ = "a_struct_t"+--     toValues v = [Value Word8 (aSF1 v)]+-- @+structInstance :: CStruct -> String+structInstance cstruct =+    "instance " ++ instanceHead ++ " where\n" +++    unlines (map ("  " ++ ) instanceBody)+  where+    instanceHead = "Struct" ++ " " ++ instanceName+    instanceName = cStructName2Haskell $ cStructName cstruct++    instanceBody = [ instanceTypename, instanceToValues ]++    instanceTypename = "typename" ++ " " ++ "_" ++ " = " ++ show (cStructName cstruct)++    instanceToValues =+      "toValues" ++ " " ++ "v" ++ " = " ++ "[ " ++ intercalate ", " valueDecls ++ " ]"++    valueDecls = map (toValueDecl cstruct) (cStructFields cstruct)++    toValueDecl :: CStruct -> CField -> String+    toValueDecl c (CPlain t n) =+      "Value" ++ " " ++ cTypeName2HaskellType t+              ++ " (" ++ fieldName c n+              ++ " " ++ "v" ++ ")"++    toValueDecl c (CArray t n _len) =+      "Value" ++ " (" ++ "Array"+              ++ " " ++ cTypeName2HaskellType t ++ ")"+              ++ " " ++ "(" ++ fieldName c n+              ++ " " ++ "v" ++ ")"++-- | Convert a 'CStruct' definition to Copilot @Typed@ instance declaration.+-- For example, for the struct:+--+-- @+--   struct {+--     uint8_t f1;+--   } a_struct_t;+-- @+--+-- the corresponding @Typed@ instance could be:+--+-- @+--   instance Typed AStruct where+--     typeOf = Struct (Field 0)+-- @+typedInstance :: CStruct -> String+typedInstance cstruct =+    "instance " ++ instanceHead ++ " where\n" +++    unlines (map ("  " ++ ) instanceBody)+  where+    instanceHead = "Typed" ++ " " ++ instanceName+    instanceName = cStructName2Haskell $ cStructName cstruct++    instanceBody   = [ instanceTypeOf ]++    instanceTypeOf = "typeOf" ++ " = " ++ "Struct" ++ " "+                  ++ "(" ++ dataConstructorName ++ " " ++ unwords vs ++ ")"++    dataConstructorName = cStructName2Haskell $ cStructName cstruct++    vs = map ((\x -> "(" ++ "Field" ++ " " ++ x ++ ")") . defaultValue)+             (cStructFields cstruct)++-- * Auxiliary functions++-- | Provide a suitable field name for a record field of a 'CStruct' in Haskell.+--+-- For example, given the struct:+--+-- @+--   struct {+--     uint8_t f1;+--   } a_struct_t;+-- @+--+-- the field name in the Haskell record would be @aSF1@, where the @aS@ and+-- comes from @a_struct_t@ and the final @F1@ comes from @f1@.+fieldName :: CStruct -> String -> String+fieldName cstruct n =+    summary (cStructName2Haskell (cStructName cstruct)) ++ cStructName2Haskell n+  where+    summary :: String -> String+    summary = map toLower . filter isUpper++-- | Convert a C struct name (e.g., @some_type_t@) to a Haskell type name+-- (e.g., @SomeType@).+cStructName2Haskell :: String -> String+cStructName2Haskell = camelCaseTypeName++-- | Return the corresponding type in Copilot/Haskell for a given type.+cTypeName2HaskellType :: String -> String+cTypeName2HaskellType "float"    = "Float"+cTypeName2HaskellType "double"   = "Double"+cTypeName2HaskellType "int"      = "Int"+cTypeName2HaskellType "uint8_t"  = "Word8"+cTypeName2HaskellType "uint16_t" = "Word16"+cTypeName2HaskellType "uint32_t" = "Word32"+cTypeName2HaskellType "uint64_t" = "Word64"+cTypeName2HaskellType "int8_t"   = "Int8"+cTypeName2HaskellType "int16_t"  = "Int16"+cTypeName2HaskellType "int32_t"  = "Int32"+cTypeName2HaskellType "int64_t"  = "Int64"+cTypeName2HaskellType "bool"     = "Bool"+cTypeName2HaskellType t          = camelCaseTypeName t++-- | Create a default value in Copilot for a field of a given type.+defaultValue :: CField -> String+defaultValue CArray {}    = "(array [])"+defaultValue (CPlain t _) = defaultValueOfType t+  where+    defaultValueOfType "float"    = "0"+    defaultValueOfType "double"   = "0"+    defaultValueOfType "int"      = "0"+    defaultValueOfType "uint8_t"  = "0"+    defaultValueOfType "uint16_t" = "0"+    defaultValueOfType "uint32_t" = "0"+    defaultValueOfType "uint64_t" = "0"+    defaultValueOfType "int8_t"   = "0"+    defaultValueOfType "int16_t"  = "0"+    defaultValueOfType "int32_t"  = "0"+    defaultValueOfType "int64_t"  = "0"+    defaultValueOfType "bool"     = "True"+    defaultValueOfType _t         = "0"
+ src/Language/Trans/CStructs2MsgHandlers.hs view
@@ -0,0 +1,76 @@+-- 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.+--+-- | Generate C methods that process message dealing with the structs+-- defined in a header file.+--+-- This module contains the pure conversion from CStructs into C code.+-- Normally, this module would be implemented as a conversion between C ASTs,+-- but we want to add comments to the generated code, which are not+-- representable in the abstract syntax tree.+module Language.Trans.CStructs2MsgHandlers where++-- Internal imports: C AST representation.+import qualified Language.C.AbsC as C ( TranslationUnit (MkTranslationUnit) )++-- Internal imports: Copilot's own CStruct representation.+import Language.Copilot.CStruct ( CStruct (cStructName) )++import Language.Trans.CStruct2CopilotStruct ( camelCaseTypeName, mkCStruct )++-- | Generate a C methods that process message dealing with the structs+-- defined in a header file.+cstructs2MsgHandlers :: C.TranslationUnit -> Either String String+cstructs2MsgHandlers (C.MkTranslationUnit gs) =+  unlines <$> mapM (fmap cstruct2MsgHandler . mkCStruct) gs++-- | Generate a C method that processes one message dealing with one+-- kind of struct.+cstruct2MsgHandler :: CStruct -> String+cstruct2MsgHandler cstruct = unlines+    [ nameCStruct ++ " " ++ nameLocalVar ++ ";"+    , ""+    , "/**"+    , "* Make ICAROUS data available to Copilot and run monitors."+    , "*/"+    , "void COPILOT_Process" ++ nameVar ++ "Monitor(void)"+    , "{"+    , "  " ++ nameCStruct ++ "* msg;"+    , "  msg = (" ++ nameCStruct  ++ "*) COPILOTMsgPtr;"+    , "  " ++ nameLocalVar ++ " = *msg;"+    , ""+    , "  // Run all copilot monitors."+    , "  step();"+    , "}"+    ]+  where+    nameCStruct  = cStructName cstruct+    nameVar      = camelCaseTypeName nameCStruct+    nameLocalVar = 'm' : 'y' : camelCaseTypeName nameCStruct
+ src/Language/Trans/CoCoSpec2Copilot.hs view
@@ -0,0 +1,199 @@+-- 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 CoCoSpec 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+-- representable in the abstract syntax tree.+module Language.Trans.CoCoSpec2Copilot (boolSpec2Copilot, boolSpecNames) where++-- Internal imports+import Language.CoCoSpec.AbsCoCoSpec ( BoolConst (..), BoolNumOp (..),+                                       BoolSpec (..), Ident (..), NumExpr (..),+                                       NumOp2In (..), Op1Pre (..), Op2In (..),+                                       Op2Pre (..) )++-- | Return the Copilot representation of a CoCoSpec 'BoolSpec'.+--+-- This function returns the temporal property only. The string does not+-- contain any top-level names, any imports, or auxiliary definitions that+-- may be required.+boolSpec2Copilot :: BoolSpec -> String+boolSpec2Copilot b = case b of+  BoolSpecPar bs                 -> "( " ++ boolSpec2Copilot bs ++ " )"+  BoolSpecConstI bc              -> show bc+  BoolSpecConstD bc              -> show bc+  BoolSpecConstB bc              -> const2Copilot bc+  BoolSpecSignal i               -> ident2Copilot i+  BoolSpecOp1Pre op spec         -> opOnePre2Copilot op ++ " (" ++ boolSpec2Copilot spec ++ ")"++  BoolSpecOp2In spec1 Op2InPre (BoolSpecOp1Pre Op1Pre spec2)+    -> "[" ++ lit2Copilot spec1 ++ "] ++ " ++ boolSpec2Copilot spec2++  BoolSpecOp2In spec1 Op2InPre spec2+    -> "mux ftp (constant " ++ lit2Copilot spec1 ++ ") (" ++ boolSpec2Copilot spec2 ++ ")"++  BoolSpecOp2In spec1 op2 spec2  -> "(" ++ boolSpec2Copilot spec1+                                 ++ " " ++ opTwoIn2Copilot op2+                                 ++ " " ++ boolSpec2Copilot spec2+                                 ++ ")"++  BoolSpecOp2Pre op2 spec1 spec2 -> opTwoPre2Copilot op2 ++ " " ++ boolSpec2Copilot spec1+                                                    ++ " " ++ boolSpec2Copilot spec2++  BoolSpecOp2HT  num1 num2 spec  -> "MTL.alwaysBeen"+                                       ++ " " ++ numExpr2Copilot num2+                                       ++ " " ++ numExpr2Copilot num1+                                       ++ " clock 1" -- clock and min time distance+                                       ++ " " ++ boolSpec2Copilot spec++  BoolSpecOp2OT  num1 num2 spec  -> "MTL.eventuallyPrev"+                                       ++ " " ++ numExpr2Copilot num2+                                       ++ " " ++ numExpr2Copilot num1+                                       ++ " clock 1" -- clock and min time distance+                                       ++ " " ++ boolSpec2Copilot spec++  BoolSpecOp2ST  num1 num2 spec1 spec2 -> "MTL.since"+                                             ++ " " ++ numExpr2Copilot num1+                                             ++ " " ++ numExpr2Copilot num2+                                             ++ " clock 1" -- clock and min time distance+                                             ++ " " ++ boolSpec2Copilot spec1+                                             ++ " " ++ boolSpec2Copilot spec2++-- | Return the Copilot representation of a CoCoSpec numeric+-- expression.+--+-- This function returns the expression only. The string does not contain any+-- top-level names, any imports, or auxiliary definitions that may be required.+numExpr2Copilot :: NumExpr -> String+numExpr2Copilot expr = case expr of+  NumExprNum i                  -> show i+  NumExprPar iExpr              -> "(" ++ numExpr2Copilot iExpr  ++ ")"+  NumExprOp2In iExpr1 op iExpr2 -> "(" ++ numExpr2Copilot iExpr1 ++ " "+                                       ++ numOpTwoIn2Copilot op    ++ " "+                                       ++ numExpr2Copilot iExpr2 ++ ")"+  NumExprId i                   -> ident2Copilot i++-- | Return the Copilot representation of a numeric CoCoSpec arithmetic+-- operator.+numOpTwoIn2Copilot :: NumOp2In -> String+numOpTwoIn2Copilot NumOp2Plus  = "+"+numOpTwoIn2Copilot NumOp2Minus = "-"+numOpTwoIn2Copilot NumOp2Mult  = "*"++-- | Return the Copilot representation of a numeric CoCoSpec comparison+-- operator.+opTwoNum2Copilot :: BoolNumOp -> String+opTwoNum2Copilot BoolNumOp2Eq = "=="+opTwoNum2Copilot BoolNumOp2Le = "<="+opTwoNum2Copilot BoolNumOp2Lt = "<"+opTwoNum2Copilot BoolNumOp2Gt = ">="+opTwoNum2Copilot BoolNumOp2Ge = ">"++-- | Return the Copilot representation of a CoCoSpec boolean+-- constant.+const2Copilot :: BoolConst -> String+const2Copilot BoolConstTrue  = "true"+const2Copilot BoolConstFalse = "false"+const2Copilot BoolConstFTP   = "ftp"++-- | Return the Copilot representation of a CoCoSpec logical+-- operator.+opOnePre2Copilot :: Op1Pre -> String+opOnePre2Copilot Op1Pre    = "pre"+opOnePre2Copilot Op1Once   = "PTLTL.eventuallyPrev"+opOnePre2Copilot Op1Hist   = "PTLTL.alwaysBeen"+opOnePre2Copilot Op1Y      = "PTLTL.previous"+opOnePre2Copilot Op1Not    = "not"+opOnePre2Copilot Op1Bang   = "not"++-- | Return the Copilot representation of a CoCoSpec logical+-- operator.+opTwoIn2Copilot :: Op2In -> String+opTwoIn2Copilot Op2Amp   = "&&"+opTwoIn2Copilot Op2And   = "&&"+opTwoIn2Copilot Op2Or    = "||"+opTwoIn2Copilot Op2Impl  = "==>"+opTwoIn2Copilot Op2InPre = "pre"+opTwoIn2Copilot (Op2NumOp n) = numOpTwoIn2Copilot n+opTwoIn2Copilot (Op2NumCmp n) = opTwoNum2Copilot n++-- | Return the Copilot representation of a CoCoSpec logical+-- operator.+opTwoPre2Copilot :: Op2Pre -> String+opTwoPre2Copilot Op2SI = "since"+opTwoPre2Copilot Op2OT = "ot"++-- | Return the Copilot representation of a CoCoSpec identifier.+ident2Copilot :: Ident -> String+ident2Copilot (Ident "FTP") = "ftp"+ident2Copilot (Ident s)     = s++-- | Return all identifiers used in a BoolSpec that are not reserved keywords.+boolSpecNames :: BoolSpec -> [String]+boolSpecNames (BoolSpecPar bs)                  = boolSpecNames bs+boolSpecNames (BoolSpecConstI _bc)              = []+boolSpecNames (BoolSpecConstD _bc)              = []+boolSpecNames (BoolSpecConstB _bc)              = []+boolSpecNames (BoolSpecSignal (Ident i))        = [i]+boolSpecNames (BoolSpecOp1Pre _op spec)         = boolSpecNames spec+boolSpecNames (BoolSpecOp2In  spec1 _op2 spec2) = boolSpecNames spec1 ++ boolSpecNames spec2+boolSpecNames (BoolSpecOp2Pre _op2 spec1 spec2) = boolSpecNames spec1 ++ boolSpecNames spec2+boolSpecNames (BoolSpecOp2HT  num1 num2 spec)   =+  numExprNames num1 ++ numExprNames num2 ++ boolSpecNames spec+boolSpecNames (BoolSpecOp2OT  num1 num2 spec)   =+  numExprNames num1 ++ numExprNames num2 ++ boolSpecNames spec+boolSpecNames (BoolSpecOp2ST  num1 num2 spec1 spec2)   =+  numExprNames num1 ++ numExprNames num2 ++ boolSpecNames spec1 ++ boolSpecNames spec2++-- | Return all identifiers used in a NumExpr that are not reserved keywords.+numExprNames :: NumExpr -> [String]+numExprNames (NumExprNum _i)                = []+numExprNames (NumExprPar expr)              = numExprNames expr+numExprNames (NumExprOp2In expr1 _op expr2) =+  numExprNames expr1 ++ numExprNames expr2+numExprNames (NumExprId (Ident i))          = [i]++-- | Return the Copilot representation of a CoCoSpec literal.+lit2Copilot :: BoolSpec -> String+lit2Copilot b = case b of+    BoolSpecConstI bc -> show bc+    BoolSpecConstD bc -> show bc+    BoolSpecConstB bc -> litConst2Copilot bc+    BoolSpecSignal i  -> ident2Copilot i+    _                 -> ":error converting literal:"+  where+    -- | Return the Copilot representation of a CoCoSpec boolean+    -- constant.+    litConst2Copilot :: BoolConst -> String+    litConst2Copilot BoolConstTrue  = "True"+    litConst2Copilot BoolConstFalse = "False"+    litConst2Copilot _              = ":error converting literal boolean:"
+ src/Language/Trans/FRETComponentSpec2Copilot.hs view
@@ -0,0 +1,327 @@+-- 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.+--+{-# LANGUAGE OverloadedStrings #-}++-- | Transform a FRET Component 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 representable+-- in the abstract syntax tree.+module Language.Trans.FRETComponentSpec2Copilot where++-- External imports+import Data.List  ( intersect, union )+import Data.Maybe ( fromMaybe )++-- External imports: auxiliary+import Data.String.Extra ( sanitizeLCIdentifier, sanitizeUCIdentifier )++-- Internal imports: language ASTs, transformers+import qualified Language.CoCoSpec.ParCoCoSpec   as CoCoSpec ( myLexer,+                                                               pBoolSpec )+import           Language.FRETComponentSpec.AST  as FRET+import qualified Language.Trans.CoCoSpec2Copilot as CoCoSpec ( boolSpec2Copilot )+import           Language.Trans.SMV2Copilot      as SMV ( boolSpec2Copilot )++-- | Options used to customize the conversion of FRET Component Specifications+-- to Copilot code.+data FRETComponentSpec2CopilotOptions = FRETComponentSpec2CopilotOptions+  { fretCS2CopilotUseCoCoSpec :: Bool+  , fretCS2CopilotIntType     :: String+  , fretCS2CopilotRealType    :: String+  }++-- | Transform a FRET TL specification into a Copilot specification.+--+-- This function may fail with a 'Left' value if the resulting Copilot+-- specification would contain name clashes or other errors.+fretComponentSpec2Copilot :: FRETComponentSpec2CopilotOptions+                          -> FRETComponentSpec+                          -> Either String String+fretComponentSpec2Copilot prefs parseResult =+  fretComponentSpec2Copilot' prefs =<< fret2CopilotAnalyze parseResult++-- | For a given FRET file, return the corresponding Copilot file, or an error+-- message if such file cannot be generated.+--+-- PRE: there are no name clashes between the variables and names used in the+-- FRET specification and any definitions in Haskell's Prelude or in Copilot.+fretComponentSpec2Copilot' :: FRETComponentSpec2CopilotOptions+                           -> FRETComponentSpec+                           -> Either String String+fretComponentSpec2Copilot' prefs fretComponentSpec =+    unlines . concat <$> sequence+      [ pure imports+      , pure externs+      , internals+      , reqs+      , pure clock+      , pure ftp+      , pure pre+      , pure spec+      , pure main'+      ]++  where++    -- Import header block+    imports :: [String]+    imports =+      [ "import           Copilot.Compile.C99"+      , "import           Copilot.Language          hiding (prop)"+      , "import           Copilot.Language.Prelude"+      , "import           Copilot.Library.LTL       (next)"+      , "import           Copilot.Library.MTL       hiding (since,"+        ++ " alwaysBeen, trigger)"+      , "import           Copilot.Library.PTLTL     (since, previous,"+        ++ " alwaysBeen)"+      , "import qualified Copilot.Library.PTLTL     as PTLTL"+      , "import qualified Copilot.Library.MTL       as MTL"+      , "import           Language.Copilot          (reify)"+      , "import           Prelude                   hiding ((&&), (||), (++),"+        ++ " (<=), (>=), (<), (>), (==), not)"+      , ""+      ]++    -- Extern streams+    externs = concatMap externVarToDecl+                        (FRET.fretExternalVariables fretComponentSpec)+      where+        externVarToDecl i = [ FRET.fretExternalVariableName i+                                ++ " :: Stream "+                                ++ "("+                                ++ fretTypeToCopilotType+                                     prefs+                                     (FRET.fretExternalVariableType i)+                                ++ ")"++                            , FRET.fretExternalVariableName i+                                ++ " = "+                                ++ "extern"+                                ++ " "+                                ++ show (FRET.fretExternalVariableName i)+                                ++ " "+                                ++ "Nothing"+                            , ""+                            ]++    -- Internal stream definitions+    internals = concat+             <$> mapM internalVarToDecl+                      (FRET.fretInternalVariables fretComponentSpec)+      where+        internalVarToDecl i = fmap (\implem ->+                                [ FRET.fretInternalVariableName i+                                    ++ " :: Stream "+                                    ++ "("+                                    ++ fretTypeToCopilotType+                                         prefs+                                         (FRET.fretInternalVariableType i)+                                    ++ ")"++                                , FRET.fretInternalVariableName i+                                    ++ " = "+                                    ++ implem++                                , ""+                                ]) implementation+          where+            implementation = if null (FRET.fretInternalVariableCopilot i)+                               then CoCoSpec.boolSpec2Copilot+                                      <$> CoCoSpec.pBoolSpec+                                            ( CoCoSpec.myLexer+                                            $ FRET.fretInternalVariableLustre i+                                            )+                               else pure (FRET.fretInternalVariableCopilot i)++    -- Encoding of requirements as boolean streams+    reqs :: Either String [String]+    reqs = concat <$> mapM reqToDecl (FRET.fretRequirements fretComponentSpec)+      where+        reqToDecl i = sequence+                        [ pure reqComment, pure reqSignature, reqBody, pure "" ]+          where+            -- Definition comment, which includes the requirement for+            -- traceability purposes.+            reqComment = "-- | "  ++ FRET.fretRequirementName i    ++ "\n" +++                         "--   @"                                  ++ "\n" +++                         "--   "  ++ FRET.fretRequirementFretish i ++ "\n" +++                         "--   @"++            -- Definition type signature.+            reqSignature = FRET.fretRequirementName i+                             ++ " :: " ++ "Stream" ++ " " ++ "Bool"++            -- Definition implementation, either in SMV or in CoCoSpec+            reqBody = if fretCS2CopilotUseCoCoSpec prefs+                        then reqBodyCoCo+                        else reqBodyPT++            reqBodyPT = fmap (\e -> FRET.fretRequirementName i ++ " = "+                                      ++ SMV.boolSpec2Copilot e+                             )+                             (fromMaybe (Left $ "No requirement for " ++ show i)+                                        (FRET.fretRequirementPTExpanded i))++            reqBodyCoCo = fmap+                            (\e -> FRET.fretRequirementName i ++ " = "+                                     ++ CoCoSpec.boolSpec2Copilot e+                            )+                            (fromMaybe (Left $ "No requirement for " ++ show i)+                                       (FRET.fretRequirementCoCoSpec i))++    -- Auxiliary streams: clock+    clock :: [String]+    clock = [ ""+            , "-- | Clock that increases in one-unit steps."+            , "clock :: Stream Int64"+            , "clock = [0] ++ (clock + 1)"+            , ""+            ]++    -- Auxiliary streams: first time point+    ftp :: [String]+    ftp = [ ""+          , "-- | First Time Point"+          , "ftp :: Stream Bool"+          , "ftp = [True] ++ false"+          , ""+          ]++    -- Auxiliary streams: pre+    pre = [ ""+          , "pre :: Stream Bool -> Stream Bool"+          , "pre = ([False] ++)"+          ]++    -- Main specification+    spec :: [String]+    spec = [ ""+           , "-- | Complete specification. Calls the C function void "+             ++ " handler(); when"+           , "-- the property is violated."+           , "spec :: Spec"+           , "spec = do"+           ]+           ++ triggers+           ++ [ "" ]+      where+        triggers :: [String]+        triggers = fmap reqTrigger (FRET.fretRequirements fretComponentSpec)++        reqTrigger :: FRETRequirement -> String+        reqTrigger r = "  trigger " ++ show handlerName ++ " (not "+                       ++ propName ++ ") " ++ "[]"+          where+            handlerName = "handler" ++ FRET.fretRequirementName r+            propName    = FRET.fretRequirementName r++    -- Main program that compiles specification to C in two files (code and+    -- header).+    main' :: [String]+    main' = [ ""+            , "main :: IO ()"+            , "main = reify spec >>= compile \"fret\""+            ]++-- | Return the corresponding type in Copilot matching a given FRET type.+fretTypeToCopilotType :: FRETComponentSpec2CopilotOptions -> String -> String+fretTypeToCopilotType _options "bool"    = "Bool"+fretTypeToCopilotType options  "int"     = fretCS2CopilotIntType options+fretTypeToCopilotType options  "integer" = fretCS2CopilotIntType options+fretTypeToCopilotType options  "real"    = fretCS2CopilotRealType options+fretTypeToCopilotType _options "string"  = "String"+fretTypeToCopilotType _options x         = x++-- | Analyze a FRET-Copilot file and determine if there will be any name+-- clashes after the conversion to Copilot.+--+-- This function does not compare against Haskell's prelude or Copilot's+-- modules. It simply makes simple conversions to comply with Copilot/Haskell's+-- grammar (e.g., variable/function names start with lowercase) and determines+-- if the conversion would make two definitions in the given specification+-- produce name clashes between them.+fret2CopilotAnalyze :: FRETComponentSpec -> Either String FRETComponentSpec+fret2CopilotAnalyze fretComponentSpec+    | not (null evnClash)+    = Left $ "Name clash detected: " ++ show evnClash++    | not (null ivnClash)+    = Left $ "Name clash detected: " ++ show ivnClash++    | not (null reqClash)+    = Left $ "Name clash detected: " ++ show reqClash++    | otherwise+    = Right $ foldr applySubstitution fretComponentSpec nameSubstitutions++  where++    -- Sets containing name clashes+    ivnClash = internalVariableNames'+                 `intersect` (externalVariableNames' `union` requirementNames')++    evnClash = externalVariableNames'+                 `intersect` (internalVariableNames' `union` requirementNames')++    reqClash = requirementNames'+                 `intersect` (internalVariableNames'+                                `union` externalVariableNames')++    -- Names used.+    internalVariableNames' = map snd internalVariableMap+    externalVariableNames' = map snd externalVariableMap+    requirementNames'      = map snd requirementNameMap++    -- Map from a variable name to its desired identifier in the code+    -- generated.+    internalVariableMap =+      map (\x -> (x, sanitizeLCIdentifier x)) internalVariableNames++    externalVariableMap =+      map (\x -> (x, sanitizeLCIdentifier x)) externalVariableNames++    requirementNameMap =+      map (\x -> (x, "prop" ++ sanitizeUCIdentifier x)) requirementNames++    nameSubstitutions = internalVariableMap+                     ++ externalVariableMap+                     ++ requirementNameMap++    -- Variable/requirement names used in the component spec.+    internalVariableNames = map fretInternalVariableName+                          $ fretInternalVariables fretComponentSpec++    externalVariableNames = map fretExternalVariableName+                          $ fretExternalVariables fretComponentSpec++    requirementNames = map fretRequirementName+                     $ fretRequirements fretComponentSpec
+ src/Language/Trans/FRETReqsDB2Copilot.hs view
@@ -0,0 +1,159 @@+-- 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 temporal logic specification contained in a requirements+-- database into a Copilot specification.+--+-- Ideally, this module would be implemented as a conversion between ASTs, but+-- we want to add comments to the generated code, which are not representable+-- in the abstract syntax tree.+module Language.Trans.FRETReqsDB2Copilot+    ( FRETReqsDB2CopilotOptions(..)+    , fret2CopilotModule+    )+  where++-- External imports+import Data.List ( nub, sort )++-- Internal imports: SMV+import qualified Language.SMV.AbsSMV        as SMV ( BoolSpec (..) )+import qualified Language.Trans.SMV2Copilot as SMV ( boolSpec2Copilot,+                                                     boolSpecNames )++-- Internal imports: CoCoSpec+import qualified Language.CoCoSpec.AbsCoCoSpec   as CoCoSpec ( BoolSpec (..) )+import qualified Language.Trans.CoCoSpec2Copilot as CoCoSpec ( boolSpec2Copilot,+                                                               boolSpecNames )++import qualified Language.FRETReqsDB.AST as FRET ( FRETReqsDB, semantics,+                                                   semanticsCoCoSpec,+                                                   semanticsFretish )++-- | Options used to customize the conversion of FRET Component Specifications+-- to Copilot code.+data FRETReqsDB2CopilotOptions = FRETReqsDB2CopilotOptions+  { fretReqsDB2CopilotUseCoCoSpec :: Bool+  }++-- | Return a string with the contents of the Copilot module that implements a+-- CoCoSpec BoolSpec.+--+-- PRE: The BoolSpec does not use any identifiers that exist in Copilot,+-- or any of @prop@, @clock@, @ftp@, @ot@, @pre@. All identifiers used are+-- valid C99 identifiers.+fret2CopilotModule :: FRETReqsDB2CopilotOptions+                   -> FRET.FRETReqsDB+                   -> Either String String+fret2CopilotModule prefs x = do+  cocoSpec <- FRET.semanticsCoCoSpec $ FRET.semantics x+  smvSpec  <- FRET.semanticsFretish  $ FRET.semantics x+  pure $ fret2CopilotModule' prefs smvSpec cocoSpec++fret2CopilotModule' :: FRETReqsDB2CopilotOptions+                    -> SMV.BoolSpec+                    -> CoCoSpec.BoolSpec+                    -> String+fret2CopilotModule' prefs smvSpec cocoSpec = unlines $ concat sections+  where+    specS = if fretReqsDB2CopilotUseCoCoSpec prefs+              then CoCoSpec.boolSpec2Copilot cocoSpec+              else SMV.boolSpec2Copilot smvSpec++    idents   = nub $ sort $ if fretReqsDB2CopilotUseCoCoSpec prefs+                              then CoCoSpec.boolSpecNames cocoSpec+                              else SMV.boolSpecNames smvSpec++    sections | fretReqsDB2CopilotUseCoCoSpec prefs+             = [ imports, propDef, externs, clock, ftp, undef, spec, main' ]++             | otherwise+             = [ imports, propDef, externs, clock, ftp, spec, main' ]++    imports :: [String]+    imports =+      [ "import           Copilot.Compile.C99"+      , "import           Copilot.Language          hiding (prop)"+      , "import           Copilot.Language.Prelude"+      , "import           Copilot.Library.LTL       (next)"+      , "import           Copilot.Library.MTL       hiding (since,"+        ++ " alwaysBeen, trigger)"+      , "import           Copilot.Library.PTLTL     (since, previous,"+        ++ " alwaysBeen)"+      , "import qualified Copilot.Library.PTLTL     as PTLTL"+      , "import           Language.Copilot          (reify)"+      , "import Prelude                   hiding ((&&), (||), (++), (<=), (>=),"+        ++ " (<), (>), (==), not)"+      , ""+      ]++    propDef  = [ ""+               , "-- | Property to monitor."+               , "prop :: Stream Bool"+               , "prop = " ++ specS+               , ""+               ]++    externs  = map (\i -> i ++ " = extern " ++ show i ++ " Nothing") idents++    clock    = [ ""+               , "-- | Clock that increases in one-unit steps."+               , "clock :: Stream Int64"+               , "clock = [0] ++ (clock + 1)"+               , ""+               ]++    ftp      = [ ""+               , "-- | First Time Point"+               , "ftp :: Stream Bool"+               , "ftp = [True] ++ false"+               , ""+               ]++    undef    = [ "ot :: Int -> Int -> Stream Bool -> Stream Bool"+               , "ot = undefined"+               , "pre :: Stream Bool -> Stream Bool"+               , "pre = undefined"+               ]++    spec     = [ ""+               , "-- | Complete specification. Calls the C function void handler(); when"+               , "-- the property is violated."+               , "spec :: Spec"+               , "spec = do"+               , "  trigger  \"handler\" prop []"+               , ""+               ]++    main'    = [ ""+               , "main :: IO ()"+               , "main = reify spec >>= compile \"fret\""+               ]
+ src/Language/Trans/SMV2Copilot.hs view
@@ -0,0 +1,216 @@+-- 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 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+-- representable in the abstract syntax tree.+module Language.Trans.SMV2Copilot where++import Language.SMV.AbsSMV (AdditiveOp (..), BoolConst (..), BoolSpec (..),+                            Ident (..), MultOp (..), NumExpr (..), Number (..),+                            Op1Name (..), OpOne (..), OpTwo (..), OrdOp (..))++-- | Return the Copilot representation of a FRET BoolSpec.+--+-- This function returns the temporal property only. The string does not+-- contain any top-level names, any imports, or auxiliary definitions that may+-- be required.+boolSpec2Copilot :: BoolSpec -> String+boolSpec2Copilot b = case b of+  BoolSpecConst bc -> const2Copilot bc++  BoolSpecNum nc -> numExpr2Copilot nc++  BoolSpecSignal i -> ident2Copilot i++  BoolSpecCmp spec1 op2 spec2 -> "(" ++ boolSpec2Copilot spec1+                              ++ " " ++ ordOp2Copilot op2+                              ++ " " ++ boolSpec2Copilot spec2+                              ++ ")"++  BoolSpecNeg spec -> "(" ++ "not"+                   ++ " " ++ boolSpec2Copilot spec+                   ++ ")"++  BoolSpecAnd spec1 spec2 -> "(" ++ boolSpec2Copilot spec1+                          ++ " " ++ "&&"+                          ++ " " ++ boolSpec2Copilot spec2+                          ++ ")"++  BoolSpecOr spec1 spec2 -> "(" ++ boolSpec2Copilot spec1+                         ++ " " ++ "||"+                         ++ " " ++ boolSpec2Copilot spec2+                         ++ ")"++  BoolSpecXor spec1 spec2 -> "(" ++ boolSpec2Copilot spec1+                          ++ " " ++ "`xor`"+                          ++ " " ++ boolSpec2Copilot spec2+                          ++ ")"++  BoolSpecImplies spec1 spec2 -> "(" ++ boolSpec2Copilot spec1+                              ++ " " ++ "==>"+                              ++ " " ++ boolSpec2Copilot spec2+                              ++ ")"++  BoolSpecEquivs spec1 spec2 -> "(" ++ boolSpec2Copilot spec1+                             ++ " " ++ "<==>"+                             ++ " " ++ boolSpec2Copilot spec2+                             ++ ")"++  BoolSpecOp1 op spec -> "(" ++ opOne2Copilot op+                      ++ " " ++ boolSpec2Copilot spec+                      ++ ")"++  BoolSpecOp2 spec1 op2 spec2 -> "(" ++ boolSpec2Copilot spec1+                              ++ " " ++ opTwo2Copilot op2+                              ++ " " ++ boolSpec2Copilot spec2+                              ++ ")"++-- | Return the Copilot representation of a FRET boolean constant.+const2Copilot :: BoolConst -> String+const2Copilot BoolConstTrue  = "true"+const2Copilot BoolConstFalse = "false"+const2Copilot BoolConstFTP   = "ftp"+const2Copilot BoolConstLAST  = "last"++-- | Return the Copilot representation of a numeric expression.+numExpr2Copilot :: NumExpr -> String+numExpr2Copilot (NumId i)        = ident2Copilot i+numExpr2Copilot (NumConstI i)    = show i+numExpr2Copilot (NumConstD i)    = show i+numExpr2Copilot (NumAdd x op y)  = "("+                                   ++ numExpr2Copilot x+                                   ++ additiveOp2Copilot op+                                   ++ numExpr2Copilot y+                                   ++ ")"+numExpr2Copilot (NumMult x op y) = "("+                                   ++ numExpr2Copilot x+                                   ++ multOp2Copilot op+                                   ++ numExpr2Copilot y+                                   ++ ")"++-- | Return the Copilot representation of a FRET additive operator.+additiveOp2Copilot :: AdditiveOp -> String+additiveOp2Copilot OpPlus  = "+"+additiveOp2Copilot OpMinus = "-"++-- | Return the Copilot representation of a FRET multiplicative operator.+multOp2Copilot :: MultOp -> String+multOp2Copilot OpTimes = "*"+multOp2Copilot OpDiv   = "/"++-- | Return the Copilot representation of a FRET comparison operator.+ordOp2Copilot :: OrdOp -> String+ordOp2Copilot OrdOpLT = "<"+ordOp2Copilot OrdOpLE = "<="+ordOp2Copilot OrdOpEQ = "=="+ordOp2Copilot OrdOpGT = ">"+ordOp2Copilot OrdOpGE = ">="++-- | Return the Copilot representation of a unary logical FRET operator.+opOne2Copilot :: OpOne -> String+opOne2Copilot (Op1Alone x)    = opOneAlone2Copilot x+opOne2Copilot (Op1MTL x op v) = opOneMTL2Copilot x op v++-- | Return the Copilot representation of a unary logical non-MTL FRET+-- operator.+opOneAlone2Copilot :: Op1Name -> String+opOneAlone2Copilot Op1Pre  = "pre"+opOneAlone2Copilot Op1X    = "next"+opOneAlone2Copilot Op1G    = "always"+opOneAlone2Copilot Op1F    = "eventually"+opOneAlone2Copilot Op1Y    = "PTLTL.previous"+opOneAlone2Copilot Op1Z    = "notPreviousNot"+opOneAlone2Copilot Op1Hist = "PTLTL.alwaysBeen"+opOneAlone2Copilot Op1O    = "PTLTL.eventuallyPrev"++-- | Return the Copilot representation of a unary logical MTL FRET operator.+opOneMTL2Copilot :: Op1Name -> OrdOp -> Number -> String+opOneMTL2Copilot operator _comparison number =+  opOneMTL2Copilot' operator ++ " " ++ show (0 :: Int)+                             ++ " " ++ number2Copilot number+                             ++ " " ++ "clock" ++ " "+                             ++ show (1 :: Int)++-- | Return the Copilot representation of a unary logical possibly MTL FRET+-- operator.+opOneMTL2Copilot' :: Op1Name -> String+opOneMTL2Copilot' Op1Pre  = "pre"+opOneMTL2Copilot' Op1X    = "next"+opOneMTL2Copilot' Op1G    = "always"+opOneMTL2Copilot' Op1F    = "eventually"+opOneMTL2Copilot' Op1Y    = "MTL.previous"+opOneMTL2Copilot' Op1Z    = "notPreviousNot"+opOneMTL2Copilot' Op1Hist = "MTL.alwaysBeen"+opOneMTL2Copilot' Op1O    = "MTL.eventuallyPrev"++-- | Return the Copilot representation of a FRET number.+number2Copilot :: Number -> String+number2Copilot (NumberInt n) = show n++-- | Return the Copilot representation of a binary logical non-MTL FRET+-- operator.+opTwo2Copilot :: OpTwo -> String+opTwo2Copilot Op2S = "`since`"+opTwo2Copilot Op2T = "`triggers`"+opTwo2Copilot Op2V = "`releases`"+opTwo2Copilot Op2U = "`until`"++-- | Return the Copilot representation of a FRET identifier.+ident2Copilot :: Ident -> String+ident2Copilot (Ident i) = i++-- | Return all identifiers used in a BoolSpec that are not reserved keywords.+boolSpecNames :: BoolSpec -> [String]+boolSpecNames b = case b of+  BoolSpecConst _bc            -> []+  BoolSpecSignal (Ident i)     -> [i]+  BoolSpecNum e                -> numExprNames e+  BoolSpecCmp spec1 _op2 spec2 -> boolSpecNames spec1 ++ boolSpecNames spec2+  BoolSpecNeg spec             -> boolSpecNames spec+  BoolSpecAnd spec1 spec2      -> boolSpecNames spec1 ++ boolSpecNames spec2+  BoolSpecOr  spec1 spec2      -> boolSpecNames spec1 ++ boolSpecNames spec2+  BoolSpecXor spec1 spec2      -> boolSpecNames spec1 ++ boolSpecNames spec2+  BoolSpecImplies spec1 spec2  -> boolSpecNames spec1 ++ boolSpecNames spec2+  BoolSpecEquivs spec1 spec2   -> boolSpecNames spec1 ++ boolSpecNames spec2+  BoolSpecOp1 _op spec         -> boolSpecNames spec+  BoolSpecOp2 spec1 _op2 spec2 -> boolSpecNames spec1 ++ boolSpecNames spec2++-- | Return all identifiers used in a numeric expression.+numExprNames :: NumExpr -> [String]+numExprNames numExpr = case numExpr of+  NumId (Ident i)         -> [i]+  NumConstI _c            -> []+  NumConstD _c            -> []+  NumAdd expr1 _op expr2  -> numExprNames expr1 ++ numExprNames expr2+  NumMult expr1 _op expr2 -> numExprNames expr1 ++ numExprNames expr2
+ templates/copilot-cfs/CMakeLists.txt view
@@ -0,0 +1,16 @@+cmake_minimum_required(VERSION 2.6.4)+project(CFE_SAMPLE_APP C)++include_directories(../../Modules/Core/Interfaces)+include_directories(../Icarouslib/fsw/platform_inc)+include_directories(../inc)+include_directories(fsw/mission_inc)+include_directories(fsw/platform_inc)++aux_source_directory(fsw/src APP_SRC_FILES)++# Create the app module+add_cfe_app(copilot_cfs ${APP_SRC_FILES})++add_custom_target(HASKELL_COPILOT COMMAND cabal v1-sandbox init COMMAND cabal update COMMAND cabal v1-install copilot COMMAND cabal v1-exec "--" ghc --make Properties.hs COMMAND ./Properties WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}/fsw/src/ SOURCES ${CMAKE_CURRENT_SOURCE_DIR}/fsw/src/Properties.hs)+add_dependencies(copilot_cfs HASKELL_COPILOT)
+ templates/copilot-cfs/fsw/for_build/Makefile view
@@ -0,0 +1,112 @@+###############################################################################+# File: CFS Application Makefile +#+# $Id: Makefile 1.8 2009/07/09 12:25:54EDT rmcgraw Exp  $+#+# $Log: Makefile  $+# Revision 1.8 2009/07/09 12:25:54EDT rmcgraw +# DCR8291:1 Changed CFE_MISSION_INC to CFS_MISSION_INC and added log+#+###############################################################################+#+# Subsystem produced by this makefile.+#+APPTARGET = copilot_cfs++# +# Entry Point for task+# +ENTRY_PT = COPILOT_CFSMain++#+# Object files required to build subsystem.+#+OBJS = copilot_cfs.o++#+# Source files required to build subsystem; used to generate dependencies.+# As long as there are no assembly files this can be automated.+#+SOURCES = $(OBJS:.o=.c)+++##+## Specify extra C Flags needed to build this subsystem+##+LOCAL_COPTS = +++##+## EXEDIR is defined here, just in case it needs to be different for a custom+## build+##+EXEDIR=../exe++##+## Certain OSs and Application Loaders require the following option for+## Shared libraries. Currently only needed for vxWorks 5.5 and RTEMS.+## For each shared library that this app depends on, you need to have an+## entry like the following:+##  -R../tst_lib/tst_lib.elf+##+SHARED_LIB_LINK = ++########################################################################+# Should not have to change below this line, except for customized +# Mission and cFE directory structures+########################################################################++#+# Set build type to CFE_APP. This allows us to +# define different compiler flags for the cFE Core and Apps.+# +BUILD_TYPE = CFE_APP++## +## Include all necessary cFE make rules+## Any of these can be copied to a local file and +## changed if needed.+##+##+##       cfe-config.mak contains PSP and OS selection+##+include ../cfe/cfe-config.mak+##+##       debug-opts.mak contains debug switches+##+include ../cfe/debug-opts.mak+##+##       compiler-opts.mak contains compiler definitions and switches/defines+##+include $(CFE_PSP_SRC)/$(PSP)/make/compiler-opts.mak++##+## Setup the include path for this subsystem+## The OS specific includes are in the build-rules.make file+##+## If this subsystem needs include files from another app, add the path here.+##+INCLUDE_PATH = \+-I$(OSAL_SRC)/inc \+-I$(CFE_CORE_SRC)/inc \+-I$(CFE_PSP_SRC)/inc \+-I$(CFE_PSP_SRC)/$(PSP)/inc \+-I$(CFS_APP_SRC)/inc \+-I$(CFS_APP_SRC)/$(APPTARGET)/fsw/src \+-I$(CFS_MISSION_INC) \+-I../cfe/inc \+-I../inc++##+## Define the VPATH make variable. +## This can be modified to include source from another directory.+## If there is no corresponding app in the cfs-apps directory, then this can be discarded, or+## if the mission chooses to put the src in another directory such as "src", then that can be +## added here as well.+##+VPATH = $(CFS_APP_SRC)/$(APPTARGET)/fsw/src ++##+## Include the common make rules for building a cFE Application+##+include $(CFE_CORE_SRC)/make/app-rules.mak
+ templates/copilot-cfs/fsw/mission_inc/copilot_cfs_perfids.h view
@@ -0,0 +1,21 @@+/************************************************************************+** File:+**   $Id: copilot_cfs_perfids.h  $+**+** Purpose: +**  Define Sample App Performance IDs+**+** Notes:+**+*************************************************************************/+#ifndef _copilot_cfs_perfids_h_+#define _copilot_cfs_perfids_h_+++#define COPILOT_CFS_PERF_ID              91 ++#endif /* _copilot_cfs_perfids_h_ */++/************************/+/*  End of File Comment */+/************************/
+ templates/copilot-cfs/fsw/platform_inc/copilot_cfs_msgids.h view
@@ -0,0 +1,23 @@+/************************************************************************+** File:+**   $Id: copilot_cfs_msgids.h  $+**+** Purpose: +**  Define Sample App  Message IDs+**+** Notes:+**+**+*************************************************************************/+#ifndef _copilot_cfs_msgids_h_+#define _copilot_cfs_msgids_h_++#define COPILOT_CFS_CMD_MID            	0x1882+#define COPILOT_CFS_SEND_HK_MID        	0x1883+#define COPILOT_CFS_HK_TLM_MID		0x0883++#endif /* _copilot_cfs_msgids_h_ */++/************************/+/*  End of File Comment */+/************************/
+ templates/copilot-cfs/fsw/src/Properties.hs view
@@ -0,0 +1,64 @@+{-# LANGUAGE DataKinds #-}++import Language.Copilot+import Copilot.Compile.C99++import Prelude hiding ((>), (<), div, (++))++position :: Stream Position+position = extern "my_position" Nothing++-- | Position information received from cFS application.++-- We hardcode 16 as the length of the array for the field TmlHeader because+-- the Haskell compiler does not accept using an identifier (e.g.,+-- tmlHeaderSize) for array lengths.+data Position = Position+  { tlmHeader   :: Field "TlmHeader" (Array 16 Word8)+  , aircraft_id :: Field "aircraft_id" Word32+  , time_gps    :: Field "time_gps" Double+  , time_boot   :: Field "time_boot" Double+  , latitute    :: Field "latitude"  Double+  , longitude   :: Field "longitude" Double+  , altitude_abs :: Field "altitude_abs" Double+  , altitude_rel :: Field "altitude_rel" Double+  , vn :: Field "vn" Double+  , ve :: Field "ve" Double+  , vd :: Field "vd" Double+  , hdg :: Field "hdg" Double+  , hdop :: Field "hdop" Word16+  , vdop :: Field "vdop" Word16+  , numSats :: Field "numSats" Int64+  }++instance Struct Position where+  typename _ = "position_t"  -- Name of the type in C++  -- Function to translate Vec to list of Value's, order should match struct.+  toValues v = [ Value (Array Word8) (tlmHeader v)+               , Value Word32 (aircraft_id v)+               , Value Double (time_gps    v)+               , Value Double (time_boot   v)+               , Value Double (latitute    v)+               , Value Double (longitude   v)+               , Value Double (altitude_abs v)+               , Value Double (altitude_rel v)+               , Value Double (vn v)+               , Value Double (ve v)+               , Value Double (vd v)+               , Value Double (hdg v)+               , Value Word16 (hdop v)+               , Value Word16 (vdop v)+               , Value Int64 (numSats v)+               ]++-- We need to provide an instance to Typed with a bogus Vec+instance Typed Position where+  typeOf = Struct (Position (Field $ array []) (Field 0) (Field 0) (Field 0) (Field 0) (Field 0) (Field 0) (Field 0) (Field 0) (Field 0) (Field 0) (Field 0) (Field 0) (Field 0) (Field 0))++spec = do+  -- Trigger that always executes, splits the vec into seperate args.+  -- trigger "split" true [arg $ vecs # x, arg $ vecs # y]+  trigger "split" (position # vn > 10) []++main = reify spec >>= compile "position"
+ templates/copilot-cfs/fsw/src/copilot_cfs.c view
@@ -0,0 +1,161 @@+/*******************************************************************************+** File: copilot_cfs.c+**+** Purpose:+**   This file contains the source code for the Sample 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"++position_t my_position;+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() -- Application 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");+    CFE_SB_Subscribe(ICAROUS_POSITION_MID, COPILOT_CommandPipe);++    CFE_EVS_SendEvent (COPILOT_STARTUP_INF_EID, CFE_EVS_INFORMATION,+               "COPILOT App Initialized. Version %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)+    {+        case ICAROUS_POSITION_MID:+            COPILOT_ProcessIcarousPosition();+            break;+        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 */++/**+ * 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();+}++/**+ * Report copilot property violations.+ */+void split(void) {+    CFE_EVS_SendEvent(COPILOT_COMMANDCPVIOL_INF_EID, CFE_EVS_ERROR,+        "COPILOT: violation");+}
+ templates/copilot-cfs/fsw/src/copilot_cfs.h view
@@ -0,0 +1,49 @@+/*******************************************************************************+** File: copilot_app.h+**+** Purpose:+**   This file is main hdr file for the COPILOT application.+**+**+*******************************************************************************/++#ifndef _copilot_app_h_+#define _copilot_app_h_++/*+** Required header files.+*/+#include "cfe.h"+#include "cfe_error.h"+#include "cfe_evs.h"+#include "cfe_sb.h"+#include "cfe_es.h"++#include <string.h>+#include <errno.h>+#include <unistd.h>++/***********************************************************************/++#define COPILOT_PIPE_DEPTH                     32++/************************************************************************+** Type Definitions+*************************************************************************/++/****************************************************************************/+/*+** Local function prototypes.+**+** Note: Except for the entry point (COPILOT_AppMain), these+**       functions are not called from any other source module.+*/+void COPILOT_AppMain(void);+void COPILOT_AppInit(void);+void COPILOT_ProcessCommandPacket(void);+void COPILOT_ProcessIcarousPosition(void);+void COPILOT_ResetCounters(void);++boolean COPILOT_VerifyCmdLength(CFE_SB_MsgPtr_t msg, uint16 ExpectedLength);++#endif /* _copilot_app_h_ */
+ templates/copilot-cfs/fsw/src/copilot_cfs_events.h view
@@ -0,0 +1,27 @@+/************************************************************************+** File:+**    copilot_app_events.h +**+** Purpose: +**  Define COPILOT App Events IDs+**+** Notes:+**+**+*************************************************************************/+#ifndef _copilot_app_events_h_+#define _copilot_app_events_h_+++#define COPILOT_RESERVED_EID                0+#define COPILOT_STARTUP_INF_EID             1 +#define COPILOT_COMMAND_ERR_EID             2+#define COPILOT_COMMANDCPVIOL_INF_EID       3+#define COPILOT_INVALID_MSGID_ERR_EID       4 +#define COPILOT_LEN_ERR_EID                 5 ++#endif /* _copilot_app_events_h_ */++/************************/+/*  End of File Comment */+/************************/
+ templates/copilot-cfs/fsw/src/copilot_cfs_msg.h view
@@ -0,0 +1,42 @@+/*******************************************************************************+** File:+**   copilot_cfs_msg.h +**+** Purpose: +**  Define COPILOT App  Messages and info+**+** Notes:+**+**+*******************************************************************************/+#ifndef _copilot_cfs_msg_h_+#define _copilot_cfs_msg_h_++/*************************************************************************/+/*+** Type definition (generic "no arguments" command)+*/+typedef struct+{+   uint8    CmdHeader[CFE_SB_CMD_HDR_SIZE];++} COPILOT_NoArgsCmd_t;++/*************************************************************************/+/*+** Type definition (COPILOT App housekeeping)+*/+typedef struct +{+    uint8              TlmHeader[CFE_SB_TLM_HDR_SIZE];+    uint8              copilot_command_error_count;+    uint8              copilot_command_count;+    uint8              spare[2];++}   OS_PACK copilot_hk_tlm_t  ;++#endif /* _copilot_cfs_msg_h_ */++/************************/+/*  End of File Comment */+/************************/
+ templates/copilot-cfs/fsw/src/copilot_cfs_version.h view
@@ -0,0 +1,24 @@+/************************************************************************+** File:+**   $Id: copilot_app_version.h  $+**+** Purpose: +**  The Sample Application header file containing version number+**+** Notes:+**+**+*************************************************************************/+#ifndef _copilot_app_version_h_+#define _copilot_app_version_h_++#define COPILOT_CFS_MAJOR_VERSION    1+#define COPILOT_CFS_MINOR_VERSION    0+#define COPILOT_CFS_REVISION         0+#define COPILOT_CFS_MISSION_REV      0+      +#endif /* _copilot_app_version_h_ */++/************************/+/*  End of File Comment */+/************************/
+ tests/Main.hs view
@@ -0,0 +1,152 @@+-- | Test ogma-core+module Main where++import Data.Monoid                    ( mempty )+import Test.Framework                 ( Test, defaultMainWithOpts )+import Test.Framework.Providers.HUnit ( testCase )+import Test.HUnit                     ( assertBool )++-- Internal imports+import Command.CStructs2Copilot          ( cstructs2Copilot )+import Command.FRETComponentSpec2Copilot ( FRETComponentSpec2CopilotOptions (..)+                                         , fretComponentSpec2Copilot+                                         )+import Command.FRETReqsDB2Copilot        ( FRETReqsDB2CopilotOptions (..)+                                         , fretReqsDB2Copilot+                                         )+import Command.Result                    ( isSuccess )++-- | Run all unit tests on ogma-core.+main :: IO ()+main =+  defaultMainWithOpts tests mempty++-- | All unit tests for ogma-core.+tests :: [Test.Framework.Test]+tests =+  [+    testCase "fret-cmd-fret-cs-ok"+      (testFretComponentSpec2Copilot "tests/fret_good.json" True)+    -- Should pass++  , testCase "fret-cmd-fret-file-not-found"+      (testFretComponentSpec2Copilot "tests/file-invalid.json" False)+    -- Should fail because the file does not exist++  , testCase "fret-cmd-fret-parse-fail-1"+      (testFretComponentSpec2Copilot+         "tests/commands-fret-error-parsing-failed-1.json"+         False+      )+    -- Should fail because the opening bracket is [ and not {++  , testCase "fret-cmd-fret-parse-fail-2"+      (testFretComponentSpec2Copilot+         "tests/commands-fret-error-parsing-failed-2.json"+         False+      )+    -- Should fail because a field is missing in an external variable++  , testCase "fret-cmd-fret-parse-fail-3"+      (testFretComponentSpec2Copilot+         "tests/commands-fret-error-parsing-failed-3.json"+         False+      )+    -- Should fail because a field is missing in an internal variable++  , testCase "fret-reqs-db-cocospec"+      (testFretReqsDBCoCoSpec2Copilot "tests/fret-example1.json" True)+    -- Should pass++  , testCase "structs-parse-ok"+      (testCStructs2Copilot "tests/reduced_geofence_msgs.h" True)+    -- Should pass++  , testCase "structs-parse-fail-1"+      (testCStructs2Copilot "tests/reduced_geofence_msgs_bad.h" False)+    -- Should fail because a keyword is incorrect+  ]++-- | Test C struct parser and conversion to Copilot structs+-- for a particular file.+--+-- This test uses the Copilot backend for C header files, so it generates+-- Copilot types and instances.+--+-- This IO action fails if any of the following are true:+--   * The given file is not found or accessible.+--   * The format in the given file is incorrect.+--   * Ogma fails due to an internal error or bug.+--+testCStructs2Copilot :: FilePath  -- ^ Path to a C header file with structs+                     -> Bool+                     -> IO ()+testCStructs2Copilot file success = do+    result <- cstructs2Copilot file++    -- True if success is expected and detected, or niether expected nor+    -- detected.+    let testPass = success == isSuccess result++    assertBool errorMsg testPass+  where+    errorMsg = "The result of the transformation of the C header file "+               ++ file ++ " to Copilot struct declarations was unexpected."++-- | Test FRET Component Spec 2 Copilot transformation.+--+-- This test uses the Copilot backend for FRET files, so it generates a Copilot+-- file.+--+-- This IO action fails if any of the following are true:+--   * The given file is not found or accessible.+--   * The format in the given file is incorrect.+--   * Ogma fails due to an internal error or bug.+testFretComponentSpec2Copilot :: FilePath  -- ^ Path to a FRET/JSON requirements file+                              -> Bool+                              -> IO ()+testFretComponentSpec2Copilot file success = do+    let opts = FRETComponentSpec2CopilotOptions+                 { fretCS2CopilotUseCoCoSpec = False+                 , fretCS2CopilotIntType     = "Int64"+                 , fretCS2CopilotRealType    = "Float"+                 }+    result <- fretComponentSpec2Copilot file opts++    -- True if success is expected and detected, or niether expected nor+    -- detected.+    let testPass = success == isSuccess result++    assertBool errorMsg testPass+  where+    errorMsg = "The result of the transformation of FRET CS file "+               ++ file ++ " to Copilot was unexpected."++-- | Test FRET Component Spec 2 Copilot transformation.+--+-- This test uses the Copilot backend for FRET files with the CoCoSpec+-- frontend.+--+-- This IO action fails if any of the following are true:+--   * The given file is not found or accessible.+--   * The format in the given file is incorrect.+--   * Ogma fails due to an internal error or bug.+--+testFretReqsDBCoCoSpec2Copilot :: FilePath  -- ^ Path to a FRET/JSON+                                            --   requirements file+                               -> Bool+                               -> IO ()+testFretReqsDBCoCoSpec2Copilot file success = do+    let opts = FRETReqsDB2CopilotOptions+                 { fretReqsDB2CopilotUseCoCoSpec = True+                 }+    result <- fretReqsDB2Copilot file opts++    -- True if success is expected and detected, or niether expected nor+    -- detected.+    let testPass = success == isSuccess result++    assertBool errorMsg testPass+  where+    errorMsg = "The result of the transformation of FRET CS file "+               ++ file ++ " to Copilot was unexpected."