A forum for Spin users

You are not logged in.

#1 2014-12-15 20:35:06

Registered: 2014-08-26
Posts: 5

initial state(s) of exported promela proctype

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

Last edited by ETAS-Eder (2014-12-19 17:41:13)


#2 2014-12-16 05:32:57

Registered: 2010-11-18
Posts: 691

Re: initial state(s) of exported promela proctype

I believe that this is indeed guaranteed, so it's a safe assumption.


#3 2014-12-16 23:25:21

Registered: 2014-08-26
Posts: 5

Re: initial state(s) of exported promela proctype

That is great news, thank you.

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.


Board footer

Powered by FluxBB