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-fix-ne' into develop. Close #71.
**Description**
Requirements that contain inequalities in conditions in the TL formulas fail to
be parsed correctly by Ogma.
**Type**
- Bug: valid FRET file cannot be parsed by Ogma.
**Additional context**
None.
**Requester**
- Alexander Will (Virginia Commonwealth University).
**Method to check presence of bug**
The following command reports an error instead of producing a monitor
specification.
```sh
$ ogma fret-component-spec --fret-file-name file.json
```
where `file.json` contains the following:
```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"
}
]
}
}
```
The error produced is:
```
$ ogma fret-component-spec --fret-file-name file.json
file.json: error: syntax error at line 1, column 10 before `!'
$ ogma fret-component-spec --cocospec --fret-file-name file.json
file.json: error: syntax error at line 1, column 11 before `>'
```
The following dockerfile uses the accompanying FRET component specification
containing inequalities in the TL formulas to generate the Copilot monitors
both for the SMV and CoCoSpec cases, and it compiles the resulting Copilot
code:
```Dockerfile
--- Dockerfile-verify-71
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-3.13
RUN apt-get install --yes git
ADD file.json /tmp/file.json
CMD git clone $REPO && \
cd $NAME && \
git checkout $COMMIT && \
cd .. && \
cabal v1-install $NAME/$PAT**/ && \
ogma fret-component-spec --fret-file-name /tmp/file.json > SMV.hs && \
cabal v1-exec -- runhaskell SMV.hs && \
gcc -c fret.c && \
ogma fret-component-spec --fret-file-name /tmp/file.json --cocospec > CoCoSpec.hs && \
cabal v1-exec -- runhaskell CoCoSpec.hs && \
gcc -c fret.c && \
echo "Success"
--- 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 -e "REPO=https://github.com/NASA/ogma" -e "NAME=ogma" -e PAT="ogma-" -e "COMMIT=<HASH>" -it ogma-verify-71
```
**Expected result**
The json file above should be usable with Ogma and produce a valid Copilot
monitor. Running the Docker image with the associated file in scope should
produce correct Copilot code which can be executed. The resulting C99
code can be compiled correctly. The word "Success" is printed after a
successful execution.
**Solution implemented**
Modify SMV grammar to accept inequality. Adjust Ogma accordingly to translate
the operator into Copilot's (/=).
Modify CoCoSpec grammar to accept inequality. Adjust Ogma accordingly to
translate the operator into Copilot's (/=).
Modify the general Copilot code generator to hide the (/=) operator imported by
default from the Prelude.
**Further notes**
None.- Loading branch information
