fond

jQuery Multi Level CSS Menu Css3Menu.com

Model Checking Contest @ Petri Nets 2016
6th edition, Toruń, Poland, June 21, 2016
Models for the MCC’2016
Last Updated
June 30, 2016

Introduction

The benchmark proposed for the MCC'2016 consists of P/T nets (1-bounded, k-bounded), 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 will be provided:

All models will be provided as PNML files. The two types of models will be 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. 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:

«Surprise» Models for 2016

We are happy to announce that there will be 11 new «surprise» models for 2016 (139 instances in total).

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

AirplaneLD, proposed by F. 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ün

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

DLC shifumi, 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 B. Barbot and M. Kwiatkowska

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 B. Barbot

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

«Known» Models for 2016

The table below summarizes the «Known» models which has 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 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 Yes 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 Yes 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.

 		Colored +
P/T equiv		 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