Properties with number ranges are not supported

[ivanperez-keera]

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 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'

using as files:`

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

--- 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"
      }
    ]
  }
}

Expected result

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

Desired result

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

Proposed solution

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.

Further notes

None.

[ivanperez-keera]

Change Manager: Confirmed that the issue exists.

[ivanperez-keera]

Technical Lead: Confirmed that the issue should be addressed.

[ivanperez-keera]

Technical Lead: Issue scheduled for Ogma 1.0.11.

Fix assigned to: @ivanperez-keera.

[ivanperez-keera]

Implementor: Solution implemented, review requested.

[ivanperez-keera]

Change Manager: Verified that:

• Solution is implemented:

  • The code proposed compiles passes the tests. Details:
    Docker image:

    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 apt-get install --yes git
    
    # We install the application first and then test it, in case any tests need to
    # run the tool.
    CMD git clone $REPO && \
        cd $NAME && \
        git checkout $COMMIT && \
        cd .. && \
        cabal v1-install $NAME/$PAT**/ --enable-tests && \
        cabal v1-install $NAME/$PAT**/ --enable-tests --run-tests -j1

    Command:

    $ docker run -e "REPO=https://github.com/ivanperez-keera/ogma" -e "NAME=ogma" -e PAT="ogma-" -e "COMMIT=ca7317116df57fa6faf703b9ee31dd935ea9a08c" -it ogma-test

  • The solution proposed fixes the issues described. Details:
    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-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"
            }
        }
    ]

    Command:

    $ docker run -e "REPO=https://github.com/ivanperez-keera/ogma" -e "NAME=ogma" -e PAT="ogma-" -e "COMMIT=ca7317116df57fa6faf703b9ee31dd935ea9a08c" -it ogma-verify-101

• Implementation is documented. Details:
  No changes needed.
• Change history is clear.
• Commit messages are clear.
• Changelogs are updated.
• Examples are updated. Details:
  No examples affected.
• Required version bumps are evaluated. Details:
  No bump needed (internal change).

[ivanperez-keera]

Change Manager: Implementation ready to be merged.