Check multiple invariants for a CFSM with Spin

[GoogleCodeExporter]

When model checking with Spin in CSight, a sizable portion of time is used to 
compile the Promela into the model checker. We will attempt to improve 
execution time of the model checking process by checking multiple invariants 
for each compiled Spin model checker.

To implement this, we need to
* Select invariants to verify based on a heuristic.
* Generate Promela for multiple invariants and verify all of them in Spin.
* Remove each satisfied invariant.
* Refine model after each counterexample.
* If a model is refined, we need to check if the counterexamples still apply to 
the refined model. We use the counterexample if it is still valid. Otherwise, 
the counterexample is discarded and the related invariant is checked later.
* Create a separate refinement loop that can handle multiple model checker 
results.

Original issue reported on code.google.com by [email protected] on 18 Jul 2014 at 7:58

[GoogleCodeExporter]

Code review comments:

- Add tests for CSightMain.chooseInvariants function. Test the corner cases for 
this, as well as the common case.

- Fix all the comments that I added that start with:
// TODO ib:

Original comment by bestchai on 18 Aug 2014 at 11:15

• Changed state: Started