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