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

Description of the «FMS» model

This Petri net is extracted  a benchmark used for SMART. It models a flexible manufacturing system.


The figure above shows this model with a marking set up for 5.

Scale factor

The scale factor is a value that changes the initial marking of places P1, P2 and P3 (M(P1)=M(P2)=M(P3)=N). Proposed instances use the following values: 2, 5, 10, 20, 50, 100, 200, 500.

Model files

PNML files and a set of properties respecting the BNF we propose are available in the submission kit.

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

Model Checking Contest, «FMS» model

PeoplePeople.html
PetersonPeterson_model.html
PhilosopherPhilosophers_model.html
SharedMemorySharedMemory_model.html
FMS
KanbanKanban_model.html
MAPKMAPK_model.html
FAQFAQ.html
BNF FormulaeBNF_for_formulae.html

Models

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