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

Please find enclosed the brute results for the ReachabilityDeadlock examination. We display only the score of tools that provide a results for at least one instance of one model. You may access to the scoring for this examination here.

The legend for the values is provided below:

Note on the display of results for formulas: each formula is considered as a flag (F if false, T if true, - or ? when the value cannot be determined). These values are concatenated in the order they appear (we assume it is the order of formulas as they were provided).

CSRepetitions (Colored)
instances cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
02 nc nc F nc nc nc nc nc nc
03 nc nc F nc nc nc nc nc nc
04 nc nc mp nc nc nc nc nc nc
05 nc nc mp nc nc nc nc nc nc
07 nc nc mp nc nc nc nc nc nc
10 nc nc mp nc nc nc nc nc nc
CSRepetitions (P/T)
instances cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
02 FF FF nc FF FF FF FF FT F-
03 F? FF nc FF FF FF FF FT F-
04 to FF nc FF FF FF FF to F-
05 to to nc FF FF FF FF to F-
07 to mp nc FF FF FF FF to F-
10 to mp nc FF FF FF FF to F-
Dekker (P/T)
instances cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
010 FT nc nc FT FT F- FT FT F-
015 FT nc nc FT FT F- FT FT F-
020 FT nc nc FT FT F- to FT F-
050 FT nc nc to to to to to F-
100 FT nc nc to to to to to F-
200 nc nc nc to nc to to to F-
DotAndBoxes (Colored)
instances cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
2 nc nc F nc nc nc nc nc nc
3 nc nc F nc nc nc nc nc nc
4 nc nc F nc nc nc nc nc nc
5 nc nc mp nc nc nc nc nc nc
DrinkVendingMachine (Colored)
instances cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
02 nc nc F nc nc nc nc nc nc
10 nc nc F nc nc nc nc nc nc
DrinkVendingMachine (P/T)
instances cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
02 FT nc nc FT FT F- FT FT F-
10 nc nc nc F- F- F- F- FT F-
Echo (P/T)
instances cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
d02r09 nc nc nc FF FF FF FF to F-
d02r11 nc nc nc FF FF FF FF to F-
d02r15 nc nc nc FF FF FF FF to F-
d02r19 nc nc nc FF FF FF FF to F-
d03r03 nc nc nc FF FF FF FF to F-
d03r05 nc nc nc FF FF FF FF to F-
d03r07 nc nc nc FF FF FF FF to F-
d04r03 nc nc nc FF FF FF FF to F-
d05r03 nc nc nc FF FF FF FF to F-
Eratosthenes (P/T)
instances cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
010 FF nc nc FF FF FF FF FT F-
020 FF nc nc FF FF FF FF FT F-
050 FF nc nc FF FF FF FF FT F-
100 FF nc nc FF FF FF FF FT F-
200 FF nc nc FF FF FF FF FT F-
500 nc nc nc FF FF FF to FT F-
FMS (P/T)
instances cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
002 nc FT nc FT FT F- FT FT F-
005 nc FT nc FT FT F- FT FT F-
010 nc FT nc FT FT F- FT FT F-
020 nc FT nc FT FT F- FT FT F-
050 nc FT nc FT FT F- FT FT F-
100 nc FT nc FT FT F- FT FT F-
200 nc to nc FT FT F- FT to F-
500 nc to nc FT FT F- FT to F-
GlobalRessAlloc (Colored)
instances cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
03 nc nc F nc nc nc nc nc nc
05 nc nc F nc nc nc nc nc nc
06 nc nc F nc nc nc nc nc nc
07 nc nc mp nc nc nc nc nc nc
09 nc nc mp nc nc nc nc nc nc
10 nc nc mp nc nc nc nc nc nc
11 nc nc mp nc nc nc nc nc nc
GlobalRessAlloc (P/T)
instances cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
03 F? FT nc FT FT F- FT FT F-
05 nc cc nc to to to F- to F-
Kanban (P/T)
instances cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
0005 nc FT nc FT FT F- FT FT F-
0010 nc FT nc FT FT F- FT FT F-
0020 nc FT nc FT FT F- FT FT F-
0050 nc FT nc FT FT F- FT FT F-
0100 nc FT nc F- F- F- FT FT F-
0200 nc T nc F- F- F- FT to F-
0500 nc T nc F- F- F- FT to F-
1000 nc to nc F- F- F- FT to F-
LamportFastMutEx (Colored)
instances cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
2 nc nc F nc nc nc nc nc nc
3 nc nc F nc nc nc nc nc nc
4 nc nc F nc nc nc nc nc nc
5 nc nc F nc nc nc nc nc nc
6 nc nc mp nc nc nc nc nc nc
7 nc nc mp nc nc nc nc nc nc
8 nc nc mp nc nc nc nc nc nc
LamportFastMutEx (P/T)
instances cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
2 FT nc nc FT FT F- FT FT F-
3 FT nc nc FT FT F- FT FT F-
4 F? nc nc FT FT F- FT FT F-
5 to nc nc F- F- to FT to F-
6 to nc nc F- F- to to to F-
7 to nc nc F- F- to to to F-
8 to nc nc to to to to to F-
MAPK (P/T)
instances cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
008 nc FT nc FT FT F- FT FT F-
020 nc FT nc F- F- F- FT FT F-
040 nc FT nc F- F- F- FT FT F-
080 nc to nc F- F- F- to FT F-
160 nc to nc F- F- F- to to F-
320 nc to nc F- F- F- to to F-
NeoElection (Colored)
instances cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
2 nc nc F nc nc nc nc nc nc
3 nc nc F nc nc nc nc nc nc
4 nc nc F nc nc nc nc nc nc
5 nc nc mp nc nc nc nc nc nc
6 nc nc mp nc nc nc nc nc nc
7 nc nc mp nc nc nc nc nc nc
8 nc nc mp nc nc nc nc nc nc
NeoElection (P/T)
instances cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
2 FF nc nc FF FF FF FF FT F-
3 FF nc nc FF FF FF FF FT F-
4 nc nc nc FF FF FF FF to F-
5 nc nc nc FF FF FF FF to F-
6 nc nc nc FF FF FF FF to F-
7 nc nc nc FF FF FF FF to F-
8 nc nc nc FF FF FF FF to F-
PermAdmissibility (Colored)
instances cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
01 nc nc F nc nc nc nc nc nc
02 nc nc mp nc nc nc nc nc nc
05 nc nc mp nc nc nc nc nc nc
10 nc nc mp nc nc nc nc nc nc
20 nc nc mp nc nc nc nc nc nc
50 nc nc mp nc nc nc nc nc nc
PermAdmissibility (P/T)
instances cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
01 FF FF nc FF FF FF FF FT F-
02 nc TF nc FF FF FF FF to F-
05 nc TF nc FF FF FF FF to F-
10 nc TF nc FF FF FF FF to F-
20 nc TF nc FF FF FF FF to F-
50 nc TF nc FF FF FF FF to F-
Peterson (Colored)
instances cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
2 nc nc F nc nc nc nc nc nc
3 nc nc F nc nc nc nc nc nc
4 nc nc mp nc nc nc nc nc nc
5 nc nc mp nc nc nc nc nc nc
6 nc nc mp nc nc nc nc nc nc
7 nc nc mp nc nc nc nc nc nc
Peterson (P/T)
instances cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
2 FT nc nc FT FT F- FT FT F-
3 FT nc nc FT FT F- FT FT F-
4 nc nc nc F- F- F- to to F-
5 to nc nc F- F- to to to F-
6 to nc nc F- F- to F- to F-
7 to nc nc F- F- to F- to F-
Philosophers (Colored)
instances cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
000005 nc nc nc nc nc nc nc nc nc
000010 nc nc nc nc nc nc nc nc nc
000020 nc nc nc nc nc nc nc nc nc
000050 nc nc nc nc nc nc nc nc nc
000100 nc nc nc nc nc nc nc nc nc
000200 nc nc nc nc nc nc nc nc nc
000500 nc nc nc nc nc nc nc nc nc
001000 nc nc nc nc nc nc nc nc nc
002000 nc nc nc nc nc nc nc nc nc
005000 nc nc nc nc nc nc nc nc nc
010000 nc nc nc nc nc nc nc nc nc
050000 nc nc nc nc nc nc nc nc nc
100000 nc nc nc nc nc nc nc nc nc
Philosophers (P/T)
instances cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
000005 FF FF nf FF FF FF FF FT F-
000010 FF FF nf FF FF FF FF FT F-
000020 FF FF nf FF FF FF FF FT F-
000050 FF FF nf FF FF FF FF FT F-
000100 FF to nf FF FF FF FF FT F-
000200 FF to nf FF FF FF FF FT F-
000500 FF to nf FF FF FF to FT F-
001000 FF mp nf FF FF FF to FT F-
002000 FF mp nf FF FF FF to to F-
005000 nc mp nf FF FF FF to to F-
010000 nc cc nf FF FF FF to to F-
PhilosophersDyn (Colored)
instances cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
03 nc nc nc nc nc nc nc nc nc
10 nc nc nc nc nc nc nc nc nc
20 nc nc nc nc nc nc nc nc nc
50 nc nc nc nc nc nc nc nc nc
80 nc nc nc nc nc nc nc nc nc
PhilosophersDyn (P/T)
instances cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
03 to FF nc FF FF FF FF FT F-
10 nc mp nc FF FF FF FF to F-
20 to mp nc FF FF FF FF to F-
Planning (P/T)
instances cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
nf nf nf nf nf nf nf nf nf
Railroad (P/T)
instances cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
005 FT nc nc FT FT F- FT FT F-
010 FT nc nc FT FT F- FT FT F-
020 to nc nc F- F- to to to F-
050 to nc nc to to to to to F-
100 nc nc nc to to to to to F-
RessAllocation (P/T)
instances cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
R002C002 FF nc nc FF FF FF FF FT F-
R003C002 FF nc nc FF FF FF FF FT F-
R003C003 FF nc nc FF FF FF FF FT F-
R003C005 FF nc nc FF FF FF FF FT F-
R003C010 FF nc nc FF FF FF FF FT F-
R003C015 FF nc nc FF FF FF FF FT F-
R003C020 FF nc nc FF FF FF FF FT F-
R003C050 FF nc nc FF FF FF FF FT F-
R003C100 FF nc nc FF FF FF FF FT F-
R005C002 FF nc nc FF FF FF FF FT F-
R010C002 FF nc nc FF FF FF FF FT F-
R015C002 FF nc nc FF FF FF FF FT F-
R020C002 FF nc nc FF FF FF FF FT F-
R050C002 FF nc nc FF FF FF FF FT F-
R100C002 F? nc nc FF FF FF FF FT F-
Ring (P/T)
instances cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
none nc nc nc F- F- F- to FT F-
RwMutex (P/T)
instances cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
r0010w0010 FT nc nc FT FT F- FT FT F-
r0010w0020 FT nc nc FT FT F- FT FT F-
r0010w0050 FT nc nc FT FT F- FT FT F-
r0010w0100 FT nc nc FT FT F- FT FT F-
r0010w0500 FT nc nc FT FT F- FT FT F-
r0010w1000 FT nc nc FT FT F- FT FT F-
r0010w2000 FT nc nc FT FT F- FT to F-
r0020w0010 FT nc nc FT FT F- FT FT F-
r0100w0010 FT nc nc FT FT F- FT cc F-
r0500w0010 FT nc nc FT FT F- FT cc F-
r1000w0010 FT nc nc FT FT F- FT cc F-
r2000w0010 FT nc nc FT FT F- FT cc F-
SharedMemory (Colored)
instances cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
000005 nc nc nc nc nc nc nc nc nc
000010 nc nc nc nc nc nc nc nc nc
000020 nc nc nc nc nc nc nc nc nc
000050 nc nc nc nc nc nc nc nc nc
000100 nc nc nc nc nc nc nc nc nc
000200 nc nc nc nc nc nc nc nc nc
000500 nc nc nc nc nc nc nc nc nc
001000 nc nc nc nc nc nc nc nc nc
002000 nc nc nc nc nc nc nc nc nc
005000 nc nc nc nc nc nc nc nc nc
010000 nc nc nc nc nc nc nc nc nc
020000 nc nc nc nc nc nc nc nc nc
050000 nc nc nc nc nc nc nc nc nc
100000 nc nc nc nc nc nc nc nc nc
SharedMemory (P/T)
instances cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
000005 FT FT nc FT FT F- FT FT F-
000010 FT FT nc FT FT F- FT FT F-
000020 FT mp nc F- F- to to FT F-
000050 FT mp nc F- F- to to to F-
000100 FT mp nc F- F- to to to F-
000200 FT cc nc F- F- F- F- to F-
SimpleLoadBal (Colored)
instances cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
02 nc nc F nc nc nc nc nc nc
05 nc nc F nc nc nc nc nc nc
10 nc nc F nc nc nc nc nc nc
15 nc nc mp nc nc nc nc nc nc
20 nc nc mp nc nc nc nc nc nc
SimpleLoadBal (P/T)
instances cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
02 FT nc nc FT FT F- FT FT F-
05 FT nc nc FT FT F- FT FT F-
10 to nc nc FT FT F- FT FT F-
15 to nc nc to to to to to F-
20 to nc nc to to to to to F-
TokenRing (Colored)
instances cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
005 nc nc nc nc nc nc nc nc nc
010 nc nc nc nc nc nc nc nc nc
020 nc nc nc nc nc nc nc nc nc
050 nc nc nc nc nc nc nc nc nc
100 nc nc nc nc nc nc nc nc nc
200 nc nc nc nc nc nc nc nc nc
500 nc nc nc nc nc nc nc nc nc
TokenRing (P/T)
instances cunf greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
005 FT FT nc FT FT F- FT FT F-
010 FT to nc FT FT F- FT FT F-
020 nc mp nc to to to to to F-
050 nc cc nc to to to to to F-