Constraining ocra expressions #54
Assignees
Labels
Comments
norro
added a commit
to boschresearch/mbeddr.formal
that referenced
this issue
Oct 19, 2020
To not pollute nusmv language models with OCRA expression/constraint
concepts, additional MPS constrants are introduced. All OCRA expressions
now extend the interface IOcraExpression, which is only allowed
('can be child of') inside OCRA contracts.
mbeddr#54
Signed-off-by: Arne Nordmann (CR/AEA2) <arne.nordmann@de.bosch.com>
norro
added a commit
to boschresearch/mbeddr.formal
that referenced
this issue
Oct 20, 2020
Some OCRA expressions are redundant to nusmv expressions as they use a different editor "textual projection". To not use both, this commit introduces a blacklist of (redundant) nusmv expressions that can't be used in ocra models, e.g., globally, historically, and, or, ... mbeddr#54 Signed-off-by: Arne Nordmann (CR/AEA2) <arne.nordmann@de.bosch.com>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add constraints for ocra expressions (some of them redundant to nusmv expressions), to exclude them from polluting nusmv models. That is:
The text was updated successfully, but these errors were encountered: