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

Please find enclosed the brute results for the ReachabilityMarkingComparison 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 lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
02 nc nc nc nc nc nc nc
03 nc nc nc nc nc nc nc
04 nc nc nc nc nc nc nc
05 nc nc nc nc nc nc nc
07 nc nc nc nc nc nc nc
10 nc nc nc nc nc nc nc
CSRepetitions (P/T)
instances greatSPN lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
02 cc FFFFFTFT FFFFFTFT FFFFF-F- FFFFFTFT FFFFTFFF FFFFTTTT
03 cc TFTFFFFF TFTFFFFF -F-FFFFF TFTFFFFF FFFTFFFF to
04 cc -FFFF--- -FFFF--- -FFFF--- to to to
05 to FFFF--FF FFFF--FF to to to FFFFTTT-
07 cc FFFFF--- FFFFF--- to to to to
10 cc -----FFF -----FFF to to to FFFFFFFF
Dekker (P/T)
instances greatSPN lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
010 nf nf nf nf nf nf nf
015 nf nf nf nf nf nf nf
020 nf nf nf nf nf nf nf
050 nf nf nf nf nf nf nf
100 nf nf nf nf nf nf nf
200 nf nf nf nf nf nf nf
DotAndBoxes (Colored)
instances greatSPN lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
2 nc nc nc nc nc nc nc
3 nc nc nc nc nc nc nc
4 nc nc nc nc nc nc nc
5 nc nc nc nc nc nc nc
DrinkVendingMachine (Colored)
instances greatSPN lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
02 nc nc nc nc nc nc nc
10 nc nc nc nc nc nc nc
DrinkVendingMachine (P/T)
instances greatSPN lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
02 nc TFFFFTFT TFFFFTFT -FFFF-F- TFFFFTFT FFFTTFFF to
10 nc cc cc cc cc FFFTFFFF to
Echo (P/T)
instances greatSPN lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
d02r09 nf nf nf nf nf nf nf
d02r11 nf nf nf nf nf nf nf
d02r15 nf nf nf nf nf nf nf
d02r19 nf nf nf nf nf nf nf
d03r03 nf nf nf nf nf nf nf
d03r05 nf nf nf nf nf nf nf
d03r07 nf nf nf nf nf nf nf
d04r03 nf nf nf nf nf nf nf
d05r03 nf nf nf nf nf nf nf
Eratosthenes (P/T)
instances greatSPN lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
010 nf nf nf nf nf nf nf
020 nf nf nf nf nf nf nf
050 nf nf nf nf nf nf nf
100 nf nf nf nf nf nf nf
200 nf nf nf nf nf nf nf
500 nf nf nf nf nf nf nf
FMS (P/T)
instances greatSPN lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
002 nf nf nf nf nf nf nf
005 nf nf nf nf nf nf nf
010 nf nf nf nf nf nf nf
020 nf nf nf nf nf nf nf
050 nf nf nf nf nf nf nf
100 nf nf nf nf nf nf nf
200 nf nf nf nf nf nf nf
500 nf nf nf nf nf nf nf
GlobalRessAlloc (Colored)
instances greatSPN lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
03 nc nc nc nc nc nc nc
05 nc nc nc nc nc nc nc
06 nc nc nc nc nc nc nc
07 nc nc nc nc nc nc nc
09 nc nc nc nc nc nc nc
10 nc nc nc nc nc nc nc
11 nc nc nc nc nc nc nc
GlobalRessAlloc (P/T)
instances greatSPN lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
03 cc TFFFTTFF TFFFTTFF -FFF--FF to FFFTFFFF to
05 cc to to to ------F- to to
Kanban (P/T)
instances greatSPN lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
0005 nf nf nf nf nf nf nf
0010 nf nf nf nf nf nf nf
0020 nf nf nf nf nf nf nf
0050 nf nf nf nf nf nf nf
0100 nf nf nf nf nf nf nf
0200 nf nf nf nf nf nf nf
0500 nf nf nf nf nf nf nf
1000 nf nf nf nf nf nf nf
LamportFastMutEx (Colored)
instances greatSPN lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
2 nc nc nc nc nc nc nc
3 nc nc nc nc nc nc nc
4 nc nc nc nc nc nc nc
5 nc nc nc nc nc nc nc
6 nc nc nc nc nc nc nc
7 nc nc nc nc nc nc nc
8 nc nc nc nc nc nc nc
LamportFastMutEx (P/T)
instances greatSPN lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
2 nc cc cc cc cc FFFTFFFF FFFFFFFF
3 nc cc cc cc cc FFFTFFFF FFFFFFFF
4 nc cc cc cc cc FFFTFFFF FFFFFFFF
5 nc cc cc cc cc to FFFFFFFF
6 nc cc cc cc cc to FFFFFFFF
7 nc cc cc cc cc to FFFFFFFF
8 nc cc cc cc cc to FFFFFFF-
MAPK (P/T)
instances greatSPN lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
008 nf nf nf nf nf nf nf
020 nf nf nf nf nf nf nf
040 nf nf nf nf nf nf nf
080 nf nf nf nf nf nf nf
160 nf nf nf nf nf nf nf
320 nf nf nf nf nf nf nf
NeoElection (Colored)
instances greatSPN lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
2 nc nc nc nc nc nc nc
3 nc nc nc nc nc nc nc
4 nc nc nc nc nc nc nc
5 nc nc nc nc nc nc nc
6 nc nc nc nc nc nc nc
7 nc nc nc nc nc nc nc
8 nc nc nc nc nc nc nc
NeoElection (P/T)
instances greatSPN lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
2 nc TTTTTFFF TTTTTFFF -----FFF TTTTTFFF FFFFFFFF TTTTTFFF
3 nc TTTFFTTT TTTFFTTT ---FF--- TTTFFTTT FFFTTFFF TTTTTFTF
4 nc to to to to to TTTTTTTT
5 nc to to to to to TTTTTTTT
6 nc to to to to to FFFFFFTF
7 nc TTTTFTFT TTTTFTFT ----F-F- to to cc
8 nc to to to to to TTTTTTTT
PermAdmissibility (Colored)
instances greatSPN lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
01 nc nc nc nc nc nc nc
02 nc nc nc nc nc nc nc
05 nc nc nc nc nc nc nc
10 nc nc nc nc nc nc nc
20 nc nc nc nc nc nc nc
50 nc nc nc nc nc nc nc
PermAdmissibility (P/T)
instances greatSPN lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
01 ?????FFF TFTFTFFF TFTFTFFF -F-F-FFF cc FFFFFFFF FFFFFFFF
02 cc FFFFF-F- FFFFF-F- to to to FFTTFFFF
05 ?????FTT --FFFFFF --FFFFFF to to to FFFFTFFF
10 ?????FFF -F-F-FFF -F-F-FFF to to to FFFFFFFF
20 ?????TTT -F-FF-F- -F-FF-F- to to to to
50 cc ---F--FT ---F--FT to to to to
Peterson (Colored)
instances greatSPN lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
2 nc nc nc nc nc nc nc
3 nc nc nc nc nc nc nc
4 nc nc nc nc nc nc nc
5 nc nc nc nc nc nc nc
6 nc nc nc nc nc nc nc
7 nc nc nc nc nc nc nc
Peterson (P/T)
instances greatSPN lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
2 nc TTTFTTTT TTTFTTTT ---F---- TTTF-TTT FFFTFFFF FTTTT-T-
3 nc TFFFFTTT TFFFFTTT -FFFF--- TFFFFTTT FFFTTFFF FTFF-TTT
4 nc ----FFFF ----FFFF to to to TTTT-FF-
5 nc -F-FF-F- -F-FF-F- to to to TTTTTTTT
6 nc ------F- ------F- to to to TTTTTFFF
7 nc ---FF-F- ---FF-F- to to to FTTT----
Philosophers (Colored)
instances greatSPN lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
000005 nc nc nc nc nc nc nc
000010 nc nc nc nc nc nc nc
000020 nc nc nc nc nc nc nc
000050 nc nc nc nc nc nc nc
000100 nc nc nc nc nc nc nc
000200 nc nc nc nc nc nc nc
000500 nc nc nc nc nc nc nc
001000 nc nc nc nc nc nc nc
002000 nc nc nc nc nc nc nc
005000 nc nc nc nc nc nc nc
010000 nc nc nc nc nc nc nc
050000 nc nc nc nc nc nc nc
100000 nc nc nc nc nc nc nc
Philosophers (P/T)
instances greatSPN lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
000005 cc TTTTFFFF TTTTFFFF ----FFFF TTTTFFFF FFFFTFFF TTTTTFFF
000010 cc TFFFFTFF TFFFFTFF -FFFF-FF TFFFFTFF FFFTFFFF FFFFTTTF
000020 cc -F-FFFFF -F-FFFFF -F-FFFFF to FFFFTFFF FFFFTFFF
000050 cc -F-FF-F- -F-FF-F- -F-FF-F- to FFFTFFFF TTTTTFFF
000100 cc FFFFF-F- FFFFF-F- FFFFF-F- to FFFTTFFF FF---TTT
000200 cc FFFFF-F- FFFFF-F- FFFFF-F- to FFFFFFFF FFFFFTT-
000500 to -F-F--F- -F-F--F- to to FFFFFFFF FFFFFTTT
001000 mp -F-FFFFF -F-FFFFF -F-FFFFF to FFFFFFFF -T-T--F-
002000 mp -FFFF-F- -FFFF-F- -FFFF-F- to to cc
005000 mp -F-FF-FF -F-FF-FF FFFFF-FF to to cc
010000 cc -F-FF-F- to to to to cc
PhilosophersDyn (Colored)
instances greatSPN lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
03 nc nc nc nc nc nc nc
10 nc nc nc nc nc nc nc
20 nc nc nc nc nc nc nc
50 nc nc nc nc nc nc nc
80 nc nc nc nc nc nc nc
PhilosophersDyn (P/T)
instances greatSPN lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
03 cc TFTFFTFT TFTFFTFT -F-FF-F- TFTFFTFT FFFFFFFF FFFF-FF-
10 cc TFTFFTTT TFTFFTTT -F-FF--- TFTFFTTT to to
20 mp to to to to to to
Planning (P/T)
instances greatSPN lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
nf nf nf nf nf nf nf
Railroad (P/T)
instances greatSPN lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
005 nf nf nf nf nf nf nf
010 nf nf nf nf nf nf nf
020 nf nf nf nf nf nf nf
050 nf nf nf nf nf nf nf
100 nf nf nf nf nf nf nf
RessAllocation (P/T)
instances greatSPN lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
R002C002 nf nf nf nf nf nf nf
R003C002 nf nf nf nf nf nf nf
R003C003 nf nf nf nf nf nf nf
R003C005 nf nf nf nf nf nf nf
R003C010 nf nf nf nf nf nf nf
R003C015 nf nf nf nf nf nf nf
R003C020 nf nf nf nf nf nf nf
R003C050 nf nf nf nf nf nf nf
R003C100 nf nf nf nf nf nf nf
R005C002 nf nf nf nf nf nf nf
R010C002 nf nf nf nf nf nf nf
R015C002 nf nf nf nf nf nf nf
R020C002 nf nf nf nf nf nf nf
R050C002 nf nf nf nf nf nf nf
R100C002 nf nf nf nf nf nf nf
Ring (P/T)
instances greatSPN lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
none nf nf nf nf nf nf nf
RwMutex (P/T)
instances greatSPN lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
r0010w0010 nf nf nf nf nf nf nf
r0010w0020 nf nf nf nf nf nf nf
r0010w0050 nf nf nf nf nf nf nf
r0010w0100 nf nf nf nf nf nf nf
r0010w0500 nf nf nf nf nf nf nf
r0010w1000 nf nf nf nf nf nf nf
r0010w2000 nf nf nf nf nf nf nf
r0020w0010 nf nf nf nf nf nf nf
r0100w0010 nf nf nf nf nf nf nf
r0500w0010 nf nf nf nf nf nf nf
r1000w0010 nf nf nf nf nf nf nf
r2000w0010 nf nf nf nf nf nf nf
SharedMemory (Colored)
instances greatSPN lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
000005 nc nc nc nc nc nc nc
000010 nc nc nc nc nc nc nc
000020 nc nc nc nc nc nc nc
000050 nc nc nc nc nc nc nc
000100 nc nc nc nc nc nc nc
000200 nc nc nc nc nc nc nc
000500 nc nc nc nc nc nc nc
001000 nc nc nc nc nc nc nc
002000 nc nc nc nc nc nc nc
005000 nc nc nc nc nc nc nc
010000 nc nc nc nc nc nc nc
020000 nc nc nc nc nc nc nc
050000 nc nc nc nc nc nc nc
100000 nc nc nc nc nc nc nc
SharedMemory (P/T)
instances greatSPN lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
000005 cc TFTFTTFF TFTFTTFF -F-F--FF -F-F--F- FFFFFFFT FFFFFTTT
000010 cc TFFFFFFT TFFFFFFT -FFFFFF- -FFFFFF- FFFTTFFF FTFFTFFT
000020 mp to to to to FFFFFFFF FFFFFFFF
000050 mp to -FFFF-FF to to to cc
000100 mp to to to to to cc
000200 cc cc cc cc cc to cc
SimpleLoadBal (Colored)
instances greatSPN lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
02 nc nc nc nc nc nc nc
05 nc nc nc nc nc nc nc
10 nc nc nc nc nc nc nc
15 nc nc nc nc nc nc nc
20 nc nc nc nc nc nc nc
SimpleLoadBal (P/T)
instances greatSPN lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
02 nc TTTFFTFT TTTFFTFT ---FF-F- ---FF-F- FFFTTFFF TTTTTFFF
05 nc TFTFFTFT TFTFFTFT -F-FF-F- TFTFFTFT FFFFTFFF FFFF-FF-
10 nc to to to to FFFFFFFF to
15 nc to to to to to to
20 nc to to to to to to
TokenRing (Colored)
instances greatSPN lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
005 nc nc nc nc nc nc nc
010 nc nc nc nc nc nc nc
020 nc nc nc nc nc nc nc
050 nc nc nc nc nc nc nc
100 nc nc nc nc nc nc nc
200 nc nc nc nc nc nc nc
500 nc nc nc nc nc nc nc
TokenRing (P/T)
instances greatSPN lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
005 cc TTTFTTFT TTTFTTFT ---F--F- TTTFTTFT FFFTFFFF TTTTTTTT
010 cc TTTFTTFT TTTFTTFT ---F--F- TTTFTTFT FFFTFFFF FFF-FTTT
020 mp to to to to to FFF--FF-
050 cc to to to to to cc