A forum for Spin users
You are not logged in.
Pages: 1
Small glitch in the earlier versions of iSpin.
By default, when you do a verification, the earlier versions did not stop at the first error found, but complete the verification run fully without writing error trails. (This is the behavior when you give ./pan the flag -c0.)
The correct default is -c1, which makes the model checker stop at the first error found, and write an error trail that can then be used in a guided simulation.
iSpin Version 6.0.3, dated January 4, 2011, fixes this problem. You can download it from the usual place: [url]http://spinroot.com/spin/Src/ispin.tcl[/url]
Offline
Pages: 1