Change Manager: Confirmed that the issue exists.

Technical Lead: Confirmed that the issue should be addressed.

Technical Lead: Issue scheduled for Ogma 1.(0+X).(7+Y).

Fix assigned to: @ivanperez-keera.

Implementor: Solution implemented, review requested.

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

  • The solution proposed fixes the issues described. Details:
    The following following Dockerfile uses the accompanying FRET component specification containing inequalities in the TL formulas to generate the FPrime monitoring component and the Copilot monitors. The output produces a second Dockerfile that can be used to compile the generated monitoring component as part of FPrime's reference application. The fprime-variables-db file added contains an extra variable just to add some noise to the test:

    --- Dockerfile-verify-77
    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
    RUN apt-get install --yes git
    
    ADD file.json .
    ADD fprime-variable-db .
    
    CMD git clone $REPO && \
        cd $NAME && \
        git checkout $COMMIT && \
        cd .. && \
        cabal v1-install $NAME/$PAT**/ --enable-tests && \
        ogma fprime --app-target-dir fprime_demo --fret-file-name file.json --variable-db fprime-variable-db && \
        ogma fret-component-spec --fret-file-name file.json > Spec.hs && \
        sed -i -e 's/"fret/"copilot/g' Spec.hs && \
        cabal v1-exec -- runhaskell Spec.hs && \
        mv copilot.c copilot.h copilot_types.h fprime_demo/
    
    --- fprime-variable-db
    ("pullup", "bool")
    ("input", "float")
    
    --- 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:

    $ docker run -v $PWD/output:/fprime_demo -e "REPO=https://github.com/NASA/ogma" -e "NAME=ogma" -e PAT="ogma-" -e "COMMIT=76fc7b0bce982619f30376ebf6ac6b4260e91224" -it ogma-verify-77
    $ cd output/
    $ docker build -t ogma-verify-77-fprime .

• Implementation is documented. Details:
  • New module is documented.
  • Cabal files are documented.
  • README is documented.
• 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 (new feature introduced).

Change Manager: Implementation ready to be merged.