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:

• nc: the tool does not compete this examination for this model/instance,
• cc: the tool cannot compute this examination for this model/instance,
• to: the tool cannot compute this examination for this model/instance within the maximum allowed time,
• mp: the tool encountered a memory problem (stack overflow or memory full),
• nf: there is no formula available for thys type of examination (typically, this concerns P/T nets where comparing marking cardinality has no signification when there is no equivalent colored net).

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