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 «scrambled» versions of «known» model).

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

ARMCacheCoherence-PT («surprise» model)

Please find below the performance char for ARMCacheCoherence-PT.

Memory Consumption

CPU Consumption

Angiogenesis-PT («surprise» model)

Please find below the performance char for Angiogenesis-PT.

Memory Consumption

CPU Consumption

CSRepetitions-COL («known» model)

Please find below the performance char for CSRepetitions-COL.

Memory Consumption

CPU Consumption

CSRepetitions-PT («known» model)

Please find below the performance char for CSRepetitions-PT.

Memory Consumption

CPU Consumption

CircadianClock-PT («surprise» model)

Please find below the performance char for CircadianClock-PT.

Memory Consumption

CPU Consumption

CircularTrains-PT («surprise» model)

Please find below the performance char for CircularTrains-PT.

Memory Consumption

CPU Consumption

DatabaseWithMutex-PT («surprise» model)

Please find below the performance char for DatabaseWithMutex-PT.

Memory Consumption

CPU Consumption

Dekker-PT («known» model)

Please find below the performance char for Dekker-PT.

Memory Consumption

CPU Consumption

Diffusion2D-PT («surprise» model)

Please find below the performance char for Diffusion2D-PT.

Memory Consumption

CPU Consumption

DotAndBoxes-COL («known» model)

Please find below the performance char for DotAndBoxes-COL.

Memory Consumption

CPU Consumption

DrinkVendingMachine-COL («known» model)

Please find below the performance char for DrinkVendingMachine-COL.

Memory Consumption

CPU Consumption

DrinkVendingMachine-PT («known» model)

Please find below the performance char for DrinkVendingMachine-PT.

Memory Consumption

CPU Consumption

ERK-PT («surprise» model)

Please find below the performance char for ERK-PT.

Memory Consumption

CPU Consumption

EnergyBus-PT («surprise» model)

Please find below the performance char for EnergyBus-PT.

Memory Consumption

CPU Consumption

Eratosthenes-PT («known» model)

Please find below the performance char for Eratosthenes-PT.

Memory Consumption

CPU Consumption

FMS-PT («known» model)

Please find below the performance char for FMS-PT.

Memory Consumption

CPU Consumption

GlobalResAllocation-COL («known» model)

Please find below the performance char for GlobalResAllocation-COL.

Memory Consumption

CPU Consumption

GlobalResAllocation-PT («known» model)

Please find below the performance char for GlobalResAllocation-PT.

Memory Consumption

CPU Consumption

HouseConstruction-PT («known» model)

Please find below the performance char for HouseConstruction-PT.

Memory Consumption

CPU Consumption

IBMB2S565S3960-PT («known» model)

Please find below the performance char for IBMB2S565S3960-PT.

Memory Consumption

CPU Consumption

Kanban-PT («known» model)

Please find below the performance char for Kanban-PT.

Memory Consumption

CPU Consumption

LamportFastMutEx-COL («known» model)

Please find below the performance char for LamportFastMutEx-COL.

Memory Consumption

CPU Consumption

LamportFastMutEx-PT («known» model)

Please find below the performance char for LamportFastMutEx-PT.

Memory Consumption

CPU Consumption

MAPK-PT («known» model)

Please find below the performance char for MAPK-PT.

Memory Consumption

CPU Consumption

MultiwaySync-PT («surprise» model)

Please find below the performance char for MultiwaySync-PT.

Memory Consumption

CPU Consumption

NeoElection-COL («known» model)

Please find below the performance char for NeoElection-COL.

Memory Consumption

CPU Consumption

NeoElection-PT («known» model)

Please find below the performance char for NeoElection-PT.

Memory Consumption

CPU Consumption

ParamProductionCell-PT («surprise» model)

Please find below the performance char for ParamProductionCell-PT.

Memory Consumption

CPU Consumption

PermAdmissibility-COL («known» model)

Please find below the performance char for PermAdmissibility-COL.

Memory Consumption

CPU Consumption

PermAdmissibility-PT («known» model)

Please find below the performance char for PermAdmissibility-PT.

Memory Consumption

CPU Consumption

Peterson-COL («known» model)

Please find below the performance char for Peterson-COL.

Memory Consumption

CPU Consumption

Peterson-PT («known» model)

Please find below the performance char for Peterson-PT.

Memory Consumption

CPU Consumption

Philosophers-COL («known» model)

Please find below the performance char for Philosophers-COL.

Memory Consumption

CPU Consumption

Philosophers-PT («known» model)

Please find below the performance char for Philosophers-PT.

Memory Consumption

CPU Consumption

PhilosophersDyn-PT («known» model)

Please find below the performance char for PhilosophersDyn-PT.

Memory Consumption

CPU Consumption

PolyORBLF-COL («surprise» model)

Please find below the performance char for PolyORBLF-COL.

Memory Consumption

CPU Consumption

PolyORBLF-PT («surprise» model)

Please find below the performance char for PolyORBLF-PT.

Memory Consumption

CPU Consumption

PolyORBNT-PT («surprise» model)

Please find below the performance char for PolyORBNT-PT.

Memory Consumption

CPU Consumption

ProductionCell-PT («surprise» model)

Please find below the performance char for ProductionCell-PT.

Memory Consumption

CPU Consumption

QuasiCertifProtocol-COL («known» model)

Please find below the performance char for QuasiCertifProtocol-COL.

Memory Consumption

CPU Consumption

QuasiCertifProtocol-PT («known» model)

Please find below the performance char for QuasiCertifProtocol-PT.

Memory Consumption

CPU Consumption

Railroad-PT («known» model)

Please find below the performance char for Railroad-PT.

Memory Consumption

CPU Consumption

ResAllocation-PT («known» model)

Please find below the performance char for ResAllocation-PT.

Memory Consumption

CPU Consumption

Ring-PT («known» model)

Please find below the performance char for Ring-PT.

Memory Consumption

CPU Consumption

RwMutex-PT («known» model)

Please find below the performance char for RwMutex-PT.

Memory Consumption

CPU Consumption

SharedMemory-COL («known» model)

Please find below the performance char for SharedMemory-COL.

Memory Consumption

CPU Consumption

SharedMemory-PT («known» model)

Please find below the performance char for SharedMemory-PT.

Memory Consumption

CPU Consumption

SimpleLoadBal-COL («known» model)

Please find below the performance char for SimpleLoadBal-COL.

Memory Consumption

CPU Consumption

SimpleLoadBal-PT («known» model)

Please find below the performance char for SimpleLoadBal-PT.

Memory Consumption

CPU Consumption

Solitaire-PT («surprise» model)

Please find below the performance char for Solitaire-PT.

Memory Consumption

CPU Consumption

SurpriseCSRepetitions-PT («scrambled» version of the «known» model)

Please find below the performance char for SurpriseCSRepetitions-PT.

Memory Consumption

CPU Consumption

SurpriseDekker-PT («scrambled» version of the «known» model)

Please find below the performance char for SurpriseDekker-PT.

Memory Consumption

CPU Consumption

SurpriseDotAndBoxes-COL («scrambled» version of the «known» model)

Please find below the performance char for SurpriseDotAndBoxes-COL.

Memory Consumption

CPU Consumption

SurpriseDrinkVendingMachine-COL («scrambled» version of the «known» model)

Please find below the performance char for SurpriseDrinkVendingMachine-COL.

Memory Consumption

CPU Consumption

SurpriseDrinkVendingMachine-PT («scrambled» version of the «known» model)

Please find below the performance char for SurpriseDrinkVendingMachine-PT.

Memory Consumption

CPU Consumption

SurpriseEcho-PT («scrambled» version of the «known» model)

Please find below the performance char for SurpriseEcho-PT.

Memory Consumption

CPU Consumption

SurpriseEratosthenes-PT («scrambled» version of the «known» model)

Please find below the performance char for SurpriseEratosthenes-PT.

Memory Consumption

CPU Consumption

SurpriseFMS-PT («scrambled» version of the «known» model)

Please find below the performance char for SurpriseFMS-PT.

Memory Consumption

CPU Consumption

SurpriseGlobalResAllocation-PT («scrambled» version of the «known» model)

Please find below the performance char for SurpriseGlobalResAllocation-PT.

Memory Consumption

CPU Consumption

SurpriseHouseConstruction-PT («scrambled» version of the «known» model)

Please find below the performance char for SurpriseHouseConstruction-PT.

Memory Consumption

CPU Consumption

SurpriseIBMB2S565S3960-PT («scrambled» version of the «known» model)

Please find below the performance char for SurpriseIBMB2S565S3960-PT.

Memory Consumption

CPU Consumption

SurpriseKanban-PT («scrambled» version of the «known» model)

Please find below the performance char for SurpriseKanban-PT.

Memory Consumption

CPU Consumption

SurpriseLamportFastMutEx-COL («scrambled» version of the «known» model)

Please find below the performance char for SurpriseLamportFastMutEx-COL.

Memory Consumption

CPU Consumption

SurpriseLamportFastMutEx-PT («scrambled» version of the «known» model)

Please find below the performance char for SurpriseLamportFastMutEx-PT.

Memory Consumption

CPU Consumption

SurpriseMAPK-PT («scrambled» version of the «known» model)

Please find below the performance char for SurpriseMAPK-PT.

Memory Consumption

CPU Consumption

SurpriseNeoElection-COL («scrambled» version of the «known» model)

Please find below the performance char for SurpriseNeoElection-COL.

Memory Consumption

CPU Consumption

SurpriseNeoElection-PT («scrambled» version of the «known» model)

Please find below the performance char for SurpriseNeoElection-PT.

Memory Consumption

CPU Consumption

SurprisePermAdmissibility-COL («scrambled» version of the «known» model)

Please find below the performance char for SurprisePermAdmissibility-COL.

Memory Consumption

CPU Consumption

SurprisePermAdmissibility-PT («scrambled» version of the «known» model)

Please find below the performance char for SurprisePermAdmissibility-PT.

Memory Consumption

CPU Consumption

SurprisePeterson-COL («scrambled» version of the «known» model)

Please find below the performance char for SurprisePeterson-COL.

Memory Consumption

CPU Consumption

SurprisePeterson-PT («scrambled» version of the «known» model)

Please find below the performance char for SurprisePeterson-PT.

Memory Consumption

CPU Consumption

SurprisePhilosophers-COL («scrambled» version of the «known» model)

Please find below the performance char for SurprisePhilosophers-COL.

Memory Consumption

CPU Consumption

SurprisePhilosophers-PT («scrambled» version of the «known» model)

Please find below the performance char for SurprisePhilosophers-PT.

Memory Consumption

CPU Consumption

SurprisePhilosophersDyn-PT («scrambled» version of the «known» model)

Please find below the performance char for SurprisePhilosophersDyn-PT.

Memory Consumption

CPU Consumption

SurprisePlanning-PT («scrambled» version of the «known» model)

Please find below the performance char for SurprisePlanning-PT.

Memory Consumption

CPU Consumption

SurpriseQuasiCertifProtocol-COL («scrambled» version of the «known» model)

Please find below the performance char for SurpriseQuasiCertifProtocol-COL.

Memory Consumption

CPU Consumption

SurpriseQuasiCertifProtocol-PT («scrambled» version of the «known» model)

Please find below the performance char for SurpriseQuasiCertifProtocol-PT.

Memory Consumption

CPU Consumption

SurpriseRailroad-PT («scrambled» version of the «known» model)

Please find below the performance char for SurpriseRailroad-PT.

Memory Consumption

CPU Consumption

SurpriseResAllocation-PT («scrambled» version of the «known» model)

Please find below the performance char for SurpriseResAllocation-PT.

Memory Consumption

CPU Consumption

SurpriseRing-PT («scrambled» version of the «known» model)

Please find below the performance char for SurpriseRing-PT.

Memory Consumption

CPU Consumption

SurpriseRwMutex-PT («scrambled» version of the «known» model)

Please find below the performance char for SurpriseRwMutex-PT.

Memory Consumption

CPU Consumption

SurpriseSharedMemory-COL («scrambled» version of the «known» model)

Please find below the performance char for SurpriseSharedMemory-COL.

Memory Consumption

CPU Consumption

SurpriseSharedMemory-PT («scrambled» version of the «known» model)

Please find below the performance char for SurpriseSharedMemory-PT.

Memory Consumption

CPU Consumption

SurpriseSimpleLoadBal-COL («scrambled» version of the «known» model)

Please find below the performance char for SurpriseSimpleLoadBal-COL.

Memory Consumption

CPU Consumption

SurpriseSimpleLoadBal-PT («scrambled» version of the «known» model)

Please find below the performance char for SurpriseSimpleLoadBal-PT.

Memory Consumption

CPU Consumption

SurpriseTokenRing-COL («scrambled» version of the «known» model)

Please find below the performance char for SurpriseTokenRing-COL.

Memory Consumption

CPU Consumption

SurpriseTokenRing-PT («scrambled» version of the «known» model)

Please find below the performance char for SurpriseTokenRing-PT.

Memory Consumption

CPU Consumption

SurpriseVasy2003-PT («scrambled» version of the «known» model)

Please find below the performance char for SurpriseVasy2003-PT.

Memory Consumption

CPU Consumption

TokenRing-COL («known» model)

Please find below the performance char for TokenRing-COL.

Memory Consumption

CPU Consumption

TokenRing-PT («known» model)

Please find below the performance char for TokenRing-PT.

Memory Consumption

CPU Consumption

UtahNoC-PT («surprise» model)

Please find below the performance char for UtahNoC-PT.

Memory Consumption

CPU Consumption

Vasy2003-PT («known» model)

Please find below the performance char for Vasy2003-PT.

Memory Consumption

CPU Consumption