From 9198add61a4d68f1461a50dd9895335c9ce66ab3 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sun, 5 Jan 2025 23:53:43 +0000 Subject: [PATCH 1/8] ogma-language-jsonspec: Extend JSON spec parser to use an IO action to parse properties. Refs #197. There is a need in Ogma to make the frontend more versatile, and to extend it to support languages unknown to Ogma without users having to modify the code of Ogma itself. To that end, we want to empower users with the ability to use a custom command to transform individual properties into a format that Ogma understands, and have Ogma call that external command on demand. Because calling an external command will be an IO action, any auxiliary sub-parsers used by Ogma should be IO actions, rather than pure functions. This commit modifies the parser for JSON specifications so that it takes as argument an IO action to parse individual properties. --- .../ogma-language-jsonspec.cabal | 1 + .../src/Language/JSONSpec/Parser.hs | 23 +++++++++++-------- 2 files changed, 15 insertions(+), 9 deletions(-) diff --git a/ogma-language-jsonspec/ogma-language-jsonspec.cabal b/ogma-language-jsonspec/ogma-language-jsonspec.cabal index b4ad7432..c37dc21b 100644 --- a/ogma-language-jsonspec/ogma-language-jsonspec.cabal +++ b/ogma-language-jsonspec/ogma-language-jsonspec.cabal @@ -74,6 +74,7 @@ library , jsonpath >= 0.3 && < 0.4 , text >= 1.2.3.1 && < 2.1 , megaparsec >= 8.0.0 && < 9.10 + , mtl >= 2.2.2 && < 2.4 , bytestring >= 0.10.8.2 && < 0.13 , ogma-spec >= 1.5.0 && < 1.6 diff --git a/ogma-language-jsonspec/src/Language/JSONSpec/Parser.hs b/ogma-language-jsonspec/src/Language/JSONSpec/Parser.hs index d57be333..d16354d8 100644 --- a/ogma-language-jsonspec/src/Language/JSONSpec/Parser.hs +++ b/ogma-language-jsonspec/src/Language/JSONSpec/Parser.hs @@ -33,6 +33,7 @@ module Language.JSONSpec.Parser where -- External imports +import Control.Monad.Except (ExceptT (..), runExceptT) import Data.Aeson (FromJSON (..), Value (..), decode, (.:)) import Data.Aeson.Key (toString) import qualified Data.Aeson.KeyMap as M @@ -107,9 +108,9 @@ parseJSONFormat jsonFormat = do , jfiRequirementExpr = jfi12 } -parseJSONSpec :: (String -> Either String a) -> JSONFormat -> Value -> Either String (Spec a) -parseJSONSpec parseExpr jsonFormat value = do - jsonFormatInternal <- parseJSONFormat jsonFormat +parseJSONSpec :: (String -> IO (Either String a)) -> JSONFormat -> Value -> IO (Either String (Spec a)) +parseJSONSpec parseExpr jsonFormat value = runExceptT $ do + jsonFormatInternal <- except $ parseJSONFormat jsonFormat let values :: [Value] values = maybe [] (`executeJSONPath` value) (jfiInternalVars jsonFormatInternal) @@ -131,7 +132,7 @@ parseJSONSpec parseExpr jsonFormat value = do , internalVariableExpr = varExpr } - internalVariableDefs <- mapM internalVarDef values + internalVariableDefs <- except $ mapM internalVarDef values let values :: [Value] values = maybe [] (`executeJSONPath` value) (jfiExternalVars jsonFormatInternal) @@ -150,7 +151,7 @@ parseJSONSpec parseExpr jsonFormat value = do , externalVariableType = varType } - externalVariableDefs <- mapM externalVarDef values + externalVariableDefs <- except $ mapM externalVarDef values let values :: [Value] values = executeJSONPath (jfiRequirements jsonFormatInternal) value @@ -158,14 +159,14 @@ parseJSONSpec parseExpr jsonFormat value = do -- requirementDef :: Value -> Either String (Requirement a) requirementDef value = do let msg = "Requirement name" - reqId <- valueToString msg =<< (listToEither msg (executeJSONPath (jfiRequirementId jsonFormatInternal) value)) + reqId <- except $ valueToString msg =<< (listToEither msg (executeJSONPath (jfiRequirementId jsonFormatInternal) value)) let msg = "Requirement expression" - reqExpr <- valueToString msg =<< (listToEither msg (executeJSONPath (jfiRequirementExpr jsonFormatInternal) value)) - reqExpr' <- parseExpr reqExpr + reqExpr <- except $ valueToString msg =<< (listToEither msg (executeJSONPath (jfiRequirementExpr jsonFormatInternal) value)) + reqExpr' <- ExceptT $ parseExpr reqExpr let msg = "Requirement description" - reqDesc <- maybe (Right "") (\e -> valueToString msg =<< (listToEither msg (executeJSONPath e value))) (jfiRequirementDesc jsonFormatInternal) + reqDesc <- except $ maybe (Right "") (\e -> valueToString msg =<< (listToEither msg (executeJSONPath e value))) (jfiRequirementDesc jsonFormatInternal) return $ Requirement { requirementName = reqId @@ -198,3 +199,7 @@ showErrorsM :: Show a => Maybe (Either a b) -> Either String (Maybe b) showErrorsM Nothing = Right Nothing showErrorsM (Just (Left s)) = Left (show s) showErrorsM (Just (Right x)) = Right (Just x) + +-- | Wrap an 'Either' value in an @ExceptT m@ monad. +except :: Monad m => Either e a -> ExceptT e m a +except = ExceptT . return From eb469be1f20357c6b2eed903d9f8971b4129c4bb Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sun, 5 Jan 2025 23:54:48 +0000 Subject: [PATCH 2/8] ogma-core: Adapt ROS, F' backend to use IO action to parse individual properties. Refs #197. There is a need in Ogma to make the frontend more versatile, and to extend it to support languages unknown to Ogma without users having to modify the code of Ogma itself. To that end, we want to empower users with the ability to use a custom command to transform individual properties into a format that Ogma understands, and have Ogma call that external command on demand. Prior commits have extended the JSON parser to use an external IO action to parse individual properties, rather than pure functions, which is suitable when those actions represent calls to external processes. This commit modifies the ROS and F' backends to wrap parser functions into IO actions, as required by the modified JSON specification parser. --- ogma-core/src/Command/FPrimeApp.hs | 17 ++++++++++------- ogma-core/src/Command/ROSApp.hs | 17 ++++++++++------- 2 files changed, 20 insertions(+), 14 deletions(-) diff --git a/ogma-core/src/Command/FPrimeApp.hs b/ogma-core/src/Command/FPrimeApp.hs index 7b953d56..b8f23b4e 100644 --- a/ogma-core/src/Command/FPrimeApp.hs +++ b/ogma-core/src/Command/FPrimeApp.hs @@ -41,8 +41,8 @@ module Command.FPrimeApp -- External imports import qualified Control.Exception as E -import Control.Monad.Except ( ExceptT, liftEither, liftIO, runExceptT, - throwError ) +import Control.Monad.Except ( ExceptT(..), liftEither, liftIO, + runExceptT, throwError ) import Data.Aeson ( eitherDecode, object, (.=) ) import Data.Char ( toUpper ) import Data.List ( find, intercalate, nub, sort ) @@ -167,12 +167,15 @@ parseOptionalFRETCS Nothing = return Nothing parseOptionalFRETCS (Just fp) = do -- Throws an exception if the file cannot be read. content <- liftIO $ B.safeReadFile fp - let fretCS :: Either String (Spec String) - fretCS = parseJSONSpec return fretFormat =<< eitherDecode =<< content - case fretCS of - Left e -> throwError $ cannotOpenFRETFile fp e - Right cs -> return $ Just cs + fretCS <- case eitherDecode =<< content of + Left e -> ExceptT $ return $ Left $ cannotOpenFRETFile fp e + Right v -> ExceptT $ do + p <- parseJSONSpec (return . return) fretFormat v + case p of + Left e -> return $ Left $ cannotOpenFRETFile fp e + Right r -> return $ Right r + return $ Just fretCS -- | Process a variable selection file, if available, and return the variable -- names. diff --git a/ogma-core/src/Command/ROSApp.hs b/ogma-core/src/Command/ROSApp.hs index 9c673706..99547c93 100644 --- a/ogma-core/src/Command/ROSApp.hs +++ b/ogma-core/src/Command/ROSApp.hs @@ -45,8 +45,8 @@ module Command.ROSApp -- External imports import qualified Control.Exception as E -import Control.Monad.Except (ExceptT, liftEither, liftIO, runExceptT, - throwError) +import Control.Monad.Except (ExceptT(..), liftEither, liftIO, + runExceptT, throwError) import Data.Aeson (eitherDecode, object, (.=)) import Data.List (find, intersperse) import Data.Maybe (fromMaybe) @@ -176,12 +176,15 @@ parseOptionalFRETCS Nothing = return Nothing parseOptionalFRETCS (Just fp) = do -- Throws an exception if the file cannot be read. content <- liftIO $ B.safeReadFile fp - let fretCS :: Either String (Spec String) - fretCS = parseJSONSpec return fretFormat =<< eitherDecode =<< content - case fretCS of - Left e -> throwError $ cannotOpenFRETFile fp e - Right cs -> return $ Just cs + fretCS <- case eitherDecode =<< content of + Left e -> ExceptT $ return $ Left $ cannotOpenFRETFile fp e + Right v -> ExceptT $ do + p <- parseJSONSpec (return . return) fretFormat v + case p of + Left e -> return $ Left $ cannotOpenFRETFile fp e + Right r -> return $ Right r + return $ Just fretCS -- | Process a variable selection file, if available, and return the variable -- names. From 7e8096f92a773c1e4539e1b365f3c263dee48d98 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sun, 5 Jan 2025 23:55:10 +0000 Subject: [PATCH 3/8] ogma-core: Extend standalone command to use external process to parse properties. Refs #197. There is a need in Ogma to make the frontend more versatile, and to extend it to support languages unknown to Ogma without users having to modify the code of Ogma itself. To that end, we want to empower users with the ability to use a custom command to transform individual properties into a format that Ogma understands, and have Ogma call that external command on demand. Prior commits have extended the JSON parser to use an external IO action to parse individual properties, rather than pure functions, which is suitable when those actions represent calls to external processes. This commit modifies the standalone backend to take an auxiliary command that is used as the process name to call to parse individual properties. --- ogma-core/ogma-core.cabal | 1 + ogma-core/src/Command/Standalone.hs | 26 +++++++++++++++++++++++++- 2 files changed, 26 insertions(+), 1 deletion(-) diff --git a/ogma-core/ogma-core.cabal b/ogma-core/ogma-core.cabal index 3cd3d9e5..07f1d7a1 100644 --- a/ogma-core/ogma-core.cabal +++ b/ogma-core/ogma-core.cabal @@ -127,6 +127,7 @@ library , graphviz >= 2999.20 && < 2999.21 , megaparsec >= 8.0.0 && < 9.10 , mtl >= 2.2.2 && < 2.4 + , process >= 1.6 && < 1.7 , text >= 1.2.3.1 && < 2.1 , ogma-extra >= 1.5.0 && < 1.6 diff --git a/ogma-core/src/Command/Standalone.hs b/ogma-core/src/Command/Standalone.hs index f7274332..b9d507a4 100644 --- a/ogma-core/src/Command/Standalone.hs +++ b/ogma-core/src/Command/Standalone.hs @@ -1,5 +1,6 @@ {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE ScopedTypeVariables #-} -- Copyright 2020 United States Government as represented by the Administrator -- of the National Aeronautics and Space Administration. All Rights Reserved. -- @@ -45,6 +46,7 @@ import Data.ByteString.Lazy (fromStrict) import Data.Foldable (for_) import Data.List (nub, (\\)) import Data.Maybe (fromMaybe) +import System.Process (readProcess) import System.FilePath (()) import Data.Text.Lazy (pack) @@ -144,13 +146,17 @@ standalone' fp options (ExprPair parse replace print ids) = do format <- read <$> readFile formatFile + let wrapper = wrapVia (standalonePropVia options) parse + -- All of the following operations use Either to return error messages. The -- use of the monadic bind to pass arguments from one function to the next -- will cause the program to stop at the earliest error. content <- B.safeReadFile fp res <- case content of Left s -> return $ Left s - Right b -> return $ parseJSONSpec parse format =<< eitherDecode b + Right b -> do case eitherDecode b of + Left e -> return $ Left e + Right v -> parseJSONSpec wrapper format v -- Complement the specification with any missing/implicit definitions let res' = fmap (addMissingIdentifiers ids) res @@ -159,6 +165,23 @@ standalone' fp options (ExprPair parse replace print ids) = do return copilot +-- | Parse a property using an auxiliary program to first translate it, if +-- available. +-- +-- If a program is given, it is first called on the property, and then the +-- result is parsed with the parser passed as an argument. If a program is not +-- given, then the parser is applied to the given string. +wrapVia :: Maybe String -- ^ Auxiliary program to translate the + -- property. + -> (String -> Either String a) -- ^ Parser used on the result. + -> String -- ^ Property to parse. + -> IO (Either String a) +wrapVia Nothing parse s = return (parse s) +wrapVia (Just f) parse s = + E.handle (\(e :: IOException) -> return $ Left $ show e) $ do + out <- readProcess f [] s + return $ parse out + -- | Options used to customize the conversion of specifications to Copilot -- code. data StandaloneOptions = StandaloneOptions @@ -168,6 +191,7 @@ data StandaloneOptions = StandaloneOptions , standalonePropFormat :: String , standaloneTypeMapping :: [(String, String)] , standaloneFilename :: String + , standalonePropVia :: Maybe String } -- * Error codes From a4cd9b28d58da37bac0fffbac857e4a43dc06a71 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Wed, 15 Jan 2025 00:45:46 +0000 Subject: [PATCH 4/8] ogma-core: Adjust tests to provide external processor to standalone command. Refs #197. There is a need in Ogma to make the frontend more versatile, and to extend it to support languages unknown to Ogma without users having to modify the code of Ogma itself. To that end, we want to empower users with the ability to use a custom command to transform individual properties into a format that Ogma understands, and have Ogma call that external command on demand. Prior commits have extended the standalone backend with the capability of taking an auxiliary command as argument and running it to transform individual properties. This commit modifies the tests for the standalone command to explicitly provide no extenal processor, indicating that the properties in the files tested are in a known format. --- ogma-core/tests/Main.hs | 2 ++ 1 file changed, 2 insertions(+) diff --git a/ogma-core/tests/Main.hs b/ogma-core/tests/Main.hs index 716d635e..88c67494 100644 --- a/ogma-core/tests/Main.hs +++ b/ogma-core/tests/Main.hs @@ -110,6 +110,7 @@ testFretComponentSpec2Copilot file success = do , standaloneFilename = "fret" , standaloneTargetDir = targetDir , standaloneTemplateDir = Nothing + , standalonePropVia = Nothing } result <- standalone file opts @@ -145,6 +146,7 @@ testFretReqsDBCoCoSpec2Copilot file success = do , standaloneFilename = "fret" , standaloneTargetDir = targetDir , standaloneTemplateDir = Nothing + , standalonePropVia = Nothing } result <- standalone file opts From 699d7d05b12deeaf920206f8cba8c7fe1743404b Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sun, 5 Jan 2025 23:55:45 +0000 Subject: [PATCH 5/8] ogma-cli: Provide ability to preprocess properties via external command. Refs #197. There is a need in Ogma to make the frontend more versatile, and to extend it to support languages unknown to Ogma without users having to modify the code of Ogma itself. To that end, we want to empower users with the ability to use a custom command to transform individual properties into a format that Ogma understands, and have Ogma call that external command on demand. Prior commits have extended the standalone backend with the capability of taking an auxiliary command as argument and running it to transform individual properties. This commit exposes that new argument to the user in the CLI. --- ogma-cli/src/CLI/CommandStandalone.hs | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/ogma-cli/src/CLI/CommandStandalone.hs b/ogma-cli/src/CLI/CommandStandalone.hs index 108e4a61..47be64f2 100644 --- a/ogma-cli/src/CLI/CommandStandalone.hs +++ b/ogma-cli/src/CLI/CommandStandalone.hs @@ -65,6 +65,7 @@ data CommandOpts = CommandOpts , standalonePropFormat :: String , standaloneTypes :: [String] , standaloneTarget :: String + , standalonePropVia :: Maybe String } -- | Transform an input specification into a Copilot specification. @@ -79,6 +80,7 @@ command c = standalone (standaloneFileName c) internalCommandOpts , Command.Standalone.standalonePropFormat = standalonePropFormat c , Command.Standalone.standaloneTypeMapping = types , Command.Standalone.standaloneFilename = standaloneTarget c + , Command.Standalone.standalonePropVia = standalonePropVia c } types :: [(String, String)] @@ -150,6 +152,13 @@ commandOptsParser = CommandOpts <> showDefault <> value "monitor" ) + <*> optional + ( strOption + ( long "parse-prop-via" + <> metavar "COMMAND" + <> help strStandalonePropViaDesc + ) + ) -- | Target dir flag description. strStandaloneTargetDirDesc :: String @@ -180,6 +189,11 @@ strStandaloneTargetDesc :: String strStandaloneTargetDesc = "Filename prefix for monitoring files in target language" +-- | External command to pre-process individual properties. +strStandalonePropViaDesc :: String +strStandalonePropViaDesc = + "Command to pre-process individual properties" + -- * Error codes -- | Encoding of reasons why the command can fail. From b98e970eba0e0afa9f9424982a78aaeae642679c Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Wed, 15 Jan 2025 00:13:04 +0000 Subject: [PATCH 6/8] ogma-language-jsonspec: Document changes in CHANGELOG. Refs #197. --- ogma-language-jsonspec/CHANGELOG.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/ogma-language-jsonspec/CHANGELOG.md b/ogma-language-jsonspec/CHANGELOG.md index 6c018ca7..249833d9 100644 --- a/ogma-language-jsonspec/CHANGELOG.md +++ b/ogma-language-jsonspec/CHANGELOG.md @@ -1,9 +1,10 @@ # Revision history for ogma-language-jsonspec -## [1.X.Y] - 2024-12-24 +## [1.X.Y] - 2025-01-14 * Add repository information to cabal package (#148). * Add version bounds to all dependencies (#119). +* Extend JSON spec parser to use an IO action to parse properties (#197). ## [1.5.0] - 2024-11-21 From 2056faa1d1831c1d22ae02e0126d6d545faa74e0 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Wed, 15 Jan 2025 00:13:57 +0000 Subject: [PATCH 7/8] ogma-core: Document changes in CHANGELOG. Refs #197. --- ogma-core/CHANGELOG.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/ogma-core/CHANGELOG.md b/ogma-core/CHANGELOG.md index 626ea3af..233f06b7 100644 --- a/ogma-core/CHANGELOG.md +++ b/ogma-core/CHANGELOG.md @@ -1,6 +1,6 @@ # Revision history for ogma-core -## [1.X.Y] - 2025-01-10 +## [1.X.Y] - 2025-01-14 * Replace queueSize with QUEUE_SIZE in FPP file (#186). * Use template expansion system to generate F' monitoring component (#185). @@ -8,6 +8,7 @@ * Add repository information to cabal package (#148). * Add version bounds to all dependencies (#119). * Add command to transform state diagrams into monitors (#194). +* Extend standalone command to use external process to parse properties (#197). ## [1.5.0] - 2024-11-21 From e148198cee74b19ee10e850503ec03403efe4372 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Wed, 15 Jan 2025 00:15:55 +0000 Subject: [PATCH 8/8] ogma-cli: Document changes in CHANGELOG. Refs #197. --- ogma-cli/CHANGELOG.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/ogma-cli/CHANGELOG.md b/ogma-cli/CHANGELOG.md index 015a50c7..2d29efb6 100644 --- a/ogma-cli/CHANGELOG.md +++ b/ogma-cli/CHANGELOG.md @@ -1,6 +1,6 @@ # Revision history for ogma-cli -## [1.X.Y] - 2025-01-10 +## [1.X.Y] - 2025-01-14 * Update contribution guidelines (#161). * Provide ability to customize template in fprime command (#185). @@ -8,6 +8,7 @@ * Add repository information to cabal package (#148). * Add version bounds to all dependencies (#119). * Introduce new diagram command (#194). +* Provide ability to preprocess properties via external command (#197). ## [1.5.0] - 2024-11-21