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

Implement widening across multiple executions of collapse #28

Open
marcelosousa opened this issue Jan 10, 2017 · 1 comment
Open

Implement widening across multiple executions of collapse #28

marcelosousa opened this issue Jan 10, 2017 · 1 comment
Assignees

Comments

@marcelosousa
Copy link
Owner

Within a configuration, we would like to apply widening even if multiple executions of collapse have been issued. That is the only way to achieve termination of the analysis.
There are two possibilities to implement this feature:

  1. In the collapse by passing extra information, e.g. the CFG annotated with the previous states.
  2. In the unfolding algorithm, by keeping track per configuration a Map from EventName to IntState.
@marcelosousa
Copy link
Owner Author

Widening needs to return actions as well.

@marcelosousa marcelosousa self-assigned this Jan 11, 2017
@marcelosousa marcelosousa added this to the CAV 2016 milestone Jan 11, 2017
@marcelosousa marcelosousa removed this from the CAV 2016 milestone Jan 21, 2017
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

1 participant