Skip to content

Commit

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

The standalone backend is capable of working with different kinds of
property languages, as well as with `--parse-prop-via`, but the same
features are not available in other backends. It also supports other
kinds of JSON/XML formats, instead of using only a fixed format. The
diagrams backend also supports the literal property "language", but
that's not available in any of the other backends.

To improve Ogma altogether and facilitate using the tool, we'd like
these features to be present in as many backends as possible.

**Type**

- Feature: extend capability to other backends.

**Additional context**

None.

**Requester**

- Ivan Perez.

**Method to check presence of bug**

Not applicable (not a bug).

**Expected result**

The standalone backend is capable of supporting the "literal" property
language. The ROS and FPrime backends support different file formats,
property languages, and the use of external pre-processors like LLMs.

The following dockerfile uses the standalone backend to generate a
monitor using a literal Copilot expression gathered from a custom JSON
file, and then uses the FPrime backend to produce an FPrime component.
The Copilot monitor is further compiled, and building the Dockerfile
generated by the FPrime backend completes the compilation process
correctly. Note that, due to a standing issue with the FPrime backend
(java is needed in newer versions), we need to modify the Dockerfile
generated to install java. This can be done in a way that does not
interfere with future tests (the modification will succeed even if java
is available on the guest image already).

```
--- Dockerfile-verify-204
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 document.json       /tmp/document.json
ADD json-format.cfg     /tmp/json-format.cfg
ADD fprime-variable-dbs /tmp/fprime-variable-dbs
ADD fprime-handlers     /tmp/fprime-handlers

CMD git clone $REPO && \
    cd $NAME && \
    git checkout $COMMIT && \
    cd .. && \
    cabal v1-sandbox init && \
    cabal v1-install copilot-4.2 $NAME/$PAT**/ --constraint="aeson>=2.0.3.0" && \
    ./.cabal-sandbox/bin/ogma standalone --file-name /tmp/document.json -f /tmp/json-format.cfg -p literal --target-file-name copilot --target-dir fprime_demo && \
    ./.cabal-sandbox/bin/ogma fprime --app-target-dir fprime_demo --handlers-file /tmp/fprime-handlers --input-file /tmp/document.json -f /tmp/json-format.cfg -p literal --variable-db /tmp/fprime-variable-db && \
    cabal v1-exec -- runhaskell fprime_demo/Copilot.hs && \
    sed -i -e '0,/RUN apt-get install/{s/\(RUN apt-get install .*\)/\1 default-jre/}' fprime_demo/Dockerfile && \
    mv copilot* fprime_demo/

--- document.json
{
  "Example": {
    "internal_variables": [],
    "external_variables": [
      {"name":"input", "type":"Float", "meaning": "Input from the system"}
    ],
    "properties": [
      {
        "id":      "MyProperty",
        "formula": "PTLTL.alwaysBeen (input /= 30.0)",
        "text":    "Input is never 30"
      }
    ]
  }
}

--- fprime-handlers
handlerMyProperty

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

--- 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"
   }
```

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

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

**Solution implemented**

Modify standalone backend to support literal format.

Modify ROS backend to support different property formats, file formats
and external processors like LLMs.

Modify FPrime backend to support different property formats, file
formats and external processors like LLMs.

Adjust tests to make file names match property formats and backend
names.

Adjust examples to make file names match property formats.

**Further notes**

We decide not to include the same ideas wrt. the cFS backend because
it's slightly different, and it might be too hard to do as part of the
same issue.
  • Loading branch information
ivanperez-keera committed Jan 20, 2025
2 parents 9065cce + 0a21238 commit 2814056
Show file tree
Hide file tree
Showing 25 changed files with 666 additions and 288 deletions.
3 changes: 2 additions & 1 deletion ogma-cli/CHANGELOG.md
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
# Revision history for ogma-cli

## [1.X.Y] - 2025-01-14
## [1.X.Y] - 2025-01-20

* Update contribution guidelines (#161).
* Provide ability to customize template in fprime command (#185).
Expand All @@ -9,6 +9,7 @@
* Add version bounds to all dependencies (#119).
* Introduce new diagram command (#194).
* Provide ability to preprocess properties via external command (#197).
* Extend support for file, property formats across backends (#204).

## [1.5.0] - 2024-11-21

Expand Down
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
97 changes: 71 additions & 26 deletions ogma-cli/src/CLI/CommandFPrimeApp.hs
Original file line number Diff line number Diff line change
Expand Up @@ -43,41 +43,50 @@ module CLI.CommandFPrimeApp
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 )

-- External imports: actions or commands supported
import Command.FPrimeApp ( ErrorCode, fprimeApp )
import Command.FPrimeApp (ErrorCode, fprimeApp)
import qualified Command.FPrimeApp

-- * Command

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

-- | Create <https://github.com/nasa/fprime FPrime> component that subscribe
-- to obtain necessary data from the bus and call Copilot when new data
-- arrives.
--
-- This is just an uncurried version of "Command.fprimeApp".
-- This is just a wrapper around "Command.fprimeApp".
command :: CommandOpts -> IO (Result ErrorCode)
command c =
fprimeApp
(fprimeAppTarget c)
(fprimeAppTemplateDir c)
(fprimeAppFRETFile c)
(fprimeAppVarNames c)
(fprimeAppVarDB c)
(fprimeAppHandlers c)
command c = fprimeApp (fprimeAppInputFile c) options
where
options =
Command.FPrimeApp.FPrimeAppOptions
{ Command.FPrimeApp.fprimeAppTargetDir = fprimeAppTarget c
, Command.FPrimeApp.fprimeAppTemplateDir = fprimeAppTemplateDir c
, Command.FPrimeApp.fprimeAppVarNames = fprimeAppVarNames c
, Command.FPrimeApp.fprimeAppVariableDB = fprimeAppVarDB c
, Command.FPrimeApp.fprimeAppHandlers = fprimeAppHandlers c
, Command.FPrimeApp.fprimeAppFormat = fprimeAppFormat c
, Command.FPrimeApp.fprimeAppPropFormat = fprimeAppPropFormat c
, Command.FPrimeApp.fprimeAppPropVia = fprimeAppPropVia c
}

-- * CLI

Expand All @@ -89,7 +98,14 @@ commandDesc = "Generate a complete F' monitoring component"
-- connected to Copilot monitors.
commandOptsParser :: Parser CommandOpts
commandOptsParser = CommandOpts
<$> strOption
<$> optional
( strOption
( long "input-file"
<> metavar "FILENAME"
<> help strFPrimeAppFileNameArgDesc
)
)
<*> strOption
( long "app-target-dir"
<> metavar "DIR"
<> showDefault
Expand All @@ -103,13 +119,6 @@ commandOptsParser = CommandOpts
<> help strFPrimeAppTemplateDirArgDesc
)
)
<*> optional
( strOption
( long "fret-file-name"
<> metavar "FILENAME"
<> help strFPrimeAppFRETFileNameArgDesc
)
)
<*> optional
( strOption
( long "variable-file"
Expand All @@ -131,6 +140,29 @@ commandOptsParser = CommandOpts
<> help strFPrimeAppHandlerListArgDesc
)
)
<*> strOption
( long "input-format"
<> short 'f'
<> metavar "FORMAT_NAME"
<> help strFPrimeAppFormatDesc
<> showDefault
<> value "fcs"
)
<*> strOption
( long "prop-format"
<> short 'p'
<> metavar "FORMAT_NAME"
<> help strFPrimeAppPropFormatDesc
<> showDefault
<> value "smv"
)
<*> optional
( strOption
( long "parse-prop-via"
<> metavar "COMMAND"
<> help strFPrimeAppPropViaDesc
)
)

-- | Argument target directory to FPrime component generation command
strFPrimeAppDirArgDesc :: String
Expand All @@ -141,10 +173,10 @@ strFPrimeAppTemplateDirArgDesc :: String
strFPrimeAppTemplateDirArgDesc =
"Directory holding F' component source template"

-- | Argument FRET CS to FPrime component generation command
strFPrimeAppFRETFileNameArgDesc :: String
strFPrimeAppFRETFileNameArgDesc =
"File containing FRET Component Specification"
-- | Argument input file to FPrime component generation command
strFPrimeAppFileNameArgDesc :: String
strFPrimeAppFileNameArgDesc =
"File containing input specification"

-- | Argument variable list to FPrime component generation command
strFPrimeAppVarListArgDesc :: String
Expand All @@ -160,3 +192,16 @@ strFPrimeAppVarDBArgDesc =
strFPrimeAppHandlerListArgDesc :: String
strFPrimeAppHandlerListArgDesc =
"File containing list of Copilot handlers used in the specification"

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

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

-- | External command to pre-process individual properties.
strFPrimeAppPropViaDesc :: String
strFPrimeAppPropViaDesc =
"Command to pre-process individual properties"
96 changes: 70 additions & 26 deletions ogma-cli/src/CLI/CommandROSApp.hs
Original file line number Diff line number Diff line change
Expand Up @@ -43,41 +43,49 @@ module CLI.CommandROSApp
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 )

-- External imports: actions or commands supported
import Command.ROSApp ( ErrorCode, rosApp )
import Command.ROSApp (ErrorCode, rosApp)
import qualified Command.ROSApp

-- * Command

-- | Options needed to generate the ROS application.
data CommandOpts = CommandOpts
{ rosAppTarget :: String
{ rosAppInputFile :: Maybe String
, rosAppTarget :: String
, rosAppTemplateDir :: Maybe String
, rosAppFRETFile :: Maybe String
, rosAppVarNames :: Maybe String
, rosAppVarDB :: Maybe String
, rosAppHandlers :: Maybe String
, rosAppFormat :: String
, rosAppPropFormat :: String
, rosAppPropVia :: Maybe String
}

-- | Create <https://www.ros.org/ Robot Operating System> (ROS) applications
-- that subscribe to obtain necessary data from topics and call Copilot when
-- new data arrives.
--
-- This is just an uncurried version of "Command.ROSApp".
-- This is just a wrapper around "Command.ROSApp".
command :: CommandOpts -> IO (Result ErrorCode)
command c =
rosApp
(rosAppTarget c)
(rosAppTemplateDir c)
(rosAppFRETFile c)
(rosAppVarNames c)
(rosAppVarDB c)
(rosAppHandlers c)
command c = rosApp (rosAppInputFile c) options
where
options = Command.ROSApp.ROSAppOptions
{ Command.ROSApp.rosAppTargetDir = rosAppTarget c
, Command.ROSApp.rosAppTemplateDir = rosAppTemplateDir c
, Command.ROSApp.rosAppVariables = rosAppVarNames c
, Command.ROSApp.rosAppVariableDB = rosAppVarDB c
, Command.ROSApp.rosAppHandlers = rosAppHandlers c
, Command.ROSApp.rosAppFormat = rosAppFormat c
, Command.ROSApp.rosAppPropFormat = rosAppPropFormat c
, Command.ROSApp.rosAppPropVia = rosAppPropVia c
}

-- * CLI

Expand All @@ -89,7 +97,14 @@ commandDesc = "Generate a ROS 2 monitoring package"
-- application connected to Copilot monitors.
commandOptsParser :: Parser CommandOpts
commandOptsParser = CommandOpts
<$> strOption
<$> optional
( strOption
( long "input-file"
<> metavar "FILENAME"
<> help strROSAppFileNameArgDesc
)
)
<*> strOption
( long "app-target-dir"
<> metavar "DIR"
<> showDefault
Expand All @@ -103,13 +118,6 @@ commandOptsParser = CommandOpts
<> help strROSAppTemplateDirArgDesc
)
)
<*> optional
( strOption
( long "fret-file-name"
<> metavar "FILENAME"
<> help strROSAppFRETFileNameArgDesc
)
)
<*> optional
( strOption
( long "variable-file"
Expand All @@ -131,6 +139,29 @@ commandOptsParser = CommandOpts
<> help strROSAppHandlerListArgDesc
)
)
<*> strOption
( long "input-format"
<> short 'f'
<> metavar "FORMAT_NAME"
<> help strROSAppFormatDesc
<> showDefault
<> value "fcs"
)
<*> strOption
( long "prop-format"
<> short 'p'
<> metavar "FORMAT_NAME"
<> help strROSAppPropFormatDesc
<> showDefault
<> value "smv"
)
<*> optional
( strOption
( long "parse-prop-via"
<> metavar "COMMAND"
<> help strROSAppPropViaDesc
)
)

-- | Argument target directory to ROS app generation command
strROSAppDirArgDesc :: String
Expand All @@ -141,10 +172,10 @@ strROSAppTemplateDirArgDesc :: String
strROSAppTemplateDirArgDesc =
"Directory holding ROS application source template"

-- | Argument FRET CS to ROS app generation command
strROSAppFRETFileNameArgDesc :: String
strROSAppFRETFileNameArgDesc =
"File containing FRET Component Specification"
-- | Argument input file to ROS app generation command
strROSAppFileNameArgDesc :: String
strROSAppFileNameArgDesc =
"File containing input specification"

-- | Argument variable list to ROS app generation command
strROSAppVarListArgDesc :: String
Expand All @@ -160,3 +191,16 @@ strROSAppVarDBArgDesc =
strROSAppHandlerListArgDesc :: String
strROSAppHandlerListArgDesc =
"File containing list of Copilot handlers used in the specification"

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

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

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

0 comments on commit 2814056

Please sign in to comment.