Symbolic Exploration

[marcelosousa]

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.