Skip to content

ogma-cli: Make cFS backend accept spec as input. Refs #252.#253

Merged
ivanperez-keera merged 5 commits intonasa:developfrom
ivanperez-keera:develop-cfs-spec
Feb 10, 2025
Merged

ogma-cli: Make cFS backend accept spec as input. Refs #252.#253
ivanperez-keera merged 5 commits intonasa:developfrom
ivanperez-keera:develop-cfs-spec

Conversation

@ivanperez-keera
Copy link
Member

Extend the cFS backend to accept an additional argument filename containing an input specification, as well as arguments indicating the formats of the file and the properties, as well as a pre-processor, as prescribed in the solution proposed for #252.

The cFS backend is lacking in features when compared with other backends
like ROS and F'. In particular, it doesn't accept a specification as
input, which means that the user must take an additional step of
extracting the variable names and handlers from the spec before using
the cfs command.

This commit modifies the cFS backend to accepts a spec as input if
provided, uses it to determine the variables and handlers to use in the
cFS application, accepts selecting the format for the file and the
properties, and can filter properties via an external pre-filter.
…nasa#252.

The cFS backend is lacking in features when compared with other backends
like ROS and F'. In particular, it doesn't accept a specification as
input, which means that the user must take an additional step of
extracting the variable names and handlers from the spec before using
the cfs command.

A prior commit has extended the cFS backend to accept an additional
argument filename containing an input specification, as well as
arguments indicating the format of the input file, the format of the
properties, and a pre-processor for properties.

This commit exposes the arguments to the user in the command-line via
additional CLI flags. With this change, a variables file is no longer
mandatory, so its default value in the CLI is removed to prevent the
backend from always trying to use that file.
.

The cFS backend is lacking in features when compared with other backends
like ROS and F'. In particular, it doesn't accept a specification as
input, which means that the user must take an additional step of
extracting the variable names and handlers from the spec before using
the cfs command.

Prior commits have extended the cFS backend to accept an additional
argument filename containing an input specification, as well as
arguments indicating the format of the input file, the format of the
properties, and a pre-processor for properties.

This commit documents the new arguments to the `cfs` command in the
README.
@ivanperez-keera
Copy link
Member Author

ivanperez-keera commented Feb 10, 2025

Change Manager: Verified that:

  • Solution is implemented:
    • The code proposed compiles and passes all tests. Details:
    • The solution proposed produces the expected result. Details:
      The following dockerfile checks that the cFS command now accepts a spec as input file, as well as the file format and property format flags, and that a variables or handlers file are no longer required, and that the generated cFS app mentions both the property name listed in the original spec and the input required by that property, after which it prints the message "Success":
      --- Dockerfile-252
      FROM ubuntu:focal
      
      ENV DEBIAN_FRONTEND=noninteractive
      RUN apt-get update
      
      RUN apt-get install --yes \
            curl g++ gcc git libgmp3-dev libz-dev make pkg-config
      
      RUN mkdir -p $HOME/.local/bin
      ENV PATH=$PATH:/root/.local/bin/
      
      RUN curl https://downloads.haskell.org/~ghcup/0.1.17.7/x86_64-linux-ghcup-0.1.17.7 -o $HOME/.local/bin/ghcup
      RUN chmod a+x $HOME/.local/bin/ghcup
      
      ENV PATH=$PATH:/root/.ghcup/bin/
      RUN ghcup install ghc 9.10
      RUN ghcup install cabal 3.12
      RUN ghcup set ghc 9.10.1
      RUN cabal update
      
      ADD document.json   /tmp/document.json
      ADD json-format.cfg /tmp/json-format.cfg
      ADD cfs-variable-db /tmp/cfs-variable-db
      
      SHELL ["/bin/bash", "-c"]
      CMD git clone $REPO \
          && cd $NAME \
          && git checkout $COMMIT \
          && cabal install ogma-cli:ogma \
          && ogma cfs --input-file /tmp/document.json --variable-db /tmp/cfs-variable-db --app-target-dir cfs/ --input-format /tmp/json-format.cfg --prop-format literal \
          && grep -q '^position_t position;' cfs/fsw/src/copilot_cfs.c \
          && grep -q 'PositionSafe' cfs/fsw/src/copilot_cfs.c \
          && echo "Complete Success"
      
      --- document.json
      {
        "Example": {
          "internal_variables": [],
          "external_variables": [
            {"name":"position", "type":"position_t", "meaning": "Position of the vehicle"}
          ],
          "properties": [
            {
              "id":      "PositionSafe",
              "formula": "PTLTL.alwaysBeen (position # x < 100 && position # y < 100)",
              "text":    "The vehicle stays withing a rectangle with side 100 meters"
            }
          ]
        }
      }
      
      --- json-format.cfg
      JSONFormat
         { specInternalVars    = Just "..internal_variables[*]"
         , specInternalVarId   = ".name"
         , specInternalVarExpr = ".meaning"
         , specInternalVarType = Just ".type"
         , specExternalVars    = Just "..external_variables[*]"
         , specExternalVarId   = ".name"
         , specExternalVarType = Just ".type"
         , specRequirements    = "..properties[*]"
         , specRequirementId   = ".id"
         , specRequirementDesc = Just ".text"
         , specRequirementExpr = ".formula"
         }
      
      --- cfs-variable-db
      ("position", "position_t", "POSITION_MID", "Position")
      
      Command (substitute variables based on new path after merge):
      $ docker run -e "REPO=https://github.com/ivanperez-keera/ogma" -e "NAME=ogma" -e "COMMIT=5796b8aafee7f4f017e2033cc3701ae91afa6999" -it ogma-verify-252
      
  • Implementation is documented. Details:
    The new code includes comments for all top-level functions. All new fields are documented, and the README is updated to explain the new fields. Old text is also updated since some arguments are no longer mandatory.
  • Change history is clear.
  • Commit messages are clear.
  • Changelogs are updated.
  • Examples are updated. Details:
    No updates needed; change does not alter the behavior of the existing examples.
  • Author is internal or has provided signed CLA.
  • Required version bumps are evaluated. Details:
    Bump needed; the change affects the API of ogma-core.

@ivanperez-keera ivanperez-keera merged commit 882d538 into nasa:develop Feb 10, 2025
2 checks passed
@ivanperez-keera ivanperez-keera deleted the develop-cfs-spec branch February 10, 2025 10:51
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant