fond
Model Checking Contest 2024
14th edition, Geneva, Switzerland, June 25, 2024
NoHD compared to other tools («All» models, StateSpace)
Last Updated
July 7, 2024

Introduction

This page presents how NoHD do cope efficiently with the StateSpace examination face to the other participating tools. In this page, we consider «All» models.

The next sections will show chart comparing performances in terms of both memory and execution time.The x-axis corresponds to the challenging tool where the y-axes represents NoHD' performances. Thus, points below the diagonal of a chart denote comparisons favorables to the tool while others corresponds to situations where the challenging tool performs better.

You might also find plots out of the range that denote the case were at least one tool could not answer appropriately (error, time-out, could not compute or did not competed).

NoHD versus GreatSPN+red

Some statistics are displayed below, based on 3564 runs (1782 for NoHD and 1782 for GreatSPN+red, so there are 1782 plots on each of the two charts). Each execution was allowed 1 hour and 16 GByte of memory. Then performance charts comparing NoHD to GreatSPN+red are shown (you may click on one graph to enlarge it).

Statistics on the executions
  NoHD GreatSPN+red Both tools   NoHD GreatSPN+red
All computed OK 160 572 356   Smallest Memory Footprint
NoHD = GreatSPN+red 2 Times tool wins 227 1017
NoHD > GreatSPN+red 0   Shortest Execution Time
NoHD < GreatSPN+red 154 Times tool wins 228 1016
Do not compete 0 0 0
Error detected 0 3 0  
Cannot Compute + Time-out 574 159 536


On the chart below, denote cases where the two tools did computed all results without error, denote cases where the two tool did computed the same number of values (but not al values in the examination), denote cases where NoHD computed more values than GreatSPN+red, denote cases where NoHD computed less values than GreatSPN+red, denote the cases where at least one tool did not competed, denote the cases where at least one tool computed a bad value and denote the cases where at least one tool stated it could not compute a result or timed-out.

NoHD wins when points are below the diagonal, GreatSPN+red wins when points are above the diagonal.

memory chart time chart

NoHD versus ITS-Tools

Some statistics are displayed below, based on 3564 runs (1782 for NoHD and 1782 for ITS-Tools, so there are 1782 plots on each of the two charts). Each execution was allowed 1 hour and 16 GByte of memory. Then performance charts comparing NoHD to ITS-Tools are shown (you may click on one graph to enlarge it).

Statistics on the executions
  NoHD ITS-Tools Both tools   NoHD ITS-Tools
All computed OK 155 511 0   Smallest Memory Footprint
NoHD = ITS-Tools 1 Times tool wins 246 937
NoHD > ITS-Tools 348   Shortest Execution Time
NoHD < ITS-Tools 168 Times tool wins 305 878
Do not compete 0 0 0
Error detected 0 0 0  
Cannot Compute + Time-out 511 155 599


On the chart below, denote cases where the two tools did computed all results without error, denote cases where the two tool did computed the same number of values (but not al values in the examination), denote cases where NoHD computed more values than ITS-Tools, denote cases where NoHD computed less values than ITS-Tools, denote the cases where at least one tool did not competed, denote the cases where at least one tool computed a bad value and denote the cases where at least one tool stated it could not compute a result or timed-out.

NoHD wins when points are below the diagonal, ITS-Tools wins when points are above the diagonal.

memory chart time chart

NoHD versus tedd

Some statistics are displayed below, based on 3564 runs (1782 for NoHD and 1782 for tedd, so there are 1782 plots on each of the two charts). Each execution was allowed 1 hour and 16 GByte of memory. Then performance charts comparing NoHD to tedd are shown (you may click on one graph to enlarge it).

Statistics on the executions
  NoHD tedd Both tools   NoHD tedd
All computed OK 124 694 370   Smallest Memory Footprint
NoHD = tedd 0 Times tool wins 265 1101
NoHD > tedd 0   Shortest Execution Time
NoHD < tedd 178 Times tool wins 162 1204
Do not compete 0 0 0
Error detected 0 0 0  
Cannot Compute + Time-out 694 124 416


On the chart below, denote cases where the two tools did computed all results without error, denote cases where the two tool did computed the same number of values (but not al values in the examination), denote cases where NoHD computed more values than tedd, denote cases where NoHD computed less values than tedd, denote the cases where at least one tool did not competed, denote the cases where at least one tool computed a bad value and denote the cases where at least one tool stated it could not compute a result or timed-out.

NoHD wins when points are below the diagonal, tedd wins when points are above the diagonal.

memory chart time chart

NoHD versus 2023-gold

Some statistics are displayed below, based on 3564 runs (1782 for NoHD and 1782 for 2023-gold, so there are 1782 plots on each of the two charts). Each execution was allowed 1 hour and 16 GByte of memory. Then performance charts comparing NoHD to 2023-gold are shown (you may click on one graph to enlarge it).

Statistics on the executions
  NoHD 2023-gold Both tools   NoHD 2023-gold
All computed OK 124 693 370   Smallest Memory Footprint
NoHD = 2023-gold 0 Times tool wins 264 1101
NoHD > 2023-gold 0   Shortest Execution Time
NoHD < 2023-gold 178 Times tool wins 169 1196
Do not compete 0 0 0
Error detected 0 0 0  
Cannot Compute + Time-out 693 124 417


On the chart below, denote cases where the two tools did computed all results without error, denote cases where the two tool did computed the same number of values (but not al values in the examination), denote cases where NoHD computed more values than 2023-gold, denote cases where NoHD computed less values than 2023-gold, denote the cases where at least one tool did not competed, denote the cases where at least one tool computed a bad value and denote the cases where at least one tool stated it could not compute a result or timed-out.

NoHD wins when points are below the diagonal, 2023-gold wins when points are above the diagonal.

memory chart time chart

NoHD versus BVT-2024

Some statistics are displayed below, based on 3564 runs (1782 for NoHD and 1782 for BVT-2024, so there are 1782 plots on each of the two charts). Each execution was allowed 1 hour and 16 GByte of memory. Then performance charts comparing NoHD to BVT-2024 are shown (you may click on one graph to enlarge it).

Important: here, NoHD is compared to BVT-2024. It is a good way to check how NoHD compete in terms of resource consomption with the best tools (even virtual). When NoHD is best, the corresponding plots are on the diagonal of the scatter plots chart.

Statistics on the executions
  NoHD BVT-2024 Both tools   NoHD BVT-2024
All computed OK 0 708 371   Smallest Memory Footprint
NoHD = BVT-2024 113 Times tool wins 0 1379
NoHD > BVT-2024 0   Shortest Execution Time
NoHD < BVT-2024 187 Times tool wins 0 1379
Do not compete 0 402 0
Error detected 0 0 0  
Cannot Compute + Time-out 1110 0 0


On the chart below, denote cases where the two tools did computed all results without error, denote cases where the two tool did computed the same number of values (but not al values in the examination), denote cases where NoHD computed more values than BVT-2024, denote cases where NoHD computed less values than BVT-2024, denote the cases where at least one tool did not competed, denote the cases where at least one tool computed a bad value and denote the cases where at least one tool stated it could not compute a result or timed-out.

NoHD wins when points are below the diagonal, BVT-2024 wins when points are above the diagonal.

memory chart time chart

NoHD versus GreatSPN

Some statistics are displayed below, based on 3564 runs (1782 for NoHD and 1782 for GreatSPN, so there are 1782 plots on each of the two charts). Each execution was allowed 1 hour and 16 GByte of memory. Then performance charts comparing NoHD to GreatSPN are shown (you may click on one graph to enlarge it).

Statistics on the executions
  NoHD GreatSPN Both tools   NoHD GreatSPN
All computed OK 164 580 356   Smallest Memory Footprint
NoHD = GreatSPN 2 Times tool wins 202 1050
NoHD > GreatSPN 0   Shortest Execution Time
NoHD < GreatSPN 150 Times tool wins 170 1082
Do not compete 0 0 0
Error detected 0 3 0  
Cannot Compute + Time-out 582 163 528


On the chart below, denote cases where the two tools did computed all results without error, denote cases where the two tool did computed the same number of values (but not al values in the examination), denote cases where NoHD computed more values than GreatSPN, denote cases where NoHD computed less values than GreatSPN, denote the cases where at least one tool did not competed, denote the cases where at least one tool computed a bad value and denote the cases where at least one tool stated it could not compute a result or timed-out.

NoHD wins when points are below the diagonal, GreatSPN wins when points are above the diagonal.

memory chart time chart