SpinSpider does not create Visualization

[GoogleCodeExporter]

What steps will reproduce the problem?
1. copy a promela file like the attached one to an path containing white
spaces e.g. "C:\Users\andi\Documents\Dokumente\Uni\Koblenz\SS2009\Formale
Spezifikation und Verifikation\09-08-05 - Blockkurs
1\examples\lect05\start\interleave01.pml"
2. try to create a visualization with jSpin 4.6 and SpinSpider
3. Nothing is displayed

What is the expected output? What do you see instead?
Expected output is the graph visualization as png immage

What version of the product are you using? On what operating system?
jspin 4.6 on Windows Vista Business x64, SP 2

Please provide any additional information below.
Tests have shown, that the dot file is correctly created, but the png file
is not created at all. Manual tests have shown, that dot.exe is not able to
handle white spaces in path names. Launching dot.exe with the created
dot-file and adding "  " around the path creates the png file correctly. So
the path-variable in SpinSpider should be embraced by ".."

Original issue reported on code.google.com by andif...@gmail.com on 5 Aug 2009 at 10:38

Attachments:

• interleave1.pml

[GoogleCodeExporter]

I have also found that if the promela file is located in a directory whose name 
begins with "u" (e.g. J:\u\spin1.pml or J:\uwhatever\spin1.pml) the jSpin 
visualization is empty (no trail/emphasize trail/only trail).

Workaround: move the file somewhere else. Visualization works the file is 
copied to J:\aaa\spin1.pml

Writing never claim
Running spin.exe -a -o3  -N J:\u\spin1.nvr J:\u\spin1.pml
Running X:\MinGW\bin\gcc.exe -DCHECK -DSAFETY -DPRINTF -DNOREDUCE -o pan pan.c
Running J:\u\pan
IO exception Cannot run program "J:\u\pan" (in directory "J:\u"): CreateProcess 
error=2, El sistema no puede hallar el archivo especificado while executing 
J:\u\pan
Running J:\u\pan -d
IO exception Cannot run program "J:\u\pan" (in directory "J:\u"): CreateProcess 
error=2, El sistema no puede hallar el archivo especificado while executing 
J:\u\pan -d
Reading -d file
FILE ERROR J:\u\spin1.d (the never claim may be missing)
Reading -DCHECK file
Writing dot file
Running C:\ARCHIV~1\Graphviz2.26.3\bin\dot.exe -Tpng -o J:\u\spin1.png 
J:\u\spin1.dot
Done

Original comment by m...@rjgodoy.com.ar on 19 Feb 2013 at 9:02

[GoogleCodeExporter]

OS: Windows XP SP3 [5.1.2600]
graphviz: version 2.26.3
Spin Version 6.2.3
jspin: 5.0
Java(TM) SE Runtime Environment (build 1.7.0_13-b20) 
Java HotSpot(TM) Client VM (build 23.7-b01)

Original comment by m...@rjgodoy.com.ar on 19 Feb 2013 at 9:05

[GoogleCodeExporter]

Apparently what is happening is that it is interpreting \u and the start of an 
unsigned number. Similarly, \x is interpreted as the start of a hex number. 
I'll try to figure out a fix, but in the meantime you can use other directory 
names.
Thanks
Moti

Original comment by moti.ben.ari@gmail.com on 19 Feb 2013 at 9:38

[GoogleCodeExporter]

There really is a problem which is caused by Spin itself not recognizing 
Windows file names with backslashes when the command is run by forking a 
process from the Java program. I tried to fix it but I can't do it without 
making jSpin non-portable. Since there is a simple workaround and since I'm not 
interested in supporting SpinSpider (in favor of a better facility in Erigone), 
I won't be pursuing this. Thanks for pointing it out.

Original comment by moti.ben.ari@gmail.com on 21 Feb 2013 at 7:23

[GoogleCodeExporter]

I understand the decision of not supporting SpinSpider. Thanks for explaining 
where is the issue. 

Original comment by m...@rjgodoy.com.ar on 22 Feb 2013 at 4:59