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-cocospec-ytopre' into develop. Close #86.
**Description**
Ogma cannot handle CoCoSpec boolean specifications containing the unary
operators `ZtoPre` or `YtoPre`. This makes some of the specifications produced
by FRET not parseable.
**Type**
- Bug: FRET specification cannot be parsed or converted to Copilot monitor.
**Additional context**
None.
**Requester**
- Ivan Perez
**Method to check presence of bug**
Compiling a specification with `ZtoPre` or `YtoPre` in the CoCoSpec property
produces an error message instead of a correct Copilot specification:
```json
{
"test_componentSpec": {
"Functions": [
],
"Internal_variables": [
],
"Other_variables": [
{
"name": "signal",
"type": "bool"
}
],
"Requirements": [
{
"CoCoSpecCode": "ZtoPre(signal)",
"fretish": "unimportant",
"name": "testCopilot-001",
"ptLTL": "signal"
}
]
}
}
```
```sh
$ ogma fret-component-spec --cocospec --fret-file-name fret-reqs-full.json
fret-reqs-full.json: error: syntax error at line 1, column 7 before `('
```
The following Dockerfile runs the FRET to Copilot translators on the
accompanying FRET component specification and FRET requirements DB, which
contain ZtoPre and YtoPre in the CoCoSpec formulas.
```
--- Dockerfile-verify-86
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 cabal v1-install copilot-3.15
RUN apt-get install --yes git
ADD fret-reqs-db.json /tmp/fret-reqs-db.json
ADD fret-reqs-cs.json /tmp/fret-reqs-cs.json
CMD git clone $REPO && \
cd $NAME && \
git checkout $COMMIT && \
cd .. && \
cabal v1-install $NAME/$PAT**/ && \
ogma fret-reqs-db --fret-file-name /tmp/fret-reqs-db.json --cocospec > DB.hs && \
cabal v1-exec -- ghc --make DB.hs && \
ogma fret-component-spec --fret-file-name /tmp/fret-reqs-cs.json --cocospec > CS.hs && \
cabal v1-exec -- ghc --make CS.hs && \
echo "Success"
--- fret-reqs-cs.json
{
"test_componentSpec": {
"Functions": [
],
"Internal_variables": [
],
"Other_variables": [
{
"name": "signal",
"type": "bool"
}
],
"Requirements": [
{
"CoCoSpecCode": "ZtoPre(signal) and YtoPre(signal)",
"fretish": "unimportant",
"name": "testCopilot-001",
"ptLTL": "TRUE"
}
]
}
}
--- fret-reqs-db.json
[
{
"reqid": "test_req1",
"parent_reqid": "",
"project": "Test",
"rationale": "",
"fulltext": "",
"semantics": {
"type": "test",
"ptExpanded": "TRUE",
"CoCoSpecCode": "ZtoPre(signal) and YtoPre(signal)"
}
}
]
```
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-86
```
**Expected result**
The execution above should produce a Copilot specification that translates
`ZtoPre` to delay initialized to `True`. If modified to use `YtoPre`, the
operator should be translated to a delay initialized to `False`.
Running the docker script prints Success, indicating that specifications
containing both ZtoPre and YtoPre can be translated and the resulting Copilot
files can be compiled, both in requirements DBs and in Component Specs.
**Solution implemented**
Modify CoCoSpec grammar to allow the unary operators `ZtoPre` and `YtoPre`.
Modify translator in `ogma-core` to perform the translation of `ZtoPre` to a
delay initialized to `True`, and `YtoPre` to a delay initialized to `False`.
Include the necessary auxiliary definitions in the generated Copilot modules.
**Further notes**
None.- Loading branch information
