Introduction
This page summarizes the performances of tools for the ReachabilityBounds 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.
CSRepetitions-PT («known» model)
Please find below the performance char for CSRepetitions-PT.
Memory Consumption
![](content/results/html/perfplots/CSRepetitions-PT-ReachabilityBounds-MEM.png)
![](images/tools-legend.png)
CPU Consumption
![](content/results/html/perfplots/CSRepetitions-PT-ReachabilityBounds-CPU.png)
![](images/tools-legend.png)
Dekker-PT («known» model)
Please find below the performance char for Dekker-PT.
Memory Consumption
![](content/results/html/perfplots/Dekker-PT-ReachabilityBounds-MEM.png)
![](images/tools-legend.png)
CPU Consumption
![](content/results/html/perfplots/Dekker-PT-ReachabilityBounds-CPU.png)
![](images/tools-legend.png)
DrinkVendingMachine-PT («known» model)
Please find below the performance char for DrinkVendingMachine-PT.
Memory Consumption
![](content/results/html/perfplots/DrinkVendingMachine-PT-ReachabilityBounds-MEM.png)
![](images/tools-legend.png)
CPU Consumption
![](content/results/html/perfplots/DrinkVendingMachine-PT-ReachabilityBounds-CPU.png)
![](images/tools-legend.png)
Eratosthenes-PT («known» model)
Please find below the performance char for Eratosthenes-PT.
Memory Consumption
![](content/results/html/perfplots/Eratosthenes-PT-ReachabilityBounds-MEM.png)
![](images/tools-legend.png)
CPU Consumption
![](content/results/html/perfplots/Eratosthenes-PT-ReachabilityBounds-CPU.png)
![](images/tools-legend.png)
FMS-PT («known» model)
Please find below the performance char for FMS-PT.
Memory Consumption
![](content/results/html/perfplots/FMS-PT-ReachabilityBounds-MEM.png)
![](images/tools-legend.png)
CPU Consumption
![](content/results/html/perfplots/FMS-PT-ReachabilityBounds-CPU.png)
![](images/tools-legend.png)
GlobalResAllocation-PT («known» model)
Please find below the performance char for GlobalResAllocation-PT.
Memory Consumption
![](content/results/html/perfplots/GlobalResAllocation-PT-ReachabilityBounds-MEM.png)
![](images/tools-legend.png)
CPU Consumption
![](content/results/html/perfplots/GlobalResAllocation-PT-ReachabilityBounds-CPU.png)
![](images/tools-legend.png)
HouseConstruction-PT («known» model)
Please find below the performance char for HouseConstruction-PT.
Memory Consumption
![](content/results/html/perfplots/HouseConstruction-PT-ReachabilityBounds-MEM.png)
![](images/tools-legend.png)
CPU Consumption
![](content/results/html/perfplots/HouseConstruction-PT-ReachabilityBounds-CPU.png)
![](images/tools-legend.png)
Kanban-PT («known» model)
Please find below the performance char for Kanban-PT.
Memory Consumption
![](content/results/html/perfplots/Kanban-PT-ReachabilityBounds-MEM.png)
![](images/tools-legend.png)
CPU Consumption
![](content/results/html/perfplots/Kanban-PT-ReachabilityBounds-CPU.png)
![](images/tools-legend.png)
LamportFastMutEx-PT («known» model)
Please find below the performance char for LamportFastMutEx-PT.
Memory Consumption
![](content/results/html/perfplots/LamportFastMutEx-PT-ReachabilityBounds-MEM.png)
![](images/tools-legend.png)
CPU Consumption
![](content/results/html/perfplots/LamportFastMutEx-PT-ReachabilityBounds-CPU.png)
![](images/tools-legend.png)
MAPK-PT («known» model)
Please find below the performance char for MAPK-PT.
Memory Consumption
![](content/results/html/perfplots/MAPK-PT-ReachabilityBounds-MEM.png)
![](images/tools-legend.png)
CPU Consumption
![](content/results/html/perfplots/MAPK-PT-ReachabilityBounds-CPU.png)
![](images/tools-legend.png)
NeoElection-PT («known» model)
Please find below the performance char for NeoElection-PT.
Memory Consumption
![](content/results/html/perfplots/NeoElection-PT-ReachabilityBounds-MEM.png)
![](images/tools-legend.png)
CPU Consumption
![](content/results/html/perfplots/NeoElection-PT-ReachabilityBounds-CPU.png)
![](images/tools-legend.png)
PermAdmissibility-PT («known» model)
Please find below the performance char for PermAdmissibility-PT.
Memory Consumption
![](content/results/html/perfplots/PermAdmissibility-PT-ReachabilityBounds-MEM.png)
![](images/tools-legend.png)
CPU Consumption
![](content/results/html/perfplots/PermAdmissibility-PT-ReachabilityBounds-CPU.png)
![](images/tools-legend.png)
Peterson-PT («known» model)
Please find below the performance char for Peterson-PT.
Memory Consumption
![](content/results/html/perfplots/Peterson-PT-ReachabilityBounds-MEM.png)
![](images/tools-legend.png)
CPU Consumption
![](content/results/html/perfplots/Peterson-PT-ReachabilityBounds-CPU.png)
![](images/tools-legend.png)
Philosophers-PT («known» model)
Please find below the performance char for Philosophers-PT.
Memory Consumption
![](content/results/html/perfplots/Philosophers-PT-ReachabilityBounds-MEM.png)
![](images/tools-legend.png)
CPU Consumption
![](content/results/html/perfplots/Philosophers-PT-ReachabilityBounds-CPU.png)
![](images/tools-legend.png)
PhilosophersDyn-PT («known» model)
Please find below the performance char for PhilosophersDyn-PT.
Memory Consumption
![](content/results/html/perfplots/PhilosophersDyn-PT-ReachabilityBounds-MEM.png)
![](images/tools-legend.png)
CPU Consumption
![](content/results/html/perfplots/PhilosophersDyn-PT-ReachabilityBounds-CPU.png)
![](images/tools-legend.png)
QuasiCertifProtocol-PT («known» model)
Please find below the performance char for QuasiCertifProtocol-PT.
Memory Consumption
![](content/results/html/perfplots/QuasiCertifProtocol-PT-ReachabilityBounds-MEM.png)
![](images/tools-legend.png)
CPU Consumption
![](content/results/html/perfplots/QuasiCertifProtocol-PT-ReachabilityBounds-CPU.png)
![](images/tools-legend.png)
Railroad-PT («known» model)
Please find below the performance char for Railroad-PT.
Memory Consumption
![](content/results/html/perfplots/Railroad-PT-ReachabilityBounds-MEM.png)
![](images/tools-legend.png)
CPU Consumption
![](content/results/html/perfplots/Railroad-PT-ReachabilityBounds-CPU.png)
![](images/tools-legend.png)
ResAllocation-PT («known» model)
Please find below the performance char for ResAllocation-PT.
Memory Consumption
![](content/results/html/perfplots/ResAllocation-PT-ReachabilityBounds-MEM.png)
![](images/tools-legend.png)
CPU Consumption
![](content/results/html/perfplots/ResAllocation-PT-ReachabilityBounds-CPU.png)
![](images/tools-legend.png)
Ring-PT («known» model)
Please find below the performance char for Ring-PT.
Memory Consumption
![](content/results/html/perfplots/Ring-PT-ReachabilityBounds-MEM.png)
![](images/tools-legend.png)
CPU Consumption
![](content/results/html/perfplots/Ring-PT-ReachabilityBounds-CPU.png)
![](images/tools-legend.png)
RwMutex-PT («known» model)
Please find below the performance char for RwMutex-PT.
Memory Consumption
![](content/results/html/perfplots/RwMutex-PT-ReachabilityBounds-MEM.png)
![](images/tools-legend.png)
CPU Consumption
![](content/results/html/perfplots/RwMutex-PT-ReachabilityBounds-CPU.png)
![](images/tools-legend.png)
SharedMemory-PT («known» model)
Please find below the performance char for SharedMemory-PT.
Memory Consumption
![](content/results/html/perfplots/SharedMemory-PT-ReachabilityBounds-MEM.png)
![](images/tools-legend.png)
CPU Consumption
![](content/results/html/perfplots/SharedMemory-PT-ReachabilityBounds-CPU.png)
![](images/tools-legend.png)
SimpleLoadBal-PT («known» model)
Please find below the performance char for SimpleLoadBal-PT.
Memory Consumption
![](content/results/html/perfplots/SimpleLoadBal-PT-ReachabilityBounds-MEM.png)
![](images/tools-legend.png)
CPU Consumption
![](content/results/html/perfplots/SimpleLoadBal-PT-ReachabilityBounds-CPU.png)
![](images/tools-legend.png)
SurpriseCSRepetitions-PT («scrambled» version of the «known» model)
Please find below the performance char for SurpriseCSRepetitions-PT.
Memory Consumption
![](content/results/html/perfplots/SurpriseCSRepetitions-PT-ReachabilityBounds-MEM.png)
![](images/tools-legend.png)
CPU Consumption
![](content/results/html/perfplots/SurpriseCSRepetitions-PT-ReachabilityBounds-CPU.png)
![](images/tools-legend.png)
SurpriseDekker-PT («scrambled» version of the «known» model)
Please find below the performance char for SurpriseDekker-PT.
Memory Consumption
![](content/results/html/perfplots/SurpriseDekker-PT-ReachabilityBounds-MEM.png)
![](images/tools-legend.png)
CPU Consumption
![](content/results/html/perfplots/SurpriseDekker-PT-ReachabilityBounds-CPU.png)
![](images/tools-legend.png)
SurpriseDrinkVendingMachine-PT («scrambled» version of the «known» model)
Please find below the performance char for SurpriseDrinkVendingMachine-PT.
Memory Consumption
![](content/results/html/perfplots/SurpriseDrinkVendingMachine-PT-ReachabilityBounds-MEM.png)
![](images/tools-legend.png)
CPU Consumption
![](content/results/html/perfplots/SurpriseDrinkVendingMachine-PT-ReachabilityBounds-CPU.png)
![](images/tools-legend.png)
SurpriseEcho-PT («scrambled» version of the «known» model)
Please find below the performance char for SurpriseEcho-PT.
Memory Consumption
![](content/results/html/perfplots/SurpriseEcho-PT-ReachabilityBounds-MEM.png)
![](images/tools-legend.png)
CPU Consumption
![](content/results/html/perfplots/SurpriseEcho-PT-ReachabilityBounds-CPU.png)
![](images/tools-legend.png)
SurpriseFMS-PT («scrambled» version of the «known» model)
Please find below the performance char for SurpriseFMS-PT.
Memory Consumption
![](content/results/html/perfplots/SurpriseFMS-PT-ReachabilityBounds-MEM.png)
![](images/tools-legend.png)
CPU Consumption
![](content/results/html/perfplots/SurpriseFMS-PT-ReachabilityBounds-CPU.png)
![](images/tools-legend.png)
SurpriseGlobalResAllocation-PT («scrambled» version of the «known» model)
Please find below the performance char for SurpriseGlobalResAllocation-PT.
Memory Consumption
![](content/results/html/perfplots/SurpriseGlobalResAllocation-PT-ReachabilityBounds-MEM.png)
![](images/tools-legend.png)
CPU Consumption
![](content/results/html/perfplots/SurpriseGlobalResAllocation-PT-ReachabilityBounds-CPU.png)
![](images/tools-legend.png)
SurpriseHouseConstruction-PT («scrambled» version of the «known» model)
Please find below the performance char for SurpriseHouseConstruction-PT.
Memory Consumption
![](content/results/html/perfplots/SurpriseHouseConstruction-PT-ReachabilityBounds-MEM.png)
![](images/tools-legend.png)
CPU Consumption
![](content/results/html/perfplots/SurpriseHouseConstruction-PT-ReachabilityBounds-CPU.png)
![](images/tools-legend.png)
SurpriseIBMB2S565S3960-PT («scrambled» version of the «known» model)
Please find below the performance char for SurpriseIBMB2S565S3960-PT.
Memory Consumption
![](content/results/html/perfplots/SurpriseIBMB2S565S3960-PT-ReachabilityBounds-MEM.png)
![](images/tools-legend.png)
CPU Consumption
![](content/results/html/perfplots/SurpriseIBMB2S565S3960-PT-ReachabilityBounds-CPU.png)
![](images/tools-legend.png)
SurpriseKanban-PT («scrambled» version of the «known» model)
Please find below the performance char for SurpriseKanban-PT.
Memory Consumption
![](content/results/html/perfplots/SurpriseKanban-PT-ReachabilityBounds-MEM.png)
![](images/tools-legend.png)
CPU Consumption
![](content/results/html/perfplots/SurpriseKanban-PT-ReachabilityBounds-CPU.png)
![](images/tools-legend.png)
SurpriseLamportFastMutEx-PT («scrambled» version of the «known» model)
Please find below the performance char for SurpriseLamportFastMutEx-PT.
Memory Consumption
![](content/results/html/perfplots/SurpriseLamportFastMutEx-PT-ReachabilityBounds-MEM.png)
![](images/tools-legend.png)
CPU Consumption
![](content/results/html/perfplots/SurpriseLamportFastMutEx-PT-ReachabilityBounds-CPU.png)
![](images/tools-legend.png)
SurpriseMAPK-PT («scrambled» version of the «known» model)
Please find below the performance char for SurpriseMAPK-PT.
Memory Consumption
![](content/results/html/perfplots/SurpriseMAPK-PT-ReachabilityBounds-MEM.png)
![](images/tools-legend.png)
CPU Consumption
![](content/results/html/perfplots/SurpriseMAPK-PT-ReachabilityBounds-CPU.png)
![](images/tools-legend.png)
SurpriseNeoElection-PT («scrambled» version of the «known» model)
Please find below the performance char for SurpriseNeoElection-PT.
Memory Consumption
![](content/results/html/perfplots/SurpriseNeoElection-PT-ReachabilityBounds-MEM.png)
![](images/tools-legend.png)
CPU Consumption
![](content/results/html/perfplots/SurpriseNeoElection-PT-ReachabilityBounds-CPU.png)
![](images/tools-legend.png)
SurprisePermAdmissibility-PT («scrambled» version of the «known» model)
Please find below the performance char for SurprisePermAdmissibility-PT.
Memory Consumption
![](content/results/html/perfplots/SurprisePermAdmissibility-PT-ReachabilityBounds-MEM.png)
![](images/tools-legend.png)
CPU Consumption
![](content/results/html/perfplots/SurprisePermAdmissibility-PT-ReachabilityBounds-CPU.png)
![](images/tools-legend.png)
SurprisePeterson-PT («scrambled» version of the «known» model)
Please find below the performance char for SurprisePeterson-PT.
Memory Consumption
![](content/results/html/perfplots/SurprisePeterson-PT-ReachabilityBounds-MEM.png)
![](images/tools-legend.png)
CPU Consumption
![](content/results/html/perfplots/SurprisePeterson-PT-ReachabilityBounds-CPU.png)
![](images/tools-legend.png)
SurprisePhilosophers-PT («scrambled» version of the «known» model)
Please find below the performance char for SurprisePhilosophers-PT.
Memory Consumption
![](content/results/html/perfplots/SurprisePhilosophers-PT-ReachabilityBounds-MEM.png)
![](images/tools-legend.png)
CPU Consumption
![](content/results/html/perfplots/SurprisePhilosophers-PT-ReachabilityBounds-CPU.png)
![](images/tools-legend.png)
SurprisePhilosophersDyn-PT («scrambled» version of the «known» model)
Please find below the performance char for SurprisePhilosophersDyn-PT.
Memory Consumption
![](content/results/html/perfplots/SurprisePhilosophersDyn-PT-ReachabilityBounds-MEM.png)
![](images/tools-legend.png)
CPU Consumption
![](content/results/html/perfplots/SurprisePhilosophersDyn-PT-ReachabilityBounds-CPU.png)
![](images/tools-legend.png)
SurprisePlanning-PT («scrambled» version of the «known» model)
Please find below the performance char for SurprisePlanning-PT.
Memory Consumption
![](content/results/html/perfplots/SurprisePlanning-PT-ReachabilityBounds-MEM.png)
![](images/tools-legend.png)
CPU Consumption
![](content/results/html/perfplots/SurprisePlanning-PT-ReachabilityBounds-CPU.png)
![](images/tools-legend.png)
SurpriseQuasiCertifProtocol-PT («scrambled» version of the «known» model)
Please find below the performance char for SurpriseQuasiCertifProtocol-PT.
Memory Consumption
![](content/results/html/perfplots/SurpriseQuasiCertifProtocol-PT-ReachabilityBounds-MEM.png)
![](images/tools-legend.png)
CPU Consumption
![](content/results/html/perfplots/SurpriseQuasiCertifProtocol-PT-ReachabilityBounds-CPU.png)
![](images/tools-legend.png)
SurpriseRailroad-PT («scrambled» version of the «known» model)
Please find below the performance char for SurpriseRailroad-PT.
Memory Consumption
![](content/results/html/perfplots/SurpriseRailroad-PT-ReachabilityBounds-MEM.png)
![](images/tools-legend.png)
CPU Consumption
![](content/results/html/perfplots/SurpriseRailroad-PT-ReachabilityBounds-CPU.png)
![](images/tools-legend.png)
SurpriseRwMutex-PT («scrambled» version of the «known» model)
Please find below the performance char for SurpriseRwMutex-PT.
Memory Consumption
![](content/results/html/perfplots/SurpriseRwMutex-PT-ReachabilityBounds-MEM.png)
![](images/tools-legend.png)
CPU Consumption
![](content/results/html/perfplots/SurpriseRwMutex-PT-ReachabilityBounds-CPU.png)
![](images/tools-legend.png)
SurpriseSharedMemory-PT («scrambled» version of the «known» model)
Please find below the performance char for SurpriseSharedMemory-PT.
Memory Consumption
![](content/results/html/perfplots/SurpriseSharedMemory-PT-ReachabilityBounds-MEM.png)
![](images/tools-legend.png)
CPU Consumption
![](content/results/html/perfplots/SurpriseSharedMemory-PT-ReachabilityBounds-CPU.png)
![](images/tools-legend.png)
SurpriseSimpleLoadBal-PT («scrambled» version of the «known» model)
Please find below the performance char for SurpriseSimpleLoadBal-PT.
Memory Consumption
![](content/results/html/perfplots/SurpriseSimpleLoadBal-PT-ReachabilityBounds-MEM.png)
![](images/tools-legend.png)
CPU Consumption
![](content/results/html/perfplots/SurpriseSimpleLoadBal-PT-ReachabilityBounds-CPU.png)
![](images/tools-legend.png)
SurpriseTokenRing-PT («scrambled» version of the «known» model)
Please find below the performance char for SurpriseTokenRing-PT.
Memory Consumption
![](content/results/html/perfplots/SurpriseTokenRing-PT-ReachabilityBounds-MEM.png)
![](images/tools-legend.png)
CPU Consumption
![](content/results/html/perfplots/SurpriseTokenRing-PT-ReachabilityBounds-CPU.png)
![](images/tools-legend.png)
TokenRing-PT («known» model)
Please find below the performance char for TokenRing-PT.
Memory Consumption
![](content/results/html/perfplots/TokenRing-PT-ReachabilityBounds-MEM.png)
![](images/tools-legend.png)
CPU Consumption
![](content/results/html/perfplots/TokenRing-PT-ReachabilityBounds-CPU.png)
![](images/tools-legend.png)