Spinroot

Dharma

Member

Registered: 2011-09-21

Posts: 13

unreached in init?

Hi,

I modeled the Petri net given in [url]http://en.wikipedia.org/wiki/File:Two-boundedness-cb.png[/url] using Promela as follows.

#define Place byte /* assume < 256 tokens per place */
Place p1, p2
Place cp1, cp2
#define inp1(x) (x>0) -> x=x-1
#define inp2(x,y) (x>0&&y>0) -> x = x-1; y=y-1
#define out1(x) x=x+1
#define out2(x,y) x=x+1; y=y+1
init
{ cp1 = 2; cp2 = 2; /* initial marking */
do
/*t1*/ :: atomic { inp1(cp1) -> out1(p1) }
/*t2*/ :: atomic { inp2(p1, cp2) -> out2(p2, cp1) }
/*t3*/ :: atomic { inp1(p2) -> out1(cp2) }
od
}

I was curious to check the 2-bounded property of this Petri net using spin. Got this output form spin:

unreached in init
    cp_net3.pml:15, state 20, "-end-"
    (1 of 20 states)

Does it mean that this model will not terminate?  Of course, the petri net is always running without any deadlock as far as I can see manually.

Of course, this model is based on SPIN exercises/examples.

Last edited by Dharma (2011-09-26 15:55:09)

spinroot

forum

Registered: 2010-11-18

Posts: 700

Website

Re: unreached in init?

it only means that there is no unreachable code in this model, and no deadlock.
to prove two-boundedness, you have to formulate the right assertion or ltl property and then prove it...