Please find enclosed the scores for the ReachabilityMix 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:
- 1st instance: the tool gets a bonus for having processed the first instance of this model (+1 point),
- instances: the tool gets 1 point per instances treated (for that, we assume that at least one formula has been successfuly computed),
- max reached: the tool could process all the instances for the model (+2 points),
- best: the tool is among the ones that processed a maximum of instances within the time and memory confinement (+2 points).
For known, a tool may collect up to 411 points.
| Total Score of the tools | ||||||||
| greatSPN | ITS-Tools | lola | lola optimistic | lola optimistic incomplete | lola pessimistic | marcie | sara | |
| Global Score | 40 | 54 | 184 | 189 | 154 | 111 | 118 | 80 |
| CSRepetitions (Colored) | ||||||||
| greatSPN | ITS-Tools | lola | lola optimistic | lola optimistic incomplete | lola pessimistic | marcie | sara | |
| 1st instance | 0 | 1 | 0 | 0 | 0 | 0 | 0 | 0 |
| instances | 0 | 2 | 0 | 0 | 0 | 0 | 0 | 0 |
| max reached | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
| best | 0 | 2 | 0 | 0 | 0 | 0 | 0 | 0 |
| subtotal | 0 | 5 | 0 | 0 | 0 | 0 | 0 | 0 |
| CSRepetitions (P/T) | ||||||||
| greatSPN | ITS-Tools | lola | lola optimistic | lola optimistic incomplete | lola pessimistic | marcie | sara | |
| 1st instance | 1 | 0 | 1 | 1 | 1 | 1 | 1 | 1 |
| instances | 2 | 0 | 6 | 6 | 3 | 3 | 2 | 3 |
| max reached | 0 | 0 | 2 | 2 | 0 | 0 | 0 | 2 |
| best | 0 | 0 | 2 | 2 | 0 | 0 | 0 | 2 |
| subtotal | 3 | 0 | 11 | 11 | 4 | 4 | 3 | 8 |
| Dekker (P/T) | ||||||||
| greatSPN | ITS-Tools | lola | lola optimistic | lola optimistic incomplete | lola pessimistic | marcie | sara | |
| 1st instance | 0 | 0 | 1 | 1 | 1 | 1 | 1 | 0 |
| instances | 0 | 0 | 3 | 4 | 5 | 3 | 3 | 0 |
| max reached | 0 | 0 | 0 | 2 | 2 | 0 | 0 | 0 |
| best | 0 | 0 | 0 | 2 | 2 | 0 | 0 | 0 |
| subtotal | 0 | 0 | 4 | 9 | 10 | 4 | 4 | 0 |
| DotAndBoxes (Colored) | ||||||||
| greatSPN | ITS-Tools | lola | lola optimistic | lola optimistic incomplete | lola pessimistic | marcie | sara | |
| 1st instance | 0 | 1 | 0 | 0 | 0 | 0 | 0 | 0 |
| instances | 0 | 2 | 0 | 0 | 0 | 0 | 0 | 0 |
| max reached | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
| best | 0 | 2 | 0 | 0 | 0 | 0 | 0 | 0 |
| subtotal | 0 | 5 | 0 | 0 | 0 | 0 | 0 | 0 |
| DrinkVendingMachine (Colored) | ||||||||
| greatSPN | ITS-Tools | lola | lola optimistic | lola optimistic incomplete | lola pessimistic | marcie | sara | |
| 1st instance | 0 | 1 | 0 | 0 | 0 | 0 | 0 | 0 |
| instances | 0 | 1 | 0 | 0 | 0 | 0 | 0 | 0 |
| max reached | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
| best | 0 | 2 | 0 | 0 | 0 | 0 | 0 | 0 |
| subtotal | 0 | 4 | 0 | 0 | 0 | 0 | 0 | 0 |
| DrinkVendingMachine (P/T) | ||||||||
| greatSPN | ITS-Tools | lola | lola optimistic | lola optimistic incomplete | lola pessimistic | marcie | sara | |
| 1st instance | 0 | 0 | 1 | 1 | 1 | 1 | 1 | 0 |
| instances | 0 | 0 | 1 | 1 | 1 | 1 | 2 | 0 |
| max reached | 0 | 0 | 0 | 0 | 0 | 0 | 2 | 0 |
| best | 0 | 0 | 0 | 0 | 0 | 0 | 2 | 0 |
| subtotal | 0 | 0 | 2 | 2 | 2 | 2 | 7 | 0 |
| Echo (P/T) | ||||||||
| greatSPN | ITS-Tools | lola | lola optimistic | lola optimistic incomplete | lola pessimistic | marcie | sara | |
| 1st instance | 0 | 0 | 1 | 1 | 1 | 1 | 0 | 1 |
| instances | 0 | 0 | 9 | 9 | 1 | 2 | 0 | 3 |
| max reached | 0 | 0 | 2 | 2 | 2 | 0 | 0 | 0 |
| best | 0 | 0 | 2 | 2 | 2 | 0 | 0 | 0 |
| subtotal | 0 | 0 | 14 | 14 | 6 | 3 | 0 | 4 |
| Eratosthenes (P/T) | ||||||||
| greatSPN | ITS-Tools | lola | lola optimistic | lola optimistic incomplete | lola pessimistic | marcie | sara | |
| 1st instance | 0 | 1 | 1 | 1 | 1 | 1 | 1 | 1 |
| instances | 0 | 6 | 5 | 5 | 4 | 4 | 6 | 2 |
| max reached | 0 | 2 | 2 | 2 | 2 | 0 | 2 | 0 |
| best | 0 | 2 | 2 | 2 | 2 | 0 | 2 | 0 |
| subtotal | 0 | 11 | 10 | 10 | 9 | 5 | 11 | 3 |
| FMS (P/T) | ||||||||
| greatSPN | ITS-Tools | lola | lola optimistic | lola optimistic incomplete | lola pessimistic | marcie | sara | |
| 1st instance | 1 | 1 | 1 | 1 | 1 | 1 | 1 | 1 |
| instances | 5 | 1 | 8 | 8 | 8 | 6 | 6 | 2 |
| max reached | 0 | 0 | 2 | 2 | 2 | 2 | 0 | 2 |
| best | 0 | 0 | 2 | 2 | 2 | 2 | 0 | 2 |
| subtotal | 6 | 2 | 13 | 13 | 13 | 11 | 7 | 7 |
| GlobalRessAlloc (Colored) | ||||||||
| greatSPN | ITS-Tools | lola | lola optimistic | lola optimistic incomplete | lola pessimistic | marcie | sara | |
| 1st instance | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
| instances | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
| max reached | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
| best | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
| subtotal | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
| GlobalRessAlloc (P/T) | ||||||||
| greatSPN | ITS-Tools | lola | lola optimistic | lola optimistic incomplete | lola pessimistic | marcie | sara | |
| 1st instance | 1 | 0 | 1 | 1 | 1 | 1 | 1 | 0 |
| instances | 1 | 0 | 1 | 1 | 1 | 1 | 1 | 0 |
| max reached | 0 | 0 | 0 | 0 | 0 | 2 | 0 | 0 |
| best | 0 | 0 | 0 | 0 | 0 | 2 | 0 | 0 |
| subtotal | 2 | 0 | 2 | 2 | 2 | 6 | 2 | 0 |
| Kanban (P/T) | ||||||||
| greatSPN | ITS-Tools | lola | lola optimistic | lola optimistic incomplete | lola pessimistic | marcie | sara | |
| 1st instance | 1 | 0 | 1 | 1 | 1 | 1 | 1 | 1 |
| instances | 4 | 0 | 8 | 8 | 8 | 7 | 5 | 4 |
| max reached | 0 | 0 | 2 | 2 | 2 | 2 | 0 | 2 |
| best | 0 | 0 | 2 | 2 | 2 | 2 | 0 | 2 |
| subtotal | 5 | 0 | 13 | 13 | 13 | 12 | 6 | 9 |
| LamportFastMutEx (Colored) | ||||||||
| greatSPN | ITS-Tools | lola | lola optimistic | lola optimistic incomplete | lola pessimistic | marcie | sara | |
| 1st instance | 0 | 1 | 0 | 0 | 0 | 0 | 0 | 0 |
| instances | 0 | 4 | 0 | 0 | 0 | 0 | 0 | 0 |
| max reached | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
| best | 0 | 2 | 0 | 0 | 0 | 0 | 0 | 0 |
| subtotal | 0 | 7 | 0 | 0 | 0 | 0 | 0 | 0 |
| LamportFastMutEx (P/T) | ||||||||
| greatSPN | ITS-Tools | lola | lola optimistic | lola optimistic incomplete | lola pessimistic | marcie | sara | |
| 1st instance | 0 | 0 | 0 | 0 | 0 | 0 | 1 | 0 |
| instances | 0 | 0 | 0 | 0 | 0 | 0 | 3 | 0 |
| max reached | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
| best | 0 | 0 | 0 | 0 | 0 | 0 | 2 | 0 |
| subtotal | 0 | 0 | 0 | 0 | 0 | 0 | 6 | 0 |
| MAPK (P/T) | ||||||||
| greatSPN | ITS-Tools | lola | lola optimistic | lola optimistic incomplete | lola pessimistic | marcie | sara | |
| 1st instance | 1 | 0 | 1 | 1 | 1 | 1 | 1 | 1 |
| instances | 2 | 0 | 6 | 6 | 6 | 4 | 4 | 3 |
| max reached | 0 | 0 | 2 | 2 | 2 | 0 | 0 | 2 |
| best | 0 | 0 | 2 | 2 | 2 | 0 | 0 | 2 |
| subtotal | 3 | 0 | 11 | 11 | 11 | 5 | 5 | 8 |
| NeoElection (Colored) | ||||||||
| greatSPN | ITS-Tools | lola | lola optimistic | lola optimistic incomplete | lola pessimistic | marcie | sara | |
| 1st instance | 0 | 1 | 0 | 0 | 0 | 0 | 0 | 0 |
| instances | 0 | 2 | 0 | 0 | 0 | 0 | 0 | 0 |
| max reached | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
| best | 0 | 2 | 0 | 0 | 0 | 0 | 0 | 0 |
| subtotal | 0 | 5 | 0 | 0 | 0 | 0 | 0 | 0 |
| NeoElection (P/T) | ||||||||
| greatSPN | ITS-Tools | lola | lola optimistic | lola optimistic incomplete | lola pessimistic | marcie | sara | |
| 1st instance | 0 | 0 | 1 | 1 | 1 | 1 | 1 | 1 |
| instances | 0 | 0 | 4 | 4 | 2 | 2 | 2 | 2 |
| max reached | 0 | 0 | 2 | 2 | 0 | 0 | 0 | 0 |
| best | 0 | 0 | 2 | 2 | 0 | 0 | 0 | 0 |
| subtotal | 0 | 0 | 9 | 9 | 3 | 3 | 3 | 3 |
| PermAdmissibility (Colored) | ||||||||
| greatSPN | ITS-Tools | lola | lola optimistic | lola optimistic incomplete | lola pessimistic | marcie | sara | |
| 1st instance | 0 | 1 | 0 | 0 | 0 | 0 | 0 | 0 |
| instances | 0 | 1 | 0 | 0 | 0 | 0 | 0 | 0 |
| max reached | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
| best | 0 | 2 | 0 | 0 | 0 | 0 | 0 | 0 |
| subtotal | 0 | 4 | 0 | 0 | 0 | 0 | 0 | 0 |
| PermAdmissibility (P/T) | ||||||||
| greatSPN | ITS-Tools | lola | lola optimistic | lola optimistic incomplete | lola pessimistic | marcie | sara | |
| 1st instance | 1 | 0 | 1 | 1 | 1 | 1 | 1 | 1 |
| instances | 5 | 0 | 4 | 4 | 2 | 2 | 1 | 2 |
| max reached | 2 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
| best | 2 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
| subtotal | 10 | 0 | 5 | 5 | 3 | 3 | 2 | 3 |
| Peterson (Colored) | ||||||||
| greatSPN | ITS-Tools | lola | lola optimistic | lola optimistic incomplete | lola pessimistic | marcie | sara | |
| 1st instance | 0 | 1 | 0 | 0 | 0 | 0 | 0 | 0 |
| instances | 0 | 2 | 0 | 0 | 0 | 0 | 0 | 0 |
| max reached | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
| best | 0 | 2 | 0 | 0 | 0 | 0 | 0 | 0 |
| subtotal | 0 | 5 | 0 | 0 | 0 | 0 | 0 | 0 |
| Peterson (P/T) | ||||||||
| greatSPN | ITS-Tools | lola | lola optimistic | lola optimistic incomplete | lola pessimistic | marcie | sara | |
| 1st instance | 0 | 0 | 1 | 1 | 1 | 1 | 1 | 1 |
| instances | 0 | 0 | 5 | 5 | 3 | 3 | 2 | 1 |
| max reached | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
| best | 0 | 0 | 2 | 2 | 0 | 0 | 0 | 0 |
| subtotal | 0 | 0 | 8 | 8 | 4 | 4 | 3 | 2 |
| Philosophers (Colored) | ||||||||
| greatSPN | ITS-Tools | lola | lola optimistic | lola optimistic incomplete | lola pessimistic | marcie | sara | |
| 1st instance | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
| instances | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
| max reached | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
| best | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
| subtotal | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
| Philosophers (P/T) | ||||||||
| greatSPN | ITS-Tools | lola | lola optimistic | lola optimistic incomplete | lola pessimistic | marcie | sara | |
| 1st instance | 1 | 0 | 1 | 1 | 1 | 1 | 1 | 1 |
| instances | 3 | 0 | 7 | 7 | 5 | 2 | 5 | 3 |
| max reached | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
| best | 0 | 0 | 2 | 2 | 0 | 0 | 0 | 0 |
| subtotal | 4 | 0 | 10 | 10 | 6 | 3 | 6 | 4 |
| PhilosophersDyn (Colored) | ||||||||
| greatSPN | ITS-Tools | lola | lola optimistic | lola optimistic incomplete | lola pessimistic | marcie | sara | |
| 1st instance | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
| instances | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
| max reached | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
| best | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
| subtotal | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
| PhilosophersDyn (P/T) | ||||||||
| greatSPN | ITS-Tools | lola | lola optimistic | lola optimistic incomplete | lola pessimistic | marcie | sara | |
| 1st instance | 1 | 0 | 1 | 1 | 1 | 1 | 1 | 0 |
| instances | 1 | 0 | 2 | 2 | 2 | 2 | 1 | 0 |
| max reached | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
| best | 0 | 0 | 2 | 2 | 2 | 2 | 0 | 0 |
| subtotal | 2 | 0 | 5 | 5 | 5 | 5 | 2 | 0 |
| Planning (P/T) | ||||||||
| greatSPN | ITS-Tools | lola | lola optimistic | lola optimistic incomplete | lola pessimistic | marcie | sara | |
| 1st instance | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
| instances | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
| max reached | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
| best | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
| subtotal | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
| Railroad (P/T) | ||||||||
| greatSPN | ITS-Tools | lola | lola optimistic | lola optimistic incomplete | lola pessimistic | marcie | sara | |
| 1st instance | 0 | 0 | 1 | 1 | 1 | 1 | 1 | 1 |
| instances | 0 | 0 | 3 | 3 | 3 | 1 | 2 | 1 |
| max reached | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
| best | 0 | 0 | 2 | 2 | 2 | 0 | 0 | 0 |
| subtotal | 0 | 0 | 6 | 6 | 6 | 2 | 3 | 2 |
| RessAllocation (P/T) | ||||||||
| greatSPN | ITS-Tools | lola | lola optimistic | lola optimistic incomplete | lola pessimistic | marcie | sara | |
| 1st instance | 0 | 0 | 1 | 1 | 1 | 1 | 1 | 1 |
| instances | 0 | 0 | 15 | 15 | 12 | 11 | 15 | 4 |
| max reached | 0 | 0 | 2 | 2 | 2 | 0 | 2 | 2 |
| best | 0 | 0 | 2 | 2 | 2 | 0 | 2 | 2 |
| subtotal | 0 | 0 | 20 | 20 | 17 | 12 | 20 | 9 |
| Ring (P/T) | ||||||||
| greatSPN | ITS-Tools | lola | lola optimistic | lola optimistic incomplete | lola pessimistic | marcie | sara | |
| 1st instance | 0 | 0 | 1 | 1 | 1 | 1 | 1 | 1 |
| instances | 0 | 0 | 1 | 1 | 1 | 1 | 1 | 1 |
| max reached | 0 | 0 | 2 | 2 | 2 | 2 | 2 | 2 |
| best | 0 | 0 | 2 | 2 | 2 | 2 | 2 | 2 |
| subtotal | 0 | 0 | 6 | 6 | 6 | 6 | 6 | 6 |
| RwMutex (P/T) | ||||||||
| greatSPN | ITS-Tools | lola | lola optimistic | lola optimistic incomplete | lola pessimistic | marcie | sara | |
| 1st instance | 0 | 0 | 1 | 1 | 1 | 1 | 1 | 1 |
| instances | 0 | 0 | 12 | 12 | 12 | 7 | 6 | 4 |
| max reached | 0 | 0 | 2 | 2 | 2 | 0 | 0 | 0 |
| best | 0 | 0 | 2 | 2 | 2 | 0 | 0 | 0 |
| subtotal | 0 | 0 | 17 | 17 | 17 | 8 | 7 | 5 |
| SharedMemory (Colored) | ||||||||
| greatSPN | ITS-Tools | lola | lola optimistic | lola optimistic incomplete | lola pessimistic | marcie | sara | |
| 1st instance | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
| instances | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
| max reached | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
| best | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
| subtotal | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
| SharedMemory (P/T) | ||||||||
| greatSPN | ITS-Tools | lola | lola optimistic | lola optimistic incomplete | lola pessimistic | marcie | sara | |
| 1st instance | 1 | 0 | 1 | 1 | 1 | 1 | 1 | 1 |
| instances | 2 | 0 | 4 | 4 | 3 | 2 | 3 | 2 |
| max reached | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
| best | 0 | 0 | 2 | 2 | 2 | 2 | 0 | 2 |
| subtotal | 3 | 0 | 7 | 7 | 6 | 5 | 4 | 5 |
| SimpleLoadBal (Colored) | ||||||||
| greatSPN | ITS-Tools | lola | lola optimistic | lola optimistic incomplete | lola pessimistic | marcie | sara | |
| 1st instance | 0 | 1 | 0 | 0 | 0 | 0 | 0 | 0 |
| instances | 0 | 3 | 0 | 0 | 0 | 0 | 0 | 0 |
| max reached | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
| best | 0 | 2 | 0 | 0 | 0 | 0 | 0 | 0 |
| subtotal | 0 | 6 | 0 | 0 | 0 | 0 | 0 | 0 |
| SimpleLoadBal (P/T) | ||||||||
| greatSPN | ITS-Tools | lola | lola optimistic | lola optimistic incomplete | lola pessimistic | marcie | sara | |
| 1st instance | 0 | 0 | 1 | 1 | 1 | 1 | 1 | 1 |
| instances | 0 | 0 | 3 | 3 | 3 | 2 | 3 | 1 |
| max reached | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
| best | 0 | 0 | 2 | 2 | 2 | 0 | 2 | 0 |
| subtotal | 0 | 0 | 6 | 6 | 6 | 3 | 6 | 2 |
| TokenRing (Colored) | ||||||||
| greatSPN | ITS-Tools | lola | lola optimistic | lola optimistic incomplete | lola pessimistic | marcie | sara | |
| 1st instance | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
| instances | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
| max reached | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
| best | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
| subtotal | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
| TokenRing (P/T) | ||||||||
| greatSPN | ITS-Tools | lola | lola optimistic | lola optimistic incomplete | lola pessimistic | marcie | sara | |
| 1st instance | 1 | 0 | 1 | 1 | 1 | 1 | 1 | 0 |
| instances | 1 | 0 | 2 | 2 | 2 | 2 | 2 | 0 |
| max reached | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
| best | 0 | 0 | 2 | 2 | 2 | 2 | 2 | 0 |
| subtotal | 2 | 0 | 5 | 5 | 5 | 5 | 5 | 0 |