Merge branch 'develop-format-localfile' into develop. Close #200.

**Description**

Ogma allows users to select the format used for the JSON file, but only
known formats can be selected. Users should be able to pass a local file
containing a JSON format specification as an argument.

**Type**

- Feature: new capability.

**Additional context**

None.

**Requester**

- Ivan Perez.

**Method to check presence of bug**

Not applicable (not a bug).

**Expected result**

Users can provide a file as JSON format specification as argument.

The following dockerfile checks that a known format can still be used,
and that, if a custom provided format is specified in the command line,
it is picked up instead and used to parse the input file, in both cases
checking also that the resulting monitor compiles successfully, after
which it prints the message "Success":

```
--- Dockerfile-verify-200
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

ADD json-custom-format /tmp/json-custom-format
ADD properties.json /tmp/properties.json

CMD git clone $REPO && \
    cd $NAME && \
    git checkout $COMMIT && \
    cd .. && \
    cabal v1-install copilot-4.2 $NAME/$PAT**/ && \
    ogma standalone --input-format fdb --file-name $NAME/ogma-cli/examples/DB.json --target-dir output1 && \
    cabal v1-exec -- runhaskell -XPartialTypeSignatures -Wno-partial-type-signatures output1/Copilot.hs && \
    ogma standalone --input-format /tmp/json-custom-format --file-name /tmp/properties.json --target-dir output2 && \
    cabal v1-exec -- runhaskell output2/Copilot.hs && \
    echo "Success"

--- json-custom-format
JSONFormat
   { specInternalVars    = Just "..internal_vars[*]"
   , specInternalVarId   = ".name"
   , specInternalVarExpr = ".meaning"
   , specInternalVarType = Just ".type"
   , specExternalVars    = Just "..other_vars[*]"
   , specExternalVarId   = ".name"
   , specExternalVarType = Just ".type"
   , specRequirements    = "..requirements[*]"
   , specRequirementId   = ".id"
   , specRequirementDesc = Just ".text"
   , specRequirementExpr = ".formula"
   }

-- properties.json
{
  "spec": {
    "internal_vars": [],
    "other_vars": [
      {"name":"param", "type":"bool"}
    ],
    "requirements": [
      {
        "id":      "req001",
        "formula": "(H param)",
        "text":    "param is always true"
      }
    ]
  }
}
```

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-200
```

**Solution implemented**

`ogma-core` now checks if the file format name provided exists as a
local file, or if, judging by the name, it refers to a local file.
Otherwise, Ogma finds the file in the package's data directory.

If neither can be found, Ogma prints an error message telling the user
that the file cannot be found, and giving the file name it attempted to
access.

**Further notes**

None.

ogma-core/CHANGELOG.md

@@ -1,6 +1,6 @@
 # Revision history for ogma-core
 
-## [1.X.Y] - 2025-01-14
+## [1.X.Y] - 2025-01-19
 
 * Replace queueSize with QUEUE_SIZE in FPP file (#186).
 * Use template expansion system to generate F' monitoring component (#185).
@@ -9,6 +9,7 @@
 * 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).
+* Enable using user-provided file as format definition spec (#200).
 
 ## [1.5.0] - 2024-11-21
 

ogma-core/ogma-core.cabal

@@ -123,6 +123,7 @@ library
     , aeson                   >= 2.0.0.0  && < 2.2
     , bytestring              >= 0.10.8.2 && < 0.13
     , containers              >= 0.5      && < 0.8
+    , directory               >= 1.3.1.5  && < 1.4
     , filepath                >= 1.4.2    && < 1.6
     , graphviz                >= 2999.20  && < 2999.21
     , megaparsec              >= 8.0.0    && < 9.10

ogma-core/src/Command/Standalone.hs

@@ -44,8 +44,9 @@ import Control.Exception    as E
 import Data.Aeson           (decode, eitherDecode, object, (.=))
 import Data.ByteString.Lazy (fromStrict)
 import Data.Foldable        (for_)
-import Data.List            (nub, (\\))
+import Data.List            (isInfixOf, nub, (\\))
 import Data.Maybe           (fromMaybe)
+import System.Directory     (doesFileExist)
 import System.Process       (readProcess)
 import System.FilePath      ((</>))
 import Data.Text.Lazy       (pack)
@@ -138,32 +139,45 @@ standalone' fp options (ExprPair parse replace print ids) = do
   let name     = standaloneFilename options
       typeMaps = typeToCopilotTypeMapping options
 
-  -- Obtain format file
+  -- Obtain format file.
+  --
+  -- A format name that exists as a file in the disk always takes preference
+  -- over a file format included with Ogma. A file format with a forward slash
+  -- in the name is always assumed to be a user-provided filename.
+  -- Regardless of whether the file is user-provided or known to Ogma, we check
+  -- (again) whether the file exists, and print an error message if not.
+  let formatName = standaloneFormat options
+  exists  <- doesFileExist formatName
   dataDir <- getDataDir
-  let formatFile =
-        dataDir </> "data" </> "formats" </>
-          (standaloneFormat options ++ "_" ++ standalonePropFormat options)
-
-  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 -> 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
-
-  let copilot = spec2Copilot name typeMaps replace print =<< specAnalyze =<< res'
-
-  return copilot
+  let formatFile
+        | isInfixOf "/" formatName || exists
+        = formatName
+        | otherwise
+        = dataDir </> "data" </> "formats" </>
+             (standaloneFormat options ++ "_" ++ standalonePropFormat options)
+  formatMissing <- not <$> doesFileExist formatFile
+
+  if formatMissing
+    then return $ Left $ standaloneIncorrectFormatSpec formatFile
+    else 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 -> 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
+
+      return $ spec2Copilot name typeMaps replace print =<< specAnalyze =<< res'
 
 -- | Parse a property using an auxiliary program to first translate it, if
 -- available.
@@ -236,6 +250,12 @@ standaloneTemplateError options fp exception =
       ++ " permissions to write in the destination directory. "
       ++ show exception
 
+-- | Error message associated to the format file not being found.
+standaloneIncorrectFormatSpec :: String -> String
+standaloneIncorrectFormatSpec formatFile =
+  "The format specification " ++ formatFile ++ " does not exist or is not "
+  ++ "readable"
+
 -- * Mapping of types from input format to Copilot
 typeToCopilotTypeMapping :: StandaloneOptions -> [(String, String)]
 typeToCopilotTypeMapping options =