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 Perfume for computing the delta between these two models and in some way outputting which nodes and edges exist in the Perfume model only. This will show which parts of the Perfume model contain behavior dependent on resource usage.
This feature can likely be accomplished by forcing Perfume first to refine as Synoptic would, then to perform any resource-bounded refinements and to note which nodes and edges changed. This would degrade inference performance somewhat, so this feature should be disabled by default.
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 Perfume for computing the delta between these two models and in some way outputting which nodes and edges exist in the Perfume model only. This will show which parts of the Perfume model contain behavior dependent on resource usage.
This feature can likely be accomplished by forcing Perfume first to refine as Synoptic would, then to perform any resource-bounded refinements and to note which nodes and edges changed. This would degrade inference performance somewhat, so this feature should be disabled by default.
Related Perfume frontend issue: issue 99.