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

Please find enclosed the brute results for the ReachabilityPlaceComparison 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 nc nc nc nc nc nc nc
03 nc FFFFFFFF 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 FTFTFFFF nc TTTFFFFT TTTFFFFT ---FFFF- ---FFFF- FFFTTFFF -----TT-
03 FFFFFFFF nc TTTTFFFT TTTTFFFT ----FFF- TTTTFFFT FFFFTFFF -----TT-
04 FFFTTFFF nc FFTFF--- FFTFF--- to to to cc
05 to nc -FFFF--- -FFFF--- to to to cc
07 mp nc ----F--- ----F--- to to to cc
10 mp nc ---FF-FF ---FF-FF to to to ------T-
Dekker (P/T)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
010 nc nc FFFFFTFT FFFFFTFT FFFFF-F- FFFFFTFT FFFFFFFF cc
015 nc nc TFTFFTFT TFTFFTFT -F-FF-F- to FFFFFFFF cc
020 nc nc to to to to FFFFTFFF cc
050 nc nc to to to to to cc
100 nc nc to to to to to cc
200 nc nc nc to to to to cc
DotAndBoxes (Colored)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
2 nc FFFFTFFF nc nc nc nc nc nc
3 nc FFFFFFFF 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 FFFFFFFF 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 TTTTTTFT TTTTTTFT ------F- TTTTTTFT FFFFFFFF cc
10 nc nc cc cc cc cc FFFFTFFF cc
Echo (P/T)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
d02r09 nc nc -F-FFFFF -F-FFFFF to -F-FF--- to cc
d02r11 nc nc FFFFFFFF FFFFFFFF FFFFFFFF FFFFFFFF to cc
d02r15 nc nc FFFFFFFF FFFFFFFF FFFFFFFF -------F to -------T
d02r19 nc nc -FFFF--- -FFFF--- to to to cc
d03r03 nc nc -F-FFFFF -F-FFFFF to to to -----TT-
d03r05 nc nc ----F-FF ----F-FF to to to cc
d03r07 nc nc FFFFFFFF FFFFFFFF FFFFFFFF FFFFFFFF to cc
d04r03 nc nc -FFFF-F- -FFFF-F- to to to cc
d05r03 nc nc -F-FFFFF -F-FFFFF to to to -----TTT
Eratosthenes (P/T)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
010 nc FFFFFFFF FFFFFTTT FFFFFTTT FFFFF--- FFTFFTTT FFFTFFFF cc
020 nc FFFF FFFFFFFF FFFFFFFF FFFFFFFF FF-FFFFF FFFTTFFF cc
050 nc FFFF to to to TF--FTFF FFFTFFFF cc
100 nc FFFFFFFF to to to TFFFTTF- FFTTFFFF cc
200 nc FFFF to to to to FFFFTFFF -----TTT
500 nc FFFFFFFF to to to to FFFTFFFF cc
FMS (P/T)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
002 FFFFFFTF nc TTTTFFFF TTTTFFFF ----FFFF ----FFF- FFFFTFFF -------T
005 FFFFFFFF nc TTTTFTFT TTTTFTFT ----F-F- ----F-F- FFFFTFFF cc
010 FFFFFFFF nc FFFFFFFF FFFFFFFF FFFFFFFF FFFFFFFF FFFFTFFF cc
020 FFFFFFFF nc T-T-F-FF T-T-F-FF ----F-FF ----F-FF FFFFTFFF cc
050 to nc ------FF ------FF to -------F FFFFFFFT cc
100 mp cc -F-FFFFF -F-FFFFF -F-FFFFF -F-FF-FF FFFFTFFF -------T
200 to nc FFFFFFFF FFFFFFFF FFFFFFFF -----FF- to cc
500 to nc -F-FFFFF -F-FFFFF -F-FFFFF -F-FF-F- to cc
GlobalRessAlloc (Colored)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
03 nc FFFFFFFF nc nc nc nc nc nc
05 nc FTFTFFFF nc nc nc nc nc nc
06 nc FFFFFFFF nc nc nc nc nc nc
07 nc mp nc nc nc nc nc nc
09 nc mp nc nc nc nc nc nc
10 nc mp nc nc nc nc nc nc
11 nc mp 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 TFTFFTFF TFTFFTFF -F-FF-FF to FFFTFFFF cc
05 cc nc to to to cc to to
Kanban (P/T)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
0005 FFFFFFFF nc TFTFFFFF TFTFFFFF -F-FFFFF ----F--- FFFFTFFF -----TT-
0010 FFFFFFFF nc FFFFFTFT FFFFFTFT FFFFF-F- -F-F---- FFTTTFFF cc
0020 FFFFFFFF nc -F-FFFFF -F-FFFFF to -F-FFFFF FFFFFFFF cc
0050 to nc ---FF-F- ---FF-F- ---FF-F- ---FF--- FFFTTFFF cc
0100 to nc FFFFFFFF FFFFFFFF FFFFFFFF ----F-F- FFFFTFFF cc
0200 TTTTT nc FFFFFFFF FFFFFFFF FFFFFFFF FFFFF-FF to cc
0500 mp nc cc cc cc cc to cc
1000 to nc -F-F-FFF -F-F-FFF -F-F-FFF -F-F-FF- to cc
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 FTFFFFFF nc nc nc nc nc nc
5 nc FFFFFFFF 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 -----TTT
3 nc nc cc cc cc cc FFFTFFFF cc
4 nc nc cc cc cc cc FFFTTFFF 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 FFFTFFFF nc TTTFTTTT TTTFTTTT ---F---- ---F---- FFFTFFFF cc
020 FFFFFFFF nc -FFFF-FF -FFFF-FF -FFFF-FF -FFFF-FF FFFTFFFT cc
040 to nc -F-F-FFF -F-F-FFF -F-F-FFF -F-F-FFF FFFFFFFF -----TT-
080 to nc -----FFF -----FFF -----FFF to FFFFFFFF cc
160 to nc -F-FFFFF -F-FFFFF -F-FFFFF to to cc
320 to nc --FFFFF- --FFFFF- --FFFFF- to to -------T
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 FFFF nc nc nc nc nc nc
4 nc FTFTFFTF 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
8 nc mp 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 TTTFFTTT TTTFFTTT ---FF--- TTTFFTTT FFFTTFFF cc
3 nc nc TTTFFTTT TTTFFTTT ---FF--- TTTFFTT- FFFTTFFF -------T
4 nc nc -FFF-TFT -FFF-TFT to to to cc
5 nc nc to to to to to cc
6 nc nc to to to to to cc
7 nc nc to to to to to cc
8 nc nc to to 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 FFFFFTTT FFFFFTTT FFFFF--- FFFFF--- FFFFFFFF cc
02 ?????FTT nc T--FFFFF T--FFFFF to to to cc
05 TTTTT??? nc FFFFF-F- FFFFF-F- to to to cc
10 FTFTT??? nc -F-FF-F- -F-FF-F- to to to cc
20 FTFFTFTT nc -F-FFFFF -F-FFFFF to to to cc
50 FFFTF??? 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 TTTTTTFT TTTTTTFT ------F- TTTTT-F- FFFFFFFF ------T-
3 nc nc TFTFFFFF TFTFFFFF -F-FFFFF -F-FFFFF FFFFTFFF cc
4 nc nc ---F--FF ---F--FF to to to -------T
5 nc nc FF-FF-FF FF-FF-FF to to to cc
6 nc nc FFFFF-FF FFFFF-FF to to to cc
7 nc nc -F-FF--- -F-FF--- to to 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 TFTFTFFF TFTFTFFF -F-F-FFF TFTFT--- FFFFFFFF -------T
000010 FFFTFFFF nf TTFFFTFF TTFFFTFF --FFF-FF --FFFTFF FFTTTFFF cc
000020 FFFFFFFF nf ----FFFF ----FFFF ----FFFF to FFFFTFFF cc
000050 FFFFFFFF nf -FFFFFFF -FFFFFFF -FFFFFFF FFFF-FFF FFFTTFFF cc
000100 FFFFFFFF nf -F-FF-F- -F-FF-F- -F-FF-F- to FFFFFFFF cc
000200 FFFFFFFF nf -F-FFFFF -F-FFFFF -F-FFFFF to FFFFFFFF cc
000500 to nf ---FF-FF ---FF-FF to to FFFTTFFF cc
001000 mp nf -F-FF-F- -F-FF-F- -F-FF-F- to FFFTTFFF cc
002000 mp nf -F-FF-F- -F-FF-F- to to to cc
005000 mp nf -FFF--F- -FFF--F- to to to cc
010000 cc nf to to to to to cc
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 TTTTTFFF TTTTTFFF -----FFF TTTTTFFF FFFFFFFF cc
10 mp nc TFFFFTFT TFFFFTFT -FFFF-F- TFFFFTFT to cc
20 mp nc to to to to to cc
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 FFFFFFFF FFFFFFFF FFFFFFFF FFFFFFFF FFFTTFFF cc
010 nc nc FFFFFTFT FFFFFTFT FFFFF-F- FFFFF--- FFFFTFFF cc
020 nc nc -F-FF-F- -F-FF-F- to 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 TTTTFTFF TTTTFTFF ----F-FF ----F--- FFFFTFFF cc
R003C002 nc nc TTTTFTFT TTTTFTFT ----F-F- TTTTFTFT FFFFTFFF -----TTT
R003C003 nc nc TTTTTFFF TTTTTFFF -----FFF TTTTTFFF FFFFFFFF cc
R003C005 nc nc TFTFFTTF TFTFFTTF -F-FF--F -F-FF--F FFFFTFFT cc
R003C010 nc nc TTTFTTFT TTTFTTFT ---F--F- ---F--F- FFFTFFFF cc
R003C015 nc nc TTTTTFFF TTTTTFFF -----FFF -----FFF FFFFFFFT cc
R003C020 nc nc FFFFF-F- FFFFF-F- to FFFFFTFT FFTTTFFF cc
R003C050 nc nc -F-F-FFF -F-F-FFF to to FFFFFFFF -----TT-
R003C100 nc nc -F-FFFFF -F-FFFFF to to FFFFFFFF -----TTT
R005C002 nc nc FFFFFTFF FFFFFTFF FFFFF-FF FFFFFTFF FFFFFFFF cc
R010C002 nc nc TFFFFFFF TFFFFFFF -FFFFFFF TFFFFFFF FFFTTFFF cc
R015C002 nc nc TFFFFFFF TFFFFFFF -FFFFFFF TFFFFFFF FFFTFFFF cc
R020C002 nc nc TFTFFFFF TFTFFFFF -F-FFFFF -F-FFFFF FFFFTFFF cc
R050C002 nc nc ------F- ------F- to to FFFFFFFF cc
R100C002 nc nc FFFFF-F- FFFFF-F- to FFFFFFFF FFFTFFFF cc
Ring (P/T)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
none nc nc -F-FF-FF -F-FF-FF -F-FF-FF to FFFFTFFT -------F
RwMutex (P/T)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
r0010w0010 nc nc TFTFFFFF TFTFFFFF -F-FFFFF -----FFF FFFFFFFF cc
r0010w0020 nc nc FFFFFTTT FFFFFTTT FFFFF--- FF-F-TTT FFFTFFFF cc
r0010w0050 nc nc TFTFFFFF TFTFFFFF -F-FFFFF -----FFF FFFFFFFF cc
r0010w0100 nc nc TTTTTTTT TTTTTTTT cc cc FFFFFFFF cc
r0010w0500 nc nc TFTFFTFT TFTFFTFT -F-FF-F- TFTFF-F- FFFTTFFF cc
r0010w1000 nc nc TFFFFFFF TFFFFFFF -FFFFFFF TFFF-FFF FFFTTFFF cc
r0010w2000 nc nc TFTFFTFT TFTFFTFT -F-FF-F- to to cc
r0020w0010 nc nc FFFFFFFF FFFFFFFF FFFFFFFF FF--FFFF to cc
r0100w0010 nc nc TTTTTFFF TTTTTFFF -----FFF ------F- cc cc
r0500w0010 nc nc TFFFTTFT TFFFTTFT -FFF--F- -FFF--F- cc cc
r1000w0010 nc nc TFTFFFFF TFTFFFFF -F-FFFFF ----F--- cc cc
r2000w0010 nc nc TFTFFFFF TFTFFFFF -F-FFFFF cc cc cc
SharedMemory (Colored)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
000005 nc cc nc nc nc nc nc nc
000010 nc cc nc nc nc nc nc nc
000020 nc cc nc nc nc nc nc nc
000050 nc cc nc nc nc nc nc nc
000100 nc cc nc nc nc nc nc nc
000200 nc cc nc nc nc nc nc nc
000500 nc cc nc nc nc nc nc nc
001000 nc cc nc nc nc nc nc nc
002000 nc cc nc nc nc nc nc nc
005000 nc cc nc nc nc nc nc nc
010000 nc cc nc nc nc nc nc nc
020000 nc cc nc nc nc nc nc nc
050000 nc cc nc nc nc nc nc nc
100000 nc cc 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 cc TFFFFTFT TFFFFTFT -FFFF-F- ---FF-F- FFFTTFFF cc
000010 FFFFFFFF cc TTTTFTFT TTTTFTFT ----F-F- to FFFFTFFF cc
000020 mp cc -F-FF-FF -F-FF-FF to to FFFFFFFT cc
000050 mp cc to to to to to cc
000100 mp cc to to to to to -----TTT
000200 cc cc 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 TTTTTTFT TTTTTTFT ------F- TTTTT--- FFFFFFFF cc
05 nc nc TFFFFFFF TFFFFFFF -FFFFFFF TFFF-TFT FFFTTFFF -----TTT
10 nc nc to to to to FFFFFFFF 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 nf nf nf nf nf nf nf nf
010 nf nf nf nf nf nf nf nf
020 nf nf nf nf nf nf nf nf
050 nf nf nf nf nf nf nf nf
100 nf nf nf nf nf nf nf nf
200 nf nf nf nf nf nf nf nf
500 nf nf nf nf nf nf nf nf
TokenRing (P/T)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
005 nf nf nf nf nf nf nf nf
010 nf nf nf nf nf nf nf nf
020 nf nf nf nf nf nf nf nf
050 nf nf nf nf nf nf nf nf