Spinroot

Maxvonhippel

Member

Registered: 2019-09-13

Posts: 20

[Solved] How are states labeled?

I know how variables are labeled: from right to left.  For example:

    mtype:cmdTypes = { Close, Connect, Listen, Timeout, Null }

yields Close = cmdTypes 5, Connect = cmdTypes 4, etc.  This is evident, for example, in the dot.out file produced when I click on the automota view in the GUI.

But how are states labeled?  For instance, if I have a model like this:

proctype awesomeModel(chan some great channel, some other fantastic channel, and yet another superb channel)
{
BANANA:
    if
    :: guard 1 -> goto MANGO;
    :: guard 2 -> do something; goto HOTDOG;
    fi
MANGO:
    if
    :: guard 3 -> do something else; goto BANANA;
    fi
HOTDOG:
    if
    :: guard 4 -> goto PEACH
    fi
... etc etc
}

... then how does Spin assign labels like S0, S1, S2, etc. to the various states?  It seems to me that these correspond monotonically with my labels (e.g., BANANA, MANGO, HOTDOG, PEACH, etc.) and with the "do something"s that happen within them, so I get some sort of partitioning like

Sa0 = BANANA
Sa1 = do something
Sa2 = MANGO
Sa3 = do something else
Sa4 = HOTDOG
Sa5 = PEACH
... etc

where a0 < a1 < s2 < a3 < a4 < a5 < ...

but I am not sure if that is correct, and I am also not sure where these numbers come from since many states don't show up at all (that is to say, { a0, a1, a2, a3, ... } != { 1, 2, 3, 4, ... }).

Any guidance on this front would be much appreciated!

Last edited by Maxvonhippel (2019-09-17 04:01:44)

spinroot

forum

Registered: 2010-11-18

Posts: 700

Website

Re: [Solved] How are states labeled?

Spin computes a FSM and does some optimization and minimization, so some of the states that are originally numbered in order of creation are usually eliminated in this process. (Some of this happens in pangen5.c, see fct mkstate(n).