This folder contains supplementary material
for the article submitted to the CSMB 2010

---------------------------------------------------------------------------------------

folder content:

IDD-MC
	a prototype of our IDD-based CTL/CSL model checker
	(64bit version for MAC OS)

	Attention: 
	On our web sides there are IDD-CSL linux versions available,
	but they currently do not support the CSL specification used in our examples  

Snoopy
	Mac OS X (32bit) & Windows (64bit) version of Snoopy
	

experiments

the subfolders  
	ANG
	ERK
	MAPK
contain input files for Snoopy and IDD-MC


---------------------------------------------------------------------------------------

IDD-MC example session:

You can run IDD-MC to repeat our experiments in the following fashion:

iddmc --net-file=ERK/erk.apnn --csl-file=ERK/transient_interval.csl --const N=10,place=MEKpp,time=40,lb=0.6,ub=0.8

it will check the model with initially 10 token on RP,RKIP,Raf1Star,ERK and MEKpp
against the CSL formula
P=?[F[40,40] MEKpp >= 10*0.6 & MEKpp <= 10*0.8 ]

using option --help will display further options as for instance
	--place-order  	(for ERK we used --place-order=1)
	--cache-layer 	(for ANG we used --cache-layer=8)


Snoopy example session:

You can run Snoopy to repeat our experiments in following fashion:

- install and run Snoopy
- load the net (erk.spstochpn)
- hit "F5" or "View" -> "Start Anim-Mode"
- press "Stochastic Simulation"
- select "Marking set" and "Parameter set" (N10)
- select Simulator (Gillespie)
- change Simulator "Properties" , simulation run count = 40000000, number of thread
- load the state property from the .sp files
- change interval end to the related value (t=40)
- press "Start Simulation"

---------------------------------------------------------------------------------------
07.05.2010
Martin Schwarick	(ms@informatik.tu-cottbus.de)
Christian Rohr 		(rohr@mpi-magdeburg.mpg.de)