Merge branch 'develop-xml' into develop. Close #202.

**Description**

There is a need in Ogma to support XML-based input files, since this is
produced by many standard tools in the industry. Like with JSON, we want
users to be able to customize the input format via a command-line flag,
so that users can work with XML-based files whose format is previously
unknown to Ogma without having to modify the tool.

**Type**

- Feature: new capability.

**Additional context**

None.

**Requester**

- Ivan Perez.

**Method to check presence of bug**

Not applicable (not a bug).

**Expected result**

Ogma is able to process and extract data from an input file in XML,
obtaining information from a configuration file provided by the user.

The following dockerfile uses the new parser, together with a custom XML
format specification, to parse read properties from an input file and
generate a Copilot monitor, checking that the produced monitor compiles
correctly, after which it prints the message "Success":

```
--- Dockerfile-verify-202
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 xml-custom-format /tmp/xml-custom-format
ADD properties.xml /tmp/properties.xml

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

--- xml-custom-format
XMLFormat
  { specInternalVars    = Nothing
  , specInternalVarId   = ("//*", Nothing)
  , specInternalVarExpr = ("//*", Nothing)
  , specInternalVarType = Nothing
  , specExternalVars    = Nothing
  , specExternalVarId   = ("//*", Nothing)
  , specExternalVarType = Nothing
  , specRequirements    = ("//Requirement", Nothing)
  , specRequirementId   = ("//Requirement/@Id/text()", Nothing)
  , specRequirementDesc = Just ("//Requirement/@Id/text()", Nothing)
  , specRequirementExpr = ("//Requirement/@Text/text()", Nothing)
  }

--- properties.xml
<?xml version="1.0" encoding="UTF-8"?>
<Requirement name="REQ-1" Id="req1" Text="!go_too_fast" />
```

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

**Solution implemented**

Introduce a parsing library for XML files, and use it in `ogma-core` to
parse input files when the user specifies that the format is XML-based.

Add several XML format specifications for known formats used in
industrial applications.

**Further notes**

None.

ogma-core/CHANGELOG.md

@@ -10,6 +10,7 @@
 * 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).
+* Add support for XML files to standalone backend (#202).
 
 ## [1.5.0] - 2024-11-21
 

ogma-core/data/formats/xml-md_cocospec

@@ -0,0 +1,13 @@
+XMLFormat
+  { XML.specInternalVars    = Nothing
+  , XML.specInternalVarId   = ("//*", Nothing)
+  , XML.specInternalVarExpr = ("//*", Nothing)
+  , XML.specInternalVarType = Nothing
+  , XML.specExternalVars    = Nothing
+  , XML.specExternalVarId   = ("//*", Nothing)
+  , XML.specExternalVarType = Nothing
+  , XML.specRequirements    = ("//sysml:Requirement", Nothing)
+  , XML.specRequirementId   = ("//sysml:Requirement/@Id/text()", Nothing)
+  , XML.specRequirementDesc = Just ("//sysml:Requirement/@Id/text()", Nothing)
+  , XML.specRequirementExpr = ("//sysml:Requirement/@Text/text()", Nothing)
+  }

ogma-core/data/formats/xml-md_smv

@@ -0,0 +1,13 @@
+XMLFormat
+  { XML.specInternalVars    = Nothing
+  , XML.specInternalVarId   = ("//*", Nothing)
+  , XML.specInternalVarExpr = ("//*", Nothing)
+  , XML.specInternalVarType = Nothing
+  , XML.specExternalVars    = Nothing
+  , XML.specExternalVarId   = ("//*", Nothing)
+  , XML.specExternalVarType = Nothing
+  , XML.specRequirements    = ("//sysml:Requirement", Nothing)
+  , XML.specRequirementId   = ("//sysml:Requirement/@Id/text()", Nothing)
+  , XML.specRequirementDesc = Just ("//sysml:Requirement/@Id/text()", Nothing)
+  , XML.specRequirementExpr = ("//sysml:Requirement/@Text/text()", Nothing)
+  }

ogma-core/data/formats/xml-reqif_cocospec

@@ -0,0 +1,13 @@
+XMLFormat
+    { specInternalVars    = Nothing
+    , specInternalVarId   = ("//*", Nothing)
+    , specInternalVarExpr = ("//*", Nothing)
+    , specInternalVarType = Nothing
+    , specExternalVars    = Nothing
+    , specExternalVarId   = ("//*", Nothing)
+    , specExternalVarType = Nothing
+    , specRequirements    = ("//SPEC-OBJECTS/SPEC-OBJECT/TYPE/SPEC-OBJECT-TYPE-REF[contains(text(),\"KEY\")]/../..", Just ("KEY", "//SPEC-OBJECT-TYPE[contains(@LONG-NAME, \"Requirement\")]/@IDENTIFIER/text()"))
+    , specRequirementId   = ("//SPEC-OBJECT/@IDENTIFIER/text()", Nothing)
+    , specRequirementDesc = Just ("//ATTRIBUTE-VALUE-XHTML/DEFINITION/ATTRIBUTE-DEFINITION-XHTML-REF[contains(text(),'KEY')]/../../THE-VALUE/div/*", Just ("KEY", "//ATTRIBUTE-DEFINITION-XHTML[contains(@LONG-NAME, \"ReqIF.Name\")]/@IDENTIFIER/text()"))
+    , specRequirementExpr = ("//ATTRIBUTE-VALUE-XHTML/DEFINITION/ATTRIBUTE-DEFINITION-XHTML-REF[contains(text(),'KEY')]/../../THE-VALUE/div/*", Just ("KEY", "//ATTRIBUTE-DEFINITION-XHTML[contains(@LONG-NAME, \"ReqIF.Text\")]/@IDENTIFIER/text()"))
+    }

ogma-core/data/formats/xml-reqif_smv

@@ -0,0 +1,13 @@
+XMLFormat
+    { specInternalVars    = Nothing
+    , specInternalVarId   = ("//*", Nothing)
+    , specInternalVarExpr = ("//*", Nothing)
+    , specInternalVarType = Nothing
+    , specExternalVars    = Nothing
+    , specExternalVarId   = ("//*", Nothing)
+    , specExternalVarType = Nothing
+    , specRequirements    = ("//SPEC-OBJECTS/SPEC-OBJECT/TYPE/SPEC-OBJECT-TYPE-REF[contains(text(),\"KEY\")]/../..", Just ("KEY", "//SPEC-OBJECT-TYPE[contains(@LONG-NAME, \"Requirement\")]/@IDENTIFIER/text()"))
+    , specRequirementId   = ("//SPEC-OBJECT/@IDENTIFIER/text()", Nothing)
+    , specRequirementDesc = Just ("//ATTRIBUTE-VALUE-XHTML/DEFINITION/ATTRIBUTE-DEFINITION-XHTML-REF[contains(text(),'KEY')]/../../THE-VALUE/div/*", Just ("KEY", "//ATTRIBUTE-DEFINITION-XHTML[contains(@LONG-NAME, \"ReqIF.Name\")]/@IDENTIFIER/text()"))
+    , specRequirementExpr = ("//ATTRIBUTE-VALUE-XHTML/DEFINITION/ATTRIBUTE-DEFINITION-XHTML-REF[contains(text(),'KEY')]/../../THE-VALUE/div/*", Just ("KEY", "//ATTRIBUTE-DEFINITION-XHTML[contains(@LONG-NAME, \"ReqIF.Text\")]/@IDENTIFIER/text()"))
+    }

ogma-core/ogma-core.cabal

@@ -78,6 +78,10 @@ data-files:          templates/copilot-cfs/CMakeLists.txt
                      data/formats/fcs_cocospec
                      data/formats/fdb_smv
                      data/formats/fdb_cocospec
+                     data/formats/xml-md_cocospec
+                     data/formats/xml-md_smv
+                     data/formats/xml-reqif_cocospec
+                     data/formats/xml-reqif_smv
 
 -- Ogma packages should be uncurated so that only the official maintainers make
 -- changes.
@@ -137,6 +141,7 @@ library
     , ogma-language-copilot   >= 1.5.0 && < 1.6
     , ogma-language-jsonspec  >= 1.5.0 && < 1.6
     , ogma-language-smv       >= 1.5.0 && < 1.6
+    , ogma-language-xmlspec   >= 1.5.0 && < 1.6
     , ogma-spec               >= 1.5.0 && < 1.6
 
   hs-source-dirs:

ogma-core/src/Command/Standalone.hs

@@ -1,4 +1,5 @@
 {-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE MultiWayIf                #-}
 {-# LANGUAGE OverloadedStrings         #-}
 {-# LANGUAGE ScopedTypeVariables       #-}
 -- Copyright 2020 United States Government as represented by the Administrator
@@ -44,7 +45,7 @@ import Control.Exception    as E
 import Data.Aeson           (decode, eitherDecode, object, (.=))
 import Data.ByteString.Lazy (fromStrict)
 import Data.Foldable        (for_)
-import Data.List            (isInfixOf, nub, (\\))
+import Data.List            (isInfixOf, isPrefixOf, nub, (\\))
 import Data.Maybe           (fromMaybe)
 import System.Directory     (doesFileExist)
 import System.Process       (readProcess)
@@ -64,6 +65,7 @@ import Paths_ogma_core (getDataDir)
 import Data.OgmaSpec (ExternalVariableDef (..), InternalVariableDef (..),
                       Requirement (..), Spec (..))
 import Language.JSONSpec.Parser (JSONFormat (..), parseJSONSpec)
+import Language.XMLSpec.Parser  (parseXMLSpec)
 
 -- Internal imports: language ASTs, transformers
 import qualified Language.CoCoSpec.AbsCoCoSpec as CoCoSpec
@@ -135,7 +137,7 @@ standalone' :: FilePath
             -> StandaloneOptions
             -> ExprPair
             -> IO (Either String (String, String, String, String, String))
-standalone' fp options (ExprPair parse replace print ids) = do
+standalone' fp options (ExprPair parse replace print ids def) = do
   let name     = standaloneFilename options
       typeMaps = typeToCopilotTypeMapping options
 
@@ -160,19 +162,25 @@ standalone' fp options (ExprPair parse replace print ids) = do
   if formatMissing
     then return $ Left $ standaloneIncorrectFormatSpec formatFile
     else do
-      format <- read <$> readFile formatFile
+      format <- 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
+      res <-
+        if | isPrefixOf "XMLFormat" format
+           -> do let xmlFormat = read format
+                 content <- readFile fp
+                 parseXMLSpec wrapper def xmlFormat content
+           | otherwise
+           -> do let jsonFormat = read format
+                 content <- B.safeReadFile fp
+                 case content of
+                   Left s  -> return $ Left s
+                   Right b -> do case eitherDecode b of
+                                   Left e  -> return $ Left e
+                                   Right v -> parseJSONSpec wrapper jsonFormat v
 
       -- Complement the specification with any missing/implicit definitions
       let res' = fmap (addMissingIdentifiers ids) res
@@ -276,11 +284,15 @@ typeToCopilotTypeMapping options =
 
 -- | Handler for boolean expressions that knows how to parse them, replace
 -- variables in them, and convert them to Copilot.
+--
+-- It also contains a default value to be used whenever an expression cannot be
+-- found in the input file.
 data ExprPair = forall a . ExprPair
   { exprParse   :: String -> Either String a
   , exprReplace :: [(String, String)] -> a -> a
   , exprPrint   :: a -> String
   , exprIdents  :: a -> [String]
+  , exprUnknown :: a
   }
 
 -- | Return a handler depending on whether it should be for CoCoSpec boolean
@@ -291,10 +303,12 @@ exprPair "cocospec" = ExprPair (CoCoSpec.pBoolSpec . CoCoSpec.myLexer)
                                (\_ -> id)
                                (CoCoSpec.boolSpec2Copilot)
                                (CoCoSpec.boolSpecNames)
+                               (CoCoSpec.BoolSpecSignal (CoCoSpec.Ident "undefined"))
 exprPair _          = ExprPair (SMV.pBoolSpec . SMV.myLexer)
                                (substituteBoolExpr)
                                (SMV.boolSpec2Copilot)
                                (SMV.boolSpecNames)
+                               (SMV.BoolSpecSignal (SMV.Ident "undefined"))
 
 -- | Add to a spec external variables for all identifiers mentioned in
 -- expressions that are not defined anywhere.

ogma-language-xmlspec/CHANGELOG.md

@@ -0,0 +1,5 @@
+# Revision history for ogma-language-xmlspec
+
+## [1.X.Y] - 2024-01-27
+
+* Initial release (#202).

ogma-language-xmlspec/Setup.hs

@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain

ogma-language-xmlspec/ogma-language-xmlspec.cabal

@@ -0,0 +1,83 @@
+-- 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.
+
+cabal-version:       2.0
+build-type:          Simple
+
+name:                ogma-language-xmlspec
+version:             1.5.0
+homepage:            http://nasa.gov
+license:             OtherLicense
+license-file:        LICENSE.pdf
+author:              Ivan Perez, Alwyn Goodloe
+maintainer:          [email protected]
+category:            Aerospace
+extra-source-files:  CHANGELOG.md
+
+synopsis:            Ogma: Runtime Monitor translator: XML Frontend
+
+description:         Ogma is a tool to facilitate the integration of safe runtime monitors into
+                     other systems. Ogma extends
+                     <https://github.com/Copilot-Language/copilot Copilot>, a high-level runtime
+                     verification framework that generates hard real-time C99 code.
+                     .
+                     This library contains a frontend to read specifications from XML files.
+
+-- Ogma packages should be uncurated so that only the official maintainers make
+-- changes.
+--
+-- Because this is a NASA project, we want to make sure that users obtain
+-- exactly what we publish, unmodified by anyone external to our project.
+x-curation: uncurated
+
+library
+
+  exposed-modules:
+    Language.XMLSpec.Parser
+    Language.XMLSpec.PrintTrees
+
+  build-depends:
+      base                >= 4.11.0.0 && < 5
+    , mtl                 >= 2.2.2    && < 2.4
+    , hxt                 >= 9.3.1.4  && < 9.4
+    , hxt-regex-xmlschema >= 9.0      && < 9.3
+    , hxt-xpath           >= 8.5      && < 9.2
+    , pretty              >= 1.1      && < 1.2
+
+    , ogma-spec           >= 1.5.0 && < 1.6
+
+  hs-source-dirs:
+    src
+
+  default-language:
+    Haskell2010
+
+  ghc-options:
+    -Wall