Support inequality operator in TL formulas in SMV and CoCoSpec. Refs #71.

[ivanperez-keera]

Add the inequality operator in the grammars of SMV and CoCoSpec, and add the appropriate translation in ogma-core, as prescribed in the solution proposed for #71.

[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=393cb1eda1034bbacfa0f3935bf3dc58c4d2173d" -it ogma-test

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

• [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 (internal change only).