-
Notifications
You must be signed in to change notification settings - Fork 25
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge branch 'develop-fprime' into develop. Close #77.
**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**
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
--- 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 (substitute variables based on new path after merge):
```sh
$ docker run -v $PWD/output:/fprime_demo -e "REPO=https://github.com/NASA/ogma" -e "NAME=ogma" -e PAT="ogma-" -e "COMMIT=<HASH>" -it ogma-verify-77
$ cd output/
$ docker build -t ogma-verify-77-fprime .
```
**Expected result**
Ogma provides a new command to generate a FPrime monitoring component, akin to
the one provided for cFS.
**Solution implemented**
Update `ogma-core` with the new command to generate FPrime package. Expose
command via `ogma-cli`.
The command produces a dockerfile, which can be used to build the generated
monitor inside FPrime's reference application (for testing purposes).
The documentation of the Main modules and Cabal files.
The README is updated with a new section explaining the backend, and providing
precise instructions to test it.
**Further notes**
None.- Loading branch information
Showing
12 changed files
with
1,095 additions
and
1 deletion.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,148 @@ | ||
| -- Copyright 2022 United States Government as represented by the Administrator | ||
| -- of the National Aeronautics and Space Administration. All Rights Reserved. | ||
| -- | ||
| -- Disclaimers | ||
| -- | ||
| -- No Warranty: THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY | ||
| -- OF ANY KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT | ||
| -- LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO | ||
| -- SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR A | ||
| -- PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT THE | ||
| -- SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT DOCUMENTATION, IF | ||
| -- PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE. THIS AGREEMENT DOES NOT, IN | ||
| -- ANY MANNER, CONSTITUTE AN ENDORSEMENT BY GOVERNMENT AGENCY OR ANY PRIOR | ||
| -- RECIPIENT OF ANY RESULTS, RESULTING DESIGNS, HARDWARE, SOFTWARE PRODUCTS OR | ||
| -- ANY OTHER APPLICATIONS RESULTING FROM USE OF THE SUBJECT SOFTWARE. FURTHER, | ||
| -- GOVERNMENT AGENCY DISCLAIMS ALL WARRANTIES AND LIABILITIES REGARDING | ||
| -- THIRD-PARTY SOFTWARE, IF PRESENT IN THE ORIGINAL SOFTWARE, AND DISTRIBUTES | ||
| -- IT "AS IS." | ||
| -- | ||
| -- Waiver and Indemnity: RECIPIENT AGREES TO WAIVE ANY AND ALL CLAIMS AGAINST | ||
| -- THE UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS, AS WELL AS | ||
| -- ANY PRIOR RECIPIENT. IF RECIPIENT'S USE OF THE SUBJECT SOFTWARE RESULTS IN | ||
| -- ANY LIABILITIES, DEMANDS, DAMAGES, EXPENSES OR LOSSES ARISING FROM SUCH USE, | ||
| -- INCLUDING ANY DAMAGES FROM PRODUCTS BASED ON, OR RESULTING FROM, RECIPIENT'S | ||
| -- USE OF THE SUBJECT SOFTWARE, RECIPIENT SHALL INDEMNIFY AND HOLD HARMLESS THE | ||
| -- UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS, AS WELL AS ANY | ||
| -- PRIOR RECIPIENT, TO THE EXTENT PERMITTED BY LAW. RECIPIENT'S SOLE REMEDY | ||
| -- FOR ANY SUCH MATTER SHALL BE THE IMMEDIATE, UNILATERAL TERMINATION OF THIS | ||
| -- AGREEMENT. | ||
| -- | ||
| -- | CLI interface to the FPrimeApp subcommand. | ||
| module CLI.CommandFPrimeApp | ||
| ( | ||
| -- * Direct command access | ||
| command | ||
| , CommandOpts | ||
| , ErrorCode | ||
|
|
||
| -- * CLI | ||
| , commandDesc | ||
| , commandOptsParser | ||
| ) | ||
| where | ||
|
|
||
| -- External imports | ||
| import Options.Applicative ( Parser, help, long, metavar, optional, showDefault, | ||
| strOption, value ) | ||
|
|
||
| -- External imports: command results | ||
| import Command.Result ( Result ) | ||
|
|
||
| -- External imports: actions or commands supported | ||
| import Command.FPrimeApp ( ErrorCode, fprimeApp ) | ||
|
|
||
| -- * Command | ||
|
|
||
| -- | Options needed to generate the FPrime component. | ||
| data CommandOpts = CommandOpts | ||
| { fprimeAppTarget :: String | ||
| , fprimeAppFRETFile :: Maybe String | ||
| , fprimeAppVarNames :: Maybe String | ||
| , fprimeAppVarDB :: Maybe String | ||
| , fprimeAppHandlers :: 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". | ||
| command :: CommandOpts -> IO (Result ErrorCode) | ||
| command c = | ||
| fprimeApp | ||
| (fprimeAppTarget c) | ||
| (fprimeAppFRETFile c) | ||
| (fprimeAppVarNames c) | ||
| (fprimeAppVarDB c) | ||
| (fprimeAppHandlers c) | ||
|
|
||
| -- * CLI | ||
|
|
||
| -- | FPrime command description | ||
| commandDesc :: String | ||
| commandDesc = "Generate a complete F' monitoring component" | ||
|
|
||
| -- | Subparser for the @fprime@ command, used to generate an FPrime component | ||
| -- connected to Copilot monitors. | ||
| commandOptsParser :: Parser CommandOpts | ||
| commandOptsParser = CommandOpts | ||
| <$> strOption | ||
| ( long "app-target-dir" | ||
| <> metavar "DIR" | ||
| <> showDefault | ||
| <> value "fprime" | ||
| <> help strFPrimeAppDirArgDesc | ||
| ) | ||
| <*> optional | ||
| ( strOption | ||
| ( long "fret-file-name" | ||
| <> metavar "FILENAME" | ||
| <> help strFPrimeAppFRETFileNameArgDesc | ||
| ) | ||
| ) | ||
| <*> optional | ||
| ( strOption | ||
| ( long "variable-file" | ||
| <> metavar "FILENAME" | ||
| <> help strFPrimeAppVarListArgDesc | ||
| ) | ||
| ) | ||
| <*> optional | ||
| ( strOption | ||
| ( long "variable-db" | ||
| <> metavar "FILENAME" | ||
| <> help strFPrimeAppVarDBArgDesc | ||
| ) | ||
| ) | ||
| <*> optional | ||
| ( strOption | ||
| ( long "handlers-file" | ||
| <> metavar "FILENAME" | ||
| <> help strFPrimeAppHandlerListArgDesc | ||
| ) | ||
| ) | ||
|
|
||
| -- | Argument target directory to FPrime component generation command | ||
| strFPrimeAppDirArgDesc :: String | ||
| strFPrimeAppDirArgDesc = "Target directory" | ||
|
|
||
| -- | Argument FRET CS to FPrime component generation command | ||
| strFPrimeAppFRETFileNameArgDesc :: String | ||
| strFPrimeAppFRETFileNameArgDesc = | ||
| "File containing FRET Component Specification" | ||
|
|
||
| -- | Argument variable list to FPrime component generation command | ||
| strFPrimeAppVarListArgDesc :: String | ||
| strFPrimeAppVarListArgDesc = | ||
| "File containing list of F' variables to make accessible" | ||
|
|
||
| -- | Argument variable database to FPrime component generation command | ||
| strFPrimeAppVarDBArgDesc :: String | ||
| strFPrimeAppVarDBArgDesc = | ||
| "File containing a DB of known F' variables" | ||
|
|
||
| -- | Argument handler list to FPrime component generation command | ||
| strFPrimeAppHandlerListArgDesc :: String | ||
| strFPrimeAppHandlerListArgDesc = | ||
| "File containing list of Copilot handlers used in the specification" |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.