diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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). diff --git a/ogma-core.cabal b/ogma-core.cabal --- a/ogma-core.cabal +++ b/ogma-core.cabal @@ -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 diff --git a/src/Command/CFSApp.hs b/src/Command/CFSApp.hs --- a/src/Command/CFSApp.hs +++ b/src/Command/CFSApp.hs @@ -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 diff --git a/src/Command/Diagram.hs b/src/Command/Diagram.hs --- a/src/Command/Diagram.hs +++ b/src/Command/Diagram.hs @@ -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 diff --git a/src/Command/Overview.hs b/src/Command/Overview.hs --- a/src/Command/Overview.hs +++ b/src/Command/Overview.hs @@ -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) diff --git a/src/Language/Trans/SpecAnalysis.hs b/src/Language/Trans/SpecAnalysis.hs new file mode 100644 --- /dev/null +++ b/src/Language/Trans/SpecAnalysis.hs @@ -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 diff --git a/templates/cfs/Dockerfile b/templates/cfs/Dockerfile new file mode 100644 --- /dev/null +++ b/templates/cfs/Dockerfile @@ -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 diff --git a/templates/cfs/copilot/CMakeLists.txt b/templates/cfs/copilot/CMakeLists.txt new file mode 100644 --- /dev/null +++ b/templates/cfs/copilot/CMakeLists.txt @@ -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) diff --git a/templates/cfs/copilot/fsw/for_build/Makefile b/templates/cfs/copilot/fsw/for_build/Makefile new file mode 100644 --- /dev/null +++ b/templates/cfs/copilot/fsw/for_build/Makefile @@ -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 diff --git a/templates/cfs/copilot/fsw/mission_inc/copilot_cfs_perfids.h b/templates/cfs/copilot/fsw/mission_inc/copilot_cfs_perfids.h new file mode 100644 --- /dev/null +++ b/templates/cfs/copilot/fsw/mission_inc/copilot_cfs_perfids.h @@ -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 */ +/************************/ diff --git a/templates/cfs/copilot/fsw/platform_inc/copilot_cfs_msgids.h b/templates/cfs/copilot/fsw/platform_inc/copilot_cfs_msgids.h new file mode 100644 --- /dev/null +++ b/templates/cfs/copilot/fsw/platform_inc/copilot_cfs_msgids.h @@ -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 */ +/************************/ diff --git a/templates/cfs/copilot/fsw/src/Properties.hs b/templates/cfs/copilot/fsw/src/Properties.hs new file mode 100644 --- /dev/null +++ b/templates/cfs/copilot/fsw/src/Properties.hs @@ -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}} diff --git a/templates/cfs/copilot/fsw/src/copilot_cfs.c b/templates/cfs/copilot/fsw/src/copilot_cfs.c new file mode 100644 --- /dev/null +++ b/templates/cfs/copilot/fsw/src/copilot_cfs.c @@ -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}} diff --git a/templates/cfs/copilot/fsw/src/copilot_cfs.h b/templates/cfs/copilot/fsw/src/copilot_cfs.h new file mode 100644 --- /dev/null +++ b/templates/cfs/copilot/fsw/src/copilot_cfs.h @@ -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 +#include +#include + +/***********************************************************************/ + +#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_ */ diff --git a/templates/cfs/copilot/fsw/src/copilot_cfs_events.h b/templates/cfs/copilot/fsw/src/copilot_cfs_events.h new file mode 100644 --- /dev/null +++ b/templates/cfs/copilot/fsw/src/copilot_cfs_events.h @@ -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 */ +/************************/ diff --git a/templates/cfs/copilot/fsw/src/copilot_cfs_msg.h b/templates/cfs/copilot/fsw/src/copilot_cfs_msg.h new file mode 100644 --- /dev/null +++ b/templates/cfs/copilot/fsw/src/copilot_cfs_msg.h @@ -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 */ +/************************/ diff --git a/templates/cfs/copilot/fsw/src/copilot_cfs_version.h b/templates/cfs/copilot/fsw/src/copilot_cfs_version.h new file mode 100644 --- /dev/null +++ b/templates/cfs/copilot/fsw/src/copilot_cfs_version.h @@ -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 */ +/************************/ diff --git a/templates/copilot-cfs/CMakeLists.txt b/templates/copilot-cfs/CMakeLists.txt deleted file mode 100644 --- a/templates/copilot-cfs/CMakeLists.txt +++ /dev/null @@ -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) diff --git a/templates/copilot-cfs/fsw/for_build/Makefile b/templates/copilot-cfs/fsw/for_build/Makefile deleted file mode 100644 --- a/templates/copilot-cfs/fsw/for_build/Makefile +++ /dev/null @@ -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 diff --git a/templates/copilot-cfs/fsw/mission_inc/copilot_cfs_perfids.h b/templates/copilot-cfs/fsw/mission_inc/copilot_cfs_perfids.h deleted file mode 100644 --- a/templates/copilot-cfs/fsw/mission_inc/copilot_cfs_perfids.h +++ /dev/null @@ -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 */ -/************************/ diff --git a/templates/copilot-cfs/fsw/platform_inc/copilot_cfs_msgids.h b/templates/copilot-cfs/fsw/platform_inc/copilot_cfs_msgids.h deleted file mode 100644 --- a/templates/copilot-cfs/fsw/platform_inc/copilot_cfs_msgids.h +++ /dev/null @@ -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 */ -/************************/ diff --git a/templates/copilot-cfs/fsw/src/Properties.hs b/templates/copilot-cfs/fsw/src/Properties.hs deleted file mode 100644 --- a/templates/copilot-cfs/fsw/src/Properties.hs +++ /dev/null @@ -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}} diff --git a/templates/copilot-cfs/fsw/src/copilot_cfs.c b/templates/copilot-cfs/fsw/src/copilot_cfs.c deleted file mode 100644 --- a/templates/copilot-cfs/fsw/src/copilot_cfs.c +++ /dev/null @@ -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}} diff --git a/templates/copilot-cfs/fsw/src/copilot_cfs.h b/templates/copilot-cfs/fsw/src/copilot_cfs.h deleted file mode 100644 --- a/templates/copilot-cfs/fsw/src/copilot_cfs.h +++ /dev/null @@ -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 -#include -#include - -/***********************************************************************/ - -#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_ */ diff --git a/templates/copilot-cfs/fsw/src/copilot_cfs_events.h b/templates/copilot-cfs/fsw/src/copilot_cfs_events.h deleted file mode 100644 --- a/templates/copilot-cfs/fsw/src/copilot_cfs_events.h +++ /dev/null @@ -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 */ -/************************/ diff --git a/templates/copilot-cfs/fsw/src/copilot_cfs_msg.h b/templates/copilot-cfs/fsw/src/copilot_cfs_msg.h deleted file mode 100644 --- a/templates/copilot-cfs/fsw/src/copilot_cfs_msg.h +++ /dev/null @@ -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 */ -/************************/ diff --git a/templates/copilot-cfs/fsw/src/copilot_cfs_version.h b/templates/copilot-cfs/fsw/src/copilot_cfs_version.h deleted file mode 100644 --- a/templates/copilot-cfs/fsw/src/copilot_cfs_version.h +++ /dev/null @@ -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 */ -/************************/ diff --git a/templates/diagram/Copilot.hs b/templates/diagram/Copilot.hs --- a/templates/diagram/Copilot.hs +++ b/templates/diagram/Copilot.hs @@ -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) diff --git a/templates/ros/copilot/src/Copilot.hs b/templates/ros/copilot/src/Copilot.hs --- a/templates/ros/copilot/src/Copilot.hs +++ b/templates/ros/copilot/src/Copilot.hs @@ -10,6 +10,9 @@ import Language.Copilot (reify) import Prelude hiding ((&&), (||), (++), (<=), (>=), (<), (>), (==), (/=), not) +{{#copilot_extra_defs}} +{{{.}}} +{{/copilot_extra_defs}} {{{copilot.externs}}} {{{copilot.internals}}} {{{copilot.reqs}}} diff --git a/templates/standalone/Copilot.hs b/templates/standalone/Copilot.hs --- a/templates/standalone/Copilot.hs +++ b/templates/standalone/Copilot.hs @@ -9,6 +9,9 @@ import Language.Copilot (reify) import Prelude hiding ((&&), (||), (++), (<=), (>=), (<), (>), (==), (/=), not) +{{#copilot_extra_defs}} +{{{.}}} +{{/copilot_extra_defs}} {{{externs}}} {{{internals}}} {{{reqs}}}