Support advanced reachability tests.
Add Invariant checking.
Refinements.
Add stop machine feature.
Stop machine is done.
ok