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.

Sign up for GitHub

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

Jump to bottom

Symbolic Exploration #2

Open
marcelosousa opened this issue Sep 22, 2015 · 0 comments
Open

Symbolic Exploration #2

marcelosousa opened this issue Sep 22, 2015 · 0 comments
Assignees
@marcelosousa
Milestone
Symbolic Unfolding

Comments

@marcelosousa
Copy link
Owner

Currently, poet is an explicit-state model checker. Modify the execution engine to allow formulas.
This involves a major revision of the current engine:

  • Convert the code to SSA on-the-fly.
  • State is just a Map Variable Value. This needs to be changed so that State can be a Formula.
  • Converter needs to be completely re-written.
  • Independence relation computation?
  • Reduce the problem of checking which transitions are enabled to a satisfiability problem.
@marcelosousa marcelosousa modified the milestone: Symbolic Unfolding Sep 22, 2015
marcelosousa added a commit that referenced this issue Jan 6, 2017
@marcelosousa
fixed #24. fixed #23. working on #2
74f6074
@marcelosousa marcelosousa self-assigned this Jan 6, 2017
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@marcelosousa marcelosousa

Labels
None yet
Projects
None yet
Milestone
Symbolic Unfolding
Development

No branches or pull requests
1 participant
@marcelosousa