Add an optional attribute to VisB Items
Description
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
Details
Assignee
Unassigned
UnassignedReporter

Priority
Created November 30, 2020 at 9:14 AM
Updated December 2, 2020 at 10:45 AM
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.