fond
Model Checking Contest 2019
9th edition, Prague, Czech Republic, April 7, 2019
Complete Results for the 2018 Edition of the Model Checking Contest
Last Updated
Nov 01, 2018
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)

1. Introduction

This page summarizes the results for the 2019 edition of the Model Checking Contest (MCC’2019). This page is divided in three sections:

IMPORTANT:all these documents can be reused in scientific material and papers but must respect the Creative Common licence CC-BY-NC-SA.

2. List of Qualified Tools in 2018

Ten tools where submitted this year. They all successfully went through a qualification process requiring about 1500 runs (each tool had to answer each examination for the first instance of each «known» model).

Data about these tools are summarized in the table below. For any tool, you can download the disk image that was provided with all its data. You may use these to reproduce measures locally and perform comparison with your own tool on the same benchmark. Please note that one tool (with two variants) was out of competition this year: this was agreed between the tool developer and the organizers and is part of an experiment with precomputed deep-learning.

IMPORTANT: all tool developers agreed to provide the original image disk embedding the tool they submitted his year (see links in the table below). You may operate these tools on your own. o do so, you need the second disk image (mounted by the other one) that contains all models for 2018 together with the produced formulas. This image is mounted with the default configuration, as well as in he default disk image provided in the tool submission kit (see here).

Summary of the Participating Tools
Tool name Supported
Petri nets
Representative Author Origin Type of execution Link to the submitted disk image Reported Techniques
(all examinations)
GreatSPN-Meddly P/T and colored Elvio Amparore Univ. Torino (Italy) Sequential Processing DECISION_DIAGRAMS TOPOLOGICAL UNFOLDING_TO_PT USE_NUPN
ITS-Tools P/T and colored Yann Therry-Mieg Sorbonne Université Collateral Processing BMC DECISION_DIAGRAMS EXPLICIT INITIAL_STATE K_INDUCTION LTSMIN PARTIAL_ORDER SAT_SMT STRUCTURAL_REDUCTION TAUTOLOGY TOPOLOGICAL USE_NUPN
ITS-Tools.L P/T and colored Yann Therry-Mieg Sorbonne Université Collateral Processing BMC DECISION_DIAGRAMS EXPLICIT INITIAL_STATE K_INDUCTION(0) LTSMIN PARTIAL_ORDER SAT_SMT STRUCTURAL_REDUCTION TAUTOLOGY TOPOLOGICAL USE_NUPN
LoLA P/T and colored Karsten Wolf & Torsten Liebke Universität Rostock Colateral Processing EXPLICIT SAT_SMT STATE_COMPRESSION STUBBORN_SETS SYMMETRIES TOPOLOGICAL UNFOLDING_TO_PT USE_NUPN
LTSMin P/T Jeroen Meijer University of Twente Parallel Processing DECISION_DIAGRAMS EXPLICIT USE_NUPN
MCC4MCC.full P/T and colored Alban Linard Université de Genève Collateral Processing or Sequential Processing BMC DECISION_DIAGRAMS EXPLICIT INITIAL_STATE K_INDUCTION SAT_SMT STATE_COMPRESSION STRUCTURAL_REDUCTION STUBBORN_SETS SYMMETRIES TAUTOLOGY TOPOLOGICAL UNFOLDING_TO_PT USE_NUPN
MCC4MCC.struct P/T and colored Alban Linard Université de Genève Collateral Processing or Sequential Processing BMC DECISION_DIAGRAMS EXPLICIT INITIAL_STATE K_INDUCTION SAT_SMT STATE_COMPRESSION STRUCTURAL_REDUCTION STUBBORN_SETS SYMMETRIES TAUTOLOGY TOPOLOGICAL UNFOLDING_TO_PT USE_NUPN
smart P/T Junad Babar & Andrew Miner Iowa State University Sequential Processing DECISION_DIAGRAMS IMPLICIT RELATIONS
Tapaal P/T and colored Jiri Srba Aalborg Universitet Collateral Processing CPN_APPROX CTL_CZERO EXPLICIT LP_APPROX QUERY_REDUCTION SAT_SMT SIPHON_TRAP STATE_COMPRESSION STRUCTURAL_REDUCTION STUBBORN_SETS TOPOLOGICAL TRACE_ABSTRACTION_REFINEMENT UNFOLDING_TO_PT
TINA.tedd P/T and colored Bernard Berthomieu & Silvano Dal Zilio LAAS/CNRS/Université de Toulouse Sequential Processing ABSTRACTIONS DECISION_DIAGRAMS STRUCTURAL_REDUCTION UNFOLDING_TO_PT USE_NUPN
Irma.full
(out of competition)
P/T and colored Alban Linard Université de Genève Collateral Processing or Sequential Processing BMC DECISION_DIAGRAMS EXPLICIT INITIAL_STATE K_INDUCTION SAT_SMT STATE_COMPRESSION STRUCTURAL_REDUCTION STUBBORN_SETS SYMMETRIES TAUTOLOGY TOPOLOGICAL UNFOLDING_TO_PT USE_NUPN
Irma.struct
(out of competition)
P/T and colored Alban Linard Université de Genève Collateral Processing or Sequential Processing BMC DECISION_DIAGRAMS EXPLICIT INITIAL_STATE K_INDUCTION SAT_SMT STATE_COMPRESSION STRUCTURAL_REDUCTION STUBBORN_SETS SYMMETRIES TAUTOLOGY TOPOLOGICAL UNFOLDING_TO_PT USE_NUPN

The table below lists the techniques reported per examination (and for all the tool variants when applicable).

Techniques Reported by the Participating Tools (per examination)
Tool name StateSpace UpperBounds Reachability CTL LTL
GreatSPN-Meddly DECISION_DIAGRAMS TOPOLOGICAL UNFOLDING_TO_PT USE_NUPN DECISION_DIAGRAMS TOPOLOGICAL UNFOLDING_TO_PT USE_NUPN DECISION_DIAGRAMS TOPOLOGICAL UNFOLDING_TO_PT USE_NUPN DECISION_DIAGRAMS TOPOLOGICAL UNFOLDING_TO_PT USE_NUPN
ITS-Tools DECISION_DIAGRAMS TOPOLOGICAL USE_NUPN DECISION_DIAGRAMS TOPOLOGICAL USE_NUPN BMC DECISION_DIAGRAMS EXPLICIT INITIAL_STATE K_INDUCTION LTSMIN PARTIAL_ORDER SAT_SMT STRUCTURAL_REDUCTION TAUTOLOGY TOPOLOGICAL USE_NUPN DECISION_DIAGRAMS TOPOLOGICAL USE_NUPN DECISION_DIAGRAMS EXPLICIT LTSMIN PARTIAL_ORDER SAT_SMT TOPOLOGICAL USE_NUPN
ITS-Tools.L DECISION_DIAGRAMS TOPOLOGICAL USE_NUPN DECISION_DIAGRAMS TOPOLOGICAL USE_NUPN BMC DECISION_DIAGRAMS EXPLICIT INITIAL_STATE K_INDUCTION LTSMIN PARTIAL_ORDER SAT_SMT STRUCTURAL_REDUCTION TAUTOLOGY TOPOLOGICAL USE_NUPN DECISION_DIAGRAMS TOPOLOGICAL USE_NUPN DECISION_DIAGRAMS EXPLICIT LTSMIN PARTIAL_ORDER SAT_SMT TOPOLOGICAL USE_NUPN
LoLA EXPLICIT STATE_COMPRESSION STUBBORN_SETS TOPOLOGICAL UNFOLDING_TO_PT USE_NUPN EXPLICIT SAT_SMT STATE_COMPRESSION STUBBORN_SETS SYMMETRIES TOPOLOGICAL UNFOLDING_TO_PT USE_NUPN EXPLICIT STATE_COMPRESSION STUBBORN_SETS TOPOLOGICAL UNFOLDING_TO_PT USE_NUPN EXPLICIT STATE_COMPRESSION STUBBORN_SETS TOPOLOGICAL UNFOLDING_TO_PT USE_NUPN
LTSMin DECISION_DIAGRAMS USE_NUPN DECISION_DIAGRAMS USE_NUPN DECISION_DIAGRAMS USE_NUPN DECISION_DIAGRAMS USE_NUPN EXPLICIT USE_NUPN
MCC4MCC.full DECISION_DIAGRAMS STATE_COMPRESSION STRUCTURAL_REDUCTION TOPOLOGICAL UNFOLDING_TO_PT USE_NUPN DECISION_DIAGRAMS EXPLICIT STATE_COMPRESSION STUBBORN_SETS TOPOLOGICAL UNFOLDING_TO_PT USE_NUPN BMC DECISION_DIAGRAMS EXPLICIT INITIAL_STATE K_INDUCTION SAT_SMT STATE_COMPRESSION STUBBORN_SETS SYMMETRIES TAUTOLOGY TOPOLOGICAL UNFOLDING_TO_PT USE_NUPN DECISION_DIAGRAMS EXPLICIT STATE_COMPRESSION STUBBORN_SETS TOPOLOGICAL UNFOLDING_TO_PT USE_NUPN DECISION_DIAGRAMS EXPLICIT STATE_COMPRESSION STUBBORN_SETS TOPOLOGICAL USE_NUPN
MCC4MCC.struct DECISION_DIAGRAMS STATE_COMPRESSION STRUCTURAL_REDUCTION TOPOLOGICAL UNFOLDING_TO_PT USE_NUPN DECISION_DIAGRAMS EXPLICIT STATE_COMPRESSION STUBBORN_SETS TOPOLOGICAL UNFOLDING_TO_PT USE_NUPN BMC DECISION_DIAGRAMS EXPLICIT INITIAL_STATE K_INDUCTION SAT_SMT STATE_COMPRESSION STRUCTURAL_REDUCTION STUBBORN_SETS SYMMETRIES TAUTOLOGY TOPOLOGICAL UNFOLDING_TO_PT USE_NUPN DECISION_DIAGRAMS EXPLICIT SEQUENTIAL_PROCESSING STATE_COMPRESSION STUBBORN_SETS TOPOLOGICAL UNFOLDING_TO_PT USE_NUPN DECISION_DIAGRAMS EXPLICIT STATE_COMPRESSION STUBBORN_SETS TOPOLOGICAL USE_NUPN
smart DECISION_DIAGRAMS IMPLICIT RELATIONS DECISION_DIAGRAMS
Tapaal EXPLICIT STATE_COMPRESSION EXPLICIT QUERY_REDUCTION SAT_SMT STATE_COMPRESSION STRUCTURAL_REDUCTION STUBBORN_SETS CPN_APPROX EXPLICIT LP_APPROX QUERY_REDUCTION SAT_SMT SIPHON_TRAP STATE_COMPRESSION STRUCTURAL_REDUCTION STUBBORN_SETS TOPOLOGICAL TRACE_ABSTRACTION_REFINEMENT UNFOLDING_TO_PT CPN_APPROX CTL_CZERO EXPLICIT LP_APPROX QUERY_REDUCTION SAT_SMT STATE_COMPRESSION STRUCTURAL_REDUCTION STUBBORN_SETS TRACE_ABSTRACTION_REFINEMENT UNFOLDING_TO_PT
TINA.tedd ABSTRACTIONS DECISION_DIAGRAMS STRUCTURAL_REDUCTION UNFOLDING_TO_PT USE_NUPN
Irma.full DECISION_DIAGRAMS STATE_COMPRESSION STRUCTURAL_REDUCTION TOPOLOGICAL UNFOLDING_TO_PT USE_NUPN DECISION_DIAGRAMS EXPLICIT STATE_COMPRESSION STUBBORN_SETS TOPOLOGICAL UNFOLDING_TO_PT USE_NUPN BMC DECISION_DIAGRAMS EXPLICIT INITIAL_STATE K_INDUCTION SAT_SMT STATE_COMPRESSION STRUCTURAL_REDUCTION STUBBORN_SETS SYMMETRIES TAUTOLOGY TOPOLOGICAL UNFOLDING_TO_PT USE_NUPN DECISION_DIAGRAMS EXPLICIT SEQUENTIAL_PROCESSING STATE_COMPRESSION STUBBORN_SETS TOPOLOGICAL UNFOLDING_TO_PT USE_NUPN DECISION_DIAGRAMS EXPLICIT STATE_COMPRESSION STUBBORN_SETS TOPOLOGICAL USE_NUPN
Irma.struct DECISION_DIAGRAMS STATE_COMPRESSION STRUCTURAL_REDUCTION TOPOLOGICAL UNFOLDING_TO_PT USE_NUPN DECISION_DIAGRAMS EXPLICIT STATE_COMPRESSION STUBBORN_SETS TOPOLOGICAL UNFOLDING_TO_PT USE_NUPN BMC DECISION_DIAGRAMS EXPLICIT INITIAL_STATE K_INDUCTION SAT_SMT STATE_COMPRESSION STRUCTURAL_REDUCTION STUBBORN_SETS SYMMETRIES TAUTOLOGY TOPOLOGICAL UNFOLDING_TO_PT USE_NUPN DECISION_DIAGRAMS EXPLICIT STATE_COMPRESSION STUBBORN_SETS TOPOLOGICAL UNFOLDING_TO_PT USE_NUPN DECISION_DIAGRAMS EXPLICIT STATE_COMPRESSION STUBBORN_SETS TOPOLOGICAL USE_NUPN

3. Experimental Conditions of the MCC'2018

Each tool was submitted to 8 523 executions in various conditions (947 model/instances and 9 examinations per model/instance) for which it could report: DNC (do not compete), CC (cannot compute) or the result of the query. These executions were handled by BenchKit, that was developed in the context of the MCC for massive testing of software. Then, from the raw data provided by BenchKit, some post-analysis scripts consolidated these and computed a ranking.

16 GB of memory were allocated to each virtual machine (both parallel and sequential tools) and a confinement of one hour was considered (execution aborted after one hour). So, a total of 102 276 runs (execution of one examination by the virtual machine) generated 29 GB of raw data (essentially log files and CSV of sampled data).

The table below shows some data about the involved machines and their contribution to the computation of these results. This year, we affected only physical cores to the virtual machines (discarding logical cores obtained from hyper-threading) so the balance between the various machine we used is quite different from he one of past years.

Involved Machines and Execution of the Benchmarks
  bluewhale03 bluewhale07 Caserta Ebro Quadhexa-1 Quadhexa-2 Small Total
Physical Cores 20 @ 2.8GHz 16 @ 3.2 GHz 96 @ 2.20 GHz 32 @ 2.7GHz 24 @ 2.66GHz 24 @ 2.66GHz 16×12 @ 2.4GHz
Memory (GB) 512 1024 2048 1024 144 128 12×64
Used Cores (sequential tools) 19,
19 VM in //
15,
15 VM in //
95,
95 VM in //
31,
31 VM in //
7,
7 VM in //
7,
7 VM in //
16×3,
16×3 VM in //
Used Cores (parallel tools) 16 (4 per VM),
4 VM in //
12 (4 per VM),
3 VM in //
92 (4 per VM),
23 VM in //
28 (4 per VM),
7 VM in //
20 (4 per VM),
5 VM in //
20 (4 per VM),
5 VM in //
16×8 (4 per VM),
16×20 VM in //
Number of runs 7 560 6 480 22 896 7 992 2 916 8 640 45 792 102 276
Total CPU required 127d, 20h, 32m, 8s 88d, 19h, 33m, 13s 369d, 2h, 22m, 38s 168d, 20h, 32m, 4s 47d, 20h, 50m, 37s 100d, 2h, 1m, 15s 832d, 13h, 25m, 14s 1735d, 3h, 17m, 9s
Total CPU About 4 years, 9 months and 1 day -
Time spent to complete benchmarks About 21 days -
Estimated boot time of VMs +
management (overhead)
17d, 18h (Included in total CPU) -

We are pleased to thanks those who helped in the execution of tools:

4. The Results of the MCC’2018

This First table below presents detailed results about the MCC'2018.

Details about the Examinations in the MCC'2018 (part I):
Details about Results and Scoring + Model Performance Charts
   Details about Results 
and Scoring
 Model Performance 
Charts
 Tool Resource 
consumption
StateSpace
UpperBounds
ReachabilityCardinality
ReachabilityDeadlock
ReachabilityFireability
CTLCardinality
CTLFireability
LTLCardinality
LTLFireability

This Second table below presents some performance analysis related to tools during the MCC'2018.

Details about the examinations in the MCC'2018 (part II)
Tool Performance Charts
  All
 models 
«Surprise»
 models only 
«Known»
 models only 
GreatSPN-Meddly
ITS-Tools
ITS-Tools.L
LoLA
LTSMin
MCC4MCC.full
MCC4MCC.struct
smart
Tapaal
TINA.tedd
Irma.full
Irma.struct

You can download the full archive (3.3 GB compressed and 32 GB uncompressed) of the 102 276 runs processed to compute the results of the MCC'2018. This archive contains execution traces, execution logs and sampling, as well as a large CSV files that summarizes all the executions and gnuplot scripts and data to generate the charts produced in the web site (please have a look on the READ_ME.txt file). Yo may get separately the two mostly interesting CSV files:

Note that from the two CSV file, you can identify the unique run identifier that allows you to find the traces and any information in the archive (they are also available on the web site when the too did participated).

5. The Winners for the MCC'2018

This section presents the results for the main examinations that are:

To avoid a too large disparity between models with numerous instances and those with only one, a normalization was applied so that the score, for an examination and a model, varies between 102 and 221 points. Therefore, providing a correct value may brings a different number of points according to the considered model. A multiplier was applied depending to the model category:

5.1. Winners in the StateSpace Category

11 tools out of 12 participated in this examination. Results based on the scoring shown below is:

Then, tools rank in the following order: LSMin (5 995 pts), smart (5 720 pts), M4M.full (3 459, M4M.Struct collected 3 418 pts) and Tapaal (3 113 pts). Variants of the out of competition tool Irma got 3 953 pts (full) and 3 938 pts (struct).

GreatSPN got both awards (Fastest-Tool and Smallest Memory Footprint).





GreatSPN (fastest 253 times)


GreatSPN (less memory 404 times)

Note that all the variants of Tina were considered as one tool with regards to the scoring (see rule E-4.5.).

Estimated Tool Confidence rate for StateSpace (based on the «significant values» computed by tools)
see section 6. for details
Tool name Reliability Correct Values «significant values»
LTSMin 99.68% 942 945
Tapaal 100.00% 630 630
M4M.full 100.00% 907 907
M4M.struct 100.00% 894 894
ITS-Tools 100.00% 1506 1506
ITS-Tools.L 100.00% 1425 1425
GreatSPN 100.00% 2075 2075
smart 100.00% 1212 1212
TINA.tedd 99.71% 2084 2090
Irma.full 100.00% 1022 1022
Irma.struct 100.00% 1019 1019

Please consider note 1 on tool confidence (bottom of this page).

5.2. Winners in the UpperBounds Category

11 tools out of 12 participated in this examination. Results based on the scoring shown below is:

Then, tools rank in the following order: ITS-Tools (9 027 pts, ITS-Tools.L collected 8 821 pts), LTSMin (7 134 pts), smart (5 750 pts), M4M.sruct (3 577, M4M.full collected 3 470 pts). Variants of the out of competition tool Irma got 4 277 pts (full) and 4 255 pts (struct).

LoLA got both awards (Fastest-Tool and Smallest Memory Footprint).





LoLA (fastest 430 times)


LoLA (less memory 464 times)

Estimated Tool Confidence rate for UpperBound (based on the «significant values» computed by tools)
see section 6. for details
Tool name Reliability Correct Values «significant values»
LTSMin 100.00% 5328 5328
Tapaal 99.98% 7439 7441
LoLA 100.00% 8826 8826
M4M.full 99.98% 3788 3789
M4M.struct 99.98% 3857 3858
ITS-Tools 100.00% 8170 8170
ITS-Tools.L 100.00% 7375 7375
GreatSPN 100.00% 8541 8541
smart 100.00% 4921 4921
Irma.full 100.00% 4926 4926
Irma.struct 100.00% 4901 4901

Please consider note 1 on tool confidence (bottom of this page).

5.3. Winners in the Reachability Formulas Category

10 tools out of 12 participated in these examinations (ReachabilityDeadlock, ReachabilityCardinality and ReachabilityFireability). Results based on the scoring shown below is:

Then, tools rank in the following order: LTSMin (23 125 pts), GreatSPN (19 900 pts), M4M.full (14 439, M4M.struct collected 14 032 pts). Variants of the out of competition tool Irma got 17 423 pts (full) and 17 395 pts (struct).

LoLA got the Fastest-Tool award and Tappal the Smallest Memory Footprint award.





LoLA (fastest 1 039 times)


Tapaal (less memory 1 404 times)

Estimated Tool Confidence rate for Reachability (based on the «significant values» computed by tools)
see section 6. for details
Tool name Reliability Correct Values «significant values»
LTSMin 99,93% 13418 13428
Tapaal 100.00% 25131 25131
LoLA 100.00% 24242 24242
M4M.full 100.00% 12533 12533
M4M.struct 100.00% 13012 13012
ITS-Tools 100.00% 20459 20459
ITS-Tools.L 100.00% 19894 19894
GreatSPN 100.00% 10350 10350
Irma.full 100.00% 13993 13993
Irma.struct 100.00% 13977 13977

Please consider note 1 on tool confidence (bottom of this page).

5.4. Winners in the CTL Formulas Category

10 tools out of 12 participated in these examinations (CTLCardinality and CTLFireability). Results based on the scoring shown below is:

Then, tools rank in the following order: LTSMin (12 011 pts), GreatSPN (11 748 pts), M4M.struct (4 342, M4M.full collected 4 261 pts). Variants of the out of competition tool Irma got 6 993 pts (struct) and 6977 pts (full).

Tapaal got the Fastest-Tool award and GreatSPN the Smallest Memory Footprint award.





Tapaal (fastest 312 times)


GreatSPN (less memory 330 times)

Estimated Tool Confidence rate for CTL (based on the «significant values» computed by tools)
see section 6. for details
Tool name Reliability Correct Values «significant values»
LTSMin 99,99% 8641 8642
Tapaal 99,99% 13983 13984
LoLA 99,96% 12751 12756
M4M.full 99,82% 4878 4887
M4M.struct 99,92% 5126 5130
ITS-Tools 100.00% 11215 11215
ITS-Tools.L 100.00% 10554 10554
GreatSPN 100.00% 9817 9817
Irma.full 100.00% 7224 7224

Please consider note 1 on tool confidence (bottom of this page).

5.5. Winners in the LTL Formulas Category

8 tools out of 12 participated in these examinations (LTLCardinality and LTLFireability). Results based on the scoring shown below is:

Then, tools rank in the following order: M4M.struct (10 376, M4M.full collected 9 845 pts). Variants of the out of competition tool Irma got 10 188 pts (struct) and 10 155 pts (full).

LoLA got both awards (Fastest-Tool and Smallest Memory Footprint).





LoLA (fastest 840 times)


LoLA (less memory 960 times)

Estimated Tool Confidence rate for LTL (based on the «significant values» computed by tools)
see section 6. for details
Tool name Reliability Correct Values «significant values»
LTSMin 100.00% 18906 18906
LoLA 100.00% 22976 22977
M4M.full 100.00% 11356 11356
M4M.struct 100.00% 12009 12009
ITS-Tools 99,99% 20289 20291
ITS-Tools.L 99,99% 20250 20252
Irma.full 100.00% 11873 11873
Irma.struct 100.00% 11947 11947

Please consider note 1 on tool confidence (bottom of this page).

6. Estimation of the Global Tool Confidence

A confidence analysis enforces the computation of «right results» based on the answers of participating tools. To do so, we considered each value provided in the contest (a value is a partial result such as the result of a formula or a number provided for state space, bound computation, etc.). To do so, we processed as follows:

  1. For each «line» (all tools for a given examination for a given instance), we selected all «significant values» where at least 3 tools do agree.
  2. Based on this subset of values, we computed the ratio between the selected values for the tool and the number of good answers hey provide for such values. This ratio gave us a tool confidence rate that is provided in the table below.
  3. This tool confidence rate rate was then applied to compute the scores presented in the dedicated section.

The table below provides, in first column, the computed confidence rates (that are naturally lower for tools where a bug was detected). Then, the table provides the number of correct results (column 2) out of the number of «significant values» selected for the tool (column 3). The last column shows the number of examinations (and their type) the tool was involved in.

Estimated Tool Confidence rate (based on the «significant values» computed by tools)
Tool name Reliability Correct Values «significant values» Involved Examinations
GreatSPN 100.00% 30783 30783 7 StateSpace, UpperBounds, ReachabilityCardinality, ReachabilityDeadlock, ReachabilityFireability, CTLCardinality, CTLFireability
smart 100.00% 6133 6133 2 StateSpace, UpperBounds
TINA.tedd 99.71% 2084 2090 1 StateSpace
ITS-Tools 100.00% 61639 61641 9 StateSpace, UpperBounds, ReachabilityCardinality, ReachabilityDeadlock, ReachabilityFireability, CTLCardinality, CTLFireability, LTLCardinality, LTLFireability
ITS-Tools.L 100.00% 59498 59500 9 StateSpace, UpperBounds, ReachabilityCardinality, ReachabilityDeadlock, ReachabilityFireability, CTLCardinality, CTLFireability, LTLCardinality, LTLFireability
LoLA 99.99% 68795 68801 8 UpperBounds, ReachabilityCardinality, ReachabilityDeadlock, ReachabilityFireability, CTLCardinality, CTLFireability, LTLCardinality, LTLFireability
LTSMin 99.97% 47235 47249 9 StateSpace, UpperBounds, ReachabilityCardinality, ReachabilityDeadlock, ReachabilityFireability, CTLCardinality, CTLFireability, LTLCardinality, LTLFireability
M4M.full 99.97% 33462 33472 9 StateSpace, UpperBounds, ReachabilityCardinality, ReachabilityDeadlock, ReachabilityFireability, CTLCardinality, CTLFireability, LTLCardinality, LTLFireability
M4M.struct 99.98% 34898 34903 9 StateSpace, UpperBounds, ReachabilityCardinality, ReachabilityDeadlock, ReachabilityFireability, CTLCardinality, CTLFireability, LTLCardinality, LTLFireability
Tapaal 99.99% 47183 47186 7 StateSpace, UpperBounds, ReachabilityCardinality, ReachabilityDeadlock, ReachabilityFireability, CTLCardinality, CTLFireability
Irma.full 100.00% 39038 39038 9 StateSpace, UpperBounds, ReachabilityCardinality, ReachabilityDeadlock, ReachabilityFireability, CTLCardinality, CTLFireability, LTLCardinality, LTLFireability
Irma.struct 100.00% 39097 39097 9 StateSpace, UpperBounds, ReachabilityCardinality, ReachabilityDeadlock, ReachabilityFireability, CTLCardinality, CTLFireability, LTLCardinality, LTLFireability