fond

jQuery Multi Level CSS Menu Css3Menu.com

Model Checking Contest 2022
12th edition, Bergen, Norway, June 21, 2022
Models for 2021
Last Updated
Jun 22, 2022

Introduction

The benchmark proposed for the MCC'2021 consists of P/T nets (1-bounded, k-bounded, unbounded), and colored Nets (1 and k-bounded per color, with and without non-equal guards on transitions, with and without cartesian product on colors, with and without successor/predecessor functions).

For a number of P/T nets, additional information about the concurrent structure of these nets is provided under the form of a NUPN (Nested-Unit Petri Net) "tool specific" element in the PNML file. This information can be exploited by tools at will.

For colored Petri Nets, equivalent P/T nets are provided in most of the cases.

Two classes of models are provided:

All models are provided as PNML files. The two types of models are provided with a detailed set of characteristics that tools can exploit when possible.

Models (both academic and industrial) are separated in two categories:

Model Contributors

The section below list the people who provided models to the various editions of the Model Checking Contest. These models are used for the contest but also serve as benchmarks for many other people (see here).

Sometime, they are authors of these models, otherwise, they have summarized or retrieved an existing model from the literature... thus, since they champion these models, they are "responsible" for them and, since they were of great help for establishing the base of our benchmark, they are listed below:

Full model archive with formulas for 2022

You can get the full archive with the formulas for 2022 (when the examination requires it) here.

«Surprise» Models for 2022

We are happy to announce the 13 «surprise» models for 2022 (206 instances in total).

Name PN Type Scale Parameter(s) Data on the Model form PNML
AutonomousCar

AutonomousCar, proposed by Lucie Muller and Hubert Garavel

This model simulates realistic scenes involving a car moving towards a destination and trying to avoid collision with obstacles

 		P/T Yes Places: up to 425, Transitions: up to 2 252, Arcs: up to 2 9816
BugTracking

BugTracking, proposed by Y. Thierry-Mieg

This Petri net models a bug tracking system managing bug reports

 		P/T Yes Places: 754, Transitions: 27 370, Arcs: 136 172
CANInsertWithFailure

CANInsertWithFailure, proposed by Rosa Mendas, Fabrice Kordon

This Petri net models the construction of a CAN (Content-Addressable Network) that considers possible failures from the network.

 		P/T Yes Places: up to 21204, Transitions: up to 60 600, Arcs: up to 162 000
DBSingleClientW

DBSingleClientW, proposed by Y. Thierry-Mieg

This model is derived from an Erlang program (produced by a converter called Soter)

 		P/T Yes Places: up to 4 763, Transitions: up to 2 478, Arcs: up to 9 912
DoubleLock

DoubleLock, proposed by Y. Thierry-Mieg

This model is derived from a concurrent C program

 		P/T Yes Places: up to 570, Transitions: up to 7 600, Arcs: up to 12 672
FunctionPointer

FunctionPointer, proposed by Y. Thierry-Mieg

This model is derived from a C concurrent program

 		P/T Yes Places: up to 2 826, Transitions: up to 8 960, Arcs: up to 36 096
Medical

Medical, proposed by Y. Thierry-Mieg

This model describes the MyHealth Protal

 		P/T Yes Places: 312, Transitions: 5 431, Arcs: 28 790
RERS2020

RERS2020, proposed by M. Jasper, F. Kordon, and H. Garavel

These models were presented to the RERS challenge in 2020 (parrallel problems)

 		P/T Yes Places: up to 2 339, Transitions: up to 153 412, Arcs: up to 610 156
RingSingleMessageInMbox

RingSingleMessageInMbox, proposed by Y. Thierry-Mieg

This model is derived from an Erlang program (produced by a converter called Soter)

 		P/T Yes Places: up to 66 950, Transitions: up to 213 625, Arcs: up to 854 500
SieveSingleMsgMbox

SieveSingleMsgMbox, proposed by Y. Thierry-Mieg

This model is derived from an Erlang program (produced by a converter called Soter)

 		P/T Yes Places: up to 23 98, Transitions: up to 1 954, Arcs: up to 7 816
StigmergyCommit

StigmergyCommit, proposed by Luca Di Stefano and Hubert Garavel

These Petri nets model a variation of a two-phase commit protocol

 		P/T Yes Places: up to 3 655, Transitions: up to 1 070 836, Arcs: up to 25 615 632
StigmergyElection

StigmergyElection, proposed by Luca Di Stefano and Hubert Garavel

This Petri net describes a an bully election algorithm among N agents

 		P/T Yes Places: up to 1 515, Transitions: up to 357 966, Arcs: up to 7 842 915
Szymanski

Szymanski, proposed by Y. Thierry-Mieg

This models are variants on Szymanski’s solution to Lamport mutual exclusion problem.

 		P/T Yes Places: up to 568, Transitions: up to 8 320, Arcs: up to 33 408

«Known» Models for 2022

The table below summarizes the «Known» models which have been enriched over the years during the past editions of the Model Checking Contest.

Name PN Type Scale Parameter(s) Data on the Model form PNML
Proposed in 2021 (11 models)
CANConstruction

CANConstruction, proposed by Rosa Mendas, Fabrice Kordon

This Petri net models the construction of a CAN (Content-Addressable Network).

 		P/T Yes Places: up to 21 202, Transitions: up to 40 800, Arcs: up to 122 000
Election2020

Election 2020, proposed by Elvio G. Amparore

The Petri net models the US election map of the 2020 elections.

 		P/T None Places: 53, Transitions: 102, Arcs: 204
GPUForwardProgress

GPU Forward Progress, proposed by Hugues Evrard, Lucas F. Salvador, Tyler Sorensen

The model describes how a GPU computation may ensure termination in the absence of inter-workgroup forward progress guarantees

 		P/T Yes Places: up to 796, Transitions: up to 827, Arcs: up to 2077
HealthRecord

Health Record, proposed by Nick Feng, Lina Marso, and Hubert Garavel

This Petri net models a computer system keeping track of personal health information.

 		P/T Yes Places: up to 624, Transitions: up to 828, Arcs: up to 1879
HirschbergSinclair

HirschbergSinclair, proposed by Tra My Nguyen, Fabrice Kordon

This net models a simplified version of the Hirschberg and Sinclair algorithm

 		P/T Yes Places: up to 1 208, Transitions: up to 1 102, Arcs: up to 3 361
LeafsetExtension

LeafsetExtension, proposed by Antoine Toullalan, Fabrice Kordon

This Petri net models the extension of a LeafSet in a pastry DHT (distributed Hash Table).

 		P/T Yes Places: up to 21 462, Transitions: up to 21 129, Arcs: up to 67 740
MultiCrashLeafsetExtension

MultiCrashLeafsetExtension, proposed by Antoine Toullalan, Fabrice Kordon

This Petri net models the extension of a LeafSet in a pastry DHT (distributed Hash Table) when there are several crashes (then extensions must be handled).

 		P/T Yes Places: up to 36 724, Transitions: up to 54 827, Arcs: up to 203 278
SemanticWebServices

SemanticWebServices, proposed by Karsten Wolf

This Petri net models a system that is a composition of web services.

 		P/T Yes Places: up to 439, Transitions: up to 27 524, Arcs: up to 270 595
ServersAndClients

ServersAndClients, proposed by Tra My Nguyen, Fabrice Kordon

This is a simple model of a Client server system

 		P/T Yes Places: up to 65 761, Transitions: up to 128 800, Arcs: up to 387 200
TwoPhaseLocking

TwoPhaseLocking, proposed by Elvio G. Amparore

The model simulates a problematic condition where a badly-designed process violates the two phase locking (2PL) protocol rules.

 		P/T Yes Places: 8, Transitions: 6, Arcs: 18
UtilityControlRoom

UtilityControlRoom, proposed by Elvio G. Amparore

This Petri net models a use case of a control room of a utility company and comes from the project HoliDes

 		Colored +
P/T equiv		 Yes Places: 13, Transitions: 12, Arcs: 37
Proposed in 2020 (10 models)
SatelliteMemory

SatelliteMemory, proposed by Frédéric Cristini and Silvano

models the stylized behaviour of the mass memory management system in a micro-satellite from the Myriade product line, designed by CNES, the French Space Agency

 		P/T Yes Places: 13, Transitions: 10, Arcs: 40
ShieldIIPs

, proposed by

This Place-Transition net models one of the six implementation variants of a circuit shield againts physical attacks

 		P/T None Places: up to 7 003, Transitions: up to 5 903, Arcs: up to 17 806
ShieldIIPt

, proposed by

This Place-Transition net models one of the six implementation variants of a circuit shield againts physical attacks

 		P/T None Places: up to 7 003, Transitions: up to 6 503, Arcs: up to 12 206
ShieldPPPs

, proposed by

This Place-Transition net models one of the six implementation variants of a circuit shield againts physical attacks

 		P/T None Places: up to 6 803, Transitions: up to 6 303, Arcs: up to 17 406
ShieldPPPt

, proposed by

This Place-Transition net models one of the six implementation variants of a circuit shield againts physical attacks

 		P/T None Places: up to 7 803, Transitions: up to 7 103, Arcs: up to 17 806
ShieldRVs

, proposed by

This Place-Transition net models one of the six implementation variants of a circuit shield againts physical attacks

 		P/T None Places: up to 4 003, Transitions: up to 4 503, Arcs: up to 14 400
ShieldRVt

, proposed by

This Place-Transition net models one of the six implementation variants of a circuit shield againts physical attacks

 		P/T None Places: up to 5 003, Transitions: up to 5 003, Arcs: up to 11 806
SmartHome

Smart Home Automation, proposed by Ajay Krishna and Hubert Garavel

This Place-Transition net models a smart home automation scenario specified using a composition of Event-Condition-Action rules

 		P/T Yes Places: up to 741, Transitions: up to 809, Arcs: up to 1 844
Sudoku

Sudoku, proposed by Elvio G. Amparore

This Place-Transition net models the constraints of the Sudoku game

 		Colored +
P/T equiv		 Yes Places: up to 5 120, Transitions: up to 4 096, Arcs: up to 20 840
ViralEpidemic

ViralEpidemic, proposed by Fabrice Kordon

This Place-Transition net models in a simple way the way an epidemic works (spread of the disease).

 		P/T Yes Places: up to 78 643, Transitions: up to 144 177, Arcs: up to 353 889
Proposed in 2019 (4 models)
CloudOpsManagement

CloudOpsManagement, proposed by Lom Messan Hillah and Fabrice Kordon

This Petri net models the behavior of management operations for deploying application runtimes on the cloud.

 		P/T Yes Places: 27, Transitions: 29, Arcs: 94
FamilyReunion

Family Reunion, proposed by Lom Messan Hillah

This Petri net models the family reunion process that a legal permanent resident in Italy must follow.

 		Colored +
P/T equiv		 Yes Places: 104, Transitions: 66, Arcs: 198
NoC3x3

NoC3x3, proposed by Wendelin Serwe and Zhen Zhang

This model describes a fault-tolerant wormhole routing algorithm for an asynchronous Network on Chip

 		P/T Yes Places: up to 9140, Transitions: upt to 14577, Arcs: up to 30726
VehicularWifi

VehicularWifi, proposed by Paolo Ballarini and Benoît Barbot

This Petri net presents different kinds of CSMA/CA based wireless networks (802.11, 802.11p, VANET), which extend 802.11 with priorities over packets.

 		Colored None Places: 21, Transitions: 41, Arcs: 136
Proposed in 2018 (13 models)
ASLink

ASLink, proposed by Aymane Bouzafour, Marc Renaudin, and Hubert Garavel

This model describes a an on-chip asynchronous serial link enabling the interconnection of a set of IP slaves designed by other vendors

 		P/T Yes Places: up to 4 410, Transitions: up to 5 405, Arcs: up to 16 377
BusinessProcesses

BusinessProcesses, proposed by Ajay Krishna and Gwen Salaün

This Petri net models a business process.

 		P/T Yes Places: 782, Transitions: 697, Arcs: 2 011
DLCflexbar

DLCflexbar, proposed by Hugues Evrard, Alastair Donaldson, and Tyler Sorensen

This model describes flexible barrier enabling application-wide thread synchronisation in the context of GPU

 		P/T Yes Places: up to 47 560, Transitions: up to 76 160, Arcs: up to 216 499
DiscoveryGPU

DiscoveryGPU, proposed by Hugues Evrard, Alastair Donaldson, and Tyler Sorensen

This model a protocol used to dynamically detect the amount of thread workgroups that can be scheduled at the same time on a given GPU, for a given application.

 		P/T Yes Places: up to 436, Transitions: up to 464, Arcs: up to 1 214
DoubleExponent

DoubleExponent, proposed by Dmitry Zaitsev

This model illustrates difference beween weak, strong, and exact Petri net computers

 		P/T None Places: up to 10 604, Transitions: up to 9 998, Arcs: up to 28 194
EGFr

EGFr, proposed by Thomas Chatain and Lo"ic Paulevé

This model describes an ERBB receptor-regulated G1/S transition to find novel targets for de novo trastuzumab resistance

 		P/T Yes Places: up to 208, Transitions: up to 378, Arcs: up to 3 198
HospitalTriage

HospitalTriage, proposed by Elvio G. Amparore

This model represents the workflow of a hospital Emergency Department.

 		P/T None Places: 228, Transitions: 680, Arcs:
MAPKbis

MAPKbis, proposed by Thomas Chatain and Lo"ic Paulevé

Petri net describes a Boolean model of Mitogen-Activated Protein Kinase network (different from the other MAPK model present in the MCC collection)

 		P/T Yes Places: 106, Transitions: 173, Arcs: 986
NQueens

NQueens, proposed by Elvio G. Amparore

This model describes the N-queens problem (parameter is the number of queens)

 		P/T Yes Places: up to 1 080, Transitions: up to 900, Arcs: up to 4 500
RERS17pb113

RERS17pb113, proposed by Jaco van de Pol

This model has been extracted from the parallel track of the 2017 RERS (Rigorous Examination of Reactive Systems) challenge.

 		P/T Yes Places: 639, Transitions: 31 353, Arcs: 125 418
RERS17pb114

RERS17pb114, proposed by Jaco van de Pol

This model has been extracted from the parallel track of the 2017 RERS (Rigorous Examination of Reactive Systems) challenge.

 		P/T Yes Places: 1 446, Transitions: 151 085, Arcs: 604 252
RERS17pb115

RERS17pb115, proposed by Jaco van de Pol

This model has been extracted from the parallel track of the 2017 RERS (Rigorous Examination of Reactive Systems) challenge.

 		P/T Yes Places: 1 399, Transitions: 144 369, Arcs: 577 414
RefineWMG

RefineWMG, proposed by Thomas Hujsa

This model represents a Weighted Marked Graph describing a DSP application.

 		P/T Yes Places: up to 504, Transitions: up to 403, Arcs: up to 1 208
Proposed in 2017 (10 models)
BART

BART, proposed by Fabrice Kordon

This model describes a sample speed controller system for the BART case study.

 		Colored +
P/T equiv		 Yes Places: 4, Transitions: 7, Arcs: 26
ClientsAndServers

ClientsAndServers, proposed by Claude Girault

This model represents a set of clients, a set of servers, a set of managers and a pool of resources.

 		P/T Yes Places: 25, Transitions: 18, Arcs: 54
CloudReconfiguration

Cloud Reconfiguration, proposed by Rim Abid, Gwen Salaün, and Noël de Palma

This model represents a dynamic reconfiguration protocol for cloud applications.

 		P/T Yes Places: up to 3554, Transitions: up to 4263, Arcs: up to 8889
DLCround

DLCround, proposed by Hugues Evrard

This model presents distributed implementations of the round game (musical chairs) generated using the DLC compiler.

 		P/T Yes Places: up to 5343, Transitions: up to 8727, Arcs: up to 24849
FlexibleBarrier

FlexibleBarrier, proposed by Hugues Evrard

This model describes a barrier algorithm that synchronizes several concurrent processes.

 		P/T Yes Places: up to 6478, Transitions: up to 7469, Arcs: up to 18797
HexagonalGrid

Hexagonal Communication Grid, proposed by Tatiana Shmeleva

The model is composed of packet switching devices whose ports are situated on the sides of a unit-size equilateral hexagon.

 		P/T Yes Places: up to 3391, Transitions: up to 6174, Arcs: up to 24696
JoinFreeModules

JoinFreeModules, proposed by Thomas Hujsa

This is a model of a schedulability problem.

 		P/T Yes Places: 5.k + 1, Transitions: 8.k + 1, Arcs: 23.k + 2
NeighborGrid

NeighborGrid, proposed by Dmitry Zaitsev

Canvas of Generalized Neighbourhood for Cellular Automata

 		P/T None Places: up to 1024, Transitions: up to 196608, Arcs: up to 393216
Referendum

Referendum, proposed by Fabrice Kordon

This net models a simple referendum system.

 		Colored +
P/T equiv		 Yes Places: 4, Transitions: 3, Arcs: 6
RobotManipulation

RobotManipulation, proposed by Fabrice Kordon

The model contains concurrent processes that manipulate robots.

 		P/T Yes Places: 15, Transitions: 11, Arcs: 34
Proposed in 2016 (11 models)
AirplaneLD

AirplaneLD, proposed by Fabrice Kordon

This Petri net models simplified version of a landing detector used to activate the flaps in the system.

 		Colored +
P/T equiv		 Yes Places: 20, Transitions: 15, Arcs: 56
AutoFlight

AutoFlight Control System, proposed by Fatma Jebali and Eric Jenn

These nets are derived from the LNT specification of an auto-flight control system proposed by Thales Avionics.

 		P/T Yes Places: up to 7894, Transitions: up to 7868, Arcs: up to 18200
CloudDeployment

Cloud Deployment, proposed by Gwen Sala"

These nets are derived from the LNT specification of a decentralized self-deployment protocol designed to automatically configure a set of software components to be deployed on different virtual machines

 		P/T Yes Places: up to 2271, Transitions: up to 19752, Arcs: up to 389666
DES

DES (Data Encryption Standard), proposed by Wendelin Serwe and Hubert Garavel

These nets are derived from the LNT specification of the DES (Data Encryption Standard) symmetric-key encryption algorithm.

 		P/T Yes Places: up to 519, Transitions: up to 470, Arcs: up to 1623
DLCshifumi

DLCshifumi, proposed by Hugues Evrard and Frédéric Lang

These nets are derived from the LNT specification of a pP/T net obtained using the DLC compiler to generate implementation models to various instances of the "rock-paper-scissor" game (also known as shifumi)

 		P/T Yes Places: up to 44243, Transitions: up to 66611, Arcs: up to 182532
DNAwalker

DNAwalker, proposed by Beno^

These nets model a DNA walker derived from a Generalised Stochastic Petri Net and implementing several types of walk.

 		P/T Yes Places: up to 164, Transitions: up to 3697, Arcs: up to 10898
GPPP

GPPP -- Glycolysis and Pentose Phosphate Pathway, proposed by Monika Heiner

This Petri net models a Glycolysis and Pentose Phosphate Pathway.

 		P/T None Places: 33, Transitions: 22, Arcs: 83
HypertorusGrid

HypertorusGrid, proposed by Dmitry Zaitsev

This Petri net models an Hypertorus grid architecture

 		P/T None Places: up to 7533, Transitions: up to 24300, Arcs: up to 97200
PaceMaker

PaceMaker, proposed by Beno^

This Petri net models a PaceMaker system in its execution environment.

 		P/T None Places: 70, Transitions: 164, Arcs: 954
TCPcondis

TCPcondis, proposed by Dmitry Zaitsev

The model describes connection and disconnection procedures of Transmission Control Protocol according to RFC 793.

 		P/T Yes Places: 30, Transitions: 32, Arcs: 108
TriangularGrid

TriangularGrid, proposed by Tatiana Shmeleva

This net represents packet switching devices whose ports are situated on sides of a unit-size equilateral triangle.

 		P/T None Places: up to 280, Transitions: up to 240, Arcs: up to 960
Proposed in 2015 (13 models)
BridgeAndVehicles

BridgeAndVehicles, proposed by Fabrice Kordon

This net models the control of a one-lane bridge used by automated vehicles.

 		Colored +
P/T equiv		 Yes Places: 15, Transitions: 11, Arcs: 57
HypercubeGrid

HypercubeCommunicationGrid, proposed by Tatiana Shmeleva

This net models an hypercube communication grid implementing packet forwarding based on store-and-forward principle.

 		P/T Yes Places: 1408 and more, Transitions: 2400 and more, Arcs: 9600 and more
IBM319

IBM319, proposed by Karsten Wolf

This net models a huge workflow structure derived from a problem described by IBM.

 		P/T None Places: 253, Transitions: 178, Arcs: 526
IBM5964

IBM5964, proposed by Karsten Wolf

This net models a huge workflow structure derived from a problem described by IBM.

 		P/T None Places: 263, Transitions: 139, Arcs: 541
IBM703

IBM703, proposed by Karsten Wolf

This net models a huge workflow structure derived from a problem described by IBM.

 		P/T None Places: 262, Transitions: 284, Arcs: 572
IOTPpurchase

IOTPpurchase, proposed by Abdulmalik Ahmad

This net models a purchase transaction in an Internet open trading protocol.

 		P/T Yes Places: 111, Transitions: 45, Arcs: 224
Parking

Parking, proposed by Jingyan Jourdan-Lu and Eric L'

This net derives from an LNT specification modelling a car park control system.

 		P/T Yes Places: 65 and more, Transitions: 97 and more, Arcs: 284 and more
PhaseVariation

Phase variation in cell colony growth, proposed by Monika Heiner

This net models the phase variation (a common microbial stochastic mechanism) in bacterial cell colonies growing in a 2-dimensional space.

 		P/T Yes Places: 14 to 2702, Transitions: 65 to 30977, Arcs: 451 to 216835
Raft

Raft, proposed by Hugues Evrard

This net models the Raft distributed consensus algorithm, which is a simpler replacement for Paxos

 		P/T Yes Places: 28 to 508, Transitions: 52 to 828, Arcs: 159 to 3359
SafeBus

SafeBus, proposed by Fabrice Kordon

This model models a safe bus that links N interlocutors together.

 		Colored +
P/T equiv		 Yes Places: 20, Transitions: 14, Arcs: 68
SmallOperatingSystem

SmallOperatingSystem, proposed by Fabrice Kordon

This net models a simplified operating system.

 		P/T Yes Places: 9, Transitions: 8, Arcs: 27
SquareGrid

SquareGrid, proposed by Ivan Zaitsev

This net models a data communication equipment (DCE) implementing packet forwarding.

 		P/T Yes Places: 13xK**2 + 8xK, Transitions: 16xK**2 + 4xK, Arcs: 34xK**2 + 16xK
SwimmingPool

SwimmingPool, proposed by Fabrice Kordon

This net models a protocol to use a swimming pool with a limited number of cabins for changing clothes, where swimmers use bags to store their clothes.

 		P/T Yes Places: 9, Transitions: 7, Arcs: 20
Proposed in 2014 (15 models)
ARMCacheCoherence

ARMCacheCoherency, proposed by Abderahman Kriouile and Wendelin Serwe

This model comes from a LNT specification of ARM's ACE cache coherence protocol for systems on chip.

 		P/T None Places: 87, Transitions: 33676, Arcs: 246935
Angiogenesis

Angiogenesis, proposed by Christian Rohr

This Petri net models the formation of new vessels from the existing ones, which is a topic of great interest in all areas of human biology.

 		P/T Yes Places: 39, Transitions: 64, Arcs: 185
CircadianClock

CircadianClock, proposed by Christian Rohr

This Petri net models circadian rhythms, which are widely used in living organisms to keep a sense of daily time.

 		P/T Yes Places: 14, Transitions: 16, Arcs: 58
CircularTrains

Circular Trains, proposed by Fabrice Kordon

This Place-Transition net represents a circular railways having S sections on which S/3 trains circulate.

 		P/T Yes Places: 2*S, Transitions: S, Arcs: 4*S
DatabaseWithMutex

DatabaseWithMutex, proposed by Benoît Barbot

This model is an extension of a well-known distributed database example, with atomic transitions and global mutex for each file.

 		Colored +
P/T equiv		 None Places: 11, Transitions: 8, Arcs: 22
Diffusion2D

Diffusion2D, proposed by Monika Heiner

This Petri net models diffusion in space, a process underlying many spatial (bio-) chemical processes.

 		P/T Yes Places: D2, Transitions: 8xD2 - 12xD + 4, Arcs: 2 ... |T|
ERK

ERK, proposed by Christian Rohr

This net models the "RKIP/MEK-ERK signalling pathway" published in 2003.

 		P/T Yes Places: 11, Transitions: 11, Arcs: 34
EnergyBus

EnergyBus, proposed by Alexander Graf-Brill

This model derives from an LNT specification of the EnergyBus, an upcoming industrial standard (based on the CANopen field bus) for electric power transmission and management.

 		P/T None Places: 157, Transitions: 4430, Arcs: 63389
MultiwaySync

MultiwaySync, proposed by Hugues Evrard and Frédéric Lang

This model derives from an LNT specification of a multiway synchronization protocol.

 		P/T None Places: 222, Transitions: 472, Arcs: 1496
ParamProductionCell

ParamProductionCell, proposed by Monika Heiner

This Petri net models the "production cell", a case study introduced in 1995 to assess different formal methods with respect to their modeling and analysis capabilities.

 		P/T Yes Places: 198-231, Transitions: 176-202, Arcs: 730-846
PolyORBLF

PolyORBLF, proposed by Fabrice Kordon

This Petri net models the microBroker component in the PolyORB middleware in its "leader-follower" implementation.

 		Colored +
P/T equiv		 Yes Places: 81, Transitions: 65, Arcs: 258
PolyORBNT

PolyORBNT, proposed by Fabrice Kordon

This Petri net models the microBroker component in the PolyORB middleware in its "no-thread" implementation.

 		Colored +
P/T equiv		 Yes Places: 48, Transitions: 38, Arcs: 140
ProductionCell

ProductionCell, proposed by Hubert Garavel and Wendelin Serwe

This model derives from an LNT specification of the Production Cell case study introduced in 1995 to assess formal methods on a common example.

 		P/T None Places: 176, Transitions: 134, Arcs: 513
Solitaire

Solitaire, proposed by Monika Heiner

This Petri net models the solitaire, that is a popular board game requiring non-obvious solution strategies.

 		P/T Yes Places: 50-75, Transitions: 84-92, Arcs: 456-644
UtahNoC

UtahNoC, proposed by Zhen Zhang and Wendelin Serwe

This Petri net is derived from an LNT specification of a fault-tolerant network-on-chip circuit with a wormhole routing algorithm.

 		P/T None Places: 216, Transitions: 977, Arcs: 2905
Proposed in 2013 (9 models)
Dekker

A variant of Dekker's algorithm for mutual exclusion, proposed by Cesar Rodriguez

This Place-Transition net represents a variant of the Dekker's mutual exclusion algorithm for N > 2 processes.

 		P/T Yes Places: 3*N, Transitions: N2+2*N, Arcs: O(N2)
DotAndBoxes

Dot&Boxes, proposed by Emmanuel Paviot-Adet

This Petri net models the Dot & Boxes game.

 		Colored Yes Places: 8, Transitions: 8, Arcs: 44
DrinkVendingMachine

A hot drink vending machine, proposed by Lom Messan Hillah

This net models a simple hot drink vending machine.

 		Colored +
P/T equiv		 Yes Places: 6, Transitions: 7, Arcs: 28
HouseConstruction

HouseConstruction, proposed by Fabrice Kordon

This net models the construction of a house (seen as a workflow).

 		P/T Yes Places: 26, Transitions: 18, Arcs: 51
IBMB2S565S3960

IBMB2S565S3960, proposed by Niels Lohmann

This net models a huge workflow structure derived from a problem described by IBM.

 		P/T None Places: 273, Transitions: 179, Arcs: 572
PermAdmissibility

Permutation admissibility in multistage interconnection networks, proposed by Fabrice Kordon

The model describes all possible permutations on a 8x8 4-stage shuffle-exchange network.

 		Colored +
P/T equiv		 Yes Places: 40, Transitions: 16, Arcs: 83
QuasiCertifProtocol

Quasi Certification Protocol over a DHT, proposed by Fabrice Kordon

This net models a quasi-certification protocol on top of a distributed hash table.

 		Colored +
P/T equiv		 Yes Places: 30, Transitions: 26, Arcs: 77
ResAllocation

Resource Allocation Model, proposed by Fernando Tricas Garcia and Joaquin Ezpeleta Mateo

This net models a family of resource allocation systems.

 		P/T Yes Places: 2 ... nR ... nC, Transitions: nC ... (nR+1), Arcs: 4 ... nR ... nC + 2 ... nR ... (nC-1)
Vasy2003

Vasy2003, proposed by Hubert Garavel

This net is derived from an industrial LOTOS specification and was submitted as a benchmark to the Petri-nets mailing list in July 2003.

 		P/T None Places: 485, Transitions: 776, Arcs: 2809
Proposed in 2012 (12 models)
CSRepetitions

Client/Server with Repetitions, proposed by Alban Linard

This Petri net models a client/server application with unreliable communication from clients to servers and fixed-size buffers to store requests.

 		Colored +
P/T equiv		 Yes Places: 1 + 3*clients + servers + clients*servers, Transitions: 3*clients + 2*clients*servers, Arcs: 7*clients + 8*clients+servers
Echo

Echo Algorithm, proposed by Niels Lohmann

This net models the Echo Algorithm defined by Reisig in 1998.

 		P/T Yes For value (3,3)
Places: 265, Transitions: 206, Arcs: 1252
Eratosthenes

Eratosthenes' sieve, proposed by Franck Pommereau

This model describes the Eratosthenes' sieve.

 		P/T Yes For value 500
Places: 499, Transitions: 2191, Arcs: 6573
GlobalResAllocation

Global Allocation Resource Management, proposed by Fabrice Kordon

This net models a resource management strategy that prevents deadlocks.

 		Colored +
P/T equiv		 Yes Places: 5, Transitions: 8, Arcs: 29
LamportFastMutEx

Lamport's fast mutual exclusion algorithm, proposed by Sami Evangelista

This net models Lamport's fast mutual exclusion algorithm designed for multi-processor architectures with a shared memory.

 		Colored +
P/T equiv		 Yes Places: 18, Transitions: 17, Arcs: 68
NeoElection

Neo election protocol, proposed by Sami Evangelista

This net models an election protocol between the master nodes of a distributed database designed by Nexedi.

 		Colored +
P/T equiv		 Yes For value N=2
Places: 18, Transitions: 22, Arcs: 98
PhilosophersDyn

Dynamic Philosophers, proposed by Alban Linard

This net models a variation of the Dining Philosophers problem, where philosophers can join or leave the table.

 		Colored +
P/T equiv		 Yes Places: N2 + 7N, Transitions: 2*N3 + 3*N2 + N, Arcs: unknown
Planning

AI Planning, proposed by Niels Lohmann

This net models the equipment (displays, canvases, documents, and lamps) of a smart conference room of the University of Rostock.

 		P/T None Places: 126, Transitions: 128, Arcs: 652
Railroad

Railroad crossing, proposed by Franck Pommereau

This net models the Petri nets semantics of an ABCD specification of a railroad crossing system.

 		P/T Yes Places: 5*n + 18, Transitions: 3*n + 10, Arcs: 13*n + 52
Ring

Three-Module Ring, proposed by Niels Lohmann

This net is derived from an example of hardware circuit.

 		P/T None Places: 139, Transitions: 87, Arcs: 410
RwMutex

Reader/Writer Mutual Exclusion, proposed by Niels Lohmann

The net models a distributed algorithm with readers and writers.

 		P/T Yes For value (10,10)
Places: 50, Transitions: 40, Arcs: 300
SimpleLoadBal

Simple load balancing system, proposed by Sami Evangelista

This net models simple load balancing system composed of a set of clients, two servers supervised by a load balancer process.

 		P/T Yes Places: 14, Transitions: 13, Arcs: 57
Proposed in 2011 (7 models)
FMS

Flexible Manufacturing System (FMS), proposed by Lom Messan Hillah

This net, extracted from the SMART benchmarks, models a flexible manufacturing system.

 		P/T Yes Places: 22, Transitions: 20, Arcs: 50
Kanban

Kanban, proposed by Lom Messan Hillah

This net, extracted from the SMART benchmarks, models a Kanban system.

 		P/T Yes Places: 16, Transitions: 16, Arcs: 40
MAPK

MAPK, proposed by Lom Messan Hillah

This net models a biochemical reaction, namely the Mitogen-Activated Protein Kinase cascade.

 		P/T Yes Places: 22, Transitions: 30, Arcs: 90
Peterson

Peterson, proposed by Emmanuel Paviot-Adet

This net models Peterson's algorithm for the mutual exclusion problem, in its generalized version for N processes

 		Colored +
P/T equiv		 Yes Places: 11, Transitions: 14, Arcs: 42
Philosophers

Philosophers, proposed by Lom Messan Hillah

This net models the famous dining philosophers problem.

 		Colored +
P/T equiv		 Yes Places: 4, Transitions: 5, Arcs: 15
SharedMemory

SharedMemory, proposed by Lom Messan Hillah

This model, extracted from a greatSPN benchmark, models a sort of COMA (Cache-Only Memory Access) system with P processors, each having its local memory.

 		Colored +
P/T equiv		 Yes Places: 6, Transitions: 5, Arcs: 16
TokenRing

Token Ring, proposed by Alexis Marechal

This net models a token ring-based system.

 		Colored +
P/T equiv		 Yes Places: 1, Transitions: 2, Arcs: 4