SUMo'2011
International Workshop on
Scalable and Usable Model Checking for
Petri Nets and other models of Concurrency

Introduction

This page will contain questions and answers that will be raised during the contest or its preparation.

Q: in PNML, shall I use Ids or the value of attribute NAME as objects (places, transitions) names?

PNML proposes the notion of Id to ensure the unique identification of nodes and edges in a specification. It is there for this technical aspect only. We ensured that all objects in our Petri nets are named differently. Thus, you can use names as a discriminant. It is recommended.

Q: I have no time to create a transfer program from PNML to my own format, what could I do ?

EVen if building such a program could be useful for the visibility of your tool, as well as its interoperability with other tools, this is not necessary for the Model Checking Contest.

If you put, in the same directory than the one containing the PNML files, a set of files dedicated to your own tool (please provide these for all the expected instances), you can use these when our running script invoke you tool instead of the PNML files. Be careful however to provide the exact same model with the exact same places and transitions (the pictures in each model presentation should help you).

A satellite event of PETRI NETS'2011 and ACSD'2011
June  21, 2011

Model Checking Contest, FAQ

PeoplePeople.html
PetersonPeterson_model.html
PhilosopherPhilosophers_model.html
SharedMemorySharedMemory_model.html
FMSFMS_model.html
KanbanKanban_model.html
MAPKMAPK_model.html
FAQ
BNF FormulaeBNF_for_formulae.html

Models

RulesRules.html
TokenRingTokenRing_model.html
Submission Kithttp://sumo.lip6.fr/SUMo-2011-MCC-BASE.tgz