fond
Model Checking Contest @ Petri Nets 2016
6th edition, Toruń, Poland, June 21, 2016
ITS-Tools compared to other tools («All» models, StateSpace)
Last Updated
June 30, 2016

Introduction

This page presents how Smart 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 termsof both memory and execution time.The x-axis corresponds to the challenging tool where the y-axes represents Smart' 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).

Smart versus ITS-Tools

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

Statistics on the execution
  Smart ITS-Tools Both tools   Smart ITS-Tools
Computed OK 48 314 209   Smallest Memory Footprint
Do not compete 337 0 0 Times tool wins 229 342
Error detected 0 102 6   Shortest Execution Time
Cannot Compute + Time-out 256 225 333 Times tool wins 209 362


On the chart below, denote cases where the two tools did computed a result without error, 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.

memory chart time chart

Smart versus LTSMin

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

Statistics on the execution
  Smart LTSMin Both tools   Smart LTSMin
Computed OK 60 221 197   Smallest Memory Footprint
Do not compete 0 0 337 Times tool wins 250 228
Error detected 6 0 0   Shortest Execution Time
Cannot Compute + Time-out 215 60 374 Times tool wins 218 260


On the chart below, denote cases where the two tools did computed a result without error, 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.

memory chart time chart

Smart versus Tapaal(PAR)

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

Statistics on the execution
  Smart Tapaal(PAR) Both tools   Smart Tapaal(PAR)
Computed OK 165 92 92   Smallest Memory Footprint
Do not compete 0 0 337 Times tool wins 242 107
Error detected 6 2 0   Shortest Execution Time
Cannot Compute + Time-out 89 166 500 Times tool wins 206 143


On the chart below, denote cases where the two tools did computed a result without error, 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.

memory chart time chart

Smart versus Marcie

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

Statistics on the execution
  Smart Marcie Both tools   Smart Marcie
Computed OK 26 354 231   Smallest Memory Footprint
Do not compete 337 0 0 Times tool wins 251 360
Error detected 6 1 0   Shortest Execution Time
Cannot Compute + Time-out 238 252 351 Times tool wins 220 391


On the chart below, denote cases where the two tools did computed a result without error, 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.

memory chart time chart

Smart versus pnmc

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

Statistics on the execution
  Smart pnmc Both tools   Smart pnmc
Computed OK 15 265 242   Smallest Memory Footprint
Do not compete 0 0 337 Times tool wins 243 279
Error detected 6 4 0   Shortest Execution Time
Cannot Compute + Time-out 263 15 326 Times tool wins 170 352


On the chart below, denote cases where the two tools did computed a result without error, 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.

memory chart time chart

Smart versus PNXDD

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

Statistics on the execution
  Smart PNXDD Both tools   Smart PNXDD
Computed OK 134 99 123   Smallest Memory Footprint
Do not compete 0 0 337 Times tool wins 251 105
Error detected 6 2 0   Shortest Execution Time
Cannot Compute + Time-out 95 134 494 Times tool wins 254 102


On the chart below, denote cases where the two tools did computed a result without error, 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.

memory chart time chart

Smart versus Tapaal(EXP)

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

Statistics on the execution
  Smart Tapaal(EXP) Both tools   Smart Tapaal(EXP)
Computed OK 152 126 105   Smallest Memory Footprint
Do not compete 0 0 337 Times tool wins 195 188
Error detected 6 0 0   Shortest Execution Time
Cannot Compute + Time-out 122 154 467 Times tool wins 194 189


On the chart below, denote cases where the two tools did computed a result without error, 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.

memory chart time chart

Smart versus Tapaal(SEQ)

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

Statistics on the execution
  Smart Tapaal(SEQ) Both tools   Smart Tapaal(SEQ)
Computed OK 160 116 97   Smallest Memory Footprint
Do not compete 0 0 337 Times tool wins 204 169
Error detected 6 1 0   Shortest Execution Time
Cannot Compute + Time-out 113 162 476 Times tool wins 190 183


On the chart below, denote cases where the two tools did computed a result without error, 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.

memory chart time chart

Smart versus ydd-pt

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

Statistics on the execution
  Smart ydd-pt Both tools   Smart ydd-pt
Computed OK 215 43 42   Smallest Memory Footprint
Do not compete 0 0 337 Times tool wins 234 66
Error detected 6 2 0   Shortest Execution Time
Cannot Compute + Time-out 39 215 550 Times tool wins 243 57


On the chart below, denote cases where the two tools did computed a result without error, 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.

memory chart time chart