EXAMPLES: dsszmc benchmark suite
=================================

This folder contains six case studies for the DSSZ-MC tool.
They are give in the Abstract Petri Net Format (APNN) in the apnn folder.
To give you the chance to create or manipulate the models we also provide the related snoopy files in the snoopy folder.
To create other philosopher files use the given Java program.

We also submit the smart folder, which contains the related SMART (see http://www.cs.ucr.edu/~ciardo/SMART/) files. 


The results are published in:
M Heiner, M Schwarick, A Tovchigrechko:
DSSZ-MC - A Tool for Symbolic Analysis of Extended Petri Nets;
Proc. PETRI NETS 2009, Paris, June 2009, Springer LNCS 5606, pp. 323-332.


FILES

_dsszmc_benchmarks.tgz			- all the following files, including this read.me

SMART					- input files for the SMART tool
					the models have been created by hand, maybe there are better place 						partitionings.

dsszmc_benchmarks/smart/erk.smart
dsszmc_benchmarks/smart/ack3.smart
dsszmc_benchmarks/smart/fms_level19.smart
dsszmc_benchmarks/smart/phils.smart
dsszmc_benchmarks/smart/kanban.smart
dsszmc_benchmarks/smart/levchenko.smart

SNOOPY					- SNOOPY files

dsszmc_benchmarks/snoopy/fms.spped
dsszmc_benchmarks/snoopy/ack3.spped
dsszmc_benchmarks/snoopy/kanban.spped
dsszmc_benchmarks/snoopy/erk.spped
dsszmc_benchmarks/snoopy/levchenko_N4.spped


dsszmc_benchmarks/Phils.class			- a small Java program to create APNN files for the 						philosophers						
					type  	"java Phils" to run it;
					the program will ask for the number of philosophers

APNN					- the input files for DSSZ-MC

dsszmc_benchmarks/apnn/erk/erk_N600.apnn
dsszmc_benchmarks/apnn/erk/erk_N100.apnn
dsszmc_benchmarks/apnn/erk/erk_N500.apnn
dsszmc_benchmarks/apnn/erk/erk_N50.apnn
dsszmc_benchmarks/apnn/erk/erk_N200.apnn
dsszmc_benchmarks/apnn/erk/erk_N700.apnn
dsszmc_benchmarks/apnn/erk/erk_N400.apnn

dsszmc_benchmarks/apnn/ack/ack3_2.apnn
dsszmc_benchmarks/apnn/ack/ack3_3.apnn
dsszmc_benchmarks/apnn/ack/ack3_4.apnn

dsszmc_benchmarks/apnn/fms/FMS_N300.apnn
dsszmc_benchmarks/apnn/fms/FMS_N100.apnn
dsszmc_benchmarks/apnn/fms/FMS_N250.apnn
dsszmc_benchmarks/apnn/fms/FMS_N200.apnn

dsszmc_benchmarks/apnn/kanban/kanban_N300.apnn
dsszmc_benchmarks/apnn/kanban/kanban_N50.apnn
dsszmc_benchmarks/apnn/kanban/kanban_N200.apnn
dsszmc_benchmarks/apnn/kanban/kanban_N100.apnn
dsszmc_benchmarks/apnn/kanban/kanban_N75.apnn

dsszmc_benchmarks/apnn/levchenko/levchenko_N120.apnn
dsszmc_benchmarks/apnn/levchenko/levchenko_N20.apnn
dsszmc_benchmarks/apnn/levchenko/levchenko_N80.apnn
dsszmc_benchmarks/apnn/levchenko/levchenko_N160.apnn
dsszmc_benchmarks/apnn/levchenko/levchenko_N40.apnn
dsszmc_benchmarks/apnn/levchenko/levchenko_N320.apnn

dsszmc_benchmarks/apnn/phils/phils_N500.apnn
dsszmc_benchmarks/apnn/phils/phils_N1000.apnn

-- the end -- 26.01.2010 -- ms --