iSpin 6.0.2

spinroot · 2011-02-11 06:37:44

iSpin version 6.0.2 is now on the website ( [url]http://spinroot.com/spin/Src/ispin.tcl[/url] )
it fixes a few small problems that have been reported in other threads
- making it easier to use DOT when located in the default directory where the Graphviz distribution places it
- collapsing a few more rarely used panels so that the ispin display is easier to use on smaller screens (e.g., laptops)
- small bug fix with the setup for verification runs, making the run stop by default at the first counter-example found

this topic area is probably also better to collect all ispin related issues, so that we don't have to hunt for them in the other forum topics...

gauhar ali · 2011-08-04 13:11:52

when i m running verification from "ltl property manager" i received the following errors:

spin: pan_in:14, Error: syntax error saw 'operator: ?'
spin: pan_in:3, Error: proctype never_0 not found
spin: 1 error(s) - aborting

spinroot · 2011-08-04 15:20:49

it's hard to tell you what the syntax error is without seeing either the ltl formula you used or the never claim or full model

Kai · 2011-08-22 03:42:26

iSpin appears to ignore the "MSC:" prefix which made xspin show selected printf output in the MSC. I always liked that xspin feature since it helped me abuse the MSC for shared variable programs. Would it make sense to port it back to ispin?

spinroot · 2011-08-22 04:26:01

Yes, good point, that's still pending.
It'll come back in a future update.

gaviocks · 2011-09-28 09:42:00

i think ispin is also nice and useful

awesan · 2011-10-22 19:13:47

When I try to verify a model for "acceptance cycles" without any accept label in the model, I would expect it to get an error (error: no accept labels defined in model (for option -a)). However, the scroll-bar on the right does not allow me to scroll up to actually see the error. I ran into other GUI related issues with LTL formula, etc (don't remember exactly now) with iSpin. Is xSpin strictly not supported (not expected to work) with the latest SPIN or is it just discouraged?

spinroot · 2011-10-22 20:01:49

The output format of Spin changed with version 6 -- mostly to support the capabilities of iSpin.
It may be that xspin still works (since it doesn't take advantage of these changes and likely doesn't depend on all of them), but it is no longer supported.
If you find a bug in iSpin though, I'll try to fix it.

awesan · 2011-10-23 01:04:06

Got it. Thanks for the quick response. The scroll-bar not moving up (as described above in my post) is a bug. Do you want me to report it as a "bug report" in this forum or the above post is just good enough?

spinroot · 2011-10-23 01:20:26

I'm checking it out, but I can't seem to reproduce this problem.
On my display I can scroll back up to the top of the window with the right scroll bar and hold it there, although as soon as you release the scroll bar it does jump back to the end.
Does it behave the same for you?

awesan · 2011-10-23 05:28:32

hmm.. No, the behavior I see is different. When it works, I can scroll up and down with the right scroll bar and release it and the text stays (which is what I expected as opposed to jumping back to the end as you see). When it does not work, I cannot scroll up at all. Even while holding the mouse button and scrolling up (not releasing at all), it does not scroll up at all.

Here are the steps to reproduce:
1. Open a simple PROMELA model with 2 processes or more with no errors and no "LTL formula/never/accept" .
2. Syntax check. OK
3. Goto verification tab
4. Select "safety" and hit "Run". Try scrolling up and down. It works.
5. Choose "non-progress cycles" and hit "Run". Try scrolling up and down. It works.
6. Choose "acceptance cycles" and hit "Run". SPIN throws error that "error: no accept labels defined in model (for option -a).. Valid options are....". Try scrolling up and down. It does NOT work and I see the error behavior.
7. Choose "non-progress cycles" and hit "Run". Try scrolling up and down. It works again. This is the work-around. I can scroll up now and see the error message for "Step-6".

It looks like when "pan" throws the error on "accept" and list the long list of "Valid options are : ", only then I see the error. Even though in step-5 (and 7), I get an error for which pan created an error trails file, the scrolling problem did not happen.

I use Ubuntu 11.04 (natty), Spin 6.1.0 and iSpin 1.0.5. If you would like more information or the versions of any other packages I have installed, please let me know.

spinroot · 2011-10-24 18:28:39

I found the problem, and was able to fix it.
You can download a new version of ispin (version 1.0.6 from 24 October 2011) from:
http://spinroot.com/spin/Src/ispin.tcl

traumfaengerin · 2011-10-31 01:51:08

Hi,
After following step by step the installation guide for spin and ispin, the message bellow appeared on my terminal on fedora 14. I used Current Version 6.1.0 (4 May 2011)* Full distribution, with sources: spin610.tar.gz (388k).

Plz let me know what I should do.
Tnx in advance

$ ispin

No protocol specified
Application initialization failed: couldn't connect to display ":0.0"
Error in startup script: invalid command name "wm"
while executing
"wm title . "ispin""
(file "./ispin.tcl" line 11)

spinroot · 2011-10-31 02:20:25

you don't have your DISPLAY variable set in the shell
try, for instance, if the command 'xterm' works -- it will fail in the same way without a display
you'll have to figure out what your window manager is and how the display has to be set.
you could try: export DISPLAY=localhost:0 (if you use the bash shell)

traumfaengerin · 2011-10-31 23:19:05

you could try: export DISPLAY=localhost:0 (if you use the bash shell)

what do you mean?

spinroot · 2011-10-31 23:28:50

I mean that if you run the bash shell (and not the csh for instance)
then you can explicitly set the DISPLAY variable with the command I showed you:
export DISPLAY=localhost:0
if the csh this becomes
set DISPLAY localhost:0

traumfaengerin · 2011-11-01 02:57:24

I mean that if you run the bash shell (and not the csh for instance) ====> how do I run the bash shell?
then you can explicitly set the DISPLAY variable with the command I showed you:
export DISPLAY=localhost:0
if the csh this becomes =====> how the csh becomes?
set DISPLAY localhost:0

spinroot · 2011-11-01 03:05:09

bash shell: type 'bash' or type 'sh'
that typically defaults to the bash shell

to get the csh, type 'csh'

it's standard unix/linux stuff

awesan · 2011-11-05 20:59:38

> spinroot wrote:

> I found the problem, and was able to fix it.
ispin 1.0.6 fixes it. Thanks. The web-page http://spinroot.com/spin/Src/ lists the version of iSpin as 3.0.6 as opposed to 1.0.6. Though launching iSpin lists the correct version.

Spinroot

#1 2011-02-11 06:37:44

iSpin 6.0.2

#2 2011-08-04 13:11:52

Re: iSpin 6.0.2

#3 2011-08-04 15:20:49

Re: iSpin 6.0.2

#4 2011-08-22 03:42:26

Re: iSpin 6.0.2

#5 2011-08-22 04:26:01

Re: iSpin 6.0.2

#6 2011-09-28 09:42:00

Re: iSpin 6.0.2

#7 2011-10-22 19:13:47

Re: iSpin 6.0.2

#8 2011-10-22 20:01:49

Re: iSpin 6.0.2

#9 2011-10-23 01:04:06

Re: iSpin 6.0.2

#10 2011-10-23 01:20:26

Re: iSpin 6.0.2

#11 2011-10-23 05:28:32

Re: iSpin 6.0.2

#12 2011-10-24 18:28:39

Re: iSpin 6.0.2

#13 2011-10-31 01:51:08

Re: iSpin 6.0.2

#14 2011-10-31 02:20:25

Re: iSpin 6.0.2

#15 2011-10-31 23:19:05

Re: iSpin 6.0.2

#16 2011-10-31 23:28:50

Re: iSpin 6.0.2

#17 2011-11-01 02:57:24

Re: iSpin 6.0.2

#18 2011-11-01 03:05:09

Re: iSpin 6.0.2

#19 2011-11-05 20:59:38

Re: iSpin 6.0.2

Board footer