diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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). diff --git a/ogma-core.cabal b/ogma-core.cabal --- a/ogma-core.cabal +++ b/ogma-core.cabal @@ -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 diff --git a/src/Command/CFSApp.hs b/src/Command/CFSApp.hs --- a/src/Command/CFSApp.hs +++ b/src/Command/CFSApp.hs @@ -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 diff --git a/src/Command/Common.hs b/src/Command/Common.hs --- a/src/Command/Common.hs +++ b/src/Command/Common.hs @@ -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 diff --git a/src/Command/FPrimeApp.hs b/src/Command/FPrimeApp.hs --- a/src/Command/FPrimeApp.hs +++ b/src/Command/FPrimeApp.hs @@ -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 diff --git a/src/Command/Overview.hs b/src/Command/Overview.hs new file mode 100644 --- /dev/null +++ b/src/Command/Overview.hs @@ -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) diff --git a/src/Command/ROSApp.hs b/src/Command/ROSApp.hs --- a/src/Command/ROSApp.hs +++ b/src/Command/ROSApp.hs @@ -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 diff --git a/src/Command/Standalone.hs b/src/Command/Standalone.hs --- a/src/Command/Standalone.hs +++ b/src/Command/Standalone.hs @@ -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 diff --git a/tests/Main.hs b/tests/Main.hs --- a/tests/Main.hs +++ b/tests/Main.hs @@ -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 = []