Here are the Petri Net benchmarks. They have been elaborated in the context of the Model Checking Contest @ Petri net since 2011 and contain contributions from the Petri net Community. Even if they often refer to well known problems or their variants, the models of these benchmarks have been proposed by colleagues coming from the following institutions:
- École Normale Supérieure de Cachan
- Universidad de Zaragoza
- Universität Rostock
- Université d’Evry Val d’Essone
- Université Geneva
- Université Paris 13
- Université Pierre & Marie Curie
Models
You can get from this page the models for your usage. However, the full archive, as well as a disk image with a virtual machine that can be operated with BenchKit are available on the Model Checking Contest @ Petri Nets web site.
These models (except planning and ring) exist for several values of one (sometimes two) scaling parameter. Colored models also exist in their P/T equivalent form.
| Model Name | PN Class | Introduced in | Archive (PNML) |
|---|---|---|---|
| CSRepetitions | Colored + equivalent P/T |
MCC’2012 | CSRepetitions.bz2 |
| Dekker | P/T | MCC’2013 | Dekker.bz2 |
| DotAndBoxes | Colored | MCC’2013 | DotAndBoxes.bz2 |
| DrinkVendingMachine | Colored + equivalent P/T |
MCC’2013 | DrinkVendingMachine.bz2 |
| Echo | P/T | MCC’2012 | Echo.bz2 |
| Eratosthenes | P/T | MCC’2012 | Eratosthenes.bz2 |
| FMS | P/T | MCC’2011 | FMS.bz2 |
| GlobalRessAlloc | Colored + equivalent P/T |
MCC’2012 | GlobalRessAlloc.bz2 |
| HouseConstruction | P/T | MCC’2013 - surprise | HouseConstruction.bz2 |
| IBMB2S565S3960 | P/T | MCC’2013 - surprise | IBMB2S565S3960.bz2 |
| Kanban | P/T | MCC’2011 | Kanban.bz2 |
| LamportFastMutEx | Colored + equivalent P/T |
MCC’2012 | LamportFastMutEx.bz2 |
| MAPK | P/T | MCC’2011 | MAPK.bz2 |
| NeoElection | Colored + equivalent P/T |
MCC’2012 | NeoElection.bz2 |
| PermAdmissibility | Colored + equivalent P/T |
MCC’2013 | PermAdmissibility.bz2 |
| Peterson | Colored + equivalent P/T |
MCC’2011 | Peterson.bz2 |
| Philosophers | Colored + equivalent P/T |
MCC’2011 | Philosophers.bz2 |
| PhilosophersDyn | Colored + equivalent P/T |
MCC’2012 | PhilosophersDyn.bz2 |
| Planning | P/T | MCC’2012 | Planning.bz2 |
| QuasiCertifProtocol | Colored + equivalent P/T |
MCC’2013 - surprise | QuasiCertifProtocol.bz2 |
| Railroad | P/T | MCC’2012 | Railroad.bz2 |
| RessAllocation | P/T | MCC’2013 | RessAllocation.bz2 |
| Ring | P/T | MCC’2012 | Ring.bz2 |
| RwMutex | P/T | MCC’2012 | RwMutex.bz2 |
| SharedMemory | Colored + equivalent P/T |
MCC’2011 | SharedMemory.bz2 |
| SimpleLoadBal | Colored + equivalent P/T |
MCC’2012 | SimpleLoadBal.bz2 |
| TokenRing | Colored + equivalent P/T |
MCC’2011 | TokenRing.bz2 |
| Vasy2003 | P/T | MCC’2013 - surprise | Vasy2003.bz2 |