Add an optional attribute to VisB Items

Description

If the observer predicate contains variables which are not present in the model, then silently ignore this item.

Useful to re-use the same JSON file for multiple machines. Could also be useful e.g. to visualise counter examples to Rodin POs, where not all variables/identifiers may be available.

Activity

Show:

Michael Leuschel December 2, 2020 at 10:45 AM

I have added an optional attribute to VisB items. Type checking errors are now ignored. The solution works but is not ideal: a formula with an unknown identifier will be re-evaluated in every state. We could filter out the optional items once at the beginning.

Details

Assignee

Reporter

Priority

Created November 30, 2020 at 9:14 AM
Updated December 2, 2020 at 10:45 AM