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

Please find enclosed the brute results for the ReachabilityCardinalityComparison 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 FFFFFFTF 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 FFFFFFTF nc TFTFFTFT TFTFFTFT -F-FF-F- TFTFFTFT FFFFFFFT cc
03 FTFTFFFF nc TFTFFFFT TFTFFFFT -F-FFFF- TFTFFTFT FFFFTFFF cc
04 FFFFTFTF nc -F-FF-FF -F-FF-FF -F-FF-FF to to cc
05 to nc ---F-FFF ---F-FFF ---F-FFF to to cc
07 mp nc cc cc cc cc to cc
10 mp nc cc cc cc cc to cc
Dekker (P/T)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
010 nc nc TFTFTTFF TFTFTTFF -F-F--FF TFTFTTFF FFFFFFFF cc
015 nc nc TTTFFFFF TTTFFFFF ---FFFFF to FFFTTFFF cc
020 nc nc to to FFFFF-F- to FFFFTFFF cc
050 nc nc -F-FFFFF -F-FFFFF -F-FFFFF to to cc
100 nc nc -FFFFFFF -FFFFFFF -FFFFFFF to to cc
200 nc nc to to to to to cc
DotAndBoxes (Colored)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
2 nc FFFFFFTF nc nc nc nc nc nc
3 nc FFFFFFTF 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 TFFFFFFF TFFFFFFF -FFFFFFF TFFFFFFF FFFTFFFF 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 -F-FFFFF -F-FFFFF to to to cc
d02r11 nc nc FFFFFFFF FFFFFFFF FFFFFFFF FFFFF-F- to cc
d02r15 nc nc ---F-FFF ---F-FFF to to to cc
d02r19 nc nc -F-FFFFF -F-FFFFF to -F-FFFFF to -----TTT
d03r03 nc nc -----FFF -----FFF to to to cc
d03r05 nc nc -F-FF-FF -F-FF-FF to to to cc
d03r07 nc nc FFFFFFFF FFFFFFFF FFFFFFFF to to -----TT-
d04r03 nc nc -F-F--F- -F-F--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 TFTFFFFF TFTFFFFF -F-FFFFF TFTF-TFT FFFFTFFF cc
020 nc FFFFFFFF FFFFFTFF FFFFFTFF FFFFF-FF FF-FFTFT FFFTFFFF -------T
050 nc FFFF FFFFFFFF FFFFFFFF FFFFFFFF FF-F-FFF FFFTFFFF cc
100 nc FFFF to to to -F-FF--- FFFFFFFF cc
200 nc FFFFFFFF FFFFF-F- FFFFF-F- to to FFFFTFFF cc
500 nc FFFF -FFFFFFF -FFFFFFF to to FFFTTFFF cc
FMS (P/T)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
002 FFFFFFTF nc FFFFFTTT FFFFFTTT FFFFF--- -F-FF--- FFFTTFFF cc
005 FFFFFFFF nc TFFFTTFT TFFFTTFT -FFF--F- --FF-TF- FFTTFFFF cc
010 FFFFFFFF nc TFTFFFFF TFTFFFFF -F-FFFFF ------F- FFFFFFFF cc
020 FFFFFFFF nc -F-FFFFF -F-FFFFF -F-FFFFF -F-FF-F- FFFFFFFF cc
050 FFFFFFFF nc ---F-FFF ---F-FFF ---F-FFF ---F-FFF FFFTFFFF -----TTT
100 F cc -F-FFFFF -F-FFFFF -F-FFFFF -F-FFFFF FFFFFFFF cc
200 to nc -F-FFFFF -F-FFFFF -F-FFFFF -F-FF-F- to cc
500 to nc ---FFFFF ---FFFFF ---FFFFF ---FFFFF to cc
GlobalRessAlloc (Colored)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
03 nc FFFFFFTF nc nc nc nc nc nc
05 nc FFFFFFFF 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 FFFFFFTF nc FFTFFTFT FFTFFTFT FF-FF-F- to FFFTTFFF cc
05 cc nc to to to cc to cc
Kanban (P/T)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
0005 FFFFFFFF nc TFTFFTFT TFTFFTFT -F-FF-F- -F-FF-F- FFFTTFFF cc
0010 FFFFFFFF nc TFTFFFFF TFTFFFFF -F-FFFFF ---F--F- FFFTFFFF -------T
0020 FFFFFFFF nc -F-FFFFF -F-FFFFF to -F-FFFF- FFFFFFFF cc
0050 to nc -F-FFFFF -F-FFFFF -F-FFFFF ---FFFFF FFFTTFFF cc
0100 FFF nc FFFFFFFF FFFFFFFF FFFFFFFF FFFFF--- FFFTTFFF -----TTT
0200 mp nc FFFFF-FF FFFFF-FF FFFFF-FF FFFFF-FF to cc
0500 mp nc --FF--F- --FF--F- --FF--F- --FF--F- to cc
1000 to nc -F-F-FFF -F-F-FFF -F-F-FFF -------F to -----TT-
LamportFastMutEx (Colored)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
2 nc FFFFFFTF 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 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 FFFTFFFF cc
3 nc nc cc cc cc cc FFTTFFFF cc
4 nc nc cc cc cc cc FFFFFFFF 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 TTTFTFFF TTTFTFFF ---F-FFF ---F--F- FFFTFFFF cc
020 FFFFFFFF nc -FFFFFFF -FFFFFFF -FFFFFFF ---FFFFF FFFTTFFF cc
040 to nc FFFFFFFF FFFFFFFF FFFFFFFF -F-FFFFF FFFFTFFF cc
080 to nc -F-FFFFF -F-FFFFF -F-FFFFF to FFFFFFFF cc
160 to nc -F-FFFFF -F-FFFFF -F-FFFFF to to -----FF-
320 to nc --FF-FFF --FF-FFF --FF-FFF 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 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
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 cc cc cc cc FFTTFFFF cc
3 nc nc TFFFT--- TFFFT--- -FFF---- cc FFFTFFFF cc
4 nc nc -----FF- -----FF- to to to cc
5 nc nc -----FFF -----FFF -----FFF -----FFF to cc
6 nc nc to to to to to cc
7 nc nc cc cc cc cc to cc
8 nc nc to to to to to to
PermAdmissibility (Colored)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
01 nc FTFTFFFF 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 FFFFFFFF FFFFFFFF FFFFFFFF FFFFFFFF FFFFTFFF cc
02 FTFTTFTF nc -F-FFFF- -F-FFFF- to to to cc
05 TTTTFFFF nc FFFFF-F- FFFFF-F- to to to cc
10 FFFFTFFF nc to to to to to cc
20 FTFTFFTF nc -F-F--F- -F-F--F- to to cc cc
50 TTTTTFFF nc FFFFFFFF FFFFFFFF FFFFFFFF FFFFFFFF to 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 TFTFFFFF TFTFFFFF -F-FFFFF -F-F-FFF FFFTTFFF cc
3 nc nc TFTFF--- TFTFF--- -F-FF--- -F-F---- FFFFFFFF cc
4 nc nc ---FF--- ---FF--- to to to cc
5 nc nc -F-FF--- -F-FF--- to to to cc
6 nc nc cc cc cc cc to cc
7 nc nc FFFFF--- FFFFF--- FFFFF--- FFFFF--- 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 ---F-FFF FFFTFFFF cc
000010 FFFFTFFF nf TTFFFFFF TTFFFFFF --FFFFFF TTFFFFFF FFTTTFFF cc
000020 FFFFFFFF nf -F-FFFFF -F-FFFFF -F-FFFFF to FFFTFFFF cc
000050 to nf cc cc cc cc FFFTTFFF cc
000100 mp nf cc cc cc cc FFFTFFFF cc
000200 mp nf cc cc cc cc FFFTFFFF cc
000500 to nf cc cc cc cc FFFFFFFF cc
001000 mp nf cc cc cc cc FFFTTFFF cc
002000 mp nf mp mp mp mp to mp
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 TTTFTFFF TTTFTFFF ---F-FFF TTTFTFFF FFFTFFFF cc
10 mp nc TTTTFTFT TTTTFTFT ----F-F- TTTTFTFT 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 TTTFFTFT TTTFFTFT ---FF-F- TTTFFTFT FFFTTFFF cc
010 nc nc FFFFFTTT FFFFFTTT FFFFF--- FFFF---- FFFFFFFF cc
020 nc nc -FFFFFFF -FFFFFFF -FFFFFFF 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 TFFFFTFF TFFFFTFF -FFFF-FF --FFF-F- FFFTTFFF -------T
R003C002 nc nc TFFFFFFF TFFFFFFF -FFFFFFF TFFFFFF- FFFTTFFF cc
R003C003 nc nc FFFFFTFT FFFFFTFT FFFFF-F- FFFFF-F- FFFTFFFF cc
R003C005 nc nc FFFFFTFF FFFFFTFF FFFFF-FF -F-FFTFF FFFFFFFT cc
R003C010 nc nc TTTFTFFF TTTFTFFF ---F-FFF --TF--FF FFFTFFFF cc
R003C015 nc nc FFFFFFFF FFFFFFFF FFFFFFFF FFFFFFFF FFFFFFFF cc
R003C020 nc nc FFFFFFFF FFFFFFFF FFFFFFFF FFFFFFFF FFFFFFFF -----TTT
R003C050 nc nc -F-FFFFF -F-FFFFF to to FFFFFFFF cc
R003C100 nc nc -FFFFFFF -FFFFFFF to to FFFTTFFF cc
R005C002 nc nc TFTFFFFF TFTFFFFF -F-FFFFF TFTFFFFF FFFFFFFF -------T
R010C002 nc nc TTTTTTFT TTTTTTFT ------F- TTTT-TFT FFFFFFFF cc
R015C002 nc nc FFFFFFFF FFFFFFFF FFFFFFFF FFFFFFFF FFFFTFFF -------T
R020C002 nc nc TFTFFTTT TFTFFTTT -F-FF--- TFTFFTTT FFFFFFFF cc
R050C002 nc nc T-T-FFFF T-T-FFFF to to FFFFTFFF cc
R100C002 nc nc -F-FFFFF -F-FFFFF -F-FFFFF -F-FFFFF FFFFFFFF cc
Ring (P/T)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
none nc nc FFFFF-F- FFFFF-F- FFFFF-F- to FFFFFFFF cc
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--- FFFFFFFF cc
r0010w0020 nc nc TFTFTTFF TFTFTTFF -F-F--FF TFTFT--- FFFFFFFF cc
r0010w0050 nc nc TFTFFTFF TFTFFTFF -F-FF-FF -----TFF FFFFFFFF cc
r0010w0100 nc nc FFFFFFFF FFFFFFFF FFFFFFFF cc FFFTFFFF cc
r0010w0500 nc nc TFFFFTFF TFFFFTFF -FFFF-FF TF---TFF FFFTTFFF cc
r0010w1000 nc nc FFFFFTFT FFFFFTFT FFFFF-F- FFFFFTFT FFFTFFFF cc
r0010w2000 nc nc TFTFTTFF TFTFTTFF -F-F--FF to to -----TT-
r0020w0010 nc nc TTTTFFFF TTTTFFFF ----FFFF ----F-F- to cc
r0100w0010 nc nc TTTFTFFF TTTFTFFF ---F-FFF to cc cc
r0500w0010 nc nc TTTFTTFF TTTFTTFF ---F--FF ---F--F- cc cc
r1000w0010 nc nc FFFFFFFF FFFFFFFF FFFFFFFF -F-F--F- cc cc
r2000w0010 nc nc FFFFFFFF FFFFFFFF FFFFFFFF to 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 FTFFFFFT cc TTTFFTTF TTTFFTTF ---FF--F ---FF--F FFFTTFFT cc
000010 FTFTFFFF cc TTTTTFFT TTTTTFFT -----FF- to FFFFFFFF cc
000020 mp cc -FFFFFFF -FFFFFFF -FFFFFFF to FFFTTFFF cc
000050 mp cc cc cc cc cc to cc
000100 mp cc cc cc cc cc to cc
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 FTFTTFFF 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 TFFFFTFT TFFFFTFT -FFFF-F- -FFF-TFT FFFTTFFF cc
05 nc nc TFTFFFFF TFTFFFFF -F-FFFFF -F-FFFFF FFFFFFFF cc
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