Let me know if you'd prefer regression tests for that assumption, so no one needs to remember it by heart. Else, I'll write them as acceptance tests in MBT Arranger: PML files as test input and state table extracts as test output.
]]>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