Merge branch 'develop-prefilters' into develop. Close nasa#197.

**Description**

There is a need in Ogma to extend it with the ability to make the
frontend more versatile, and to support languages unknown to Ogma
without users having to modify the code of Ogma itself.  For example, a
user might want to support a formal language unknown to Ogma, or use an
LLM to transform properties in English into monitors. 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.

**Type**

- Feature: New capability.

**Additional context**

None.

**Requester**

- Ivan Perez.

**Method to check presence of bug**

Not applicable (not a bug).

**Expected result**

Ogma provides an argument to the standalone command that empowers users
with the ability to specify a pre-filter or pre-processor to transform
properties into a format understood by Ogma.

The following Dockerfile uses the new flag to produce a Copilot monitor
from a spec while replacing all expressions are replaced by the
constantly true value / stream, and compiles the resulting Copilot
specification, after which it prints the message "Success":

```Dockerfile
FROM ubuntu:trusty

RUN apt-get update

RUN apt-get install --yes software-properties-common
RUN add-apt-repository ppa:hvr/ghc
RUN apt-get update

RUN apt-get install --yes ghc-8.6.5 cabal-install-2.4
RUN apt-get install --yes libz-dev

ENV PATH=/opt/ghc/8.6.5/bin:/opt/cabal/2.4/bin:$PWD/.cabal-sandbox/bin:$PATH

RUN cabal update
RUN cabal v1-sandbox init
RUN cabal v1-install alex happy --constraint='happy < 2.0'
RUN apt-get install --yes git

RUN echo "#!/bin/bash" >> /tmp/alwaystrue
RUN echo "echo TRUE" >> /tmp/alwaystrue
RUN chmod a+x /tmp/alwaystrue

CMD git clone $REPO && \
    cd $NAME && \
    git checkout $COMMIT && \
    cd .. && \
    cabal v1-install copilot-4.2 $NAME/$PAT**/ --enable-tests && \
    ogma standalone --input-format fdb --file-name $NAME/ogma-cli/examples/DB.json --target-dir output --parse-prop-via /tmp/alwaystrue && \
    cabal v1-exec -- runhaskell output/Copilot.hs && \
    echo "Success"
```

Command (substitute variables based on new path after merge):
```sh
$ docker run -e "REPO=https://github.com/NASA/ogma" -e "NAME=ogma" -e "PAT=ogma"  -e "COMMIT=<HASH>" -it ogma-verify-197
```

**Proposed solution**

Modify JSON spec parser in `ogma-language-jsonspec` to be able to use an
external command (e.g., `IO`) to parse individual properties.

Modify existing backends in `ogma-core` to adapt to change in JSON spec
parser.

Modify standalone command in `ogma-core` to receive an additional
argument with the name of a program to use to pre-process properties.

Modify tests in `ogma-core` to provide the new arguments to the
standalone backend so that tests keep working.

Modify `ogma-cli` to give users the ability to pick a preprocessor
via an optional input argument (exposing the corresponding argument from
`ogma-core`).

**Further notes**

None.

ogma-cli/CHANGELOG.md

@@ -1,13 +1,14 @@
 # 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).
 * Provide ability to customize template in standalone command (#189).
 * 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
 

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.

ogma-core/CHANGELOG.md

@@ -1,13 +1,14 @@
 # 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).
 * Use template expansion system to generate standalone Copilot monitor (#189).
 * 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
 

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

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.

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.

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

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
 

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
 

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

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,22 +151,22 @@ parseJSONSpec parseExpr jsonFormat value = do
                    , externalVariableType    = varType
                    }
 
-  externalVariableDefs <- mapM externalVarDef values
+  externalVariableDefs <- except $ mapM externalVarDef values
 
   let values :: [Value]
       values = executeJSONPath (jfiRequirements jsonFormatInternal) value
 
       -- 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