Skip to content

Commit

Permalink
Merge branch 'develop-cfs-spec' into develop. Close #252.
Browse files Browse the repository at this point in the history
**Description**

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.

The `cfs` command should accept the same flags as other commands like `ros` and
`fprime`, use an input spec if provided, and accept selecting the format for
the file and the properties, as well as an external pre-filter or
pre-processor.

**Type**

- Feature: Add to cFS backend features available in other backends.

**Additional context**

None.

**Requester**

- Ivan Perez.

**Method to check presence of bug**

Not applicable (not a bug).

**Expected result**

The `cfs` command accepts the same flags as other commands like `ros` and
`fprime`, uses an input spec if provided 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.

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):
```sh
$ docker run -e "REPO=https://github.com/NASA/ogma" -e "NAME=ogma" -e "COMMIT=<HASH>" -it ogma-verify-252
```

**Solution implemented**

Modify cFS backend in `ogma-core` by porting over features from the ROS and
FPrime backends to read and process input specifications.

Modify cFS CLI to expose new arguments, and remove default value from argument
that is no longer mandatory.

Update README to document the new arguments available.

**Further notes**

None.
  • Loading branch information
ivanperez-keera committed Feb 10, 2025
2 parents 8576131 + 5796b8a commit 882d538
Show file tree
Hide file tree
Showing 5 changed files with 377 additions and 43 deletions.
1 change: 1 addition & 0 deletions ogma-cli/CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@
* Update README with new FPrime template variables (#246).
* Adjust CLI to match new backend API (#248).
* Expose template-vars argument to ROS, FPrime, standalone backends (#250).
* Expose spec processing arguments to cFS backend in CLI (#252).

## [1.6.0] - 2025-01-21

Expand Down
31 changes: 27 additions & 4 deletions ogma-cli/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -124,20 +124,43 @@ necessary messages and make it available to Copilot. Ogma provides additional
flags to customize the list of known variables, so that projects can maintain
their own variable databases beyond what Ogma includes by default.

cFS applications are generated using the Ogma command `cfs`, which receives
four main arguments:
cFS applications are generated using the Ogma command `cfs`, which accepts
the following arguments:
- `--input-file FILENAME`: location of the specification or source file for
which a cFS application is being generated.
- `--app-target-dir DIR`: location where the cFS application files must be
stored.
- `--app-template-dir DIR`: location of the cFS application template to use.
- `--variable-file FILENAME`: a file containing a list of variables that must
be made available to the monitor.
- `--variable-file FILENAME`: a file containing a list of variables to monitor
in the cFS application.
- `--variable-db FILENAME`: a file containing a database of known variables,
and the message they are included with.
- `--handlers-file FILENAME`: a file containing a list of known fault handlers
or triggers.
- `--input-format FORMAT_NAME`: the name of a know input format description
file in JSON or XML. It can be a path to a file containing such description.
- `--prop-format FORMAT_NAME`: the name of the format or language in which the
properties are encoded. For example, a file may contain a list of properties,
and each property may contain a field with a formula in SMV (`smv`) or
Copilot (`literal`).
- `--parse-prop-via COMMAND`: a command in the `PATH` capable of translating
properties as listed in the specification file into properties in the target
property language. This external process may be a translation tool, or an LLM
capable of translating into the target language.
- `--template-vars FILENAME`: a JSON file containing a list of additional
variables to expand in the template.

> [!NOTE]
> Ogma does not guarantee that the result of a translation carried out by
> calling an external command or LLM with the flag `--parse-prop-via` is
> correct. It is your responsibility as the user to check the output produced
> by the auxiliary translation command for accuracy. Ogma will accept whatever
> output the command produces as a replacement for the property's formula, and
> use it without changes if the property format selected is `literal`, or try
> to translate it into Copilot if a different property format has been
> selected. This limitation applies even in the case where the subsequent
> translation to Copilot succeeds.
The following execution generates an initial cFS application for runtime
monitoring using Copilot:
```
Expand Down
69 changes: 62 additions & 7 deletions ogma-cli/src/CLI/CommandCFSApp.hs
Original file line number Diff line number Diff line change
Expand Up @@ -43,8 +43,8 @@ module CLI.CommandCFSApp
where

-- External imports
import Options.Applicative ( Parser, help, long, metavar, optional, showDefault,
strOption, value )
import Options.Applicative ( Parser, help, long, metavar, optional, short,
showDefault, strOption, value )

-- External imports: command results
import Command.Result ( Result )
Expand All @@ -57,11 +57,15 @@ import qualified Command.CFSApp

-- | Options needed to generate the cFS application.
data CommandOpts = CommandOpts
{ cFSAppTarget :: String
{ cFSAppInputFile :: Maybe String
, cFSAppTarget :: String
, cFSAppTemplateDir :: Maybe String
, cFSAppVarNames :: Maybe String
, cFSAppVarDB :: Maybe String
, cFSAppHandlers :: Maybe String
, cFSAppFormat :: String
, cFSAppPropFormat :: String
, cFSAppPropVia :: Maybe String
, cFSAppTemplateVars :: Maybe String
}

Expand All @@ -74,11 +78,15 @@ command :: CommandOpts -> IO (Result ErrorCode)
command c = Command.CFSApp.command options
where
options = Command.CFSApp.CommandOptions
{ Command.CFSApp.commandTargetDir = cFSAppTarget c
{ Command.CFSApp.commandInputFile = cFSAppInputFile c
, Command.CFSApp.commandTargetDir = cFSAppTarget c
, Command.CFSApp.commandTemplateDir = cFSAppTemplateDir c
, Command.CFSApp.commandVariables = cFSAppVarNames c
, Command.CFSApp.commandVariableDB = cFSAppVarDB c
, Command.CFSApp.commandHandlers = cFSAppHandlers c
, Command.CFSApp.commandFormat = cFSAppFormat c
, Command.CFSApp.commandPropFormat = cFSAppPropFormat c
, Command.CFSApp.commandPropVia = cFSAppPropVia c
, Command.CFSApp.commandExtraVars = cFSAppTemplateVars c
}

Expand All @@ -92,7 +100,14 @@ commandDesc = "Generate a complete cFS/Copilot application"
-- System application connected to Copilot monitors.
commandOptsParser :: Parser CommandOpts
commandOptsParser = CommandOpts
<$> strOption
<$> optional
( strOption
( long "input-file"
<> metavar "FILENAME"
<> help strCFSAppFileNameArgDesc
)
)
<*> strOption
( long "app-target-dir"
<> metavar "DIR"
<> showDefault
Expand All @@ -110,8 +125,6 @@ commandOptsParser = CommandOpts
( strOption
( long "variable-file"
<> metavar "FILENAME"
<> showDefault
<> value "variables"
<> help strCFSAppVarListArgDesc
)
)
Expand All @@ -129,6 +142,29 @@ commandOptsParser = CommandOpts
<> help strCFSAppHandlerListArgDesc
)
)
<*> strOption
( long "input-format"
<> short 'f'
<> metavar "FORMAT_NAME"
<> help strCFSAppFormatDesc
<> showDefault
<> value "fcs"
)
<*> strOption
( long "prop-format"
<> short 'p'
<> metavar "FORMAT_NAME"
<> help strCFSAppPropFormatDesc
<> showDefault
<> value "smv"
)
<*> optional
( strOption
( long "parse-prop-via"
<> metavar "COMMAND"
<> help strCFSAppPropViaDesc
)
)
<*> optional
( strOption
( long "template-vars"
Expand All @@ -146,6 +182,12 @@ strCFSAppTemplateDirArgDesc :: String
strCFSAppTemplateDirArgDesc =
"Directory holding cFS application source template"

-- | Argument input file to CFS app generation command
strCFSAppFileNameArgDesc :: String
strCFSAppFileNameArgDesc =
"File containing input specification"


-- | Argument variable list to cFS app generation command
strCFSAppVarListArgDesc :: String
strCFSAppVarListArgDesc =
Expand All @@ -161,6 +203,19 @@ strCFSAppHandlerListArgDesc :: String
strCFSAppHandlerListArgDesc =
"File containing list of Copilot handlers used in the specification"

-- | Format flag description.
strCFSAppFormatDesc :: String
strCFSAppFormatDesc = "Format of the input file"

-- | Property format flag description.
strCFSAppPropFormatDesc :: String
strCFSAppPropFormatDesc = "Format of temporal or boolean properties"

-- | External command to pre-process individual properties.
strCFSAppPropViaDesc :: String
strCFSAppPropViaDesc =
"Command to pre-process individual properties"

-- | Argument template variables to cFS app generation command
strCFSAppTemplateVarsArgDesc :: String
strCFSAppTemplateVarsArgDesc =
Expand Down
1 change: 1 addition & 0 deletions ogma-core/CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,7 @@
* Make structured data available to FPrime template (#246).
* Equalize backends (#248).
* Update ROS, FPrime, standalone backends to process template vars file (#250).
* Make cFS backend accept spec as input (#252).

## [1.6.0] - 2025-01-21

Expand Down
Loading

0 comments on commit 882d538

Please sign in to comment.