Handle CoCoSpec's ZtoPre and YtoPre unary operators. Refs #86.

[ivanperez-keera]

Extend CoCoSpec grammar with and add translation to Copilot for unary operators ZtoPre and YtoPre, as prescribed in the solution proposed for #86.

[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=6a1054f489edf4373831f8997c06d118db375d35" -it ogma-test

  • The solution proposed fixes the issues described. Details:
    The following Dockerfile runs the FRET to Copilot translators on the accompanying FRET component specification and FRET requirements DB, which contain ZtoPre and YtoPre in the CoCoSpec formulas.

    --- Dockerfile-verify-86
    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.15
    RUN apt-get install --yes git
    
    ADD fret-reqs-db.json /tmp/fret-reqs-db.json
    ADD fret-reqs-cs.json /tmp/fret-reqs-cs.json
    
    CMD git clone $REPO && \
        cd $NAME && \
        git checkout $COMMIT && \
        cd .. && \
        cabal v1-install $NAME/$PAT**/ && \
        ogma fret-reqs-db --fret-file-name /tmp/fret-reqs-db.json --cocospec > DB.hs && \
        cabal v1-exec -- ghc --make DB.hs && \
        ogma fret-component-spec --fret-file-name /tmp/fret-reqs-cs.json --cocospec > CS.hs && \
        cabal v1-exec -- ghc --make CS.hs && \
        echo "Success"
    
    --- fret-reqs-cs.json
    {
      "test_componentSpec": {
        "Functions": [
        ],
        "Internal_variables": [
        ],
        "Other_variables": [
          {
            "name": "signal",
            "type": "bool"
          }
        ],
        "Requirements": [
          {
            "CoCoSpecCode": "ZtoPre(signal) and YtoPre(signal)",
            "fretish": "unimportant",
            "name": "testCopilot-001",
            "ptLTL": "TRUE"
          }
        ]
      }
    }
    
    --- fret-reqs-db.json
    [
        {
            "reqid": "test_req1",
            "parent_reqid": "",
            "project": "Test",
            "rationale": "",
            "fulltext": "",
            "semantics": {
                "type": "test",
                "ptExpanded": "TRUE",
                "CoCoSpecCode": "ZtoPre(signal) and YtoPre(signal)"
            }
        }
    ]

    Command:

    $ docker run -e "REPO=https://github.com/NASA/ogma" -e "NAME=ogma" -e PAT="ogma-" -e "COMMIT=6a1054f489edf4373831f8997c06d118db375d35" -it ogma-verify-86

• Implementation is documented. Details:
  No changes needed (Change is internal).
• 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).