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

Please find enclosed the brute results for the ReachabilityMix 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 greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
02 nc FFFFFFFF nc nc nc nc nc nc
03 nc FTFTFFFF nc nc nc nc nc nc
04 nc mp nc nc nc nc nc nc
05 nc mp nc nc nc nc nc nc
07 nc mp nc nc nc nc nc nc
10 nc mp nc nc nc nc nc nc
CSRepetitions (P/T)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
02 FFFFFFFF nc TFTFFFFF TFTFFFFF -F-FFFFF -F-FF--- FFFFFFFF cc
03 FTFTFFFF nc TFTFFTFT TFTFFTFT -F-FF-F- TFTFF--- FFFFTFFF ------T-
04 to nc FFFF-FFF FFFF-FFF FFFF-FFF ------F- to TFTF---T
05 to nc -F-FF-F- -F-FF-F- to to to cc
07 mp nc -F-FF--- -F-FF--- to to to cc
10 mp nc ------F- ------F- to to to -----TTT
Dekker (P/T)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
010 nc nc FFFFFFFF FFFFFFFF FFFFFFFF FFFFFFFF FFFTFFFF cc
015 nc nc FFFFFTFT FFFFFTFT FFFFF-F- FFFFFTFT FFFTFFFF cc
020 nc nc to to ---FFFFF to FFFTTFFF cc
050 nc nc FFFFFFFF FFFFFFFF FFFFFFFF FFFFFFFF to cc
100 nc nc to to to to to cc
200 nc nc nc FFFFFFFF FFFFFFFF to to cc
DotAndBoxes (Colored)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
2 nc FFFFFFFF nc nc nc nc nc nc
3 nc FFFFTF nc nc nc nc nc nc
4 nc cc nc nc nc nc nc nc
5 nc mp nc nc nc nc nc nc
DrinkVendingMachine (Colored)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
02 nc FFFFFFFF nc nc nc nc nc nc
10 nc cc nc nc nc nc nc nc
DrinkVendingMachine (P/T)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
02 nc nc TFTFFTFT TFTFFTFT -F-FF-F- TFTFF-F- FFFFFFFF cc
10 nc nc cc cc cc cc FFFTFFFF cc
Echo (P/T)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
d02r09 nc nc FFFFF-F- FFFFF-F- to ----F--- to cc
d02r11 nc nc -F-FFFFF -F-FFFFF to to to cc
d02r15 nc nc -F-FF-F- -F-FF-F- to to to cc
d02r19 nc nc -FFFFFFF -FFFFFFF to to to cc
d03r03 nc nc FFFFF-FF FFFFF-FF to FFFFFFF- to -------F
d03r05 nc nc FFFFF-F- FFFFF-F- to to to -----TTT
d03r07 nc nc -F-FFFFF -F-FFFFF to to to cc
d04r03 nc nc -FFFFFFF -FFFFFFF to to to -----FF-
d05r03 nc nc FFFFFFFF FFFFFFFF FFFFFFFF to to cc
Eratosthenes (P/T)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
010 nc FFFFFFFF FFFFFTFT FFFFFTFT FFFFF-F- FFFFFTFT FFFFFFFF FFTTFTTT
020 nc FFFFFFFF FFFFFFFF FFFFFFFF FFFFFFFF FFFF--F- FFFFFFFF cc
050 nc FFFF to to to -F-FFFFF FFTTTFFF cc
100 nc FFFFFFFF -F-FFFFF -F-FFFFF to -F-FFFFF FFFFFFFF -----FFF
200 nc FFFF TFTFFFFF TFTFFFFF -F-FFFFF to FFFFFFFF cc
500 nc FFFF FFFFFFFF FFFFFFFF FFFFFFFF to FFFFFFFF cc
FMS (P/T)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
002 FFFFFFFF nc FFFFFFFF FFFFFFFF FFFFFFFF FFFFF-F- FFFFFFFF cc
005 FFFFFFFF nc TFTFFFFF TFTFFFFF -F-FFFFF cc FFFFFFFF cc
010 FFFFFFFF nc TFTFFFFF TFTFFFFF -F-FFFFF -----FFF FFFFFFFF cc
020 FFFFFFFF nc TFFFFFFF TFFFFFFF -FFFFFFF ---F--F- FFFTFFFF cc
050 FFFFFFFF nc FFFFF-F- FFFFF-F- FFFFF-F- FFFFF-F- FFFTFFFF cc
100 mp F -----FFF -----FFF -----FFF ------F- FFFFFFFF ------T-
200 to nc -F-FFFFF -F-FFFFF -F-FFFFF cc to cc
500 to nc FFFFFFFF FFFFFFFF FFFFFFFF -F-FF-F- to FFFFF-T-
GlobalRessAlloc (Colored)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
03 nc nc nc nc nc nc nc nc
05 nc nc nc nc nc nc nc nc
06 nc nc nc nc nc nc nc nc
07 nc nc nc nc nc nc nc nc
09 nc nc nc nc nc nc nc nc
10 nc nc nc nc nc nc nc nc
11 nc nc nc nc nc nc nc nc
GlobalRessAlloc (P/T)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
03 FFFFFFFF nc TFTFTTFT TFTFTTFT -F-F--F- to FFFTFFFF cc
05 cc nc to to to -F-FF-F- to to
Kanban (P/T)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
0005 FFFFFFFF nc FFFFFTFT FFFFFTFT FFFFF-F- FFFF--F- FFFFFFFF cc
0010 FFFFFFFF nc FFFFFFFF FFFFFFFF FFFFFFFF -F-FF--- FFFFFFFF cc
0020 FFFFFFFF nc -F-FFFFF -F-FFFFF -F-FFFFF -----FFF FFFFFFFF -----FFF
0050 FFFFFFFF nc FFFFF-F- FFFFF-F- FFFFF-F- FFFFF-F- FFFFFFFF cc
0100 mp nc -F-FF--- -F-FF--- -F-FF--- cc FFFFFFFF cc
0200 mp nc FFFFFFFF FFFFFFFF FFFFFFFF -F-FF-F- to ------T-
0500 mp nc FFFFFFFF FFFFFFFF FFFFFFFF -F-FF--- to ------T-
1000 to nc -F-FFFFF -F-FFFFF -F-FFFFF ----F-F- to ------F-
LamportFastMutEx (Colored)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
2 nc FFFFFFFF nc nc nc nc nc nc
3 nc FFFFFFFF nc nc nc nc nc nc
4 nc FFFFFFFF nc nc nc nc nc nc
5 nc FTFTFFFF nc nc nc nc nc nc
6 nc mp nc nc nc nc nc nc
7 nc mp nc nc nc nc nc nc
8 nc mp nc nc nc nc nc nc
LamportFastMutEx (P/T)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
2 nc nc cc cc cc cc FFFFFFFF cc
3 nc nc cc cc cc cc FFFTTFFF cc
4 nc nc cc cc cc cc FFFTFFFF cc
5 nc nc cc cc cc cc to cc
6 nc nc cc cc cc cc to cc
7 nc nc cc cc cc cc to cc
8 nc nc cc cc cc cc to cc
MAPK (P/T)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
008 FFFFFFFF nc TTTTTFFF TTTTTFFF -----FFF ------FF FFFFFFFF -------T
020 FFFFFFFF nc FFFFFFFF FFFFFFFF FFFFFFFF -F-FFFFF FFFFFFFF cc
040 to nc ---FFFFF ---FFFFF ---FFFFF ---FF-F- FFFTTFFF -----TTT
080 to nc FFFFFFFF FFFFFFFF FFFFFFFF FFFFFFFF FFFFTFFF cc
160 to nc FFFFFFFF FFFFFFFF FFFFFFFF to to cc
320 to nc -FFFFFFF -FFFFFFF -FFFFFFF to to ------F-
NeoElection (Colored)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
2 nc FFFFFFFF nc nc nc nc nc nc
3 nc FFFFFFFF nc nc nc nc nc nc
4 nc nc nc nc nc nc nc nc
5 nc nc nc nc nc nc nc nc
6 nc nc nc nc nc nc nc nc
7 nc nc nc nc nc nc nc nc
8 nc nc nc nc nc nc nc nc
NeoElection (P/T)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
2 nc nc TTTTTTFT TTTTTTFT ------F- TTTTTTFT FFFFFFFF -----TTT
3 nc nc TFTFFTFT TFTFFTFT -F-FF-F- TFTFFTFT FFFFTFFF cc
4 nc nc cc cc to to to cc
5 nc nc -F-FFFFF -F-FFFFF to to to -----TTT
6 nc nc to to to to to cc
7 nc nc to to to to to cc
8 nc nc FFFFF-FF FFFFF-FF to to to cc
PermAdmissibility (Colored)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
01 nc FFFFFFFF nc nc nc nc nc nc
02 nc mp nc nc nc nc nc nc
05 nc mp nc nc nc nc nc nc
10 nc mp nc nc nc nc nc nc
20 nc mp nc nc nc nc nc nc
50 nc mp nc nc nc nc nc nc
PermAdmissibility (P/T)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
01 to nc TFTFFTFF TFTFFTFF -F-FF-FF TFTFFTFF FFFFFFFF -----TT-
02 ?????FFF nc -F-FF-F- -F-FF-F- to to to cc
05 FFFTTFTF nc to to to to to ------F-
10 FFFTTFFF nc -F-FFFFF -F-FFFFF to to to cc
20 TTTTTFFF nc FFFFFFFF FFFFFFFF FFFFFFFF FFFF-FFF to to
50 ?????FTF nc to to to to cc cc
Peterson (Colored)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
2 nc FFFFFFFF nc nc nc nc nc nc
3 nc FFFFFFFF nc nc nc nc nc nc
4 nc mp nc nc nc nc nc nc
5 nc mp nc nc nc nc nc nc
6 nc mp nc nc nc nc nc nc
7 nc mp nc nc nc nc nc nc
Peterson (P/T)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
2 nc nc TFTTTTFF TFTTTTFF -F----FF TFTT--F- FFFTFFFF -FFFF-T-
3 nc nc FFFFFTFT FFFFFTFT FFFFF-F- -F-F-TFT FFFFFFFF cc
4 nc nc FFFFFFFF FFFFFFFF FFFFFFFF FFFFFFFF to cc
5 nc nc -F-FF--- -F-FF--- to to to cc
6 nc nc -F-FF-FF -F-FF-FF to to to cc
7 nc nc cc cc cc cc to cc
Philosophers (Colored)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
000005 nc nc nc nc nc nc nc nc
000010 nc nc nc nc nc nc nc nc
000020 nc nc nc nc nc nc nc nc
000050 nc nc nc nc nc nc nc nc
000100 nc nc nc nc nc nc nc nc
000200 nc nc nc nc nc nc nc nc
000500 nc nc nc nc nc nc nc nc
001000 nc nc nc nc nc nc nc nc
002000 nc nc nc nc nc nc nc nc
005000 nc nc nc nc nc nc nc nc
010000 nc nc nc nc nc nc nc nc
050000 nc nc nc nc nc nc nc nc
100000 nc nc nc nc nc nc nc nc
Philosophers (P/T)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
000005 FFFFFFFF nf TFTFFFFF TFTFFFFF -F-FFFFF TFTFFFFF FFFFFFFF cc
000010 FTFTFFFF nf FFTFTTFT FFTFTTFT FF-F--F- FFTFTTFT FFFFFFFF TF-FF---
000020 FTFTFFTF nf FFFFFFF- FFFFFFF- FFFFFFF- to FFFFFFFT cc
000050 to nf cc cc cc cc FFFFTFFF cc
000100 mp nf ------F- ------F- ------F- to FFFFFFFF cc
000200 mp nf cc cc cc cc to cc
000500 to nf -----FFF -----FFF -----FFF to to ------F-
001000 mp nf -F-FFFFF -F-FFFFF to to to ------T-
002000 mp nf ------F- ------F- to to to cc
005000 mp nf to to to to to to
010000 cc nf to to to to to to
PhilosophersDyn (Colored)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
03 nc nc nc nc nc nc nc nc
10 nc nc nc nc nc nc nc nc
20 nc nc nc nc nc nc nc nc
50 nc nc nc nc nc nc nc nc
80 nc nc nc nc nc nc nc nc
PhilosophersDyn (P/T)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
03 FFFFFFFF nc TFTFTFFF TFTFTFFF -F-F-FFF TFTFTFFF FFFTFFFF cc
10 mp nc TFTFFTFT TFTFFTFT -F-FF-F- TFTFFTFT to cc
20 mp nc to to to to to to
Planning (P/T)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
nf nf nf nf nf nf nf nf
Railroad (P/T)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
005 nc nc TFTFFFFF TFTFFFFF -F-FFFFF TFTFFFFF FFFFFFFF -----TT-
010 nc nc TFTFTFFF TFTFTFFF -F-F-FFF cc FFFFFFFF cc
020 nc nc -F-FFT-T -F-FFT-T -F-FF--- to to cc
050 nc nc to to to to to cc
100 nc nc to to to to to cc
RessAllocation (P/T)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
R002C002 nc nc TFFFTTFF TFFFTTFF -FFF--FF TFFFT-FF FFFTFFFF cc
R003C002 nc nc TFTFFFFF TFTFFFFF -F-FFFFF TFTFFFFF FFFFFFFF ------T-
R003C003 nc nc TFTFFTFT TFTFFTFT -F-FF-F- TFTFF-F- FFFTTFFF cc
R003C005 nc nc TFTFFTFT TFTFFTFT -F-FF-F- TF-FFTFT FFFFFFFF cc
R003C010 nc nc TTTTTTFT TTTTTTFT ------F- -----TFT FFFFFFFF -----TFT
R003C015 nc nc TFTFFTFT TFTFFTFT -F-FF-F- -F-FF-F- FFFFFFFF cc
R003C020 nc nc FFFFF-FF FFFFF-FF to FFFFF--F FFFTFFFF cc
R003C050 nc nc ----FFFF ----FFFF to to FFFFTFFF ------T-
R003C100 nc nc FFFFF-F- FFFFF-F- to to FFFFFFFF cc
R005C002 nc nc FFFFFFFF FFFFFFFF FFFFFFFF FFFFFFFF FFFFFFFF cc
R010C002 nc nc FFFFFTFT FFFFFTFT FFFFF-F- TFTFTTFT FFFFFFFF cc
R015C002 nc nc FFFFFTFT FFFFFTFT FFFFF-F- FFFFF-F- FFFFTFFF cc
R020C002 nc nc FFFFFTFT FFFFFTFT FFFFF-F- FFFFFTFT FFFTTFFF cc
R050C002 nc nc TFTFTFFF TFTFTFFF -F-F-FFF to FFFFFFFF to
R100C002 nc nc -FFFFFFF -FFFFFFF -FFFFFFF to FFFTFFFF ------T-
Ring (P/T)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
none nc nc FFFFFFFF FFFFFFFF FFFFFFFF FFFFFFFF FFFFFFFF -----FFF
RwMutex (P/T)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
r0010w0010 nc nc TFTFFTFT TFTFFTFT -F-FF-F- TFTFF-F- FFFFFFFF cc
r0010w0020 nc nc TFTFTTFT TFTFTTFT -F-F--F- TFTF-TFT FFFFFFFF ------T-
r0010w0050 nc nc TTTTTTFT TTTTTTFT ------F- cc FFFFFFFF -----TTT
r0010w0100 nc nc FFFFFTFT FFFFFTFT FFFFF-F- cc FFFFTFFF -----TTT
r0010w0500 nc nc TFTFFFFF TFTFFFFF -F-FFFFF TFTF-FFF FFFTFFFF cc
r0010w1000 nc nc TFTFFTFT TFTFFTFT -F-FF-F- TFTF-TFT FFFFFFFF cc
r0010w2000 nc nc TTTTFTFT TTTTFTFT ----F-F- to to cc
r0020w0010 nc nc FFFFFFFF FFFFFFFF FFFFFFFF cc to cc
r0100w0010 nc nc FFFFFTFF FFFFFTFF FFFFF-FF -F-F---- cc cc
r0500w0010 nc nc TFTFFFFF TFTFFFFF -F-FFFFF -F-FFFFF cc cc
r1000w0010 nc nc FFFFFFFF FFFFFFFF FFFFFFFF FFFFF-F- cc ------T-
r2000w0010 nc nc FFFFFTFT FFFFFTFT FFFFF-F- cc cc cc
SharedMemory (Colored)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
000005 nc nc nc nc nc nc nc nc
000010 nc nc nc nc nc nc nc nc
000020 nc nc nc nc nc nc nc nc
000050 nc nc nc nc nc nc nc nc
000100 nc nc nc nc nc nc nc nc
000200 nc nc nc nc nc nc nc nc
000500 nc nc nc nc nc nc nc nc
001000 nc nc nc nc nc nc nc nc
002000 nc nc nc nc nc nc nc nc
005000 nc nc nc nc nc nc nc nc
010000 nc nc nc nc nc nc nc nc
020000 nc nc nc nc nc nc nc nc
050000 nc nc nc nc nc nc nc nc
100000 nc nc nc nc nc nc nc nc
SharedMemory (P/T)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
000005 FFFFFFFF nc FFFFFTFF FFFFFTFF FFFFF-FF FF----F- FFTTTFFF cc
000010 FFFFFFFF nc FFFFFTFF FFFFFTFF FFFFF-FF to FFTTFFFF -------T
000020 mp nc FF-FF-F- FF-FF-F- to to FFFFFFFF cc
000050 mp nc FFFFF--- FFFFF--- FFFFF--- -F-FF--- to TFTF----
000100 mp nc cc cc cc cc to cc
000200 cc nc cc cc cc cc to cc
SimpleLoadBal (Colored)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
02 nc FFFFFFFF nc nc nc nc nc nc
05 nc FFFFFFFF nc nc nc nc nc nc
10 nc FFFFFFFF nc nc nc nc nc nc
15 nc mp nc nc nc nc nc nc
20 nc mp nc nc nc nc nc nc
SimpleLoadBal (P/T)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
02 nc nc TTTFTFFF TTTFTFFF ---F-FFF TTTFTTFT FFFTFFFF cc
05 nc nc FFTFTTFT FFTFTTFT FF-F--F- FFTFT-F- FFFFFFFF ------T-
10 nc nc FFFFFFFF FFFFFFFF FFFFFFFF cc FFFFTFFF cc
15 nc nc to to to to to cc
20 nc nc to to to to to cc
TokenRing (Colored)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
005 nc nc nc nc nc nc nc nc
010 nc nc nc nc nc nc nc nc
020 nc nc nc nc nc nc nc nc
050 nc nc nc nc nc nc nc nc
100 nc nc nc nc nc nc nc nc
200 nc nc nc nc nc nc nc nc
500 nc nc nc nc nc nc nc nc
TokenRing (P/T)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
005 FTFFFFTF nc TFTFTTFT TFTFTTFT -F-F--F- -F-F--F- FTFFTFTF to
010 to nc TFTFFTFT TFTFFTFT -F-FF-F- -F-F--F- FTFTFFTF cc
020 mp nc to to to to to cc
050 cc nc cc cc cc cc to cc