Spinroot

A forum for Spin users

You are not logged in.

#1 2011-11-20 02:41:38

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

Extra Verifier Generator Options does not work in simulation mode

The options that I pass to "Extra Verifier Generator Options" field under "Verification" tab (like "-DTEST1") does not work in random or interactive simulation mode under "Simulate/Replay". I have to either modify these definitions in the model every time or go command-line. It would be nice either to add an extra field for "Extra Verifier Generator Options" in "Simulate/Replay" tab or allow the ones chosen in "Verification" tab to be effective for simulation. People might think former might be ideal and more intuitive but the latter is equally acceptable for me.

Offline

#2 2011-11-25 05:32:22

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

Re: Extra Verifier Generator Options does not work in simulation mode

As a matter of fact, "Extra Verifier Generator Options" field under "Verification" tab (like "-DTEST1") does not get passed to spin in "Guided Simulation with Trail"  under "Simulate/Replay" also. You can check this by observing the text-box "Background command executed". This could be very confusing, since "Replay" actually uses a different model (without the preprocesor directive like "-DTEST1" passed to it) than the one verified with that directive. I get weird errors like "transition failed" on replaying the error trail. So, for now, if using iSpin, it is a good idea to refrain from using "Extra Verifier Generator Options" and define the directive directly in the model (for instance, #define TEST1 1). Or, use "command-line" spin directly and do NOT forget to pass the preprocessor directive while replaying the error trail also.

Offline

#3 2011-11-29 23:50:34

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

Re: Extra Verifier Generator Options does not work in simulation mode

I agree that this is annoying -- I'll plan on fixing this for the next update of ispin.

Offline

#4 2012-01-25 06:44:31

Jamesmorris
Member
From: Boca Raton, FL
Registered: 2012-01-25
Posts: 1
Website

Re: Extra Verifier Generator Options does not work in simulation mode

When will be the update available ?

Offline

#5 2012-01-25 06:46:39

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

Re: Extra Verifier Generator Options does not work in simulation mode

sorry for the long wait -- i'll try to get to it soon

Offline

#6 2012-06-01 00:17:23

glemoh
Member
Registered: 2012-06-01
Posts: 1
Website

Re: Extra Verifier Generator Options does not work in simulation mode

Is there new version and when its update will release?

Offline

#7 2012-06-04 06:05:36

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

Re: Extra Verifier Generator Options does not work in simulation mode

no newer version yet -- it's long overdue

Offline

#8 2012-06-06 19:28:27

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

Re: Extra Verifier Generator Options does not work in simulation mode

A new version of ispin.tcl is now available at:
http://spinroot.com/spin/Src/
(it has not yet been updated within the .zip file or the main source distribution though, so make sure you use the direct download of ispin.tcl itself on this page)
The version number for the fixed version of ispin is:  iSpin Version 1.1.0 -- 7 June 2012.

Offline

Board footer

Powered by FluxBB