`ogma-core`: Spec2Copilot backend does not perform variable substitution in top-level property names

[ivanperez-keera]

Description

When using property names as arguments to trigger, the Spec2Copilot backend does not apply the same variable/name substitution that was applied in their definition, thus referring in the call to trigger to an undefined argument.

Type

• Bug: code produced by backend does not compile.

Additional context

None.

Requester

• Ivan Perez

Method to check presence of bug

Running the backend with one of the examples available in ogma produces code that does not compile.

$ ogma fret-component-spec --fret-file-name ogma-core/tests/fret_good.json  > Example.hs
$ runhaskell Example.hs
Example.hs:58:35: error:
    Variable not in scope: behnazOne :: Stream Bool
   |
58 |   trigger "handlerbehnazOne" (not behnazOne) []

Expected result

When executed, the code produced by the Spec2Copilot backend does not report to an error due to a trigger stream identifier being undefined.

Desired result

When executed, the code produced by the Spec2Copilot backend does not report to an error due to a trigger stream identifier being undefined.

Proposed solution

Modify the definition of Spec2Copilot backend to apply the name substitution function to trigger argument names.

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/ogma-cli/ $NAME/ogma-core/ --enable-tests --constraint "ogma-language-fret-reqs -test" && \ cabal v1-install $NAME/ogma-cli/ $NAME/ogma-core/ --enable-tests --constraint "ogma-language-fret-reqs -test" --run-tests -j1

  Command:
  ```sh
  $ docker run -e "REPO=https://github.com/nasa/ogma" -e "NAME=ogma" -e PAT="ogma-" -e "COMMIT=448465b5d5bdbb4d62f051d7a27a475e1bdbc417" -it ogma-test

  • [X] The solution proposed fixes the issues described. Details: The following Dockerfile checks that the given given backend produces a Copilot spec that compiles, in which case it prints the message "Success".

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

  ADD sample.json /tmp/

  RUN cabal v1-install BNFC copilot-3.18.1

  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**/ && \ ogma fret-component-spec --fret-file-name /tmp/sample.json > sample.hs && \ cabal v1-exec -- runhaskell sample.hs && \ echo "Success"

  -- sample.json { "RTSASpec": { "Internal_variables": [], "Other_variables": [ {"name":"param", "type":"bool"} ], "Requirements": [ { "name": "one", "CoCoSpecCode": "true", "ptLTL": "((H (param) ))", "fretish": "Meaning not specified" } ] } }

  Command:

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

• [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: Bump not needed (bug fix to comply with intended API).

[ivanperez-keera]

Change Manager: Implementation ready to be merged.