Perfume's resource-bounded invariants subsume the corresponding Synoptic invariants, so Perfume's refinements to an initial model will always be a superset of how Synoptic would refine that model. Because Perfume will perform all refinements that Synoptic would have plus additional refinements due to resource bound violations in the model, the Perfume model is guaranteed to contain less behavior than Synoptic's model for the same inputs.
Add support in the frontend for displaying the delta between these two models: the nodes and edges that exist in the Perfume model only. This will show which parts of the Perfume model contain behavior dependent on resource usage. This feature will require requesting the delta information from the Perfume backend. As of the time of writing, the backend does not yet have this feature (see issue linked below).
Perfume's resource-bounded invariants subsume the corresponding Synoptic invariants, so Perfume's refinements to an initial model will always be a superset of how Synoptic would refine that model. Because Perfume will perform all refinements that Synoptic would have plus additional refinements due to resource bound violations in the model, the Perfume model is guaranteed to contain less behavior than Synoptic's model for the same inputs.
Add support in the frontend for displaying the delta between these two models: the nodes and edges that exist in the Perfume model only. This will show which parts of the Perfume model contain behavior dependent on resource usage. This feature will require requesting the delta information from the Perfume backend. As of the time of writing, the backend does not yet have this feature (see issue linked below).
Related Perfume backend issue: issue 401.
[Issue created by ohmann: 2015-12-22]