Spinroot

A forum for Spin users

You are not logged in.

#1 2011-11-07 01:51:10

awesan
Member
Registered: 2011-04-30
Posts: 45

iSpin verification choice is not sticky

After opening a model, if I switch to "verification" tab, "non-progress cycles" is selected by default. I think that is ok. However, if I choose "safety" and verify and then go to "Edit/View" tab and come back to "verification" tab, I see that "non-progress cycles" is selected again by default. I would expect whatever verification options I chose before (in this case, "safety") to be sticky. And, it is my expectation and I would not complain if the current behavior is by design though.

Offline

#2 2011-11-07 02:22:59

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: iSpin verification choice is not sticky

the option is pre-selected if iSpin notices that you have a progress label defined.
it's true that that can get annoying if you want to verify safety properties instead,
but it's equally annoying to forget to enable non-progress cycle checks, and then
erroneously conclude that there were none.  difficult choice here for the tool.

Offline

#3 2011-11-07 02:52:26

awesan
Member
Registered: 2011-04-30
Posts: 45

Re: iSpin verification choice is not sticky

I see your point. However, sometimes, it defaults to "acceptance cycles", even if I did not have any progress label defined. Not sure whether it happens, if I have "ltl formulae" in the model. It is a bit confusing and I cannot catch the exact pattern. One can argue this way "iSpin can default to any settings when a model is opened first. However, if one switches to other tab to modify/reopen the model and switches back to verification tab, he would normally expect the same verification options to stay, since it is more likely he is modifying the model to fix the errors thrown earlier".  On the other hand, one can certainly live with it with a mind-set to check all the verification configuration options before hitting "Run" after modifying the model every time.

Offline

Board footer

Powered by FluxBB