A forum for Spin users

You are not logged in.

- Topics: Active | Unanswered

Pages: **1**

**Dharma****Member**- Registered: 2011-09-21
- Posts: 13

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)*

Offline

Pages: **1**