Add FPrime support

[ivanperez-keera]

Description

We have determined that supporting FPrime would generally be useful for Ogma and related projects (e.g., FRET). a backend for FPrime should be officially added.

Type

• New feature.

Additional context

None.

Requester

• Ivan Perez

Method to check presence of bug

A sample FRET file can be compiled into a FPrime monitoring node and package, and compilation in a FPrime docker image succeeds.

Expected result

Ogma provides a new command to generate a FPrime monitoring package, akin to the one provided for cFS.

Desired result

Ogma provides a new command to generate a FPrime monitoring package, akin to the one provided for cFS.

Proposed solution

Update ogma-core with the new command to generate FPrime package. Expose command via ogma-cli.

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 Ogma 1.(0+X).(7+Y).

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

  • [X] 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 .

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

[ivanperez-keera]

Change Manager: Implementation ready to be merged.