fond
Model Checking Contest 2020
10th edition, Paris, France, June 23, 2020
Tools Consumption of Ressources for CTLCardinality
Last Updated
Oct 13, 2019
under construction
The MCC web site is currently under construction
Please have a look at the previous editions' material at this stage (see upper-right menu)

Introduction

This page presents how tools are efficient to cope with time and memory when dealing with the CTLCardinality examination and depending on the categories of models (Known, Surprise, both).

Each chart shows how time (or memory) evolves when dealing with model instances. The X axis represents all the possible models of a given category and the Y axis the corresponding value for time (or memory). Noe that time (or memory) consumtption have been sorted ascending for each tool separately so the values may not correspond to he same models.

«Surprise» models

The charts are below, click on the chart to enlarge it. 49 instances of models had to be processed. When the curves become vertical, it means the corresponding tool cannot compute anymore model.

Evolution of Memory

Evolution of Time

«Known» models

The charts are below, click on the chart to enlarge it. 969 instances of models had to be processed. When the curves become vertical, it means the corresponding tool cannot compute anymore model.

Evolution of Memory

Evolution of Time

All categories of Models Together

The charts are below, click on the chart to enlarge it. 1987 instances of models had to be processed. When the curves become vertical, it means the corresponding tool cannot compute anymore model.

Evolution of Memory

Evolution of Time