Spinroot

Hi there,

we want to process PROMELA proctypes as automata. With MBT Arranger one can define data, state and transition coverage criteria to generate NOTRACEs, which in turn generate testcases.
I have published a video on youtoube ( http://youtu.be/8SjWP42uoq4 ) where you can watch the 3 processing stages involved:
(1b) the raw machine automaton is visualized, as output by SPIN.
(2b) a trimmed version of that automaton is visualized, as processed by consuming ARRANGE operators.
(3b) a depth-first transition covering test sequence is rendered.

As you can see, MBT Arranger trims the terminal sequence fine, it is well recognizable. I have a question regarding initial state. How should the initial state(s) be identified.
The current approach is to use the first state from the DIGRAPH listing, e.g. S12 in

digraph p_boaClient1 {
  GT [shape=box,style=dotted,label="boaClient1"];
    S12 -> S2  [color=black,style=bold,label="chin?cfg_buffer,_"];
    S12 -> S4  [color=black,style=bold,label="chin?cfg_channel,_"];
    S12 -> S6  [color=black,style=bold,label="chin?cfg_baudrate,_"];
    S12 -> S8  [color=black,style=bold,label="chin?cfg_selfRcpt,_"];
    S12 -> S10  [color=black,style=bold,label="chin?tx"];
    S12 -> S15  [color=black,style=bold,label="goto :b0"];
    S2 -> S12  [color=black,style=bold,label="chout!cfg_return"];
    S4 -> S12  [color=black,style=bold,label="chout!cfg_return"];
    S6 -> S12  [color=black,style=bold,label="chout!cfg_return"];
    S8 -> S12  [color=black,style=bold,label="chout!cfg_return"];
    S10 -> S12  [color=black,style=bold,label="chout!rx"];
    S15 -> S0  [color=black,style=solid,label="-end-"];
  S15 [color=blue,style=bold,shape=box];
}

Manual inspection of DIGRAPHs exported from SPIN gave me empirical confidence, but is this guaranteed by design?
I could easily replace the DIGRAPH parser with a parser for your state table exports. Both have exported transitions in identical order.

Kind regards
Dennis