Closed Andersen0 closed 6 months ago
Thank you @Andersen0 . I can confirm that the issue is there. This will be an easy fix.
Description
The SMV to Copilot translator translates equivalences as (<==>)
. However, that operator does not exist in Copilot, it is simply (==)
for Bool
s.
Type
Additional context
None.
Requester
Method to check presence of bug
Compiling a specification with <->
in the ptLTL
field produces Copilot code that does not compile:
{
"test_componentSpec": {
"Functions": [
],
"Internal_variables": [
],
"Other_variables": [
{
"name": "a",
"type": "bool"
}
],
"Requirements": [
{
"CoCoSpecCode": "true",
"fretish": "unimportant",
"name": "testCopilot001",
"ptLTL": "a <-> a"
}
]
}
}
• Variable not in scope:
(<==>) :: Stream Bool -> Stream Bool -> Stream Bool
• Perhaps you meant ‘==>’ (imported from Copilot.Language)
|
20 | propTestCopilot001 = (a <==> a)
Expected result
The execution above should produce a Copilot specification that can be compiled and where ==
is used in Copilot where an equivalence between booleans needs to be expressed.
Desired result
The execution above should produce a Copilot specification that can be compiled and where ==
is used in Copilot where an equivalence between booleans needs to be expressed.
Proposed solution
Modify the SMV translator to use (==)
instead of <==>
.
Further notes
None.
Change Manager: Confirmed that the issue exists.
Technical Lead: Confirmed that the issue should be addressed.
Technical Lead: Issue scheduled for fixing in Ogma 1.3.
Fix assigned to: @ivanperez-keera.
Implementor: Solution implemented, review requested.
Change Manager: Verified that:
Solution is implemented:
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 apt-get install --yes git
CMD git clone $REPO && \ cd $NAME && \ git checkout $COMMIT && \ cd .. && \ cabal v1-install $NAME/$PAT/ --enable-tests && \ cabal v1-install $NAME/$PAT/ --enable-tests --run-tests -j1
Command:
```sh
$ docker run -e "REPO=https://github.com/nasa/ogma" -e "NAME=ogma" -e PAT="ogma-" -e "COMMIT=d3ebffca2227cd61e1ea3e520fb5610f487e3633" -it ogma-test
--- Dockerfile-verify-126
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.18.1 RUN apt-get install --yes git
ADD reqs.json /tmp/reqs.json
CMD git clone $REPO && \ cd $NAME && \ git checkout $COMMIT && \ cd .. && \ cabal v1-install $NAME/$PAT**/ && \ ogma fret-component-spec --fret-file-name /tmp/reqs.json > CS.hs && \ cabal v1-exec -- ghc --make CS.hs && \ echo "Success"
--- reqs.json { "test_spec": { "Functions": [ ], "Internal_variables": [ ], "Other_variables": [ { "name": "a", "type": "bool" } ], "Requirements": [ { "CoCoSpecCode": "true", "fretish": "unimportant", "name": "testCopilot001", "ptLTL": "a <-> a" } ] } }
Command:
```sh
$ docker run -e "REPO=https://github.com/nasa/ogma" -e "NAME=ogma" -e PAT="ogma-" -e "COMMIT=d3ebffca2227cd61e1ea3e520fb5610f487e3633" -it ogma-verify-126
Change Manager: Implementation ready to be merged.
When using an equivalence operator (as used in, for example, FRETISH requirements as
<=>
) the returned Monitor will not be able to properly run because the Haskell Monitor cannot use the<==>
operator that is defined in the code.The command used for generation of the Monitor was: _ogma fret-component-spec --fret-file-name fretspecifications.json > Monitor.hs
The command used for compiling and linking: ghc -package copilot-c99 -package copilot-language -package copilot-libraries Monitor.hs
Acquired error message:
Suggested fix: Defining a custom infix operator that compares two boolean arguments and returns true if they are both true or both false