Experiments on Extended Petri nets

Table 1 compares the running times and memory consumption of the Expand, Enlarge and Check prototype presented in [1] (columnEEC), with two previous prototype based on backward-search. Column Pre presents the performances of a prototype that implements the plain backward search. Column Pre+Inv reports on an an improved version that uses structural invariants of the system analyzed, in order to reduce the search space (see [2] for more details).

Table 1: results obtained on INTEL XEON 3Ghz with 4Gb of memory : cat. : category of example (PN = (unbounded) Petri net, PNT = Petri net with transfer arcs, BPN = bounded Petri net) P : number of places, T: number of transitions. EEC : results obtained with the ``Expand, Enlarge and Check'' algorithm. Pre + Inv: results obtained with a backward approach, using invariant heuristics, Pre: same without invariants. All the memory consumptions in KB and times in second.

Example					EEC		Pre+Inv		Pre
cat.	name	P	T	Safe	Time	Mem	Time	Mem	Time	Mem
PNT	CSMbroad	13	8	$\surd$	0.01	1,596	0.02	2,252	0.07	2,464
PNT	MOESI	9	11	$\surd$	0.01	1,536	0	2,160	0	2,156
PNT	german	12	8	$\surd$	0	1,472	0	2,128	0.07	2,476
PNT	Java	44	37	$\times$	8.47	23,852	1.40	3,816	time out
PNT	Javasanserreur	44	38	$\surd$	5.44	16,624	0.02	2,548	time out
PNT	consprod	18	14	$\surd$	0.05	2,012	0	1,096	21.54	5,364
PNT	consprod2	18	14	$\surd$	0.05	2,012	0	2,196	0.64	2,556
PNT	delegatebuffer	50	52	$\surd$	180.78	116,608	time out		time out
PNT	examplelea	48	42	$\surd$	6.23	10,448	4.92	9,184	time out
PNT	leabasicapproach	16	12	$\times$	0.01	1,608	0.02	2,248	0.03	2,376
PNT	queuedbusyflag	80	104	$\surd$	28.87	21,338	time out		time out
PNT	simplejavaexample	32	28	$\times$	0.19	2,656	0.56	2,784	2.70	3,720
PNT	transthesis	90	117	$\surd$	17.42	33,232	0.12	3,852	time out
PNT	efm	6	5	$\surd$	0	1,316	0.01	2,096	0.01	2,096
PN	basicME	5	4	$\surd$	0	1,064	0	1,308	0	2,076
PN	csm	14	13	$\surd$	0.02	1,748	0.09	2,516	0.11	2,512
PN	fms	22	20	$\surd$	54.43	52,796	0	1,356	28.49	8,048
PN	kanban	16	16	$\surd$	4.18	10,688	0	1,068	1111.45	24,756
PN	mesh2x2	32	32	$\surd$	0.33	3,164	0.89	2,740	0.81	2,740
PN	mesh3x2	52	54	$\surd$	1.59	6,044	10.92	4,568	8.57	4,604
PN	multipool	18	21	$\surd$	0.76	4,052	0	1,124	1.46	2,980
PN	pncsacover	31	36	$\times$	7.54	13,704	40.83	5,012	time out
BPN	lamport	11	9	$\surd$	0	1,428	0.02	2,132	0.06	2,468
BPN	newdekker	16	14	$\surd$	0.01	1,684	0.05	2,260	0.54	2,536
BPN	newrtp	9	12	$\surd$	0	1,404	0	1,096	0.05	2,340
BPN	peterson	14	12	$\surd$	0	1,520	0.04	2,244	0.12	2,504
BPN	read-write	13	9	$\surd$	0.19	2,224	0.16	2,480	0.42	2,496