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
![](content/results/charts/modlperf_BridgeAndVehicles_CTLCardinality_COL_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_BridgeAndVehicles_CTLCardinality_COL_CTLCardinality_tim.png)
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
![](content/results/charts/modlperf_BridgeAndVehicles_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_BridgeAndVehicles_CTLCardinality_PTN_CTLCardinality_tim.png)
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
![](content/results/charts/modlperf_HypercubeGrid_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_HypercubeGrid_CTLCardinality_PTN_CTLCardinality_tim.png)
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
![](content/results/charts/modlperf_IBM319_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_IBM319_CTLCardinality_PTN_CTLCardinality_tim.png)
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
![](content/results/charts/modlperf_IBM5964_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_IBM5964_CTLCardinality_PTN_CTLCardinality_tim.png)
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
![](content/results/charts/modlperf_IBM703_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_IBM703_CTLCardinality_PTN_CTLCardinality_tim.png)
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
![](content/results/charts/modlperf_IOTPpurchase_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_IOTPpurchase_CTLCardinality_PTN_CTLCardinality_tim.png)
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
![](content/results/charts/modlperf_Parking_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_Parking_CTLCardinality_PTN_CTLCardinality_tim.png)
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
![](content/results/charts/modlperf_PhaseVariation_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_PhaseVariation_CTLCardinality_PTN_CTLCardinality_tim.png)
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
![](content/results/charts/modlperf_Raft_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_Raft_CTLCardinality_PTN_CTLCardinality_tim.png)
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
![](content/results/charts/modlperf_SafeBus_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_SafeBus_CTLCardinality_PTN_CTLCardinality_tim.png)
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
![](content/results/charts/modlperf_SmallOperatingSystem_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_SmallOperatingSystem_CTLCardinality_PTN_CTLCardinality_tim.png)
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
![](content/results/charts/modlperf_SwimmingPool_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_SwimmingPool_CTLCardinality_PTN_CTLCardinality_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
![](content/results/charts/modlperf_Angiogenesis (stripped)_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_Angiogenesis (stripped)_CTLCardinality_PTN_CTLCardinality_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
![](content/results/charts/modlperf_CSRepetitions (stripped)_CTLCardinality_COL_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_CSRepetitions (stripped)_CTLCardinality_COL_CTLCardinality_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
![](content/results/charts/modlperf_CSRepetitions (stripped)_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_CSRepetitions (stripped)_CTLCardinality_PTN_CTLCardinality_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
![](content/results/charts/modlperf_CircadianClock (stripped)_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_CircadianClock (stripped)_CTLCardinality_PTN_CTLCardinality_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
![](content/results/charts/modlperf_CircularTrains (stripped)_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_CircularTrains (stripped)_CTLCardinality_PTN_CTLCardinality_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
![](content/results/charts/modlperf_DatabaseWithMutex (stripped)_CTLCardinality_COL_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_DatabaseWithMutex (stripped)_CTLCardinality_COL_CTLCardinality_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
![](content/results/charts/modlperf_DatabaseWithMutex (stripped)_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_DatabaseWithMutex (stripped)_CTLCardinality_PTN_CTLCardinality_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
![](content/results/charts/modlperf_Dekker (stripped)_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_Dekker (stripped)_CTLCardinality_PTN_CTLCardinality_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
![](content/results/charts/modlperf_Diffusion2D (stripped)_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_Diffusion2D (stripped)_CTLCardinality_PTN_CTLCardinality_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
![](content/results/charts/modlperf_DotAndBoxes (stripped)_CTLCardinality_COL_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_DotAndBoxes (stripped)_CTLCardinality_COL_CTLCardinality_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
![](content/results/charts/modlperf_DrinkVendingMachine (stripped)_CTLCardinality_COL_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_DrinkVendingMachine (stripped)_CTLCardinality_COL_CTLCardinality_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
![](content/results/charts/modlperf_DrinkVendingMachine (stripped)_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_DrinkVendingMachine (stripped)_CTLCardinality_PTN_CTLCardinality_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
![](content/results/charts/modlperf_ERK (stripped)_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_ERK (stripped)_CTLCardinality_PTN_CTLCardinality_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
![](content/results/charts/modlperf_EnergyBus (stripped)_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_EnergyBus (stripped)_CTLCardinality_PTN_CTLCardinality_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
![](content/results/charts/modlperf_Eratosthenes (stripped)_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_Eratosthenes (stripped)_CTLCardinality_PTN_CTLCardinality_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
![](content/results/charts/modlperf_FMS (stripped)_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_FMS (stripped)_CTLCardinality_PTN_CTLCardinality_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
![](content/results/charts/modlperf_GlobalResAllocation (stripped)_CTLCardinality_COL_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_GlobalResAllocation (stripped)_CTLCardinality_COL_CTLCardinality_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
![](content/results/charts/modlperf_GlobalResAllocation (stripped)_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_GlobalResAllocation (stripped)_CTLCardinality_PTN_CTLCardinality_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
![](content/results/charts/modlperf_HouseConstruction (stripped)_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_HouseConstruction (stripped)_CTLCardinality_PTN_CTLCardinality_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
![](content/results/charts/modlperf_Kanban (stripped)_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_Kanban (stripped)_CTLCardinality_PTN_CTLCardinality_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
![](content/results/charts/modlperf_LamportFastMutEx (stripped)_CTLCardinality_COL_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_LamportFastMutEx (stripped)_CTLCardinality_COL_CTLCardinality_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
![](content/results/charts/modlperf_LamportFastMutEx (stripped)_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_LamportFastMutEx (stripped)_CTLCardinality_PTN_CTLCardinality_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
![](content/results/charts/modlperf_MAPK (stripped)_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_MAPK (stripped)_CTLCardinality_PTN_CTLCardinality_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
![](content/results/charts/modlperf_MultiwaySync (stripped)_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_MultiwaySync (stripped)_CTLCardinality_PTN_CTLCardinality_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
![](content/results/charts/modlperf_NeoElection (stripped)_CTLCardinality_COL_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_NeoElection (stripped)_CTLCardinality_COL_CTLCardinality_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
![](content/results/charts/modlperf_NeoElection (stripped)_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_NeoElection (stripped)_CTLCardinality_PTN_CTLCardinality_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
![](content/results/charts/modlperf_ParamProductionCell (stripped)_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_ParamProductionCell (stripped)_CTLCardinality_PTN_CTLCardinality_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
![](content/results/charts/modlperf_PermAdmissibility (stripped)_CTLCardinality_COL_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_PermAdmissibility (stripped)_CTLCardinality_COL_CTLCardinality_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
![](content/results/charts/modlperf_PermAdmissibility (stripped)_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_PermAdmissibility (stripped)_CTLCardinality_PTN_CTLCardinality_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
![](content/results/charts/modlperf_Peterson (stripped)_CTLCardinality_COL_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_Peterson (stripped)_CTLCardinality_COL_CTLCardinality_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
![](content/results/charts/modlperf_Peterson (stripped)_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_Peterson (stripped)_CTLCardinality_PTN_CTLCardinality_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
![](content/results/charts/modlperf_Philosophers (stripped)_CTLCardinality_COL_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_Philosophers (stripped)_CTLCardinality_COL_CTLCardinality_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
![](content/results/charts/modlperf_Philosophers (stripped)_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_Philosophers (stripped)_CTLCardinality_PTN_CTLCardinality_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
![](content/results/charts/modlperf_PhilosophersDyn (stripped)_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_PhilosophersDyn (stripped)_CTLCardinality_PTN_CTLCardinality_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
![](content/results/charts/modlperf_PolyORBLF (stripped)_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_PolyORBLF (stripped)_CTLCardinality_PTN_CTLCardinality_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
![](content/results/charts/modlperf_PolyORBNT (stripped)_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_PolyORBNT (stripped)_CTLCardinality_PTN_CTLCardinality_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
![](content/results/charts/modlperf_QuasiCertifProtocol (stripped)_CTLCardinality_COL_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_QuasiCertifProtocol (stripped)_CTLCardinality_COL_CTLCardinality_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
![](content/results/charts/modlperf_QuasiCertifProtocol (stripped)_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_QuasiCertifProtocol (stripped)_CTLCardinality_PTN_CTLCardinality_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
![](content/results/charts/modlperf_Railroad (stripped)_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_Railroad (stripped)_CTLCardinality_PTN_CTLCardinality_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
![](content/results/charts/modlperf_ResAllocation (stripped)_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_ResAllocation (stripped)_CTLCardinality_PTN_CTLCardinality_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
![](content/results/charts/modlperf_RwMutex (stripped)_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_RwMutex (stripped)_CTLCardinality_PTN_CTLCardinality_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
![](content/results/charts/modlperf_SharedMemory (stripped)_CTLCardinality_COL_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_SharedMemory (stripped)_CTLCardinality_COL_CTLCardinality_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
![](content/results/charts/modlperf_SharedMemory (stripped)_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_SharedMemory (stripped)_CTLCardinality_PTN_CTLCardinality_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
![](content/results/charts/modlperf_SimpleLoadBal (stripped)_CTLCardinality_COL_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_SimpleLoadBal (stripped)_CTLCardinality_COL_CTLCardinality_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
![](content/results/charts/modlperf_SimpleLoadBal (stripped)_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_SimpleLoadBal (stripped)_CTLCardinality_PTN_CTLCardinality_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
![](content/results/charts/modlperf_Solitaire (stripped)_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_Solitaire (stripped)_CTLCardinality_PTN_CTLCardinality_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
![](content/results/charts/modlperf_TokenRing (stripped)_CTLCardinality_COL_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_TokenRing (stripped)_CTLCardinality_COL_CTLCardinality_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
![](content/results/charts/modlperf_TokenRing (stripped)_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_TokenRing (stripped)_CTLCardinality_PTN_CTLCardinality_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
![](content/results/charts/modlperf_UtahNoC (stripped)_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_UtahNoC (stripped)_CTLCardinality_PTN_CTLCardinality_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
![](content/results/charts/modlperf_ARMCacheCoherence_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_ARMCacheCoherence_CTLCardinality_PTN_CTLCardinality_tim.png)
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
![](content/results/charts/modlperf_Angiogenesis_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_Angiogenesis_CTLCardinality_PTN_CTLCardinality_tim.png)
CSRepetitions, Colored
This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.
Memory Consumption
![](content/results/charts/modlperf_CSRepetitions_CTLCardinality_COL_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_CSRepetitions_CTLCardinality_COL_CTLCardinality_tim.png)
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
![](content/results/charts/modlperf_CSRepetitions_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_CSRepetitions_CTLCardinality_PTN_CTLCardinality_tim.png)
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
![](content/results/charts/modlperf_CircadianClock_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_CircadianClock_CTLCardinality_PTN_CTLCardinality_tim.png)
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
![](content/results/charts/modlperf_CircularTrains_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_CircularTrains_CTLCardinality_PTN_CTLCardinality_tim.png)
DatabaseWithMutex, Colored
This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.
Memory Consumption
![](content/results/charts/modlperf_DatabaseWithMutex_CTLCardinality_COL_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_DatabaseWithMutex_CTLCardinality_COL_CTLCardinality_tim.png)
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
![](content/results/charts/modlperf_DatabaseWithMutex_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_DatabaseWithMutex_CTLCardinality_PTN_CTLCardinality_tim.png)
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
![](content/results/charts/modlperf_Dekker_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_Dekker_CTLCardinality_PTN_CTLCardinality_tim.png)
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
![](content/results/charts/modlperf_Diffusion2D_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_Diffusion2D_CTLCardinality_PTN_CTLCardinality_tim.png)
DotAndBoxes, Colored
This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.
Memory Consumption
![](content/results/charts/modlperf_DotAndBoxes_CTLCardinality_COL_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_DotAndBoxes_CTLCardinality_COL_CTLCardinality_tim.png)
DrinkVendingMachine, Colored
This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.
Memory Consumption
![](content/results/charts/modlperf_DrinkVendingMachine_CTLCardinality_COL_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_DrinkVendingMachine_CTLCardinality_COL_CTLCardinality_tim.png)
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
![](content/results/charts/modlperf_DrinkVendingMachine_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_DrinkVendingMachine_CTLCardinality_PTN_CTLCardinality_tim.png)
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
![](content/results/charts/modlperf_ERK_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_ERK_CTLCardinality_PTN_CTLCardinality_tim.png)
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
![](content/results/charts/modlperf_Eratosthenes_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_Eratosthenes_CTLCardinality_PTN_CTLCardinality_tim.png)
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
![](content/results/charts/modlperf_FMS_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_FMS_CTLCardinality_PTN_CTLCardinality_tim.png)
GlobalResAllocation, Colored
This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.
Memory Consumption
![](content/results/charts/modlperf_GlobalResAllocation_CTLCardinality_COL_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_GlobalResAllocation_CTLCardinality_COL_CTLCardinality_tim.png)
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
![](content/results/charts/modlperf_GlobalResAllocation_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_GlobalResAllocation_CTLCardinality_PTN_CTLCardinality_tim.png)
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
![](content/results/charts/modlperf_HouseConstruction_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_HouseConstruction_CTLCardinality_PTN_CTLCardinality_tim.png)
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
![](content/results/charts/modlperf_Kanban_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_Kanban_CTLCardinality_PTN_CTLCardinality_tim.png)
LamportFastMutEx, Colored
This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.
Memory Consumption
![](content/results/charts/modlperf_LamportFastMutEx_CTLCardinality_COL_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_LamportFastMutEx_CTLCardinality_COL_CTLCardinality_tim.png)
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
![](content/results/charts/modlperf_LamportFastMutEx_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_LamportFastMutEx_CTLCardinality_PTN_CTLCardinality_tim.png)
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
![](content/results/charts/modlperf_MAPK_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_MAPK_CTLCardinality_PTN_CTLCardinality_tim.png)
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
![](content/results/charts/modlperf_MultiwaySync_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_MultiwaySync_CTLCardinality_PTN_CTLCardinality_tim.png)
NeoElection, Colored
This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.
Memory Consumption
![](content/results/charts/modlperf_NeoElection_CTLCardinality_COL_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_NeoElection_CTLCardinality_COL_CTLCardinality_tim.png)
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
![](content/results/charts/modlperf_NeoElection_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_NeoElection_CTLCardinality_PTN_CTLCardinality_tim.png)
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
![](content/results/charts/modlperf_ParamProductionCell_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_ParamProductionCell_CTLCardinality_PTN_CTLCardinality_tim.png)
PermAdmissibility, Colored
This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.
Memory Consumption
![](content/results/charts/modlperf_PermAdmissibility_CTLCardinality_COL_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_PermAdmissibility_CTLCardinality_COL_CTLCardinality_tim.png)
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
![](content/results/charts/modlperf_PermAdmissibility_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_PermAdmissibility_CTLCardinality_PTN_CTLCardinality_tim.png)
Peterson, Colored
This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.
Memory Consumption
![](content/results/charts/modlperf_Peterson_CTLCardinality_COL_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_Peterson_CTLCardinality_COL_CTLCardinality_tim.png)
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
![](content/results/charts/modlperf_Peterson_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_Peterson_CTLCardinality_PTN_CTLCardinality_tim.png)
Philosophers, Colored
This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.
Memory Consumption
![](content/results/charts/modlperf_Philosophers_CTLCardinality_COL_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_Philosophers_CTLCardinality_COL_CTLCardinality_tim.png)
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
![](content/results/charts/modlperf_Philosophers_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_Philosophers_CTLCardinality_PTN_CTLCardinality_tim.png)
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
![](content/results/charts/modlperf_PhilosophersDyn_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_PhilosophersDyn_CTLCardinality_PTN_CTLCardinality_tim.png)
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
![](content/results/charts/modlperf_PolyORBLF_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_PolyORBLF_CTLCardinality_PTN_CTLCardinality_tim.png)
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
![](content/results/charts/modlperf_PolyORBNT_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_PolyORBNT_CTLCardinality_PTN_CTLCardinality_tim.png)
QuasiCertifProtocol, Colored
This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.
Memory Consumption
![](content/results/charts/modlperf_QuasiCertifProtocol_CTLCardinality_COL_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_QuasiCertifProtocol_CTLCardinality_COL_CTLCardinality_tim.png)
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
![](content/results/charts/modlperf_QuasiCertifProtocol_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_QuasiCertifProtocol_CTLCardinality_PTN_CTLCardinality_tim.png)
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
![](content/results/charts/modlperf_Railroad_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_Railroad_CTLCardinality_PTN_CTLCardinality_tim.png)
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
![](content/results/charts/modlperf_ResAllocation_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_ResAllocation_CTLCardinality_PTN_CTLCardinality_tim.png)
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
![](content/results/charts/modlperf_RwMutex_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_RwMutex_CTLCardinality_PTN_CTLCardinality_tim.png)
SharedMemory, Colored
This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.
Memory Consumption
![](content/results/charts/modlperf_SharedMemory_CTLCardinality_COL_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_SharedMemory_CTLCardinality_COL_CTLCardinality_tim.png)
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
![](content/results/charts/modlperf_SharedMemory_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_SharedMemory_CTLCardinality_PTN_CTLCardinality_tim.png)
SimpleLoadBal, Colored
This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.
Memory Consumption
![](content/results/charts/modlperf_SimpleLoadBal_CTLCardinality_COL_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_SimpleLoadBal_CTLCardinality_COL_CTLCardinality_tim.png)
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
![](content/results/charts/modlperf_SimpleLoadBal_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_SimpleLoadBal_CTLCardinality_PTN_CTLCardinality_tim.png)
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
![](content/results/charts/modlperf_Solitaire_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_Solitaire_CTLCardinality_PTN_CTLCardinality_tim.png)
TokenRing, Colored
This model is a «known» model. You will find the performance charts below, click on the chart to enlarge it.
Memory Consumption
![](content/results/charts/modlperf_TokenRing_CTLCardinality_COL_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_TokenRing_CTLCardinality_COL_CTLCardinality_tim.png)
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
![](content/results/charts/modlperf_TokenRing_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_TokenRing_CTLCardinality_PTN_CTLCardinality_tim.png)
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
![](content/results/charts/modlperf_UtahNoC_CTLCardinality_PTN_CTLCardinality_mem.png)
Execution time
![](content/results/charts/modlperf_UtahNoC_CTLCardinality_PTN_CTLCardinality_tim.png)