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:

• First, we list the qualified tools for the MCC'2019,
• Then, we provide some informations about the experimental conditions of the MCC'2019,
• Then, we present an access to details about results,
• Then, we provide the list of winners of the MCC'2019,
• Finally, we provide an attempt to evaluate tool reliability based on the comparison of the results provided in the contest.

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

2. List of Qualified Tools in 2019

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 2019 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).

IMPORTANT: You also have access to the archive containing all models and the corresponding formulas for 2019 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)
enPAC	P/T	Shuo Li	Tongji University, Shanghai (China)	Sequential Processing		ABSTRACTIONS EXPLICIT LTLNFBA TOPOLOGICAL
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.M	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
LoLA	P/T and colored	Karsten Wolf & Torsten Liebke	Universität Rostock	Colateral Processing		EXPLICIT SAT_SMT SEQUENTIAL_PROCESSING STATE_COMPRESSION STUBBORN_SETS SYMMETRIES TOPOLOGICAL UNFOLDING_TO_PT USE_NUPN
LTSMin	P/T	Jeroen Meijer & Tom van Dijk	University of Twente	Parallel Processing		DECISION_DIAGRAMS PARALLEL_PROCESSING 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		DECISION_DIAGRAMS EQUATIONAL_ABSTRACTION STRUCTURAL_REDUCTION 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	GlobalProperties	UpperBounds	Reachability	CTL	LTL
enPAC	EXPLICIT TOPOLOGICAL	—	—	—	—	ABSTRACTIONS LTLNFBA SEQUENTIAL TOPOLOGICAL
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	DECISION_DIAGRAMS TOPOLOGICAL UNFOLDING_TO_PT USE_NUPN	—
ITS-Tools	DECISION_DIAGRAMS TOPOLOGICAL USE_NUPN	DECISION_DIAGRAMS EXPLICIT LTSMIN PARTIAL_ORDER SAT_SMT STRUCTURAL_REDUCTION TOPOLOGICAL USE_NUPN	DECISION_DIAGRAMS TOPOLOGICAL USE_NUPN	BMC DECISION_DIAGRAMS EXPLICIT INITIAL_STATE K_INDUCTION LTSMIN PARTIAL_ORDER SAT_SMT TAUTOLOGY TOPOLOGICAL USE_NUPN	DECISION_DIAGRAMS TOPOLOGICAL USE_NUPN	DECISION_DIAGRAMS EXPLICIT LTSMIN PARTIAL_ORDER SAT_SMT TOPOLOGICAL USE_NUPN
ITS-Tools.M	DECISION_DIAGRAMS TOPOLOGICAL USE_NUPN	DECISION_DIAGRAMS EXPLICIT LTSMIN PARTIAL_ORDER SAT_SMT STRUCTURAL_REDUCTION 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 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	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	—	—	—
smart	DECISION_DIAGRAMS IMPLICIT RELATIONS	—	DECISION_DIAGRAMS	—	—	—
Tapaal	EXPLICIT STATE_COMPRESSION	EXPLICIT LP_APPROX QUERY_REDUCTION SAT_SMT SIPHON_TRAP STATE_COMPRESSION STRUCTURAL_REDUCTION STUBBORN_SETS TOPOLOGICAL TRACE_ABSTRACTION_REFINEMENT	CPN_APPROX EXPLICIT QUERY_REDUCTION SAT_SMT STATE_COMPRESSION STRUCTURAL_REDUCTION STUBBORN_SETS	CPN_APPROX EXPLICIT LP_APPROX QUERY_REDUCTION SAT_SMT STATE_COMPRESSION STRUCTURAL_REDUCTION STUBBORN_SETS 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	DECISION_DIAGRAMS EQUATIONAL_ABSTRACTION STRUCTURAL_REDUCTION UNFOLDING_TO_PT USE_NUPN	—	—	—	—	—

3. Experimental Conditions of the MCC'2019

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.

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

• Caserta was made available by colleagues at University of Twente,
• Ebro was made available by colleagues at Rostock University,
• Octoginta-2 were made available by colleagues at Université Paris Nanterre and was partially funded by LIP6,
• Quadhexa-2 were made available by colleagues at Université Paris Nanterre (used to produce formulas),
• Small is one of the two clusters at LIP6 (we got 13 nodes out of 23) Sorbonne Université.

4. The Results of the MCC’2019

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

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

You can download the full archive (2.3 GB compressed and 28 GB uncompressed) of the 91 619 runs processed to compute the results of the MCC'2019. 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:

• GlobalSummary.csv that summarizes all results from all runs in the contest (18 MB when expanded),
• raw-result-analysis.csv that contains the same data as the previous one but enriched with scoring information and the expected results (computed as a majority of tools pondered by their confidence rate, 23 MB when expanded).

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'2019

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

• State Space generation,
• GlobalProperties computation,
• UpperBounds computation,
• Reachability Formulas (ReachabilityCardinality, ReachabilityFireability),
• CTL Formulas (CTLCardinality, CTLFireability),
• LTL Formulas (LTLCardinality, LTLFireability),

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:

• ×1 for «Known» models,
• ×4 for «Surprise» models.

5.1. Winners in the StateSpace Category

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

• TINA.tedd ranked first (8 232 pts),
Fastest-Tool
• GreatSPN ranked second (7 702),
• ITS-Tools ranked third (5 973 pts, ITS-Tools.M collected 5 478 pts).

Then, tools rank in the following order: LSMin (4 714 pts), smart (4 248 pts), Tapaal (2 493 pts) and enPac (84 pts). The Golf-medal of 2018 collected 8 767 pts. BVS (Best Virtual Score tool) collected 8767 points.

TINA.tedd got the Fastest-Tool and no tool this year could neat the 2018 gold medal for the Memory Footprint awards.

TINA.tedd (fastest 202 times) 2018-Gold (less memory 251 times)

Note that all the variants of ITA-Tools 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»
enPAC	78.31%	65	83
LTSMin	100%	1086	1086
Tapaal	100.00%	645	645
ITS-Tools	100.00%	1482	1482
ITS-Tools.M	100.00%	1373	1373
GreatSPN	100.00%	2260	2260
smart	100.00%	1212	1212
TINA.tedd	100%	2284	2284
2018-Gold	100%	2129	2129

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

5.2. Winners in the GlobalProperties Category

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

• Tapaal ranked first (10 105 pts),
• ITS-Tools ranked second (9 733 pts),
• LoLA ranked third (8 285 pts, ITS-Tools.M collected 9 696 points).

Then, tools rank in the following order: GreatSPN (6 181 pts). This is a new examination so there was no Gold medal provided last year. BVS (Best Virtual Score tool) collected 11 648 points.

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

Tapaal (fastest 768 times) Tapaal (less memory 774 times)

Estimated Tool Confidence rate for GlobalPropertiesScores (based on the «significant values» computed by tools) see section 6. for details
Tool name	Reliability	Correct Values	«significant values»
Tapaal	100.00%	719	719
LoLA	100.00%	620	620
ITS-Tools	100.00%	728	728
ITS-Tools.M	100.00%	739	739
GreatSPN	100.00%	438	438

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

5.3. Winners in the UpperBounds Category

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

• Tapaal ranked first (11 554 pts),
• LoLA ranked second (10 612 pts),
• ITS-Tools.M ranked third (7 404 pts, ITS-Tools collected 6 793 pts).

Then, tools rank in the following order: GreatSPN (7 280 pts), LTSMin (5 616 pts), and smart (5 098 pts). The Gold-medal of 2018 collected 10 562 pts. BVS (Best Virtual Score tool) collected 11 812 points.

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

2018-Gold (fastest 460 times) 2018-Gold (less memory 385 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%	6267	6267
Tapaal	100.00%	13156	13156
LoLA	100.00%	12575	12575
ITS-Tools	100.00%	8048	8048
ITS-Tools.M	99.90%	8760	8769
GreatSPN	100.00%	8936	8936
smart	100.00%	5513	5513
Golf-2018	100.00%	12547	12547

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

5.4. Winners in the Reachability Formulas Category

5 tools out of 9 participated in these examinations (ReachabilityCardinality and ReachabilityFireability). Results based on the scoring shown below is:

• Tapaal ranked first (23 887 pts),
• LoLA ranked second (22 227 pts),
• ITS-Tools ranked third (16 809 pts, ITS-Tools.M collected 16 130 pts).

Then, tools rank in the following order: GreatSPN (9 350 pts). The Gold-medal of 2018 collected 23 714 pts. BVS (Best Virtual Score tool) collected 24 823 points.

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

2018-Gold (fastest 679 times) 2018-Gold (less memory 976 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»
Tapaal	100.00%	28370	28370
LoLA	99.98%	26915	26918
ITS-Tools	100.00%	20072	20072
ITS-Tools.M	99.97%	18784	18789
GreatSPN	100.00%	10546	10546
2018-Gold	100.00%	28377	28377

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

5.5. Winners in the CTL Formulas Category

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

• Tapaal ranked first (21 322 pts),
• LoLA ranked second (18 971 pts),
• ITS-Tools.M ranked third (10 895 pts, ITS-Tools collected 10 012 pts).

Then, tools rank in the following order: GreatSPN (9 402 pts). The Gold-medal of 2018 collected 21 244 pts. BVS (Best Virtual Score tool) collected 22 365 points.

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

GreatSPN (fastest 368 times) GreatSPN (less memory 348 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»
Tapaal	99,99%	23572	23573
LoLA	99,99%	12751	12756
ITS-Tools	100.00%	11044	11044
ITS-Tools.M	99.99%	11829	11832
GreatSPN	100.00%	10345	10345
2018-Gold	99,97%	23566	23573

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

5.6. Winners in the LTL Formulas Category

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

• LoLA ranked first (22 634 pts),
• ITS-Tools ranked second (18 424 pts, ITS-Tools.M collected 17 102 pt),
• enPAC ranked third (842 pts).

The Gold-medal of 2018 collected 23 154 pts. BVS (Best Virtual Score tool) collected 23 770 points.

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

2018-Gold (fastest 965 times) 2018-Gold (less memory 1 076 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»
enPAC	85.87%	2248	2618
LoLA	99.99%	22163	22164
ITS-Tools	100.00%	21800	21800
ITS-Tools.M	100.00%	20073	20073
2018-Gold	99.98%	22303	22306

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
enPAC	85.63%	2313	2701	3 StateSpace, LTLCardinality, LTLFireability
GreatSPN	100.00%	32525	32525	7 StateSpace, GlobalProperties, UpperBounds, ReachabilityCardinality, ReachabilityFireability, CTLCardinality, CTLFireability
smart	100.00%	6725	6725	2 StateSpace, UpperBounds
TINA.tedd	100.00%	2284	2284	1 StateSpace
ITS-Tools	100.00%	63174	63174	9 StateSpace, GlobalProperties, UpperBounds, ReachabilityCardinality, ReachabilityFireability, CTLCardinality, CTLFireability, LTLCardinality, LTLFireability
ITS-Tools.M	99.95%	61585	61585	9 StateSpace, GlobalProperties, UpperBounds, ReachabilityCardinality, ReachabilityFireability, CTLCardinality, CTLFireability, LTLCardinality, LTLFireability
LoLA	99.99%	85034	85039	8 GlobalProperties, UpperBounds, ReachabilityCardinality, ReachabilityFireability, CTLCardinality, CTLFireability, LTLCardinality, LTLFireability
LTSMin	100.00%	1086	1086	2 StateSpace, UpperBounds
Tapaal	100.00%	66462	66462	7 StateSpace, GlobalProperties, UpperBounds, ReachabilityCardinality, ReachabilityFireability, CTLCardinality, CTLFireability
2018-Gold	99.99%	88922	88926	7 StateSpace, GlobalProperties, UpperBounds, ReachabilityCardinality, ReachabilityFireability, CTLCardinality, CTLFireability