search

ModelInference / synoptic

Inferring models of systems from observations of their behavior
Other
81 stars 25 forks source link

Parallelize McScM model checking #377

Closed GoogleCodeExporter closed 9 years ago

GoogleCodeExporter commented 9 years ago 
The same CFSM model can be model checked against multiple invariants 
simultaneously to speed-up CSight.

The same CFSM can be augmented with different invariants to run multiple McScM 
instances. A total of N model checking processes can be ran at once. When one 
of the processes return safe, start another process to maintain the 
parallelization factor. When one of the processes return unsafe, stop all model 
checking processes and refine the model.

Original issue reported on code.google.com by bobyan...@gmail.com on 18 Jul 2014 at 5:24

GoogleCodeExporter commented 9 years ago 
Merged into default with revision 2c21e2909bf0

Original comment by bestchai on 14 Aug 2014 at 6:57