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
_CTLFireability_PTN_CTLFireability_mem.png)
Execution time
_CTLFireability_PTN_CTLFireability_tim.png)
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
_CTLFireability_PTN_CTLFireability_mem.png)
Execution time
_CTLFireability_PTN_CTLFireability_tim.png)
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
_CTLFireability_COL_CTLFireability_mem.png)
Execution time
_CTLFireability_COL_CTLFireability_tim.png)
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
_CTLFireability_PTN_CTLFireability_mem.png)
Execution time
_CTLFireability_PTN_CTLFireability_tim.png)
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
_CTLFireability_PTN_CTLFireability_mem.png)
Execution time
_CTLFireability_PTN_CTLFireability_tim.png)
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
_CTLFireability_PTN_CTLFireability_mem.png)
Execution time
_CTLFireability_PTN_CTLFireability_tim.png)
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
_CTLFireability_COL_CTLFireability_mem.png)
Execution time
_CTLFireability_COL_CTLFireability_tim.png)
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
_CTLFireability_PTN_CTLFireability_mem.png)
Execution time
_CTLFireability_PTN_CTLFireability_tim.png)
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
_CTLFireability_PTN_CTLFireability_mem.png)
Execution time
_CTLFireability_PTN_CTLFireability_tim.png)
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
_CTLFireability_PTN_CTLFireability_mem.png)
Execution time
_CTLFireability_PTN_CTLFireability_tim.png)
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
_CTLFireability_COL_CTLFireability_mem.png)
Execution time
_CTLFireability_COL_CTLFireability_tim.png)
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
_CTLFireability_COL_CTLFireability_mem.png)
Execution time
_CTLFireability_COL_CTLFireability_tim.png)
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
_CTLFireability_PTN_CTLFireability_mem.png)
Execution time
_CTLFireability_PTN_CTLFireability_tim.png)
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
_CTLFireability_PTN_CTLFireability_mem.png)
Execution time
_CTLFireability_PTN_CTLFireability_tim.png)
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
_CTLFireability_PTN_CTLFireability_mem.png)
Execution time
_CTLFireability_PTN_CTLFireability_tim.png)
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
_CTLFireability_PTN_CTLFireability_mem.png)
Execution time
_CTLFireability_PTN_CTLFireability_tim.png)
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
_CTLFireability_PTN_CTLFireability_mem.png)
Execution time
_CTLFireability_PTN_CTLFireability_tim.png)
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
_CTLFireability_COL_CTLFireability_mem.png)
Execution time
_CTLFireability_COL_CTLFireability_tim.png)
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
_CTLFireability_PTN_CTLFireability_mem.png)
Execution time
_CTLFireability_PTN_CTLFireability_tim.png)
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
_CTLFireability_PTN_CTLFireability_mem.png)
Execution time
_CTLFireability_PTN_CTLFireability_tim.png)
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
_CTLFireability_PTN_CTLFireability_mem.png)
Execution time
_CTLFireability_PTN_CTLFireability_tim.png)
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
_CTLFireability_PTN_CTLFireability_mem.png)
Execution time
_CTLFireability_PTN_CTLFireability_tim.png)
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
_CTLFireability_COL_CTLFireability_mem.png)
Execution time
_CTLFireability_COL_CTLFireability_tim.png)
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
_CTLFireability_PTN_CTLFireability_mem.png)
Execution time
_CTLFireability_PTN_CTLFireability_tim.png)
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
_CTLFireability_PTN_CTLFireability_mem.png)
Execution time
_CTLFireability_PTN_CTLFireability_tim.png)
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
_CTLFireability_PTN_CTLFireability_mem.png)
Execution time
_CTLFireability_PTN_CTLFireability_tim.png)
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
_CTLFireability_COL_CTLFireability_mem.png)
Execution time
_CTLFireability_COL_CTLFireability_tim.png)
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
_CTLFireability_PTN_CTLFireability_mem.png)
Execution time
_CTLFireability_PTN_CTLFireability_tim.png)
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
_CTLFireability_PTN_CTLFireability_mem.png)
Execution time
_CTLFireability_PTN_CTLFireability_tim.png)
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
_CTLFireability_COL_CTLFireability_mem.png)
Execution time
_CTLFireability_COL_CTLFireability_tim.png)
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
_CTLFireability_PTN_CTLFireability_mem.png)
Execution time
_CTLFireability_PTN_CTLFireability_tim.png)
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
_CTLFireability_COL_CTLFireability_mem.png)
Execution time
_CTLFireability_COL_CTLFireability_tim.png)
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
_CTLFireability_PTN_CTLFireability_mem.png)
Execution time
_CTLFireability_PTN_CTLFireability_tim.png)
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
_CTLFireability_COL_CTLFireability_mem.png)
Execution time
_CTLFireability_COL_CTLFireability_tim.png)
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
_CTLFireability_PTN_CTLFireability_mem.png)
Execution time
_CTLFireability_PTN_CTLFireability_tim.png)
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
_CTLFireability_PTN_CTLFireability_mem.png)
Execution time
_CTLFireability_PTN_CTLFireability_tim.png)
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
_CTLFireability_PTN_CTLFireability_mem.png)
Execution time
_CTLFireability_PTN_CTLFireability_tim.png)
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
_CTLFireability_PTN_CTLFireability_mem.png)
Execution time
_CTLFireability_PTN_CTLFireability_tim.png)
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
_CTLFireability_PTN_CTLFireability_mem.png)
Execution time
_CTLFireability_PTN_CTLFireability_tim.png)
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
_CTLFireability_COL_CTLFireability_mem.png)
Execution time
_CTLFireability_COL_CTLFireability_tim.png)
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
_CTLFireability_PTN_CTLFireability_mem.png)
Execution time
_CTLFireability_PTN_CTLFireability_tim.png)
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
_CTLFireability_PTN_CTLFireability_mem.png)
Execution time
_CTLFireability_PTN_CTLFireability_tim.png)
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
_CTLFireability_PTN_CTLFireability_mem.png)
Execution time
_CTLFireability_PTN_CTLFireability_tim.png)
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
_CTLFireability_PTN_CTLFireability_mem.png)
Execution time
_CTLFireability_PTN_CTLFireability_tim.png)
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
_CTLFireability_PTN_CTLFireability_mem.png)
Execution time
_CTLFireability_PTN_CTLFireability_tim.png)
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
_CTLFireability_COL_CTLFireability_mem.png)
Execution time
_CTLFireability_COL_CTLFireability_tim.png)
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
_CTLFireability_PTN_CTLFireability_mem.png)
Execution time
_CTLFireability_PTN_CTLFireability_tim.png)
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
_CTLFireability_COL_CTLFireability_mem.png)
Execution time
_CTLFireability_COL_CTLFireability_tim.png)
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
_CTLFireability_PTN_CTLFireability_mem.png)
Execution time
_CTLFireability_PTN_CTLFireability_tim.png)
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
_CTLFireability_PTN_CTLFireability_mem.png)
Execution time
_CTLFireability_PTN_CTLFireability_tim.png)
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
_CTLFireability_COL_CTLFireability_mem.png)
Execution time
_CTLFireability_COL_CTLFireability_tim.png)
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
_CTLFireability_PTN_CTLFireability_mem.png)
Execution time
_CTLFireability_PTN_CTLFireability_tim.png)
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
_CTLFireability_PTN_CTLFireability_mem.png)
Execution time
_CTLFireability_PTN_CTLFireability_tim.png)
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
_CTLFireability_PTN_CTLFireability_mem.png)
Execution time
_CTLFireability_PTN_CTLFireability_tim.png)
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
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
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
