SpinSpider (automata): transitions from init to proctype

[GoogleCodeExporter]

What steps will reproduce the problem?
1. Open example.pml (attached)
2. SpinSpinner, automata, run 

What is the expected output? 
 There subgraphs for init and proctype dstore should be disjoint

What do you see instead?
 There is a transition from the statement in line 44 (init state 2) to the statement in line 30 (dstore state 7).

What version of the product are you using? 
 5.0

Please provide any additional information below.

 Read.createStatements increments the process number if (s.indexOf("proctype") != -1), but ignores the line that begins with "init". Then two statements may be assigned with the same process number and the same id, and the input to dot is wrong. 

I modified Read as follows:

s=trim();
if (s.startsWith("proctype") || s.startsWith("init")) ...

Original issue reported on code.google.com by m...@rjgodoy.com.ar on 19 Feb 2013 at 4:34

Attachments:

• pan-d-output
• example.pml

[GoogleCodeExporter]

Hi,

SpinSpider is intended for use with _very small_ programs of at most 20-30 
states that you can use in teaching basic concepts. Your example program has 
_thousands_ of states and the graph would be impossible to read. Furthermore, 
the software is _very fragile_ because Spin was not designed for this purpose 
and I used many "hacks". SpinSpider will not work with programs that use 
advanced features of Spin.

For all these reasons, I will not continue to develop SpinSpider (as opposed to 
jSpin itself which I regard as an active project). Instead, I developed a 
Spin-compatible model checker called Erigone which very much simplifies the 
production of state space graphs (even incrementally!!). Again, the intention 
is only to use it for _very small_ Promela programs. You can find it by 
searching "Erigone" on Google Project Hosting or by following a link on the 
jSpin page. I do consider Erigone including its support for visualization 
(called VMC) to be an active project and will respond to bugs and consider 
suggestions for improvements.

Moti

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