Inequality is not supported

[ivanperez-keera]

Description

Requirements that contain inequalities in conditions in the TL formulas fail to be parsed correctly by Ogma.

Type

• Bug: valid FRET file cannot be parsed by Ogma.

Additional context

None.

Requester

• Alexander Will (Virginia Commonwealth University).

Method to check presence of bug

The following command reports an error instead of producing a monitor specification.

$ ogma fret-component-spec --fret-file-name file.json

where file.json contains the following:

{
  "mySpec": {
    "Internal_variables": [ ],
    "Other_variables": [ {"name":"input", "type":"real"} ],
    "Functions": [ ],
    "Requirements": [
      { "name": "REQ",
        "ptLTL": "(H (input != 30.0))",
        "CoCoSpecCode": "(H( input <> 30.0 ))",
        "fretish": "Irrelevant for the example"
      }
    ]
  }
}

The error produced is:

$ ogma fret-component-spec --fret-file-name file.json
file.json: error: syntax error at line 1, column 10 before `!'
$ ogma fret-component-spec --cocospec --fret-file-name file.json
file.json: error: syntax error at line 1, column 11 before `>'

Expected result

The json file above should be usable with Ogma and produce a valid Copilot monitor.

Desired result

The json file above should be usable with Ogma and produce a valid Copilot monitor.

Proposed solution

Modify SMV grammar to accept inequality. Adjust the rest of Ogma accordingly (e.g., translation to Copilot).

Modify CoCoSpec grammar to accept inequality. Adjust the rest of Ogma accordingly (e.g., translation to Copilot).

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+X).(7+Y).

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/NASA/ogma" -e "NAME=ogma" -e PAT="ogma-" -e "COMMIT=393cb1eda1034bbacfa0f3935bf3dc58c4d2173d" -it ogma-test

  • The solution proposed fixes the issues described. Details:
    The following Dockerfile uses the accompanying FRET component specification containing inequalities in the TL formulas to generate the Copilot monitors both for the SMV and CoCoSpec cases, and it compiles the resulting Copilot code.

    --- Dockerfile-verify-71
    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.13
    RUN apt-get install --yes git
    
    ADD file.json /tmp/file.json
    
    CMD git clone $REPO && \
        cd $NAME && \
        git checkout $COMMIT && \
        cd .. && \
        cabal v1-install $NAME/$PAT**/ && \
        ogma fret-component-spec --fret-file-name /tmp/file.json > SMV.hs && \
        cabal v1-exec -- runhaskell SMV.hs && \
        gcc -c fret.c && \
        ogma fret-component-spec --fret-file-name /tmp/file.json --cocospec > CoCoSpec.hs && \
        cabal v1-exec -- runhaskell CoCoSpec.hs && \
        gcc -c fret.c && \
        echo "Success"
    
    --- file.json
    {
      "mySpec": {
        "Internal_variables": [ ],
        "Other_variables": [ {"name":"input", "type":"real"} ],
        "Functions": [ ],
        "Requirements": [
          { "name": "REQ",
            "ptLTL": "(H (input != 30.0))",
            "CoCoSpecCode": "(H( input <> 30.0 ))",
            "fretish": "Irrelevant for the example"
          }
        ]
      }
    }

    Command:

    $ docker run -e "REPO=https://github.com/NASA/ogma" -e "NAME=ogma" -e PAT="ogma-" -e "COMMIT=393cb1eda1034bbacfa0f3935bf3dc58c4d2173d" -it ogma-verify-71

• 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 only).

[ivanperez-keera]

Change Manager: Implementation ready to be merged.