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 LTSMin 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 LTSMin' 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).

LTSMin versus ITS-Tools

Some statistics are displayed below, based on 2378 runs (1189 for LTSMin 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 LTSMin to ITS-Tools are shown (you may click on one graph to enlarge it).

Statistics on the execution
  LTSMin ITS-Tools Both tools   LTSMin ITS-Tools
Computed OK 126 231 292   Smallest Memory Footprint
Do not compete 337 0 0 Times tool wins 174 475
Error detected 0 108 0   Shortest Execution Time
Cannot Compute + Time-out 107 231 327 Times tool wins 254 395


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

LTSMin versus Tapaal(PAR)

Some statistics are displayed below, based on 2378 runs (1189 for LTSMin 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 LTSMin to Tapaal(PAR) are shown (you may click on one graph to enlarge it).

Statistics on the execution
  LTSMin Tapaal(PAR) Both tools   LTSMin Tapaal(PAR)
Computed OK 235 1 183   Smallest Memory Footprint
Do not compete 0 0 337 Times tool wins 269 150
Error detected 0 2 0   Shortest Execution Time
Cannot Compute + Time-out 2 234 432 Times tool wins 276 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

LTSMin versus Marcie

Some statistics are displayed below, based on 2378 runs (1189 for LTSMin 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 LTSMin to Marcie are shown (you may click on one graph to enlarge it).

Statistics on the execution
  LTSMin Marcie Both tools   LTSMin Marcie
Computed OK 33 200 385   Smallest Memory Footprint
Do not compete 337 0 0 Times tool wins 177 441
Error detected 0 1 0   Shortest Execution Time
Cannot Compute + Time-out 90 259 344 Times tool wins 219 399


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

LTSMin versus pnmc

Some statistics are displayed below, based on 2378 runs (1189 for LTSMin 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 LTSMin to pnmc are shown (you may click on one graph to enlarge it).

Statistics on the execution
  LTSMin pnmc Both tools   LTSMin pnmc
Computed OK 22 111 396   Smallest Memory Footprint
Do not compete 0 0 337 Times tool wins 133 396
Error detected 0 4 0   Shortest Execution Time
Cannot Compute + Time-out 113 20 321 Times tool wins 140 389


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

LTSMin versus PNXDD

Some statistics are displayed below, based on 2378 runs (1189 for LTSMin 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 LTSMin to PNXDD are shown (you may click on one graph to enlarge it).

Statistics on the execution
  LTSMin PNXDD Both tools   LTSMin PNXDD
Computed OK 198 2 220   Smallest Memory Footprint
Do not compete 0 0 337 Times tool wins 249 171
Error detected 0 2 0   Shortest Execution Time
Cannot Compute + Time-out 2 196 432 Times tool wins 363 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

LTSMin versus Smart

Some statistics are displayed below, based on 2378 runs (1189 for LTSMin and 1189 for Smart, 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 LTSMin to Smart are shown (you may click on one graph to enlarge it).

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


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

LTSMin versus Tapaal(EXP)

Some statistics are displayed below, based on 2378 runs (1189 for LTSMin 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 LTSMin to Tapaal(EXP) are shown (you may click on one graph to enlarge it).

Statistics on the execution
  LTSMin Tapaal(EXP) Both tools   LTSMin Tapaal(EXP)
Computed OK 199 12 219   Smallest Memory Footprint
Do not compete 0 0 337 Times tool wins 203 227
Error detected 0 0 0   Shortest Execution Time
Cannot Compute + Time-out 12 199 422 Times tool wins 259 171


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

LTSMin versus Tapaal(SEQ)

Some statistics are displayed below, based on 2378 runs (1189 for LTSMin 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 LTSMin to Tapaal(SEQ) are shown (you may click on one graph to enlarge it).

Statistics on the execution
  LTSMin Tapaal(SEQ) Both tools   LTSMin Tapaal(SEQ)
Computed OK 215 10 203   Smallest Memory Footprint
Do not compete 0 0 337 Times tool wins 228 200
Error detected 0 1 0   Shortest Execution Time
Cannot Compute + Time-out 11 215 423 Times tool wins 270 158


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

LTSMin versus ydd-pt

Some statistics are displayed below, based on 2378 runs (1189 for LTSMin 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 LTSMin to ydd-pt are shown (you may click on one graph to enlarge it).

Statistics on the execution
  LTSMin ydd-pt Both tools   LTSMin ydd-pt
Computed OK 333 0 85   Smallest Memory Footprint
Do not compete 0 0 337 Times tool wins 350 68
Error detected 0 2 0   Shortest Execution Time
Cannot Compute + Time-out 0 331 434 Times tool wins 404 14


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