fond
Model Checking Contest @ Petri Nets 2015
Bruxelles, Belgium, June 23, 2015
ITS-Tools compared to other tools («All» models, ReachabilityFireability)
Last Updated
August 19, 2015

Introduction

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

The next sections will show chart comparing performances in termsof both memory and execution time.The x-axis corresponds to the challenging tool where the y-axes represents ITS-Tools' performances. Thus, points below the diagonal of a chart denote comparisons favorables to the tool whileothers 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).

ITS-Tools versus Cunf

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

Statistics on the execution
  ITS-Tools Cunf Both tools   ITS-Tools Cunf
Computed OK 402 103 49   Smallest Memory Footprint
Do not compete 0 652 0 Times tool wins 412 142
Error detected 273 4 3   Shortest Execution Time
Cannot Compute + Time-out 165 81 37 Times tool wins 414 140


On the chart below, denote cases where the two tools did computed a result, denote the cases where at least one tool did not competed, denote the cases where at least one tool did a mistake and denote the cases where at least one tool stated it could not compute a result or timed-out.

memory chart time chart

ITS-Tools versus GreatSPN-Meddly

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

Statistics on the execution
  ITS-Tools GreatSPN-Meddly Both tools   ITS-Tools GreatSPN-Meddly
Computed OK 424 58 27   Smallest Memory Footprint
Do not compete 0 228 0 Times tool wins 428 81
Error detected 146 94 130   Shortest Execution Time
Cannot Compute + Time-out 107 297 95 Times tool wins 444 65


On the chart below, denote cases where the two tools did computed a result, denote the cases where at least one tool did not competed, denote the cases where at least one tool did a mistake and denote the cases where at least one tool stated it could not compute a result or timed-out.

memory chart time chart

ITS-Tools versus LoLA2.0

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

Statistics on the execution
  ITS-Tools LoLA2.0 Both tools   ITS-Tools LoLA2.0
Computed OK 206 366 245   Smallest Memory Footprint
Do not compete 0 301 0 Times tool wins 259 558
Error detected 272 6 4   Shortest Execution Time
Cannot Compute + Time-out 196 1 6 Times tool wins 313 504


On the chart below, denote cases where the two tools did computed a result, denote the cases where at least one tool did not competed, denote the cases where at least one tool did a mistake and denote the cases where at least one tool stated it could not compute a result or timed-out.

memory chart time chart

ITS-Tools versus LTSMin

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

Statistics on the execution
  ITS-Tools LTSMin Both tools   ITS-Tools LTSMin
Computed OK 203 360 248   Smallest Memory Footprint
Do not compete 0 0 0 Times tool wins 327 484
Error detected 262 2 14   Shortest Execution Time
Cannot Compute + Time-out 104 207 98 Times tool wins 400 411


On the chart below, denote cases where the two tools did computed a result, denote the cases where at least one tool did not competed, denote the cases where at least one tool did a mistake and denote the cases where at least one tool stated it could not compute a result or timed-out.

memory chart time chart

ITS-Tools versus Marcie

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

Statistics on the execution
  ITS-Tools Marcie Both tools   ITS-Tools Marcie
Computed OK 287 241 164   Smallest Memory Footprint
Do not compete 0 0 0 Times tool wins 443 249
Error detected 275 0 1   Shortest Execution Time
Cannot Compute + Time-out 40 361 162 Times tool wins 406 286


On the chart below, denote cases where the two tools did computed a result, denote the cases where at least one tool did not competed, denote the cases where at least one tool did a mistake and denote the cases where at least one tool stated it could not compute a result or timed-out.

memory chart time chart

ITS-Tools versus TAPAAL(MC)

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

Statistics on the execution
  ITS-Tools TAPAAL(MC) Both tools   ITS-Tools TAPAAL(MC)
Computed OK 227 332 224   Smallest Memory Footprint
Do not compete 0 301 0 Times tool wins 321 462
Error detected 273 12 3   Shortest Execution Time
Cannot Compute + Time-out 171 26 31 Times tool wins 352 431


On the chart below, denote cases where the two tools did computed a result, denote the cases where at least one tool did not competed, denote the cases where at least one tool did a mistake and denote the cases where at least one tool stated it could not compute a result or timed-out.

memory chart time chart

ITS-Tools versus TAPAAL(SEQ)

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

Statistics on the execution
  ITS-Tools TAPAAL(SEQ) Both tools   ITS-Tools TAPAAL(SEQ)
Computed OK 199 362 252   Smallest Memory Footprint
Do not compete 0 301 0 Times tool wins 284 529
Error detected 274 0 2   Shortest Execution Time
Cannot Compute + Time-out 190 0 12 Times tool wins 368 445


On the chart below, denote cases where the two tools did computed a result, denote the cases where at least one tool did not competed, denote the cases where at least one tool did a mistake and denote the cases where at least one tool stated it could not compute a result or timed-out.

memory chart time chart

ITS-Tools versus TAPAAL-OTF(PAR)

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

Statistics on the execution
  ITS-Tools TAPAAL-OTF(PAR) Both tools   ITS-Tools TAPAAL-OTF(PAR)
Computed OK 420 139 31   Smallest Memory Footprint
Do not compete 0 301 0 Times tool wins 433 157
Error detected 247 11 29   Shortest Execution Time
Cannot Compute + Time-out 109 325 93 Times tool wins 435 155


On the chart below, denote cases where the two tools did computed a result, denote the cases where at least one tool did not competed, denote the cases where at least one tool did a mistake and denote the cases where at least one tool stated it could not compute a result or timed-out.

memory chart time chart

ITS-Tools versus TAPAAL-OTF(SEQ)

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

Statistics on the execution
  ITS-Tools TAPAAL-OTF(SEQ) Both tools   ITS-Tools TAPAAL-OTF(SEQ)
Computed OK 374 235 77   Smallest Memory Footprint
Do not compete 0 301 0 Times tool wins 422 264
Error detected 276 2 0   Shortest Execution Time
Cannot Compute + Time-out 128 240 74 Times tool wins 432 254


On the chart below, denote cases where the two tools did computed a result, denote the cases where at least one tool did not competed, denote the cases where at least one tool did a mistake and denote the cases where at least one tool stated it could not compute a result or timed-out.

memory chart time chart