Merge branch 'develop-mtl-ranges' into develop. Close #101.

**Description**

The current parser for the SMV language does not support MTL operators with
number ranges as arguments to MTL operators. The only syntax currently
supported is using `<MTLOperator>[<ComparisonOperator><Number>]`, where
<ComparisonOperator> is a numeric comparison operator like `<=`, `<`, and so
on.

This limitation makes some of the component specifications produced from FRET
not parseable with Ogma.

**Type**

- Bug/Feature/Maintenance: valid SMV properties cannot be parsed by Ogma.

**Additional context**

None.

**Requester**

- Giann Carlos Nandi (Instituto Superior de Engenharia do Porto).

**Method to check presence of bug**

Compiling a property that contains a number range in the `ptLTL` field currently fails:

```
$ ogma fret-reqs-db --fret-file-name /tmp/fret-reqs-db.json
fret-reqs-db.json: error: syntax error at line 1, column 3 before `2'
$ ogma fret-component-spec --fret-file-name /tmp/fret-reqs-cs.json
fret-reqs-cs.json: error: Error in $.Requirements[0]: error: parsing of ptLTL field of requirement "testCopilot-001" failed with syntax error at line 1, column 3 before `2'
```

The following Dockerfile uses the accompanying FRET component specification and
requirements DB containing MTL operators with number ranges in the past-time
LTL SMV formulas to generate the Copilot monitors both for the CS and Reqs DB
cases, and it compiles the resulting Copilot code.

```Dockerfile
--- Dockerfile-verify-101
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
RUN cabal v1-install copilot-3.16.1
RUN apt-get install --yes git

ADD fret-reqs-cs.json /tmp/fret-reqs-cs.json
ADD fret-reqs-db.json /tmp/fret-reqs-db.json

CMD git clone $REPO && \
    cd $NAME && \
    git checkout $COMMIT && \
    cd .. && \
    cabal v1-install $NAME/$PAT**/ && \
    ogma fret-component-spec --fret-file-name /tmp/fret-reqs-cs.json > CS.hs && \
    cabal v1-exec -- runhaskell CS.hs && \
    gcc -c fret.c && \
    ogma fret-reqs-db --fret-file-name /tmp/fret-reqs-db.json > DB.hs && \
    cabal v1-exec -- runhaskell DB.hs && \
    gcc -c fret.c && \
    echo "Success"

--- fret-reqs-cs.json
{
  "test_componentSpec": {
    "Functions": [
    ],
    "Internal_variables": [
    ],
    "Other_variables": [
      {
        "name": "signal",
        "type": "bool"
      }
    ],
    "Requirements": [
      {
        "CoCoSpecCode": "signal",
        "fretish": "unimportant",
        "name": "testCopilot-001",
        "ptLTL": "O[2,5] signal"
      }
    ]
  }
}

--- fret-reqs-db.json
[
    {
        "reqid": "test_req1",
        "parent_reqid": "",
        "project": "Test",
        "rationale": "",
        "fulltext": "",
        "semantics": {
            "type": "test",
            "ptExpanded": "O[2,5] signal",
            "CoCoSpecCode": "signal"
        }
    }
]
```

**Expected result**

Parsing files that include ranges with MTL operators compiles and produces
correct Copilot code.

Running the docker image above should print the message "Success", indicating
that the MTL operators with number ranges are being translated into correct
Copilot and C code.

**Solution implemented**

Modify SMV grammar to support number ranges as arguments to MTL operators.

Modify translation from SMV to Copilot to produce the equivalent number range
in Copilot's MTL implementation.

Modify requirements DB to Copilot backend to import MTL module qualified.

**Further notes**

None.

ogma-core/CHANGELOG.md

@@ -1,5 +1,9 @@
 # Revision history for ogma-core
 
+## [1.X.Y] - 2023-07-21
+
+* Support MTL operators with number ranges in SMV (#101).
+
 ## [1.0.10] - 2023-07-21
 
 * Version bump 1.0.10 (#98).

ogma-core/src/Language/Trans/FRETReqsDB2Copilot.hs

@@ -112,6 +112,7 @@ fret2CopilotModule' prefs smvSpec cocoSpec = unlines $ concat sections
       , "import           Copilot.Library.PTLTL     (since, previous,"
         ++ " alwaysBeen)"
       , "import qualified Copilot.Library.PTLTL     as PTLTL"
+      , "import qualified Copilot.Library.MTL       as MTL"
       , "import           Language.Copilot          (reify)"
       , "import Prelude                   hiding ((&&), (||), (++), (<=), (>=),"
         ++ " (<), (>), (==), (/=), not)"

ogma-core/src/Language/Trans/SMV2Copilot.hs

@@ -142,6 +142,7 @@ ordOp2Copilot OrdOpGE = ">="
 opOne2Copilot :: OpOne -> String
 opOne2Copilot (Op1Alone x)    = opOneAlone2Copilot x
 opOne2Copilot (Op1MTL x op v) = opOneMTL2Copilot x op v
+opOne2Copilot (Op1MTLRange op mn mx) = opOneMTLRange2Copilot op mn mx
 
 -- | Return the Copilot representation of a unary logical non-MTL FRET
 -- operator.
@@ -163,6 +164,15 @@ opOneMTL2Copilot operator _comparison number =
                              ++ " " ++ "clock" ++ " "
                              ++ show (1 :: Int)
 
+-- | Return the Copilot representation of a unary logical MTL FRET operator
+-- that uses an explicit range.
+opOneMTLRange2Copilot :: Op1Name -> Number -> Number -> String
+opOneMTLRange2Copilot operator mn mx =
+  opOneMTL2Copilot' operator ++ " " ++ number2Copilot mn
+                             ++ " " ++ number2Copilot mx
+                             ++ " " ++ "clock" ++ " "
+                             ++ show (1 :: Int)
+
 -- | Return the Copilot representation of a unary logical possibly MTL FRET
 -- operator.
 opOneMTL2Copilot' :: Op1Name -> String

ogma-language-smv/CHANGELOG.md

@@ -1,5 +1,9 @@
 # Revision history for ogma-language-smv
 
+## [1.X.Y] - 2023-07-21
+
+* Support MTL operators with number ranges (#101).
+
 ## [1.0.10] - 2023-07-21
 
 * Version bump 1.0.10 (#98).

ogma-language-smv/grammar/SMV.cf

@@ -83,8 +83,9 @@ BoolConstFalse. BoolConst ::= "FALSE";
 BoolConstFTP.   BoolConst ::= "FTP";
 BoolConstLAST.  BoolConst ::= "LAST";
 
-Op1Alone . OpOne ::= Op1Name;
-Op1MTL.    OpOne ::= Op1Name "[" OrdOp Number "]";
+Op1Alone .   OpOne ::= Op1Name;
+Op1MTL.      OpOne ::= Op1Name "[" OrdOp Number "]";
+Op1MTLRange. OpOne ::= Op1Name "[" Number "," Number "]";
 
 NumberInt . Number ::= Integer;
 _ . Number ::= "<b>" Number "</b>";