fond
Model Checking Contest @ Petri Nets 2015
Bruxelles, Belgium, June 23, 2015
GreatSPN-Meddly compared to other tools («Known» models, ReachabilityFireabilitySimple)
Last Updated
August 19, 2015

Introduction

This page presents how GreatSPN-Meddly do cope efficiently with the ReachabilityFireabilitySimple examination face to the other participating tools. In this page, we consider «Known» 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 GreatSPN-Meddly' 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).

GreatSPN-Meddly versus Cunf

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

Statistics on the execution
  GreatSPN-Meddly Cunf Both tools   GreatSPN-Meddly Cunf
Computed OK 42 60 15   Smallest Memory Footprint
Do not compete 0 163 114 Times tool wins 42 75
Error detected 82 0 1   Shortest Execution Time
Cannot Compute + Time-out 105 6 45 Times tool wins 42 75


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

GreatSPN-Meddly versus ITS-Tools

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

Statistics on the execution
  GreatSPN-Meddly ITS-Tools Both tools   GreatSPN-Meddly ITS-Tools
Computed OK 5 168 52   Smallest Memory Footprint
Do not compete 114 0 0 Times tool wins 43 182
Error detected 81 5 2   Shortest Execution Time
Cannot Compute + Time-out 80 107 70 Times tool wins 24 201


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

GreatSPN-Meddly versus LoLA2.0

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

Statistics on the execution
  GreatSPN-Meddly LoLA2.0 Both tools   GreatSPN-Meddly LoLA2.0
Computed OK 0 208 57   Smallest Memory Footprint
Do not compete 0 23 114 Times tool wins 1 264
Error detected 82 1 1   Shortest Execution Time
Cannot Compute + Time-out 150 0 0 Times tool wins 2 263


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

GreatSPN-Meddly versus LTSMin

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

Statistics on the execution
  GreatSPN-Meddly LTSMin Both tools   GreatSPN-Meddly LTSMin
Computed OK 1 203 56   Smallest Memory Footprint
Do not compete 114 0 0 Times tool wins 45 215
Error detected 78 1 5   Shortest Execution Time
Cannot Compute + Time-out 125 114 25 Times tool wins 38 222


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

GreatSPN-Meddly versus Marcie

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

Statistics on the execution
  GreatSPN-Meddly Marcie Both tools   GreatSPN-Meddly Marcie
Computed OK 6 117 51   Smallest Memory Footprint
Do not compete 114 0 0 Times tool wins 56 118
Error detected 83 0 0   Shortest Execution Time
Cannot Compute + Time-out 45 131 105 Times tool wins 39 135


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

GreatSPN-Meddly versus TAPAAL(MC)

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

Statistics on the execution
  GreatSPN-Meddly TAPAAL(MC) Both tools   GreatSPN-Meddly TAPAAL(MC)
Computed OK 2 183 55   Smallest Memory Footprint
Do not compete 0 23 114 Times tool wins 15 225
Error detected 83 1 0   Shortest Execution Time
Cannot Compute + Time-out 128 6 22 Times tool wins 12 228


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

GreatSPN-Meddly versus TAPAAL(SEQ)

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

Statistics on the execution
  GreatSPN-Meddly TAPAAL(SEQ) Both tools   GreatSPN-Meddly TAPAAL(SEQ)
Computed OK 0 204 57   Smallest Memory Footprint
Do not compete 0 23 114 Times tool wins 9 252
Error detected 83 0 0   Shortest Execution Time
Cannot Compute + Time-out 144 0 6 Times tool wins 14 247


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

GreatSPN-Meddly versus TAPAAL-OTF(PAR)

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

Statistics on the execution
  GreatSPN-Meddly TAPAAL-OTF(PAR) Both tools   GreatSPN-Meddly TAPAAL-OTF(PAR)
Computed OK 10 75 47   Smallest Memory Footprint
Do not compete 0 23 114 Times tool wins 29 103
Error detected 83 7 0   Shortest Execution Time
Cannot Compute + Time-out 58 46 92 Times tool wins 19 113


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

GreatSPN-Meddly versus TAPAAL-OTF(SEQ)

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

Statistics on the execution
  GreatSPN-Meddly TAPAAL-OTF(SEQ) Both tools   GreatSPN-Meddly TAPAAL-OTF(SEQ)
Computed OK 13 104 44   Smallest Memory Footprint
Do not compete 0 23 114 Times tool wins 30 131
Error detected 83 0 0   Shortest Execution Time
Cannot Compute + Time-out 82 51 68 Times tool wins 19 142


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