ogma-core: equivalence operator should be translated to (==)

[Andersen0]

When using an equivalence operator (as used in, for example, FRETISH requirements as <=>) the returned Monitor will not be able to properly run because the Haskell Monitor cannot use the <==> operator that is defined in the code.

The command used for generation of the Monitor was:
ogma fret-component-spec --fret-file-name fret_specifications.json > Monitor.hs

The command used for compiling and linking:
ghc -package copilot-c99 -package copilot-language -package copilot-libraries Monitor.hs

Acquired error message:

Variable not in scope:
      (<==>) :: Stream Bool -> Stream Bool -> Stream Bool
    Suggested fix: Perhaps use ‘==>’ (imported from Copilot.Language)

Suggested fix:
Defining a custom infix operator that compares two boolean arguments and returns true if they are both true or both false

infix 4 <==>
(<==>) :: Stream (Bool) -> Stream (Bool) -> Stream (Bool)
a <==> b = a == b

[ivanperez-keera]

Thank you @Andersen0 . I can confirm that the issue is there. This will be an easy fix.

[ivanperez-keera]

Description

The SMV to Copilot translator translates equivalences as (<==>). However, that operator does not exist in Copilot, it is simply (==) for Bools.

Type

• Bug: backend generates incorrect code.

Additional context

None.

Requester

• Tage Andersen and Elias Evjen Hartmark (NMBU, Norway)

Method to check presence of bug

Compiling a specification with <-> in the ptLTL field produces Copilot code that does not compile:

{
  "test_componentSpec": {
    "Functions": [
    ],
    "Internal_variables": [
    ],
    "Other_variables": [
      {
        "name": "a",
        "type": "bool"
      }
    ],
    "Requirements": [
      {
        "CoCoSpecCode": "true",
        "fretish": "unimportant",
        "name": "testCopilot001",
        "ptLTL": "a <-> a"
      }
    ]
  }
}

    • Variable not in scope:
        (<==>) :: Stream Bool -> Stream Bool -> Stream Bool
    • Perhaps you meant ‘==>’ (imported from Copilot.Language)
   |
20 | propTestCopilot001 = (a <==> a)

Expected result

The execution above should produce a Copilot specification that can be compiled and where == is used in Copilot where an equivalence between booleans needs to be expressed.

Desired result

The execution above should produce a Copilot specification that can be compiled and where == is used in Copilot where an equivalence between booleans needs to be expressed.

Proposed solution

Modify the SMV translator to use (==) instead of <==>.

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 fixing in Ogma 1.3.

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=d3ebffca2227cd61e1ea3e520fb5610f487e3633" -it ogma-test

  • The solution proposed fixes the issues described. Details:
    The following Dockerfile uses the spec containing an equivalence operator in the SMV property, and it compiles the resulting Copilot code.

    --- Dockerfile-verify-126
    FROM ubuntu:trusty
    
    ENV DEBIAN_FRONTEND=noninteractive
    
    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.18.1
    RUN apt-get install --yes git
    
    ADD reqs.json /tmp/reqs.json
    
    CMD git clone $REPO && \
        cd $NAME && \
        git checkout $COMMIT && \
        cd .. && \
        cabal v1-install $NAME/$PAT**/ && \
        ogma fret-component-spec --fret-file-name /tmp/reqs.json > CS.hs && \
        cabal v1-exec -- ghc --make CS.hs && \
        echo "Success"
    
    --- reqs.json
    {
      "test_spec": {
        "Functions": [
        ],
        "Internal_variables": [
        ],
        "Other_variables": [
          {
            "name": "a",
            "type": "bool"
          }
        ],
        "Requirements": [
          {
            "CoCoSpecCode": "true",
            "fretish": "unimportant",
            "name": "testCopilot001",
            "ptLTL": "a <-> a"
          }
        ]
      }
    }

    Command:

    $ docker run -e "REPO=https://github.com/nasa/ogma" -e "NAME=ogma" -e PAT="ogma-" -e "COMMIT=d3ebffca2227cd61e1ea3e520fb5610f487e3633" -it ogma-verify-126

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