fond
Model Checking Contest @ Petri Nets 2015
Bruxelles, Belgium, June 23, 2015
Performances on Models for ReachabilityComputeBounds
Last Updated
August 19, 2015

Introduction

This page summarizes the performances of tools for the StateSpace examination, model per model. Models are presented in alphabetical order (some with prefix «surprise» are in fact «stripped» versions of «known» model).

Important: charts are generated only if at least one tool is able to process successfully one instance.

BridgeAndVehicles, Colored

This model is a «surprise» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

BridgeAndVehicles, P/T

This model is a «surprise» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

HypercubeGrid, P/T

This model is a «surprise» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

IBM319, P/T

This model is a «surprise» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

IBM5964, P/T

This model is a «surprise» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

IBM703, P/T

This model is a «surprise» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

IOTPpurchase, P/T

This model is a «surprise» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

Parking, P/T

This model is a «surprise» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

PhaseVariation, P/T

This model is a «surprise» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

Raft, P/T

This model is a «surprise» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

SafeBus, P/T

This model is a «surprise» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

SmallOperatingSystem, P/T

This model is a «surprise» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

SquareGrid, P/T

This model is a «surprise» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

SwimmingPool, P/T

This model is a «surprise» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

ARMCacheCoherence (stripped), P/T

This model is a «stripped» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

Angiogenesis (stripped), P/T

This model is a «stripped» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

CSRepetitions (stripped), Colored

This model is a «stripped» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

CSRepetitions (stripped), P/T

This model is a «stripped» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

CircadianClock (stripped), P/T

This model is a «stripped» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

CircularTrains (stripped), P/T

This model is a «stripped» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

DatabaseWithMutex (stripped), Colored

This model is a «stripped» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

DatabaseWithMutex (stripped), P/T

This model is a «stripped» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

Dekker (stripped), P/T

This model is a «stripped» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

Diffusion2D (stripped), P/T

This model is a «stripped» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

DotAndBoxes (stripped), Colored

This model is a «stripped» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

DrinkVendingMachine (stripped), Colored

This model is a «stripped» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

DrinkVendingMachine (stripped), P/T

This model is a «stripped» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

ERK (stripped), P/T

This model is a «stripped» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

Echo (stripped), P/T

This model is a «stripped» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

EnergyBus (stripped), P/T

This model is a «stripped» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

Eratosthenes (stripped), P/T

This model is a «stripped» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

FMS (stripped), P/T

This model is a «stripped» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

GlobalResAllocation (stripped), Colored

This model is a «stripped» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

GlobalResAllocation (stripped), P/T

This model is a «stripped» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

HouseConstruction (stripped), P/T

This model is a «stripped» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

IBMB2S565S3960 (stripped), P/T

This model is a «stripped» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

Kanban (stripped), P/T

This model is a «stripped» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

LamportFastMutEx (stripped), Colored

This model is a «stripped» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

LamportFastMutEx (stripped), P/T

This model is a «stripped» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

MAPK (stripped), P/T

This model is a «stripped» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

MultiwaySync (stripped), P/T

This model is a «stripped» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

NeoElection (stripped), Colored

This model is a «stripped» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

NeoElection (stripped), P/T

This model is a «stripped» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

ParamProductionCell (stripped), P/T

This model is a «stripped» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

PermAdmissibility (stripped), Colored

This model is a «stripped» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

PermAdmissibility (stripped), P/T

This model is a «stripped» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

Peterson (stripped), Colored

This model is a «stripped» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

Peterson (stripped), P/T

This model is a «stripped» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

Philosophers (stripped), Colored

This model is a «stripped» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

Philosophers (stripped), P/T

This model is a «stripped» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

PhilosophersDyn (stripped), P/T

This model is a «stripped» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

Planning (stripped), P/T

This model is a «stripped» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

PolyORBLF (stripped), P/T

This model is a «stripped» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

PolyORBNT (stripped), P/T

This model is a «stripped» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

ProductionCell (stripped), P/T

This model is a «stripped» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

QuasiCertifProtocol (stripped), Colored

This model is a «stripped» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

QuasiCertifProtocol (stripped), P/T

This model is a «stripped» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

Railroad (stripped), P/T

This model is a «stripped» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

ResAllocation (stripped), P/T

This model is a «stripped» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

Ring (stripped), P/T

This model is a «stripped» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

RwMutex (stripped), P/T

This model is a «stripped» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

SharedMemory (stripped), Colored

This model is a «stripped» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

SharedMemory (stripped), P/T

This model is a «stripped» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

SimpleLoadBal (stripped), Colored

This model is a «stripped» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

SimpleLoadBal (stripped), P/T

This model is a «stripped» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

Solitaire (stripped), P/T

This model is a «stripped» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

TokenRing (stripped), Colored

This model is a «stripped» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

TokenRing (stripped), P/T

This model is a «stripped» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

UtahNoC (stripped), P/T

This model is a «stripped» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

Vasy2003 (stripped), P/T

This model is a «stripped» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

ARMCacheCoherence, P/T

This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

Angiogenesis, P/T

This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

CSRepetitions, Colored

This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

CSRepetitions, P/T

This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

CircadianClock, P/T

This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

CircularTrains, P/T

This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

DatabaseWithMutex, Colored

This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

DatabaseWithMutex, P/T

This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

Dekker, P/T

This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

Diffusion2D, P/T

This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

DotAndBoxes, Colored

This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

DrinkVendingMachine, Colored

This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

DrinkVendingMachine, P/T

This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

ERK, P/T

This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

Echo, P/T

This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

EnergyBus, P/T

This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

Eratosthenes, P/T

This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

FMS, P/T

This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

GlobalResAllocation, Colored

This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

GlobalResAllocation, P/T

This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

HouseConstruction, P/T

This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

IBMB2S565S3960, P/T

This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

Kanban, P/T

This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

LamportFastMutEx, Colored

This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

LamportFastMutEx, P/T

This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

MAPK, P/T

This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

MultiwaySync, P/T

This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

NeoElection, Colored

This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

NeoElection, P/T

This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

ParamProductionCell, P/T

This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

PermAdmissibility, Colored

This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

PermAdmissibility, P/T

This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

Peterson, Colored

This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

Peterson, P/T

This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

Philosophers, Colored

This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

Philosophers, P/T

This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

PhilosophersDyn, P/T

This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

Planning, P/T

This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

PolyORBLF, P/T

This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

PolyORBNT, P/T

This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

ProductionCell, P/T

This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

QuasiCertifProtocol, Colored

This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

QuasiCertifProtocol, P/T

This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

Railroad, P/T

This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

ResAllocation, P/T

This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

Ring, P/T

This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

RwMutex, P/T

This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

SharedMemory, Colored

This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

SharedMemory, P/T

This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

SimpleLoadBal, Colored

This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

SimpleLoadBal, P/T

This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

Solitaire, P/T

This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

TokenRing, Colored

This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

TokenRing, P/T

This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

UtahNoC, P/T

This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time

Vasy2003, P/T

This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.

Memory Consumption

Execution time