ogma-core 1.7.0 → 1.8.0
raw patch · 9 files changed
+319/−42 lines, 9 filesdep ~ogma-extradep ~ogma-language-cdep ~ogma-language-copilot
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
Files
- CHANGELOG.md +6/−0
- ogma-core.cabal +12/−11
- src/Command/CFSApp.hs +14/−6
- src/Command/Common.hs +42/−2
- src/Command/FPrimeApp.hs +14/−6
- src/Command/Overview.hs +162/−0
- src/Command/ROSApp.hs +14/−6
- src/Command/Standalone.hs +51/−9
- tests/Main.hs +4/−2
CHANGELOG.md view
@@ -1,5 +1,11 @@ # Revision history for ogma-core +## [1.8.0] - 2025-07-13++* Version bump 1.8.0 (#275).+* Introduce overview command (#272).+* Extend code backends to accept expressions to monitor as arguments (#121).+ ## [1.7.0] - 2025-03-21 * Version bump 1.7.0 (#268).
ogma-core.cabal view
@@ -32,7 +32,7 @@ build-type: Simple name: ogma-core-version: 1.7.0+version: 1.8.0 homepage: https://github.com/nasa/ogma bug-reports: https://github.com/nasa/ogma/issues license: OtherLicense@@ -112,6 +112,7 @@ Command.CStructs2MsgHandlers Command.Diagram Command.FPrimeApp+ Command.Overview Command.Result Command.ROSApp Command.Standalone@@ -147,16 +148,16 @@ , process >= 1.6 && < 1.7 , text >= 1.2.3.1 && < 2.2 - , ogma-extra >= 1.7.0 && < 1.8- , ogma-language-c >= 1.7.0 && < 1.8- , ogma-language-copilot >= 1.7.0 && < 1.8- , ogma-language-csv >= 1.7.0 && < 1.8- , ogma-language-jsonspec >= 1.7.0 && < 1.8- , ogma-language-lustre >= 1.7.0 && < 1.8- , ogma-language-smv >= 1.7.0 && < 1.8- , ogma-language-xlsx >= 1.7.0 && < 1.8- , ogma-language-xmlspec >= 1.7.0 && < 1.8- , ogma-spec >= 1.7.0 && < 1.8+ , ogma-extra >= 1.8.0 && < 1.9+ , ogma-language-c >= 1.8.0 && < 1.9+ , ogma-language-copilot >= 1.8.0 && < 1.9+ , ogma-language-csv >= 1.8.0 && < 1.9+ , ogma-language-jsonspec >= 1.8.0 && < 1.9+ , ogma-language-lustre >= 1.8.0 && < 1.9+ , ogma-language-smv >= 1.8.0 && < 1.9+ , ogma-language-xlsx >= 1.8.0 && < 1.9+ , ogma-language-xmlspec >= 1.8.0 && < 1.9+ , ogma-spec >= 1.8.0 && < 1.9 hs-source-dirs: src
src/Command/CFSApp.hs view
@@ -50,7 +50,7 @@ where -- External imports-import Control.Applicative ( liftA2 )+import Control.Applicative ( liftA2, (<|>) ) import qualified Control.Exception as E import Control.Monad.Except ( ExceptT (..), liftEither ) import Data.Aeson ( ToJSON (..) )@@ -106,11 +106,14 @@ rs <- parseRequirementsListFile handlersFile varDB <- openVarDBFilesWithDefault varDBFile - spec <- maybe (return Nothing) (\f -> Just <$> parseInputFile' f) fp+ specT <- maybe (return Nothing) (\e -> Just <$> parseInputExpr' e) cExpr+ specF <- maybe (return Nothing) (\f -> Just <$> parseInputFile' f) fp + let spec = specT <|> specF+ liftEither $ checkArguments spec vs rs - copilotM <- sequenceA $ liftA2 processSpec spec fp+ copilotM <- sequenceA $ (\spec' -> processSpec spec' fp cExpr) <$> spec let varNames = fromMaybe (specExtractExternalVariables spec) vs monitors = maybe@@ -125,6 +128,7 @@ where + cExpr = commandConditionExpr options fp = commandInputFile options varNameFile = commandVariables options varDBFile = maybeToList $ commandVariableDB options@@ -133,11 +137,14 @@ propFormatName = commandPropFormat options propVia = commandPropVia options + parseInputExpr' e =+ parseInputExpr e propFormatName propVia exprT+ parseInputFile' f = parseInputFile f formatName propFormatName propVia exprT - processSpec spec' fp' =- Command.Standalone.commandLogic fp' "copilot" [] exprT spec'+ processSpec spec' expr' fp' =+ Command.Standalone.commandLogic expr' fp' "copilot" [] exprT spec' -- | Generate a variable substitution map for a cFS application. commandLogic :: VariableDB@@ -163,7 +170,8 @@ -- | Options used to customize the conversion of specifications to ROS -- applications. data CommandOptions = CommandOptions- { commandInputFile :: Maybe FilePath -- ^ Input specification file.+ { commandConditionExpr :: Maybe String -- ^ Trigger condition.+ , commandInputFile :: Maybe FilePath -- ^ Input specification file. , commandTargetDir :: FilePath -- ^ Target directory where the -- application should be created. , commandTemplateDir :: Maybe FilePath -- ^ Directory where the template is
src/Command/Common.hs view
@@ -34,7 +34,8 @@ -- -- | Shared functions across multiple backends. module Command.Common- ( parseInputFile+ ( parseInputExpr+ , parseInputFile , parseVariablesFile , parseRequirementsListFile , openVarDBFiles@@ -72,7 +73,8 @@ import Data.String.Extra (sanitizeLCIdentifier, sanitizeUCIdentifier) -- External imports: ogma-import Data.OgmaSpec (Spec, externalVariableName, externalVariables,+import Data.OgmaSpec (Requirement (..), Spec (..),+ externalVariableName, externalVariables, requirementName, requirementResultType, requirements) import Language.CSVSpec.Parser (parseCSVSpec)@@ -102,6 +104,30 @@ import Data.Location (Location (..)) import Paths_ogma_core (getDataDir) +-- | Process input specification from a single expression and return its+-- abstract representation.+parseInputExpr :: String+ -> String+ -> Maybe String+ -> ExprPairT a+ -> ExceptT ErrorTriplet IO (Spec a)+parseInputExpr expr propFormatName propVia exprT =+ ExceptT $ do+ let ExprPairT parse replace print ids def = exprT++ let wrapper = wrapVia propVia parse++ result <- wrapper expr++ let spec = do+ expr' <- result+ let req = Requirement "triggerCondition" expr' "" Nothing Nothing+ return $ Spec [] [] [ req ]++ case spec of+ Left e -> return $ Left $ cannotReadConditionExpr expr e+ Right s -> return $ Right s+ -- | Process input specification, if available, and return its abstract -- representation. parseInputFile :: FilePath@@ -348,6 +374,16 @@ "the arguments provided are insufficient: you must provide an input " ++ "specification, or both a variables and a handlers file." +-- | Exception handler to deal with the case in which the trigger expression+-- cannot be understood.+cannotReadConditionExpr :: String -> String -> ErrorTriplet+cannotReadConditionExpr expr errorMsg =+ ErrorTriplet ecCannotReadConditionExpr msg LocationNothing+ where+ msg =+ "cannot parse condition or trigger expression " ++ show expr ++ ":"+ ++ errorMsg+ -- | Exception handler to deal with the case in which the input file cannot be -- opened. cannotOpenInputFile :: FilePath -> ErrorTriplet@@ -427,6 +463,10 @@ -- | Error: wrong arguments provided. ecWrongArguments :: ErrorCode ecWrongArguments = 1++-- | Error: the trigger expression provided by the user cannot be parsed.+ecCannotReadConditionExpr :: ErrorCode+ecCannotReadConditionExpr = 1 -- | Error: the input specification provided by the user cannot be opened. ecCannotOpenInputFile :: ErrorCode
src/Command/FPrimeApp.hs view
@@ -45,7 +45,7 @@ where -- External imports-import Control.Applicative ( liftA2 )+import Control.Applicative ( liftA2, (<|>) ) import qualified Control.Exception as E import Control.Monad.Except ( ExceptT(..), liftEither ) import Data.Aeson ( ToJSON, toJSON )@@ -100,11 +100,14 @@ rs <- parseRequirementsListFile handlersFile varDB <- openVarDBFilesWithDefault varDBFile - spec <- maybe (return Nothing) (\f -> Just <$> parseInputFile' f) fp+ specT <- maybe (return Nothing) (\e -> Just <$> parseInputExpr' e) cExpr+ specF <- maybe (return Nothing) (\f -> Just <$> parseInputFile' f) fp + let spec = specT <|> specF+ liftEither $ checkArguments spec vs rs - copilotM <- sequenceA $ liftA2 processSpec spec fp+ copilotM <- sequenceA $ (\spec' -> processSpec spec' fp cExpr) <$> spec let varNames = fromMaybe (specExtractExternalVariables spec) vs monitors = maybe@@ -120,6 +123,7 @@ where + cExpr = commandConditionExpr options fp = commandInputFile options varNameFile = commandVariables options varDBFile = maybeToList $ commandVariableDB options@@ -128,18 +132,22 @@ propFormatName = commandPropFormat options propVia = commandPropVia options + parseInputExpr' e =+ parseInputExpr e propFormatName propVia exprT+ parseInputFile' f = parseInputFile f formatName propFormatName propVia exprT - processSpec spec' fp' =- Command.Standalone.commandLogic fp' "copilot" [] exprT spec'+ processSpec spec' expr' fp' =+ Command.Standalone.commandLogic expr' fp' "copilot" [] exprT spec' -- ** Argument processing -- | Options used to customize the conversion of specifications to F' -- applications. data CommandOptions = CommandOptions- { commandInputFile :: Maybe FilePath -- ^ Input specification file.+ { commandConditionExpr :: Maybe String -- ^ Trigger condition.+ , commandInputFile :: Maybe FilePath -- ^ Input specification file. , commandTargetDir :: FilePath -- ^ Target directory where the -- component should be created. , commandTemplateDir :: Maybe FilePath -- ^ Directory where the template is
+ src/Command/Overview.hs view
@@ -0,0 +1,162 @@+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE ScopedTypeVariables #-}+-- Copyright 2024 United States Government as represented by the Administrator+-- of the National Aeronautics and Space Administration. All Rights Reserved.+--+-- Disclaimers+--+-- No Warranty: THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY+-- OF ANY KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT+-- LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO+-- SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR A+-- PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT THE+-- SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT DOCUMENTATION, IF+-- PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE. THIS AGREEMENT DOES NOT, IN+-- ANY MANNER, CONSTITUTE AN ENDORSEMENT BY GOVERNMENT AGENCY OR ANY PRIOR+-- RECIPIENT OF ANY RESULTS, RESULTING DESIGNS, HARDWARE, SOFTWARE PRODUCTS OR+-- ANY OTHER APPLICATIONS RESULTING FROM USE OF THE SUBJECT SOFTWARE. FURTHER,+-- GOVERNMENT AGENCY DISCLAIMS ALL WARRANTIES AND LIABILITIES REGARDING+-- THIRD-PARTY SOFTWARE, IF PRESENT IN THE ORIGINAL SOFTWARE, AND DISTRIBUTES+-- IT "AS IS."+--+-- Waiver and Indemnity: RECIPIENT AGREES TO WAIVE ANY AND ALL CLAIMS AGAINST+-- THE UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS, AS WELL AS+-- ANY PRIOR RECIPIENT. IF RECIPIENT'S USE OF THE SUBJECT SOFTWARE RESULTS IN+-- ANY LIABILITIES, DEMANDS, DAMAGES, EXPENSES OR LOSSES ARISING FROM SUCH USE,+-- INCLUDING ANY DAMAGES FROM PRODUCTS BASED ON, OR RESULTING FROM, RECIPIENT'S+-- USE OF THE SUBJECT SOFTWARE, RECIPIENT SHALL INDEMNIFY AND HOLD HARMLESS THE+-- UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS, AS WELL AS ANY+-- PRIOR RECIPIENT, TO THE EXTENT PERMITTED BY LAW. RECIPIENT'S SOLE REMEDY+-- FOR ANY SUCH MATTER SHALL BE THE IMMEDIATE, UNILATERAL TERMINATION OF THIS+-- AGREEMENT.+--+-- | Produce an overview of the input files.+module Command.Overview+ ( command+ , CommandOptions(..)+ , CommandSummary(..)+ , ErrorCode+ )+ where++-- External imports+import Control.Monad.Except (runExceptT)+import Data.Aeson (ToJSON (..))+import Data.List (nub, (\\))+import GHC.Generics (Generic)++-- External imports: Ogma+import Data.OgmaSpec (ExternalVariableDef (..), InternalVariableDef (..),+ 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)++-- | Generate overview of a spec given in an input file.+--+-- PRE: The file given is readable, contains a valid file with recognizable+-- format, the formulas in the file do not use any identifiers that exist in+-- Copilot, or any of @prop@, @clock@, @ftp@, @notPreviousNot@. All identifiers+-- used are valid C99 identifiers. The template, if provided, exists and uses+-- the variables needed by the overview application generator. The target+-- directory is writable and there's enough disk space to copy the files over.+command :: FilePath -- ^ Path to a file containing a specification+ -> CommandOptions -- ^ Customization options+ -> IO (Maybe CommandSummary, Result ErrorCode)+command fp options = do+ let functions = exprPair (commandPropFormat options)++ copilot <- command' fp options functions++ return $ commandResult options fp copilot++-- | Generate overview of a spec given in an input file.+--+-- PRE: The file given is readable, contains a valid file with recognizable+-- format, the formulas in the file do not use any identifiers that exist in+-- Copilot, or any of @prop@, @clock@, @ftp@, @notPreviousNot@. All identifiers+-- used are valid C99 identifiers. The template, if provided, exists and uses+-- the variables needed by the overview application generator. The target+-- directory is writable and there's enough disk space to copy the files over.+command' :: FilePath+ -> CommandOptions+ -> ExprPair+ -> 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++ let summary = do+ spec1 <- spec'+ spec3 <- specAnalyze $ addMissingIdentifiers ids spec1+ return $ CommandSummary (length (externalVariables spec3))+ (length (internalVariables spec3))+ (length (requirements spec3))+ return summary++ where++ parseInputFile' f = parseInputFile f formatName propFormatName propVia exprT+ formatName = commandFormat options+ propFormatName = commandPropFormat options+ propVia = commandPropVia options++ ExprPairT _parse _replace _print ids _def = exprT++data CommandSummary = CommandSummary+ { commandExternalVariables :: Int+ , commandInternalVariables :: Int+ , commandRequirements :: Int+ }+ deriving (Generic, Show)++instance ToJSON CommandSummary++-- | Options used to customize the interpretation of input specifications.+data CommandOptions = CommandOptions+ { commandFormat :: String+ , commandPropFormat :: String+ , commandPropVia :: Maybe String+ }++-- * Error codes++-- | Error: the input file cannot be read due to it being unreadable or the+-- format being incorrect.+ecOverviewError :: ErrorCode+ecOverviewError = 1++-- * Result++-- | Process the result of the transformation function.+commandResult :: CommandOptions+ -> FilePath+ -> Either String a+ -> (Maybe a, Result ErrorCode)+commandResult _options fp result = case result of+ Left msg -> (Nothing, Error ecOverviewError msg (LocationFile fp))+ Right t -> (Just t, Success)++-- | Add to a spec external variables for all identifiers mentioned in+-- expressions that are not defined anywhere.+addMissingIdentifiers :: (a -> [String]) -> Spec a -> Spec a+addMissingIdentifiers f s = s { externalVariables = vars' }+ where+ vars' = externalVariables s ++ newVars+ newVars = map (\n -> ExternalVariableDef n "") newVarNames++ -- Names that are not defined anywhere+ newVarNames = identifiers \\ existingNames++ -- Identifiers being mentioned in the requirements.+ identifiers = nub $ concatMap (f . requirementExpr) (requirements s)++ -- Names that are defined in variables.+ existingNames = map externalVariableName (externalVariables s)+ ++ map internalVariableName (internalVariables s)
src/Command/ROSApp.hs view
@@ -49,7 +49,7 @@ where -- External imports-import Control.Applicative (liftA2)+import Control.Applicative (liftA2, (<|>)) import qualified Control.Exception as E import Control.Monad.Except (ExceptT (..), liftEither) import Data.Aeson (ToJSON (..))@@ -104,11 +104,14 @@ rs <- parseRequirementsListFile handlersFile varDB <- openVarDBFilesWithDefault varDBFile - spec <- maybe (return Nothing) (\f -> Just <$> parseInputFile' f) fp+ specT <- maybe (return Nothing) (\e -> Just <$> parseInputExpr' e) cExpr+ specF <- maybe (return Nothing) (\f -> Just <$> parseInputFile' f) fp + let spec = specT <|> specF+ liftEither $ checkArguments spec vs rs - copilotM <- sequenceA $ liftA2 processSpec spec fp+ copilotM <- sequenceA $ (\spec' -> processSpec spec' fp cExpr) <$> spec let varNames = fromMaybe (specExtractExternalVariables spec) vs monitors = maybe@@ -124,6 +127,7 @@ where + cExpr = commandConditionExpr options fp = commandInputFile options varNameFile = commandVariables options varDBFile = maybeToList $ commandVariableDB options@@ -132,18 +136,22 @@ propFormatName = commandPropFormat options propVia = commandPropVia options + parseInputExpr' e =+ parseInputExpr e propFormatName propVia exprT+ parseInputFile' f = parseInputFile f formatName propFormatName propVia exprT - processSpec spec' fp' =- Command.Standalone.commandLogic fp' "copilot" [] exprT spec'+ processSpec spec' expr' fp' =+ Command.Standalone.commandLogic expr' fp' "copilot" [] exprT spec' -- ** Argument processing -- | Options used to customize the conversion of specifications to ROS -- applications. data CommandOptions = CommandOptions- { commandInputFile :: Maybe FilePath -- ^ Input specification file.+ { commandConditionExpr :: Maybe String -- ^ Trigger condition.+ , commandInputFile :: Maybe FilePath -- ^ Input specification file. , commandTargetDir :: FilePath -- ^ Target directory where the -- application should be created. , commandTemplateDir :: Maybe FilePath -- ^ Directory where the template is
src/Command/Standalone.hs view
@@ -44,6 +44,7 @@ where -- External imports+import Control.Applicative ((<|>)) import Control.Exception as E import Control.Monad.Except (ExceptT (..), liftEither) import Data.Aeson (ToJSON (..))@@ -112,29 +113,44 @@ -- Read spec and complement the specification with any missing/implicit -- definitions.- input <- parseInputFile fp formatName propFormatName propVia exprT- commandLogic fp name typeMaps exprT input+ specT <- maybe (return Nothing) (\e -> Just <$> parseInputExpr' e) triggerExprM+ specF <- maybe (return Nothing) (\f -> Just <$> parseInputFile' f) fpM+ let spec = specT <|> specF++ case spec of+ Nothing -> liftEither $ Left $ commandMissingSpec+ Just spec' -> commandLogic triggerExprM fpM name typeMaps exprT spec'+ where- fp = commandInputFile options+ triggerExprM = commandConditionExpr options+ fpM = commandInputFile options name = commandFilename options typeMaps = typeToCopilotTypeMapping (commandTypeMapping options) formatName = commandFormat options propFormatName = commandPropFormat options propVia = commandPropVia options + parseInputExpr' e =+ parseInputExpr e propFormatName propVia exprT++ parseInputFile' f =+ parseInputFile f formatName propFormatName propVia exprT++ -- | Generate the data of a new standalone Copilot monitor that implements the -- spec, using a subexpression handler.-commandLogic :: FilePath+commandLogic :: Maybe String+ -> Maybe FilePath -> String -> [(String, String)] -> ExprPairT a -> Spec a -> ExceptT ErrorTriplet IO AppData-commandLogic fp name typeMaps exprT input = do+commandLogic expr fp name typeMaps exprT input = do let spec = addMissingIdentifiers ids input -- Analyze the spec for incorrect identifiers and convert it to Copilot. -- If there is an error, we change the error to a message we control.- let appData = mapLeft (commandIncorrectSpec fp) $ do+ let appData = mapLeft commandIncorrectSpec' $ do spec' <- specAnalyze spec res <- spec2Copilot name typeMaps replace print spec' @@ -147,6 +163,11 @@ where + commandIncorrectSpec' = case (expr, fp) of+ (Nothing, Just fp') -> commandIncorrectSpecF fp'+ (Just expr', _) -> commandIncorrectSpecE expr'+ (_, _) -> error "Both expression and file are missing"+ ExprPairT parse replace print ids def = exprT -- ** Argument processing@@ -154,7 +175,8 @@ -- | Options used to customize the conversion of specifications to Copilot -- code. data CommandOptions = CommandOptions- { commandInputFile :: FilePath -- ^ Input specification file.+ { commandConditionExpr :: Maybe String+ , commandInputFile :: Maybe FilePath -- ^ Input specification file. , commandTargetDir :: FilePath -- ^ Target directory where the -- application should be created. , commandTemplateDir :: Maybe FilePath -- ^ Directory where the template@@ -197,15 +219,35 @@ instance ToJSON AppData +-- | Error message associated to not having a spec of any kind.+commandMissingSpec :: ErrorTriplet+commandMissingSpec =+ ErrorTriplet ecMissingSpec msg LocationNothing+ where+ msg =+ "No input specification has been provided."+ -- | Error message associated to not being able to formalize the input spec.-commandIncorrectSpec :: String -> String -> ErrorTriplet-commandIncorrectSpec file e =+commandIncorrectSpecF :: String -> String -> ErrorTriplet+commandIncorrectSpecF file e = ErrorTriplet ecIncorrectSpec msg (LocationFile file) where msg = "The input specification " ++ file ++ " canbot be formalized: " ++ e +-- | Error message associated to not being able to formalize the input spec.+commandIncorrectSpecE :: String -> String -> ErrorTriplet+commandIncorrectSpecE expr e =+ ErrorTriplet ecIncorrectSpec msg LocationNothing+ where+ msg =+ "The input specification " ++ show expr ++ " cannot be formalized: " ++ e+ -- ** Error codes++-- | Error: there is no input argument.+ecMissingSpec :: ErrorCode+ecMissingSpec = 1 -- | Error: the input specification cannot be formalized. ecIncorrectSpec :: ErrorCode
tests/Main.hs view
@@ -103,7 +103,8 @@ testStandaloneFCS file success = do targetDir <- getTemporaryDirectory let opts = CommandOptions- { commandInputFile = file+ { commandConditionExpr = Nothing+ , commandInputFile = Just file , commandFormat = "fcs" , commandPropFormat = "smv" , commandTypeMapping = [("int", "Int64"), ("real", "Float")]@@ -140,7 +141,8 @@ testStandaloneFDB file success = do targetDir <- getTemporaryDirectory let opts = CommandOptions- { commandInputFile = file+ { commandConditionExpr = Nothing+ , commandInputFile = Just file , commandFormat = "fdb" , commandPropFormat = "lustre" , commandTypeMapping = []