Skip to:

  1. Skip to Jira Navigation
  2. Skip to Side Navigation
  3. Skip to Main Content

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
Configure