Spinroot

awesan

Member

Registered: 2011-04-30

Posts: 45

iSpin passes "-f" option to pan incorrectly while verifying safety

Steps to reproduce this issue:
1. Open a model in iSpin
2. In "Verification" tab, choose "non-progress cycles" and click "enforce weak fairness constraint"
3. Hit "Run"
4. Choose "safety"
5. Hit "Run"
You get the following error :
**************************
./pan -m10000  -f
Pid: 5719
saw option -f
Spin Version 6.1.0 -- 2 May 2011
    -a,-l,-f  -> are disabled by -DSAFETY
**************************
It looks like "enforce weak fairness constraint" is a "liveness" related option and iSpin should not pass "-f" to pan when "safety" is chosen for verification.