Introduction

This page summarizes the performances of tools for the CTLFireability 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

CPU Consumption

Dekker-PT («known» model)

Please find below the performance char for Dekker-PT.

Memory Consumption

CPU Consumption

DrinkVendingMachine-PT («known» model)

Please find below the performance char for DrinkVendingMachine-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-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

Kanban-PT («known» model)

Please find below the performance char for Kanban-PT.

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

NeoElection-PT («known» model)

Please find below the performance char for NeoElection-PT.

Memory Consumption

CPU Consumption

PermAdmissibility-PT («known» model)

Please find below the performance char for PermAdmissibility-PT.

Memory Consumption

CPU Consumption

Peterson-PT («known» model)

Please find below the performance char for Peterson-PT.

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

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-PT («known» model)

Please find below the performance char for SharedMemory-PT.

Memory Consumption

CPU Consumption

SimpleLoadBal-PT («known» model)

Please find below the performance char for SimpleLoadBal-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

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

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-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-PT («scrambled» version of the «known» model)

Please find below the performance char for SurpriseNeoElection-PT.

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-PT («scrambled» version of the «known» model)

Please find below the performance char for SurprisePeterson-PT.

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

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

Please find below the performance char for SurprisePlanning-PT.

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

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

Please find below the performance char for SurpriseRwMutex-PT.

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-PT («scrambled» version of the «known» model)

Please find below the performance char for SurpriseSimpleLoadBal-PT.

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

TokenRing-PT («known» model)

Please find below the performance char for TokenRing-PT.

Memory Consumption

CPU Consumption