Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Display delta between Synoptic and Perfume model #80

Open
bestchai opened this issue May 27, 2020 · 0 comments
Open

Display delta between Synoptic and Perfume model #80

bestchai opened this issue May 27, 2020 · 0 comments
Labels
enhancement New feature or request

Comments

@bestchai
Copy link
Member

bestchai commented May 27, 2020

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]

@bestchai bestchai added the enhancement New feature or request label May 27, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request
Projects
None yet
Development

No branches or pull requests

1 participant