fond
Model Checking Contest @ Petri Nets 2013
Milano, Italy, June 25, 2013
Scores for the ReachabilityDeadlock Examination
Last Updated
Apr. 26, 2013

Please find enclosed the scores for the ReachabilityDeadlock examination. We display only the score of tools that provide a results for at least one instance of one model. The total is first listed in the table below followed by a detail, for each proposed model. You may access the corresponding result page here

Meaning of the line labels are:

For known, a tool may collect up to 411 points.

Total Score of the tools
  cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
Global Score 98 48 52 216 216 202 185 116 251
CSRepetitions (Colored)
  cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
1st instance 0 0 1 0 0 0 0 0 0
instances 0 0 2 0 0 0 0 0 0
max reached 0 0 0 0 0 0 0 0 0
best 0 0 2 0 0 0 0 0 0
subtotal 0 0 5 0 0 0 0 0 0
CSRepetitions (P/T)
  cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
1st instance 1 1 0 1 1 1 1 1 1
instances 2 3 0 6 6 6 6 2 6
max reached 0 0 0 2 2 2 2 0 2
best 0 0 0 2 2 2 2 0 2
subtotal 3 4 0 11 11 11 11 3 11
Dekker (P/T)
  cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
1st instance 1 0 0 1 1 1 1 1 1
instances 5 0 0 3 3 3 2 3 6
max reached 0 0 0 0 0 0 0 0 2
best 0 0 0 0 0 0 0 0 2
subtotal 6 0 0 4 4 4 3 4 11
DotAndBoxes (Colored)
  cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
1st instance 0 0 1 0 0 0 0 0 0
instances 0 0 3 0 0 0 0 0 0
max reached 0 0 0 0 0 0 0 0 0
best 0 0 2 0 0 0 0 0 0
subtotal 0 0 6 0 0 0 0 0 0
DrinkVendingMachine (Colored)
  cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
1st instance 0 0 1 0 0 0 0 0 0
instances 0 0 2 0 0 0 0 0 0
max reached 0 0 2 0 0 0 0 0 0
best 0 0 2 0 0 0 0 0 0
subtotal 0 0 7 0 0 0 0 0 0
DrinkVendingMachine (P/T)
  cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
1st instance 1 0 0 1 1 1 1 1 1
instances 1 0 0 2 2 2 2 2 2
max reached 0 0 0 2 2 2 2 2 2
best 0 0 0 2 2 2 2 2 2
subtotal 2 0 0 7 7 7 7 7 7
Echo (P/T)
  cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
1st instance 0 0 0 1 1 1 1 0 1
instances 0 0 0 9 9 9 9 0 9
max reached 0 0 0 2 2 2 2 0 2
best 0 0 0 2 2 2 2 0 2
subtotal 0 0 0 14 14 14 14 0 14
Eratosthenes (P/T)
  cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
1st instance 1 0 0 1 1 1 1 1 1
instances 5 0 0 6 6 6 5 6 6
max reached 0 0 0 2 2 2 0 2 2
best 0 0 0 2 2 2 0 2 2
subtotal 6 0 0 11 11 11 6 11 11
FMS (P/T)
  cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
1st instance 0 1 0 1 1 1 1 1 1
instances 0 6 0 8 8 8 8 6 8
max reached 0 0 0 2 2 2 2 0 2
best 0 0 0 2 2 2 2 0 2
subtotal 0 7 0 13 13 13 13 7 13
GlobalRessAlloc (Colored)
  cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
1st instance 0 0 1 0 0 0 0 0 0
instances 0 0 3 0 0 0 0 0 0
max reached 0 0 0 0 0 0 0 0 0
best 0 0 2 0 0 0 0 0 0
subtotal 0 0 6 0 0 0 0 0 0
GlobalRessAlloc (P/T)
  cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
1st instance 1 1 0 1 1 1 1 1 1
instances 1 1 0 1 1 1 2 1 2
max reached 0 0 0 0 0 0 2 0 2
best 0 0 0 0 0 0 2 0 2
subtotal 2 2 0 2 2 2 7 2 7
Kanban (P/T)
  cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
1st instance 0 1 0 1 1 1 1 1 1
instances 0 7 0 8 8 8 8 5 8
max reached 0 0 0 2 2 2 2 0 2
best 0 0 0 2 2 2 2 0 2
subtotal 0 8 0 13 13 13 13 6 13
LamportFastMutEx (Colored)
  cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
1st instance 0 0 1 0 0 0 0 0 0
instances 0 0 4 0 0 0 0 0 0
max reached 0 0 0 0 0 0 0 0 0
best 0 0 2 0 0 0 0 0 0
subtotal 0 0 7 0 0 0 0 0 0
LamportFastMutEx (P/T)
  cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
1st instance 1 0 0 1 1 1 1 1 1
instances 3 0 0 6 6 3 4 3 7
max reached 0 0 0 0 0 0 0 0 2
best 0 0 0 0 0 0 0 0 2
subtotal 4 0 0 7 7 4 5 4 12
MAPK (P/T)
  cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
1st instance 0 1 0 1 1 1 1 1 1
instances 0 3 0 6 6 6 3 4 6
max reached 0 0 0 2 2 2 0 0 2
best 0 0 0 2 2 2 0 0 2
subtotal 0 4 0 11 11 11 4 5 11
NeoElection (Colored)
  cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
1st instance 0 0 1 0 0 0 0 0 0
instances 0 0 3 0 0 0 0 0 0
max reached 0 0 0 0 0 0 0 0 0
best 0 0 2 0 0 0 0 0 0
subtotal 0 0 6 0 0 0 0 0 0
NeoElection (P/T)
  cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
1st instance 1 0 0 1 1 1 1 1 1
instances 2 0 0 7 7 7 7 2 7
max reached 0 0 0 2 2 2 2 0 2
best 0 0 0 2 2 2 2 0 2
subtotal 3 0 0 12 12 12 12 3 12
PermAdmissibility (Colored)
  cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
1st instance 0 0 1 0 0 0 0 0 0
instances 0 0 1 0 0 0 0 0 0
max reached 0 0 0 0 0 0 0 0 0
best 0 0 2 0 0 0 0 0 0
subtotal 0 0 4 0 0 0 0 0 0
PermAdmissibility (P/T)
  cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
1st instance 1 1 0 1 1 1 1 1 1
instances 1 6 0 6 6 6 6 1 6
max reached 0 2 0 2 2 2 2 0 2
best 0 2 0 2 2 2 2 0 2
subtotal 2 11 0 11 11 11 11 2 11
Peterson (Colored)
  cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
1st instance 0 0 1 0 0 0 0 0 0
instances 0 0 2 0 0 0 0 0 0
max reached 0 0 0 0 0 0 0 0 0
best 0 0 2 0 0 0 0 0 0
subtotal 0 0 5 0 0 0 0 0 0
Peterson (P/T)
  cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
1st instance 1 0 0 1 1 1 1 1 1
instances 2 0 0 6 6 3 4 2 6
max reached 0 0 0 2 2 0 2 0 2
best 0 0 0 2 2 0 2 0 2
subtotal 3 0 0 11 11 4 9 3 11
Philosophers (Colored)
  cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
1st instance 0 0 0 0 0 0 0 0 0
instances 0 0 0 0 0 0 0 0 0
max reached 0 0 0 0 0 0 0 0 0
best 0 0 0 0 0 0 0 0 0
subtotal 0 0 0 0 0 0 0 0 0
Philosophers (P/T)
  cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
1st instance 1 1 0 1 1 1 1 1 1
instances 9 4 0 11 11 11 6 8 11
max reached 0 0 0 2 2 2 0 0 2
best 0 0 0 2 2 2 0 0 2
subtotal 10 5 0 16 16 16 7 9 16
PhilosophersDyn (Colored)
  cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
1st instance 0 0 0 0 0 0 0 0 0
instances 0 0 0 0 0 0 0 0 0
max reached 0 0 0 0 0 0 0 0 0
best 0 0 0 0 0 0 0 0 0
subtotal 0 0 0 0 0 0 0 0 0
PhilosophersDyn (P/T)
  cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
1st instance 0 1 0 1 1 1 1 1 1
instances 0 1 0 3 3 3 3 1 3
max reached 0 0 0 2 2 2 2 0 2
best 0 0 0 2 2 2 2 0 2
subtotal 0 2 0 8 8 8 8 2 8
Planning (P/T)
  cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
1st instance 0 0 0 0 0 0 0 0 0
instances 0 0 0 0 0 0 0 0 0
max reached 0 0 0 0 0 0 0 0 0
best 0 0 0 0 0 0 0 0 0
subtotal 0 0 0 0 0 0 0 0 0
Railroad (P/T)
  cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
1st instance 1 0 0 1 1 1 1 1 1
instances 2 0 0 3 3 2 2 2 5
max reached 0 0 0 0 0 0 0 0 2
best 0 0 0 0 0 0 0 0 2
subtotal 3 0 0 4 4 3 3 3 10
RessAllocation (P/T)
  cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
1st instance 1 0 0 1 1 1 1 1 1
instances 15 0 0 15 15 15 15 15 15
max reached 2 0 0 2 2 2 2 2 2
best 2 0 0 2 2 2 2 2 2
subtotal 20 0 0 20 20 20 20 20 20
Ring (P/T)
  cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
1st instance 0 0 0 1 1 1 0 1 1
instances 0 0 0 1 1 1 0 1 1
max reached 0 0 0 2 2 2 0 2 2
best 0 0 0 2 2 2 0 2 2
subtotal 0 0 0 6 6 6 0 6 6
RwMutex (P/T)
  cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
1st instance 1 0 0 1 1 1 1 1 1
instances 12 0 0 12 12 12 12 7 12
max reached 2 0 0 2 2 2 2 0 2
best 2 0 0 2 2 2 2 0 2
subtotal 17 0 0 17 17 17 17 8 17
SharedMemory (Colored)
  cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
1st instance 0 0 0 0 0 0 0 0 0
instances 0 0 0 0 0 0 0 0 0
max reached 0 0 0 0 0 0 0 0 0
best 0 0 0 0 0 0 0 0 0
subtotal 0 0 0 0 0 0 0 0 0
SharedMemory (P/T)
  cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
1st instance 1 1 0 1 1 1 1 1 1
instances 6 2 0 6 6 3 3 3 6
max reached 2 0 0 2 2 2 2 0 2
best 2 0 0 2 2 2 2 0 2
subtotal 11 3 0 11 11 8 8 4 11
SimpleLoadBal (Colored)
  cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
1st instance 0 0 1 0 0 0 0 0 0
instances 0 0 3 0 0 0 0 0 0
max reached 0 0 0 0 0 0 0 0 0
best 0 0 2 0 0 0 0 0 0
subtotal 0 0 6 0 0 0 0 0 0
SimpleLoadBal (P/T)
  cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
1st instance 1 0 0 1 1 1 1 1 1
instances 2 0 0 3 3 3 3 3 5
max reached 0 0 0 0 0 0 0 0 2
best 0 0 0 0 0 0 0 0 2
subtotal 3 0 0 4 4 4 4 4 10
TokenRing (Colored)
  cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
1st instance 0 0 0 0 0 0 0 0 0
instances 0 0 0 0 0 0 0 0 0
max reached 0 0 0 0 0 0 0 0 0
best 0 0 0 0 0 0 0 0 0
subtotal 0 0 0 0 0 0 0 0 0
TokenRing (P/T)
  cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
1st instance 1 1 0 1 1 1 1 1 1
instances 2 1 0 2 2 2 2 2 4
max reached 0 0 0 0 0 0 0 0 2
best 0 0 0 0 0 0 0 0 2
subtotal 3 2 0 3 3 3 3 3 9