Skip to content

Commit

Permalink
Merge branch 'develop-fprime-templates' into develop. Close #185.
Browse files Browse the repository at this point in the history
**Description**

The F' application generation backend uses a fixed template to generate
the f' application. That template does not fit all use cases, so we are
finding users heavily modifying the output (which is hard to keep up
with when there are changes), and or not using ogma altogether for that
reason.

Allowing users to pick their own F' template would make Ogma more
versatile.

**Type**

- Feature: Enable customizing output produced.

**Additional context**

None.

**Requester**

- Ivan Perez.

**Method to check presence of bug**

Not applicable (not a bug).

**Expected result**

Ogma allows users to pick the custom F' application template they want
to use instead of relying on the one provided by default.

The following dockerfile generates the F' component using the default
template and using a copy and the default template and checks that both
are the same. It then adds a file to the copy of the template and checks
that the file is copied to the target directory when the custom template
is used, after which it prints the message "Success". Compiling the
produced component completes successfully:

```
--- fprime-handlers
handlerMyProperty

--- fprime-variable-dbs
("pullup", "bool")
("input", "float")

--- fprime-variables
variables

--- Monitor.hs
import           Copilot.Compile.C99
import           Copilot.Language      hiding (prop)
import qualified Copilot.Library.PTLTL as PTLTL
import           Language.Copilot      (reify)
import           Prelude               hiding (not, (/=))

input :: Stream Float
input = extern "input" Nothing

myProperty :: Stream Bool
myProperty = PTLTL.alwaysBeen (input /= 30.0)

spec :: Spec
spec = do
  trigger "handlerMyProperty" (not myProperty) []

main :: IO ()
main = reify spec >>= compile "copilot"

--- Dockerfile
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 apt-get install --yes git

ADD fprime-variables    /tmp/fprime-variables
ADD fprime-handlers     /tmp/fprime-handlers
ADD fprime-variable-dbs /tmp/fprime-variable-dbs
ADD Monitor.hs          /tmp/Monitor.hs

CMD git clone $REPO                                                              && \
    cd $NAME                                                                     && \
    git checkout $COMMIT                                                         && \
    cd ..                                                                        && \
    cp -r $NAME/ogma-core/templates/fprime custom-template-fprime                && \
    cabal v1-sandbox init                                                        && \
    cabal v1-install copilot $NAME/$PAT**/                                          \
      --constraint="aeson>=2.0.3.0"                                                 \
      --constraint="copilot>=4.1"                                                   \
      --constraint="copilot-core>=4.1"                                              \
      --constraint="copilot-language>=4.1"                                          \
      --constraint="copilot-theorem>=4.1"                                           \
      --constraint="copilot-c99>=4.1"                                               \
      --constraint="copilot-interpreter>=4.1"                                       \
      --constraint="copilot-prettyprinter>=4.1"                                  && \
    ./.cabal-sandbox/bin/ogma fprime --app-target-dir original                      \
                                     --variable-file /tmp/fprime-variables          \
                                     --handlers-file /tmp/fprime-handlers           \
                                     --variable-db /tmp/fprime-variable-dbs      && \
    ./.cabal-sandbox/bin/ogma fprime --app-target-dir new                           \
                                     --app-template-dir custom-template-fprime      \
                                     --variable-file /tmp/fprime-variables          \
                                     --handlers-file /tmp/fprime-handlers           \
                                     --variable-db /tmp/fprime-variable-dbs      && \
    diff -rq original new                                                        && \
    rm -rf new/*                                                                 && \
    echo "Success" >> custom-template-fprime/test                                && \
    ./.cabal-sandbox/bin/ogma fprime --app-target-dir new                           \
                                     --app-template-dir custom-template-fprime      \
                                     --variable-file /tmp/fprime-variables          \
                                     --handlers-file /tmp/fprime-handlers           \
                                     --variable-db /tmp/fprime-variable-dbs      && \
    cabal v1-exec -- runhaskell /tmp/Monitor.hs                                  && \
    mv copilot* new/                                                             && \
    cat new/test
```

Command (substitute variables based on new path after merge):

```sh
$ docker run -v $PWD/fprime_demo/:/new -e "REPO=https://github.com/NASA/ogma" -e "NAME=ogma" -e "PAT=ogma"  -e "COMMIT=<HASH>" -it ogma-verify-185
$ cd fprime_demo
$ docker build -t ogma-verify-185-fprime -f Dockerfile .
```

**Solution implemented**

Modify `ogma-core` to use variable expansion based on mustache to create
the output files.

Modify `ogma-core`'s template to use the variables used by the F'
component generation module.

Modify `ogma-core` to give users the ability to pick a template
directory via an optional input argument.

Modify `ogma-cli` to give users the ability to pick a template directory
via an optional input argument (exposing the corresponding argument from
`ogma-core`).

Modify `README` to demonstrate new capability.

Deprecate functions from `ogma-extra` that no package needs anymore.

**Further notes**

None.
  • Loading branch information
ivanperez-keera committed Dec 6, 2024
2 parents 786cc80 + 56e2467 commit c4060bf
Show file tree
Hide file tree
Showing 11 changed files with 387 additions and 280 deletions.
3 changes: 2 additions & 1 deletion ogma-cli/CHANGELOG.md
Original file line number Diff line number Diff line change
@@ -1,8 +1,9 @@
# Revision history for ogma-cli

## [1.X.Y] - 2024-11-23
## [1.X.Y] - 2024-11-26

* Update contribution guidelines (#161).
* Provide ability to customize template in fprime command (#185).

## [1.5.0] - 2024-11-21

Expand Down
62 changes: 62 additions & 0 deletions ogma-cli/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -401,6 +401,7 @@ F' components are generated using the Ogma command `fprime`, which receives
five main arguments:
- `--app-target-dir DIR`: location where the F' application files must be
stored.
- `--app-template-dir DIR`: directory holding F' component source template.
- `--variable-file FILENAME`: a file containing a list of variables that must
be made available to the monitor.
- `--variable-db FILENAME`: a file containing a database of known variables,
Expand Down Expand Up @@ -464,6 +465,67 @@ $ cat handlers
handlerpropREQ_001
```

### Template Customization

By default, Ogma uses a pre-defined template to generate the F' monitoring
component. It's possible to customize the output by providing a directory with
a set of files with an F' component template, which Ogma will use instead.

To choose this feature, one must call Ogma's `fprime` command with the argument
`--app-template-dir DIR`, where `DIR` is the path to a directory containing an
F' component specification template. For example, assuming that the directory
`my_template` contains a custom F' component template, one can execute:

```
$ ogma fprime --app-template-dir my_template/ --handlers filename --variable-file variables --variable-db fprime-variable-db --app-target-dir fprime_demo
```

Ogma will copy the files in that directory to the target path, filling in
several holes with specific information. For the component interface, the
variables are:

- {{{ifaceTypePorts}}}: Contain the type declarations for the types used by the
ports.

- {{{ifaceInputPorts}}}: Contains the declarations of the `async input` port,
to provide information needed by the monitors.

- {{{ifaceViolationEvents}}}: Contains the output port declarations, used to
emit property violations.

For the monitor's header file, the variables are:

- {{{hdrHandlers}}}: Contains the declarations of operations to execute when
new information is received in an input port, prior to re-evaluating the
monitors.

For the monitor's implementation, the variables are:

- {{{implInputs}}}: Contains the declarations of the variables with inputs
needed by the monitor.

- {{{implMonitorResults}}}: Contains the declarations of boolean variables,
each holding the result of the evaluation of one of the monitors.

- {{{implInputHandlers}}}: Contains the implementations of operations to
execute when new information is received in an input port, prior to
re-evaluating the monitors.

- {{{implTriggerResultReset}}}: Contains instructions that reset the status of
the monitors.

- {{{implTriggerChecks}}}: Contains instructions that check whether any monitor
has resulted in a violation and, if so, sends an event via the corresponding
port.

- {{{implTriggers}}}: Contains the implementations of the functions that set
the result of a monitor evaluation to true when the Copilot implementation
finds a violation.

We understand that this level of customization may be insufficient for your
application. If that is the case, feel free to reach out to our team to discuss
how we could make the template expansion system more versatile.

### Current limitations

The user must place the code generated by Copilot monitors in three files,
Expand Down
24 changes: 19 additions & 5 deletions ogma-cli/src/CLI/CommandFPrimeApp.hs
Original file line number Diff line number Diff line change
Expand Up @@ -56,11 +56,12 @@ import Command.FPrimeApp ( ErrorCode, fprimeApp )

-- | Options needed to generate the FPrime component.
data CommandOpts = CommandOpts
{ fprimeAppTarget :: String
, fprimeAppFRETFile :: Maybe String
, fprimeAppVarNames :: Maybe String
, fprimeAppVarDB :: Maybe String
, fprimeAppHandlers :: Maybe String
{ fprimeAppTarget :: String
, fprimeAppTemplateDir :: Maybe String
, fprimeAppFRETFile :: Maybe String
, fprimeAppVarNames :: Maybe String
, fprimeAppVarDB :: Maybe String
, fprimeAppHandlers :: Maybe String
}

-- | Create <https://github.com/nasa/fprime FPrime> component that subscribe
Expand All @@ -72,6 +73,7 @@ command :: CommandOpts -> IO (Result ErrorCode)
command c =
fprimeApp
(fprimeAppTarget c)
(fprimeAppTemplateDir c)
(fprimeAppFRETFile c)
(fprimeAppVarNames c)
(fprimeAppVarDB c)
Expand All @@ -94,6 +96,13 @@ commandOptsParser = CommandOpts
<> value "fprime"
<> help strFPrimeAppDirArgDesc
)
<*> optional
( strOption
( long "app-template-dir"
<> metavar "DIR"
<> help strFPrimeAppTemplateDirArgDesc
)
)
<*> optional
( strOption
( long "fret-file-name"
Expand Down Expand Up @@ -127,6 +136,11 @@ commandOptsParser = CommandOpts
strFPrimeAppDirArgDesc :: String
strFPrimeAppDirArgDesc = "Target directory"

-- | Argument template directory to FPrime component generation command
strFPrimeAppTemplateDirArgDesc :: String
strFPrimeAppTemplateDirArgDesc =
"Directory holding F' component source template"

-- | Argument FRET CS to FPrime component generation command
strFPrimeAppFRETFileNameArgDesc :: String
strFPrimeAppFRETFileNameArgDesc =
Expand Down
1 change: 1 addition & 0 deletions ogma-core/CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@
## [1.X.Y] - 2024-12-04

* Replace queueSize with QUEUE_SIZE in FPP file (#186).
* Use template expansion system to generate F' monitoring component (#185).

## [1.5.0] - 2024-11-21

Expand Down
3 changes: 3 additions & 0 deletions ogma-core/ogma-core.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -66,6 +66,9 @@ data-files: templates/copilot-cfs/CMakeLists.txt
templates/ros/copilot/src/copilot_monitor.cpp
templates/ros/copilot/package.xml
templates/fprime/CMakeLists.txt
templates/fprime/Copilot.cpp
templates/fprime/Copilot.fpp
templates/fprime/Copilot.hpp
templates/fprime/Dockerfile
templates/fprime/instance-copilot
data/formats/fcs_smv
Expand Down
Loading

0 comments on commit c4060bf

Please sign in to comment.