Spinroot
A forum for Spin users
You are not logged in.
- Topics: Active | Unanswered
#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
#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
#8 2012-06-06 19:28:27
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