`ogma-core`: Spec2Copilot translator does not sanitize handler names

[ivanperez-keera]

Description

The Spec to Copilot translator is not sanitizing handler names. This causes the Copilot generated code not to compile if the property identifiers have a hyphen.

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 a hyphen in a requirement name produces Copilot code that does not compile:

{
  "test_componentSpec": {
    "Functions": [
    ],
    "Internal_variables": [
    ],
    "Other_variables": [
    ],
    "Requirements": [
      {
        "CoCoSpecCode": "true",
        "fretish": "unimportant",
        "name": "testCopilot-001",
        "ptLTL": "TRUE"
      }
    ]
  }
}

Monitor.hs: '-' is not a nondigit
CallStack (from HasCallStack):
  error, called at src/Language/C99/Util/Expr.hs:78:10 in language-c99-util-0.2.0-987ZdxxqOvYC4hudkeZk8i:Language.C99.Util.Expr

Expected result

The execution above should produce a Copilot specification that can be compiled and where - has been converted to an underscore.

Desired result

The execution above should produce a Copilot specification that can be compiled and where - has been converted to an underscore.

Proposed solution

Modify the Spec translator to sanitize handler names the same way that the ROS backend does.

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:

  • [X] 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:
  ```sh
  $ docker run -e "REPO=https://github.com/nasa/ogma" -e "NAME=ogma" -e PAT="ogma-" -e "COMMIT=7ce5a4058a1f0527d1051b84406446a15a0ba31d" -it ogma-test

  • [X] 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-127
    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.19 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 --force-reinstall $NAME/$PAT**/ && \ ogma fret-component-spec --fret-file-name /tmp/reqs.json --target-file-name monitor > CS.hs && \ cabal v1-exec -- runhaskell CS.hs && \ gcc -c monitor.c && \ echo "Success"

  --- reqs.json { "test_componentSpec": { "Functions": [ ], "Internal_variables": [ ], "Other_variables": [ ], "Requirements": [ { "CoCoSpecCode": "true", "fretish": "unimportant", "name": "testCopilot-001", "ptLTL": "TRUE" } ] } }

  Command:
  ```sh
  $ docker run -e "REPO=https://github.com/nasa/ogma" -e "NAME=ogma" -e PAT="ogma-" -e "COMMIT=7ce5a4058a1f0527d1051b84406446a15a0ba31d" -it ogma-verify-127

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

[ivanperez-keera]

Change Manager: Implementation ready to be merged.