ogma-core 1.12.0 → 1.13.0
raw patch · 30 files changed
+1029/−671 lines, 30 filesdep +copilot-coredep +copilot-languagedep +copilot-theoremdep ~ogma-extradep ~ogma-language-cdep ~ogma-language-copilotPVP ok
version bump matches the API change (PVP)
Dependencies added: copilot-core, copilot-language, copilot-theorem, hint
Dependency ranges changed: ogma-extra, ogma-language-c, ogma-language-copilot, ogma-language-csv, ogma-language-jsonspec, ogma-language-lustre, ogma-language-smv, ogma-language-xlsx, ogma-language-xmlspec, ogma-spec
API changes (from Hackage documentation)
+ Command.Overview: [commandRequirementsConsistent] :: CommandSummary -> Bool
+ Command.Overview: [commandRequirementsFalse] :: CommandSummary -> Int
+ Command.Overview: [commandRequirementsTrue] :: CommandSummary -> Int
- Command.Overview: CommandSummary :: Int -> Int -> Int -> CommandSummary
+ Command.Overview: CommandSummary :: Int -> Int -> Int -> Int -> Int -> Bool -> CommandSummary
Files
- CHANGELOG.md +9/−0
- ogma-core.cabal +27/−21
- src/Command/CFSApp.hs +1/−1
- src/Command/Diagram.hs +10/−12
- src/Command/Overview.hs +33/−17
- src/Language/Trans/SpecAnalysis.hs +312/−0
- templates/cfs/Dockerfile +38/−0
- templates/cfs/copilot/CMakeLists.txt +48/−0
- templates/cfs/copilot/fsw/for_build/Makefile +112/−0
- templates/cfs/copilot/fsw/mission_inc/copilot_cfs_perfids.h +21/−0
- templates/cfs/copilot/fsw/platform_inc/copilot_cfs_msgids.h +23/−0
- templates/cfs/copilot/fsw/src/Properties.hs +50/−0
- templates/cfs/copilot/fsw/src/copilot_cfs.c +195/−0
- templates/cfs/copilot/fsw/src/copilot_cfs.h +51/−0
- templates/cfs/copilot/fsw/src/copilot_cfs_events.h +27/−0
- templates/cfs/copilot/fsw/src/copilot_cfs_msg.h +42/−0
- templates/cfs/copilot/fsw/src/copilot_cfs_version.h +24/−0
- templates/copilot-cfs/CMakeLists.txt +0/−48
- templates/copilot-cfs/fsw/for_build/Makefile +0/−112
- templates/copilot-cfs/fsw/mission_inc/copilot_cfs_perfids.h +0/−21
- templates/copilot-cfs/fsw/platform_inc/copilot_cfs_msgids.h +0/−23
- templates/copilot-cfs/fsw/src/Properties.hs +0/−47
- templates/copilot-cfs/fsw/src/copilot_cfs.c +0/−195
- templates/copilot-cfs/fsw/src/copilot_cfs.h +0/−51
- templates/copilot-cfs/fsw/src/copilot_cfs_events.h +0/−27
- templates/copilot-cfs/fsw/src/copilot_cfs_msg.h +0/−42
- templates/copilot-cfs/fsw/src/copilot_cfs_version.h +0/−24
- templates/diagram/Copilot.hs +0/−30
- templates/ros/copilot/src/Copilot.hs +3/−0
- templates/standalone/Copilot.hs +3/−0
CHANGELOG.md view
@@ -1,5 +1,14 @@ # Revision history for ogma-core +## [1.13.0] - 2026-03-21++* Version bump (1.13.0) (#373).+* Remove unused functions from diagram template (#351).+* Add dockerfile to cFS template (#353).+* Augment overview command to formally analyze specs (#356).+* Augment overview command to determine consistency of specs (#366).+* Expand extra definitions in Copilot specs in templates (#368).+ ## [1.12.0] - 2026-01-21 * Version bump 1.12.0 (#336).
ogma-core.cabal view
@@ -19,7 +19,7 @@ build-type: Simple name: ogma-core-version: 1.12.0+version: 1.13.0 homepage: https://github.com/nasa/ogma bug-reports: https://github.com/nasa/ogma/issues license: Apache-2.0@@ -45,16 +45,17 @@ . 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+data-files: templates/cfs/Dockerfile+ templates/cfs/copilot/CMakeLists.txt+ templates/cfs/copilot/fsw/for_build/Makefile+ templates/cfs/copilot/fsw/mission_inc/copilot_cfs_perfids.h+ templates/cfs/copilot/fsw/platform_inc/copilot_cfs_msgids.h+ templates/cfs/copilot/fsw/src/Properties.hs+ templates/cfs/copilot/fsw/src/copilot_cfs_msg.h+ templates/cfs/copilot/fsw/src/copilot_cfs.c+ templates/cfs/copilot/fsw/src/copilot_cfs_version.h+ templates/cfs/copilot/fsw/src/copilot_cfs.h+ templates/cfs/copilot/fsw/src/copilot_cfs_events.h templates/ros/Dockerfile templates/ros/screenrc templates/ros/copilot/CMakeLists.txt@@ -122,6 +123,7 @@ Command.Common Command.Errors Command.VariableDB+ Language.Trans.SpecAnalysis autogen-modules: Paths_ogma_core@@ -131,24 +133,28 @@ , aeson >= 2.0.0.0 && < 2.3 , bytestring >= 0.10.8.2 && < 0.13 , containers >= 0.5 && < 0.8+ , copilot-core >= 4.6.1 && < 4.7+ , copilot-language >= 4.6.1 && < 4.7+ , copilot-theorem >= 4.6.1 && < 4.7 , directory >= 1.3.1.5 && < 1.4 , filepath >= 1.4.2 && < 1.6 , graphviz >= 2999.20 && < 2999.21+ , hint >= 0.9.0 && < 1.10 , megaparsec >= 8.0.0 && < 9.10 , mtl >= 2.2.2 && < 2.4 , process >= 1.6 && < 1.7 , text >= 1.2.3.1 && < 2.2 - , ogma-extra >= 1.12.0 && < 1.13- , ogma-language-c >= 1.12.0 && < 1.13- , ogma-language-copilot >= 1.12.0 && < 1.13- , ogma-language-csv >= 1.12.0 && < 1.13- , ogma-language-jsonspec >= 1.12.0 && < 1.13- , ogma-language-lustre >= 1.12.0 && < 1.13- , ogma-language-smv >= 1.12.0 && < 1.13- , ogma-language-xlsx >= 1.12.0 && < 1.13- , ogma-language-xmlspec >= 1.12.0 && < 1.13- , ogma-spec >= 1.12.0 && < 1.13+ , ogma-extra >= 1.13.0 && < 1.14+ , ogma-language-c >= 1.13.0 && < 1.14+ , ogma-language-copilot >= 1.13.0 && < 1.14+ , ogma-language-csv >= 1.13.0 && < 1.14+ , ogma-language-jsonspec >= 1.13.0 && < 1.14+ , ogma-language-lustre >= 1.13.0 && < 1.14+ , ogma-language-smv >= 1.13.0 && < 1.14+ , ogma-language-xlsx >= 1.13.0 && < 1.14+ , ogma-language-xmlspec >= 1.13.0 && < 1.14+ , ogma-spec >= 1.13.0 && < 1.14 hs-source-dirs: src
src/Command/CFSApp.hs view
@@ -65,7 +65,7 @@ -> IO (Result ErrorCode) command options = processResult $ do -- Obtain template dir- templateDir <- locateTemplateDir mTemplateDir "copilot-cfs"+ templateDir <- locateTemplateDir mTemplateDir "cfs" templateVars <- parseTemplateVarsFile templateVarsF
src/Command/Diagram.hs view
@@ -91,12 +91,11 @@ -- -- PRE: The file given is readable, contains a valid file with recognizable -- format, the formulas in the file do not use any identifiers that exist in--- Copilot, or any of @stateMachine@, @externalState@, @noneOf@,--- @checkValidTransitions@, @main@, @spec@, @stateMachine1@, @clock@, @ftp@,--- @notPreviousNot@. All identifiers used are valid C99 identifiers. The--- template, if provided, exists and uses the variables needed by the diagram--- application generator. The target directory is writable and there's enough--- disk space to copy the files over.+-- Copilot, or any of @stateMachine@, @externalState@, @main@, @spec@,+-- @stateMachine1@, @clock@, @ftp@, @notPreviousNot@. All identifiers used are+-- valid C99 identifiers. The template, if provided, exists and uses the+-- variables needed by the diagram application generator. The target directory+-- is writable and there's enough disk space to copy the files over. diagram :: FilePath -- ^ Path to a file containing a diagram -> DiagramOptions -- ^ Customization options -> IO (Result ErrorCode)@@ -138,12 +137,11 @@ -- -- PRE: The file given is readable, contains a valid file with recognizable -- format, the formulas in the file do not use any identifiers that exist in--- Copilot, or any of @stateMachine@, @externalState@, @noneOf@,--- @checkValidTransitions@, @main@, @spec@, @stateMachine1@, @clock@, @ftp@,--- @notPreviousNot@. All identifiers used are valid C99 identifiers. The--- template, if provided, exists and uses the variables needed by the diagram--- application generator. The target directory is writable and there's enough--- disk space to copy the files over.+-- Copilot, or any of @stateMachine@, @externalState@, @main@, @spec@,+-- @stateMachine1@, @clock@, @ftp@, @notPreviousNot@. All identifiers used are+-- valid C99 identifiers. The template, if provided, exists and uses the+-- variables needed by the diagram application generator. The target directory+-- is writable and there's enough disk space to copy the files over. diagram' :: FilePath -> DiagramOptions -> ExprPair
src/Command/Overview.hs view
@@ -39,11 +39,12 @@ Requirement (..), Spec (..)) -- Internal imports-import Command.Common-import Command.Errors (ErrorCode, ErrorTriplet(..))-import Command.Result (Result (..))-import Data.Location (Location (..))-import Language.Trans.Spec2Copilot (specAnalyze)+import Command.Common+import Command.Errors (ErrorCode, ErrorTriplet (..))+import Command.Result (Result (..))+import Data.Location (Location (..))+import qualified Language.Trans.Spec2Copilot as Spec2Copilot+import qualified Language.Trans.SpecAnalysis as SpecAnalysis -- | Generate overview of a spec given in an input file. --@@ -77,16 +78,28 @@ -> IO (Either String CommandSummary) command' fp options (ExprPair exprT) = do spec <- runExceptT $ parseInputFile' fp- let spec' = either (\(ErrorTriplet _ec msg _loc) -> Left msg) Right spec+ case spec of+ Left (ErrorTriplet _ec msg _loc) -> return $ Left msg - let summary = do- spec1 <- spec'- spec3 <- specAnalyze $ addMissingIdentifiers ids spec1- return $ CommandSummary (length (externalVariables spec3))- (length (internalVariables spec3))- (length (requirements spec3))- return summary+ Right spec' -> do+ let specCompleted = addMissingIdentifiers ids spec'+ specAnalyzed = Spec2Copilot.specAnalyze specCompleted + specFormalAnalysis <-+ SpecAnalysis.specAnalyze [] replace printExpr specCompleted++ pure $ do+ numExterns <- length . externalVariables <$> specAnalyzed+ numInternal <- length . internalVariables <$> specAnalyzed+ numReqs <- length . requirements <$> specAnalyzed+ numTrues <- SpecAnalysis.numAlwaysTrue <$> specFormalAnalysis+ numFalses <- SpecAnalysis.numAlwaysFalse <$> specFormalAnalysis+ consistent <- SpecAnalysis.consistent <$> specFormalAnalysis++ pure $+ CommandSummary+ numExterns numInternal numReqs numTrues numFalses consistent+ where parseInputFile' f = parseInputFile f formatName propFormatName propVia exprT@@ -94,12 +107,15 @@ propFormatName = commandPropFormat options propVia = commandPropVia options - ExprPairT _parse _replace _print ids _def = exprT+ ExprPairT _parse replace printExpr ids _def = exprT data CommandSummary = CommandSummary- { commandExternalVariables :: Int- , commandInternalVariables :: Int- , commandRequirements :: Int+ { commandExternalVariables :: Int+ , commandInternalVariables :: Int+ , commandRequirements :: Int+ , commandRequirementsTrue :: Int+ , commandRequirementsFalse :: Int+ , commandRequirementsConsistent :: Bool } deriving (Generic, Show)
+ src/Language/Trans/SpecAnalysis.hs view
@@ -0,0 +1,312 @@+-- Copyright 2024 United States Government as represented by the Administrator+-- of the National Aeronautics and Space Administration. All Rights Reserved.+--+-- Disclaimers+--+-- Licensed under the Apache License, Version 2.0 (the "License"); you may+-- not use this file except in compliance with the License. You may obtain a+-- copy of the License at+--+-- https://www.apache.org/licenses/LICENSE-2.0+--+-- Unless required by applicable law or agreed to in writing, software+-- distributed under the License is distributed on an "AS IS" BASIS, WITHOUT+-- WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the+-- License for the specific language governing permissions and limitations+-- under the License.++-- | Formally analyze specifications and provide information about them.+module Language.Trans.SpecAnalysis+ ( AnalysisResult(..)+ , specAnalyze+ )+ where++-- External imports+import qualified Copilot.Core as Core+import qualified Copilot.Language as Copilot+import qualified Copilot.Language.Reify as Copilot+import Copilot.Theorem.What4 (SatResult (..), Solver (Z3),+ prove)+import Data.List (intercalate, lookup)+import Data.Maybe (fromMaybe)+import qualified Language.Haskell.Interpreter as HI++-- External imports: auxiliary+import Data.String.Extra (sanitizeLCIdentifier, sanitizeUCIdentifier)++-- External imports: ogma-spec+import Data.OgmaSpec (ExternalVariableDef (..), InternalVariableDef (..),+ Requirement (..), Spec (..))++-- * Analysis of Specs++-- | Result of analyzing a specification.+data AnalysisResult = AnalysisResult+ { numAlwaysTrue :: Int -- ^ Number of always true requirements.+ , numAlwaysFalse :: Int -- ^ Number of always false requirements.+ , consistent :: Bool -- ^ Whether requirements are mutually consistent.+ }++-- | Formally analyze a specification for redundancies, conflicts, etc.+specAnalyze :: [(String, String)] -- Type substitution table+ -> ([(String, String)] -> a -> a) -- Expr substitution function+ -> (a -> String) -- Expr show function+ -> Spec a -- Specification+ -> IO (Either String AnalysisResult)+specAnalyze typeMaps exprTransform showExpr spec = do+ let structuredSpec =+ spec2Copilot typeMaps exprTransform showExpr spec++ coreSpec <- reifySpec defaultSpecImports $ showSpec structuredSpec++ let properties = zip propertyNames propertyGuards+ propertyNames = map (\(_, p, _, _, _) -> p)+ $ copilotProperties structuredSpec+ propertyGuards = map Core.triggerGuard $ Core.specTriggers coreSpec++ constantProperties <- mapM (uncurry $ exprIsConstant coreSpec) properties++ let numTrue = length $ filter fst constantProperties+ numFalse = length $ filter snd constantProperties++ let negatedConjunction = Core.Op1 Core.Not+ $ foldr (Core.Op2 Core.And) true propertyGuards+ true = Core.Const Core.Bool True++ provedNegatedConjunction <-+ exprIsConstant coreSpec "ogma_inc" negatedConjunction++ -- The requirements are considered consistent if it was *not* possible to+ -- prove that their conjunction is always false.+ let consistent = not $ fst provedNegatedConjunction++ return $ Right $ AnalysisResult numTrue numFalse consistent++-- * Auxiliary++-- ** Structured Copilot specifications++-- | A structured Copilot specification.+data CopilotSpec = CopilotSpec+ { copilotProperties :: [(String, String, String, String, String)]+ -- ^ Requirement name, property name, handler name,+ -- implementation and arguments.++ , copilotAuxDefs :: [(String, String, String)]+ -- ^ Name, type, implementation+ }++-- | Given a 'Spec', return a structured version the corresponding Copilot spec+-- that differentiates between the auxiliary definitions (inputs, outputs) and+-- the properties or requirements to check.+--+-- PRE: There are no name clashes between the variables and names used in the+-- specification and any definitions in Haskell's Prelude or in Copilot.+spec2Copilot :: [(String, String)] -- Type substitution table+ -> ([(String, String)] -> a -> a) -- Expr substitution function+ -> (a -> String) -- Expr show function+ -> Spec a -- Specification+ -> CopilotSpec+spec2Copilot typeMaps exprTransform showExpr spec = CopilotSpec reqs auxDefs+ where+ -- Encoding of requirements as boolean streams+ reqs :: [(String, String, String, String, String)]+ reqs = map reqToDecl (requirements spec)+ where+ reqToDecl i =+ ( reqName+ , propName+ , handlerName+ , reqBody nameSubstitutions+ , handlerArg+ )+ where+ reqName = requirementName i++ propName = safeMap nameSubstitutions (requirementName i)++ handlerName = "handler" ++ sanitizeUCIdentifier (requirementName i)++ -- Definition implementation. We use an auxiliary function to+ -- transform the implementation into Copilot, applying a+ -- substitution.+ reqBody subs = showExpr (exprTransform subs (requirementExpr i))++ handlerArg =+ case (requirementResultType i, requirementResultExpr i) of+ (Just _, Just ex) -> "[ arg (" ++ showExpr ex ++ " ) ]"+ _ -> "[]"++ auxDefs :: [(String, String, String)]+ auxDefs = externs ++ internals++ externs :: [(String, String, String)]+ externs = map externVarToDecl (externalVariables spec)+ where+ externVarToDecl i = (propName, streamType, implementation)+ where+ propName = safeMap nameSubstitutions (externalVariableName i)++ streamType = "Stream " ++ "(" ++ valueType ++ ")"+ valueType = safeMap typeMaps (externalVariableType i)++ implementation = "extern" ++ " " ++ show (externalVariableName i)+ ++ " " ++ "Nothing"++ -- Internal stream definitions+ internals :: [(String, String, String)]+ internals = map internalVarToDecl (internalVariables spec)+ where+ internalVarToDecl i = (propName, streamType, implementation)+ where+ propName = safeMap nameSubstitutions (internalVariableName i)++ streamType = "Stream " ++ "(" ++ valueType ++ ")"+ valueType = safeMap typeMaps (internalVariableType i)++ implementation = internalVariableExpr i++ nameSubstitutions = internalVariableMap+ ++ externalVariableMap+ ++ 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++ -- Variable/requirement names used in the input spec.+ internalVariableNames = map internalVariableName+ $ internalVariables spec++ externalVariableNames = map externalVariableName+ $ externalVariables spec++ requirementNames = map requirementName+ $ requirements spec++-- | Render a 'CopilotSpec' as a Haskell definition of a 'Copilot.Spec',+-- listing the elements in the spec with the necessary indentation.+--+-- The shown 'Copilot.Spec' has a list of top-level triggers, as well as+-- several auxiliary definitions.+showSpec :: CopilotSpec -> String+showSpec spec = template ++ "\n" ++ extra ++ "\n" ++ triggers+ where+ -- Initial template used for analysis purposes.+ template :: String+ template = unlines+ [ "do let"+ , ""+ , " clock :: Stream Int64"+ , " clock = [0] ++ (clock + 1)"+ , ""+ , " ftp :: Stream Bool"+ , " ftp = [True] ++ false"+ , ""+ , " pre :: Stream Bool -> Stream Bool"+ , " pre = ([False] ++)"+ , ""+ , " tpre :: Stream Bool -> Stream Bool"+ , " tpre = ([True] ++)"+ , ""+ , " notPreviousNot :: Stream Bool -> Stream Bool"+ , " notPreviousNot = not . PTLTL.previous . not"+ ]++ extra = unlines+ $ intercalate [""]+ $ map formatDef+ $ copilotAuxDefs spec++ triggers = unlines+ $ intercalate [""]+ $ map formatTrigger+ $ copilotProperties spec++ formatDef (n, t, i) =+ map (" " ++) [ n ++ " :: " ++ t, n ++ " = " ++ i ]++ formatTrigger (_, _, h, g, a) =+ map (" " ++) [ "trigger " ++ show h ++ " (" ++ g ++ ") " ++ a ]++-- | Default imports for a 'Spec' that was converted into a 'Copilot.Spec'.+defaultSpecImports :: [(String, Maybe String)]+defaultSpecImports =+ [ ("Control.Monad.Writer", Nothing)+ , ("Copilot.Language", Nothing)+ , ("Copilot.Language.Spec", Nothing)+ , ("Data.Functor.Identity", Nothing)+ , ("Language.Copilot", Nothing)+ , ("Copilot.Library.PTLTL", Just "PTLTL")+ , ("Prelude", Just "P")+ ]++-- ** Typechecking of Copilot specs++-- | Read a specification from a 'String' and reify it.+--+-- This function receives a list of possibly qualified imports.+reifySpec :: [(String, Maybe String)] -> String -> IO Core.Spec+reifySpec imports specText = do+ coreSpecE <- HI.runInterpreter $ do+ HI.setImportsQ imports+ copilotSpec <- HI.interpret specText (HI.as :: Copilot.Spec)+ HI.liftIO $ Copilot.reify copilotSpec++ case coreSpecE of+ Left err -> do putStrLn $ "Error: " ++ show err+ error $ show err++ Right coreSpec -> return coreSpec++-- ** Analysis of Copilot specs++-- | Determine if a boolean expression is always 'True' or always 'False'.+--+-- The first boolean in the result is 'True' if the expression can be proven+-- always 'True'. The second boolean in the expression is 'True' is the+-- expression can be proven always 'False'.+--+-- They values in the tuple cannot both 'True' at the same time.+exprIsConstant :: Core.Spec+ -> Core.Name+ -> Core.Expr Bool+ -> IO (Bool, Bool)+exprIsConstant spec name expr = do+ r1 <- propIsValid spec name (Core.Forall expr)+ r2 <- propIsValid spec name (Core.Forall (Core.Op1 Core.Not expr))+ pure (r1, r2)++-- | 'True' if the Copilot 'Prop' with the given name and expression is+-- constantly 'True', or valid, and 'False' otherwise (not always 'True' or+-- unknown).+propIsValid :: Core.Spec+ -> Core.Name+ -> Core.Prop+ -> IO Bool+propIsValid spec name expr =+ maybe False isValid . lookup name <$> prove Z3 spec'+ where+ spec' = spec { Core.specProperties = prop' : Core.specProperties spec }+ prop' = Core.Property name expr++ isValid :: SatResult -> Bool+ isValid Valid = True+ isValid _ = False++-- ** Auxiliary list functions++-- | Substitute a key based on a given substitution table from key to+-- alternative key.+--+-- They key is left unchanged if it cannot be found in the substitution table.+safeMap :: Eq k => [(k, k)] -> k -> k+safeMap ls k = fromMaybe k $ lookup k ls
+ templates/cfs/Dockerfile view
@@ -0,0 +1,38 @@+FROM ubuntu:22.04++RUN apt-get update+ENV DEBIAN_FRONTEND=noninteractive+RUN apt-get install --yes \+ alex \+ cabal-install \+ cmake \+ gcc-multilib \+ ghc \+ git \+ happy \+ libz-dev \+ pkg-config++ENV PATH="$HOME/.cabal/bin:$HOME/.ghcup/bin":$PATH++WORKDIR /root++# Obtain cFS+RUN git clone https://github.com/nasa/cfs.git cfs+WORKDIR /root/cfs+RUN git checkout v6.7.0a+RUN git submodule update --init --recursive++# Copy Copilot app with other cFS apps+ADD copilot /root/cfs/apps/copilot++# Copy default setup, list of CPUs and applications+RUN cp cfe/cmake/Makefile.sample Makefile+RUN cp -r cfe/cmake/sample_defs .++# Enable Ogma-generated cFS app in cFS+RUN sed -i -e 's/\(SET(TGT1_APPLIST.*\))/\1 copilot)/g' sample_defs/targets.cmake+RUN sed -i -e '0,/^!/s//CFE_APP, \/cf\/copilot_cfs.so, COPILOT_AppMain, COPILOT_APP, 50, 16384, 0x0, 0;\n&/' sample_defs/cpu1_cfe_es_startup.scr++RUN make SIMULATION=native prep+RUN make install
+ templates/cfs/copilot/CMakeLists.txt view
@@ -0,0 +1,48 @@+cmake_minimum_required(VERSION 2.6.4)+project(CFE_COPILOT_APP C)++include_directories(../../Modules/Core/Interfaces)+{{#included_libraries}}+include_directories({{{.}}})+{{/included_libraries}}+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}+ ${CMAKE_CURRENT_SOURCE_DIR}/fsw/src/copilot.c+ ${CMAKE_CURRENT_SOURCE_DIR}/fsw/src/copilot.h+ ${CMAKE_CURRENT_SOURCE_DIR}/fsw/src/copilot_types.h+)++add_custom_command(+ OUTPUT ${CMAKE_CURRENT_SOURCE_DIR}/fsw/src/cabal.sandbox.config+ WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}/fsw/src/+ COMMAND cabal v1-sandbox init+ COMMAND cabal update+ COMMAND cabal v1-install copilot+ COMMENT "Installing Copilot"+)++add_custom_command(+ DEPENDS ${CMAKE_CURRENT_SOURCE_DIR}/fsw/src/cabal.sandbox.config+ DEPENDS ${CMAKE_CURRENT_SOURCE_DIR}/fsw/src/Properties.hs+ OUTPUT ${CMAKE_CURRENT_SOURCE_DIR}/fsw/src/copilot.c+ ${CMAKE_CURRENT_SOURCE_DIR}/fsw/src/copilot.h+ ${CMAKE_CURRENT_SOURCE_DIR}/fsw/src/copilot_types.h+ WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}/fsw/src/+ COMMAND cabal v1-exec "--" runhaskell Properties.hs+ COMMENT "Compiling Copilot code"+)++add_custom_target(HASKELL_COPILOT+ DEPENDS ${CMAKE_CURRENT_SOURCE_DIR}/fsw/src/copilot.c+ ${CMAKE_CURRENT_SOURCE_DIR}/fsw/src/copilot.h+ ${CMAKE_CURRENT_SOURCE_DIR}/fsw/src/copilot_types.h+ SOURCES ${CMAKE_CURRENT_SOURCE_DIR}/fsw/src/Properties.hs+)+add_dependencies(copilot_cfs HASKELL_COPILOT)
+ templates/cfs/copilot/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/cfs/copilot/fsw/mission_inc/copilot_cfs_perfids.h view
@@ -0,0 +1,21 @@+/************************************************************************+** File:+** $Id: copilot_cfs_perfids.h $+**+** Purpose:+** Define Copilot 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/cfs/copilot/fsw/platform_inc/copilot_cfs_msgids.h view
@@ -0,0 +1,23 @@+/************************************************************************+** File:+** $Id: copilot_cfs_msgids.h $+**+** Purpose:+** Define Copilot 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/cfs/copilot/fsw/src/Properties.hs view
@@ -0,0 +1,50 @@+{{#copilot}}+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)++{{#copilot_extra_defs}}+{{{.}}}+{{/copilot_extra_defs}}+{{{copilot.externs}}}+{{{copilot.internals}}}+{{{copilot.reqs}}}++-- | Clock that increases in one-unit steps.+clock :: Stream Int64+clock = [0] ++ (clock + 1)++-- | First Time Point+ftp :: Stream Bool+ftp = [True] ++ false++pre :: Stream Bool -> Stream Bool+pre = ([False] ++)++tpre :: Stream Bool -> Stream Bool+tpre = ([True] ++)++notPreviousNot :: Stream Bool -> Stream Bool+notPreviousNot = not . PTLTL.previous . not++-- | Complete specification. Calls C handler functions when properties are+-- violated.+spec :: Spec+spec = do+{{{copilot.triggers}}}++main :: IO ()+main = reify spec >>= compileWith settings "{{{copilot.specName}}}"+ where+ settings = mkDefaultCSettings { cSettingsStepFunctionName = "copilot_step" }+{{/copilot}}+{{^copilot}}+-- No specification provided. Place your specification in this file.+{{/copilot}}
+ templates/cfs/copilot/fsw/src/copilot_cfs.c view
@@ -0,0 +1,195 @@+/*******************************************************************************+** File: copilot_cfs.c+**+** Purpose:+** This file contains the source code for the Copilot App.+**+*******************************************************************************/++/*+** Include Files:+*/++#include "copilot_cfs.h"+#include "copilot_cfs_perfids.h"+#include "copilot_cfs_msgids.h"+#include "copilot_cfs_msg.h"+#include "copilot_cfs_events.h"+#include "copilot_cfs_version.h"+{{#impl_extra_header}}+{{{.}}}+{{/impl_extra_header}}+{{#copilot}}+#include "{{{copilot.specName}}}_types.h"+#include "{{{copilot.specName}}}.h"+{{/copilot}}++{{#variables}}+{{varDeclType}} {{varDeclName}};+{{/variables}}++/*+** 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");+ {{#msgIds}}+ CFE_SB_Subscribe({{.}}, COPILOT_CommandPipe);+ {{/msgIds}}+++ 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)+ {+ {{#msgCases}}+ case {{msgInfoId}}:+ COPILOT_Process{{msgInfoDesc}}();+ break;++ {{/msgCases}}++ 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}}+/**+* Make received data available to Copilot and run monitors.+*/+void COPILOT_Process{{msgDataDesc}}(void)+{+ {{#msgDataFromType}}+ {{msgDataFromType}}* msg;+ msg = ({{.}}*) COPILOTMsgPtr;+ {{/msgDataFromType}}+ {{^msgDataFromType}}+ {{msgDataVarType}}* msg;+ msg = ({{msgDataVarType}}*) COPILOTMsgPtr;+ {{/msgDataFromType}}+ {{#msgDataFromField}}+ {{msgDataVarName}} = msg->{{.}};+ {{/msgDataFromField}}+ {{^msgDataFromField}}+ {{msgDataVarName}} = *msg;+ {{/msgDataFromField}}++ // Run all copilot monitors.+ copilot_step();+}++{{/msgHandlers}}+++{{#triggers}}+/**+ * Report copilot property violations.+ */+{{#triggerType}}+void {{triggerName}}({{.}} arg) {+{{/triggerType}}+{{^triggerType}}+void {{triggerName}}(void) {+{{/triggerType}}+ CFE_EVS_SendEvent(COPILOT_COMMANDCPVIOL_INF_EID, CFE_EVS_ERROR,+ "COPILOT: violation: {{triggerName}}");+}+{{/triggers}}
+ templates/cfs/copilot/fsw/src/copilot_cfs.h view
@@ -0,0 +1,51 @@+/*******************************************************************************+** 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);+{{#msgCases}}+void COPILOT_Process{{msgInfoDesc}}(void);+{{/msgCases}}+void COPILOT_ResetCounters(void);++boolean COPILOT_VerifyCmdLength(CFE_SB_MsgPtr_t msg, uint16 ExpectedLength);++#endif /* _copilot_app_h_ */
+ templates/cfs/copilot/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/cfs/copilot/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/cfs/copilot/fsw/src/copilot_cfs_version.h view
@@ -0,0 +1,24 @@+/************************************************************************+** File:+** $Id: copilot_app_version.h $+**+** Purpose:+** The Copilot 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 */+/************************/
− templates/copilot-cfs/CMakeLists.txt
@@ -1,48 +0,0 @@-cmake_minimum_required(VERSION 2.6.4)-project(CFE_COPILOT_APP C)--include_directories(../../Modules/Core/Interfaces)-{{#included_libraries}}-include_directories({{{.}}})-{{/included_libraries}}-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}- ${CMAKE_CURRENT_SOURCE_DIR}/fsw/src/copilot.c- ${CMAKE_CURRENT_SOURCE_DIR}/fsw/src/copilot.h- ${CMAKE_CURRENT_SOURCE_DIR}/fsw/src/copilot_types.h-)--add_custom_command(- OUTPUT ${CMAKE_CURRENT_SOURCE_DIR}/fsw/src/cabal.sandbox.config- WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}/fsw/src/- COMMAND cabal v1-sandbox init- COMMAND cabal update- COMMAND cabal v1-install copilot- COMMENT "Installing Copilot"-)--add_custom_command(- DEPENDS ${CMAKE_CURRENT_SOURCE_DIR}/fsw/src/cabal.sandbox.config- DEPENDS ${CMAKE_CURRENT_SOURCE_DIR}/fsw/src/Properties.hs- OUTPUT ${CMAKE_CURRENT_SOURCE_DIR}/fsw/src/copilot.c- ${CMAKE_CURRENT_SOURCE_DIR}/fsw/src/copilot.h- ${CMAKE_CURRENT_SOURCE_DIR}/fsw/src/copilot_types.h- WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}/fsw/src/- COMMAND cabal v1-exec "--" runhaskell Properties.hs- COMMENT "Compiling Copilot code"-)--add_custom_target(HASKELL_COPILOT- DEPENDS ${CMAKE_CURRENT_SOURCE_DIR}/fsw/src/copilot.c- ${CMAKE_CURRENT_SOURCE_DIR}/fsw/src/copilot.h- ${CMAKE_CURRENT_SOURCE_DIR}/fsw/src/copilot_types.h- SOURCES ${CMAKE_CURRENT_SOURCE_DIR}/fsw/src/Properties.hs-)-add_dependencies(copilot_cfs HASKELL_COPILOT)
− templates/copilot-cfs/fsw/for_build/Makefile
@@ -1,112 +0,0 @@-###############################################################################-# 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
@@ -1,21 +0,0 @@-/************************************************************************-** File:-** $Id: copilot_cfs_perfids.h $-**-** Purpose:-** Define Copilot 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
@@ -1,23 +0,0 @@-/************************************************************************-** File:-** $Id: copilot_cfs_msgids.h $-**-** Purpose:-** Define Copilot 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
@@ -1,47 +0,0 @@-{{#copilot}}-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)--{{{copilot.externs}}}-{{{copilot.internals}}}-{{{copilot.reqs}}}---- | Clock that increases in one-unit steps.-clock :: Stream Int64-clock = [0] ++ (clock + 1)---- | First Time Point-ftp :: Stream Bool-ftp = [True] ++ false--pre :: Stream Bool -> Stream Bool-pre = ([False] ++)--tpre :: Stream Bool -> Stream Bool-tpre = ([True] ++)--notPreviousNot :: Stream Bool -> Stream Bool-notPreviousNot = not . PTLTL.previous . not---- | Complete specification. Calls C handler functions when properties are--- violated.-spec :: Spec-spec = do-{{{copilot.triggers}}}--main :: IO ()-main = reify spec >>= compileWith settings "{{{copilot.specName}}}"- where- settings = mkDefaultCSettings { cSettingsStepFunctionName = "copilot_step" }-{{/copilot}}-{{^copilot}}--- No specification provided. Place your specification in this file.-{{/copilot}}
− templates/copilot-cfs/fsw/src/copilot_cfs.c
@@ -1,195 +0,0 @@-/*******************************************************************************-** File: copilot_cfs.c-**-** Purpose:-** This file contains the source code for the Copilot App.-**-*******************************************************************************/--/*-** Include Files:-*/--#include "copilot_cfs.h"-#include "copilot_cfs_perfids.h"-#include "copilot_cfs_msgids.h"-#include "copilot_cfs_msg.h"-#include "copilot_cfs_events.h"-#include "copilot_cfs_version.h"-{{#impl_extra_header}}-{{{.}}}-{{/impl_extra_header}}-{{#copilot}}-#include "{{{copilot.specName}}}_types.h"-#include "{{{copilot.specName}}}.h"-{{/copilot}}--{{#variables}}-{{varDeclType}} {{varDeclName}};-{{/variables}}--/*-** 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");- {{#msgIds}}- CFE_SB_Subscribe({{.}}, COPILOT_CommandPipe);- {{/msgIds}}--- 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)- {- {{#msgCases}}- case {{msgInfoId}}:- COPILOT_Process{{msgInfoDesc}}();- break;-- {{/msgCases}}-- 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}}-/**-* Make received data available to Copilot and run monitors.-*/-void COPILOT_Process{{msgDataDesc}}(void)-{- {{#msgDataFromType}}- {{msgDataFromType}}* msg;- msg = ({{.}}*) COPILOTMsgPtr;- {{/msgDataFromType}}- {{^msgDataFromType}}- {{msgDataVarType}}* msg;- msg = ({{msgDataVarType}}*) COPILOTMsgPtr;- {{/msgDataFromType}}- {{#msgDataFromField}}- {{msgDataVarName}} = msg->{{.}};- {{/msgDataFromField}}- {{^msgDataFromField}}- {{msgDataVarName}} = *msg;- {{/msgDataFromField}}-- // Run all copilot monitors.- copilot_step();-}--{{/msgHandlers}}---{{#triggers}}-/**- * Report copilot property violations.- */-{{#triggerType}}-void {{triggerName}}({{.}} arg) {-{{/triggerType}}-{{^triggerType}}-void {{triggerName}}(void) {-{{/triggerType}}- CFE_EVS_SendEvent(COPILOT_COMMANDCPVIOL_INF_EID, CFE_EVS_ERROR,- "COPILOT: violation: {{triggerName}}");-}-{{/triggers}}
− templates/copilot-cfs/fsw/src/copilot_cfs.h
@@ -1,51 +0,0 @@-/*******************************************************************************-** 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);-{{#msgCases}}-void COPILOT_Process{{msgInfoDesc}}(void);-{{/msgCases}}-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
@@ -1,27 +0,0 @@-/************************************************************************-** 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
@@ -1,42 +0,0 @@-/*******************************************************************************-** 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
@@ -1,24 +0,0 @@-/************************************************************************-** File:-** $Id: copilot_app_version.h $-**-** Purpose:-** The Copilot 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 */-/************************/
templates/diagram/Copilot.hs view
@@ -46,33 +46,3 @@ ifThenElses ((s1,i,s2):ss) = ifThenElse (previousState == constant s1 && i) (constant s2) (ifThenElses ss)---- | True when the given input stream does hold any of the values in the given--- list.-noneOf :: [Stream Bool] -> Stream Bool-noneOf [] = true-noneOf (x:xs) = not x && noneOf xs---- | Given a list of transitions, and a current state, and a list of possible--- destination states, produce a list of booleans indicating if a transition to--- each of the destination states would be valid.-checkValidTransitions :: [(Word8, Stream Bool, Word8)]- -> Stream Word8- -> [Word8]- -> [Stream Bool]-checkValidTransitions transitions curState destinations =- map (checkValidTransition transitions curState) destinations---- | Given a list of transitions, and a current state, and destination states,--- produce a list of booleans indicating if a transition to each of the--- destination states would be valid.-checkValidTransition :: [(Word8, Stream Bool, Word8)]- -> Stream Word8- -> Word8- -> Stream Bool-checkValidTransition [] _ _ = true-checkValidTransition ((so1, c, sd1):sx) so2 sd2 =- ifThenElse- ((constant so1 == so2) && (constant sd1 == constant sd2))- c- (checkValidTransition sx so2 sd2)
templates/ros/copilot/src/Copilot.hs view
@@ -10,6 +10,9 @@ import Language.Copilot (reify) import Prelude hiding ((&&), (||), (++), (<=), (>=), (<), (>), (==), (/=), not) +{{#copilot_extra_defs}}+{{{.}}}+{{/copilot_extra_defs}} {{{copilot.externs}}} {{{copilot.internals}}} {{{copilot.reqs}}}
templates/standalone/Copilot.hs view
@@ -9,6 +9,9 @@ import Language.Copilot (reify) import Prelude hiding ((&&), (||), (++), (<=), (>=), (<), (>), (==), (/=), not) +{{#copilot_extra_defs}}+{{{.}}}+{{/copilot_extra_defs}} {{{externs}}} {{{internals}}} {{{reqs}}}