Please find enclosed the brute results for the CTLCardinalityComparison 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	FTTF?FTT	F-F--T--	F-F--T--	cc	F----T--	cc	cc
03	FTTTTTTF	TTF--T--	TTF--T--	-T---T--	TTF--T--	FFFFFFFF	cc
04	to	-FTF-F--	-FTF-F--	-FTF-F--	-FTF-F--	to	cc
05	to	cc	cc	cc	to	to	cc
07	mp	cc	cc	cc	cc	to	cc
10	mp	cc	cc	cc	cc	to	cc
Dekker (P/T)
instances	greatSPN	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
010	nc	FT----T-	FT----T-	-T----T-	FT----T-	FFFFFFFF	cc
015	nc	--FT--TT	--FT--TT	------T-	to	FFFFFFFF	cc
020	nc	to	to	to	to	FFFFTFFF	cc
050	nc	-F----F-	-F----F-	-F----F-	to	cc	cc
100	nc	to	to	to	to	to	cc
200	nc	to	to	to	to	to	cc
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	FTFTTT-F	FTFTTT-F	FT-TTT-F	TFFTTF-T	FFFTTFFF	cc
10	nc	cc	cc	cc	cc	FFFFFFFF	cc
Echo (P/T)
instances	greatSPN	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
d02r09	nc	FTFF--TF	FTFF--TF	FTFF--TF	FTFF--TF	to	cc
d02r11	nc	-T----F-	-T----F-	to	-T----F-	cc	cc
d02r15	nc	-----FTT	-----FTT	to	to	to	-----TF-
d02r19	nc	------TT	------TT	to	to	to	cc
d03r03	nc	------T-	------T-	to	to	to	cc
d03r05	nc	FFFF--TT	FFFF--TT	to	FFFF----	to	cc
d03r07	nc	---T-FTT	---T-FTT	to	to	cc	-----TF-
d04r03	nc	---F--F-	---F--F-	---F--F-	---F--F-	to	cc
d05r03	nc	-----FF-	-----FF-	to	to	to	cc
Eratosthenes (P/T)
instances	greatSPN	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
010	nc	TFF---T-	TFF---T-	-F----T-	-F----T-	cc	cc
020	nc	FTT-----	FTT-----	FTT-----	FT------	FFFTFFFF	cc
050	nc	-----T--	-----T--	-----T--	-----F--	FFFTFFFF	cc
100	nc	-T-F-F--	-T-F-F--	to	-T------	FFFTFFFF	cc
200	nc	-F------	-F------	to	to	FFFTFFFF	cc
500	nc	-F-----F	-F-----F	to	to	FFFFFFFF	cc
FMS (P/T)
instances	greatSPN	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
002	FTTTFFFF	--F--FFF	--F--FFF	-----FFF	-----FFF	FFFFFFFF	cc
005	FTTT?FTF	-TF--F-F	-TF--F-F	-T---F-F	-----F-F	cc	cc
010	FTFF?TTT	-F-F-T--	-F-F-T--	---F-T--	---F-T--	cc	-----F--
020	TTFT?FTF	F-T----F	F-T----F	-------F	-------F	cc	cc
050	to	------T-	------T-	to	------T-	FFFFFFFF	cc
100	to	--T--F-T	--T--F-T	--T--F-T	-------T	FFFTFFFF	cc
200	to	F-----F-	F-----F-	F-----F-	F-------	to	cc
500	to	--TFTT-T	--TFTT-T	--TFTT-T	--TFT---	to	cc
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	FFFTFFFF	TT-T----	TT-T----	---T----	to	FFFTFFFF	cc
05	cc	to	to	to	cc	to	cc
Kanban (P/T)
instances	greatSPN	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
0005	TFTTTFFF	FFTT--F-	FFTT--F-	-FTT--F-	-FTT----	FFFTTFFF	cc
0010	FFFTFTTF	-F-T-F--	-F-T-F--	-F-T----	-F-T----	FFFFFFFF	cc
0020	FFFF?FTF	-FFF--T-	-FFF--T-	-FFF--T-	---F----	cc	cc
0050	to	---F-TFT	---F-TFT	---F-TFT	---F-TFT	cc	cc
0100	to	---TFT--	---TFT--	---TFT--	---TFT--	FFFFTFFF	cc
0200	mp	---F--FT	---F--FT	---F--FT	------F-	to	cc
0500	mp	-------T	-------T	-------T	cc	cc	cc
1000	to	---T-FTF	---T-FTF	---T-FTF	---T----	to	cc
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	cc	cc
3	nc	cc	cc	cc	cc	FFFFFFFF	cc
4	nc	cc	cc	cc	cc	FFFFTFFF	cc
5	nc	cc	cc	cc	cc	to	cc
6	nc	cc	cc	cc	cc	cc	cc
7	nc	cc	cc	cc	cc	cc	cc
8	nc	cc	cc	cc	cc	to	cc
MAPK (P/T)
instances	greatSPN	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
008	FTTTTTTT	--TT-FT-	--TT-FT-	--TT--T-	--TT--T-	FFTTTFFT	cc
020	TTFFFFFT	---F--FT	---F--FT	---F--FT	------FT	FFFFTFFF	cc
040	TTTTTFFF	cc	cc	cc	cc	FFFFFFFF	cc
080	to	-F-F----	-F-F----	-F-F----	-F-F----	FFFFTFFF	cc
160	to	-FFF-TF-	-FFF-TF-	-FFF-TF-	-FFF-TF-	to	cc
320	to	-T-T-F--	-T-T-F--	-T-T-F--	to	to	cc
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	cc	cc	cc	cc	FFFTFFFF	cc
3	nc	-------T	-------T	cc	cc	FFTTFFFF	cc
4	nc	cc	cc	cc	cc	cc	cc
5	nc	cc	cc	to	to	to	cc
6	nc	cc	cc	cc	cc	to	cc
7	nc	to	to	to	to	cc	to
8	nc	--F-----	--F-----	cc	to	cc	cc
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	to	-T----T-	-T----T-	-T----T-	-T----T-	FFFTTFFF	cc
02	TTFFFTTT	---T----	---T----	to	to	to	cc
05	FTFTTTTF	-T----FF	-T----FF	-T----FF	-T----FF	to	cc
10	FFTT?FFF	---T-FT-	---T-FT-	to	to	cc	cc
20	FTFTFTFT	cc	cc	to	to	cc	cc
50	TFTTTFFF	T-TF----	T-TF----	to	to	to	cc
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	--TF-TT-	--TF-TT-	---F--T-	--TF-TT-	FFFFFFFF	cc
3	nc	cc	cc	cc	cc	FFFTFFFF	cc
4	nc	cc	cc	cc	cc	cc	cc
5	nc	---F----	---F----	to	to	to	cc
6	nc	cc	cc	cc	cc	cc	cc
7	nc	cc	cc	cc	cc	to	cc
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	TTTTTTTF	F--F-TTF	F--F-TTF	-----TTF	F--F-TTF	FFFFTFFF	cc
000010	TTTTTFTF	-F-F-T--	-F-F-T--	cc	-F-F-T--	FFFFTFFF	cc
000020	TTFTFTTF	-----TTF	-----TTF	-----TTF	to	FFFTFFFT	cc
000050	to	cc	cc	cc	cc	FFFTFFFF	cc
000100	mp	cc	cc	cc	cc	FFFFFFFF	cc
000200	FTFF	cc	cc	cc	cc	FFFTTFFF	cc
000500	to	cc	cc	cc	cc	FFFTFFFF	cc
001000	mp	cc	cc	cc	cc	FFFTFFFF	cc
002000	mp	cc	cc	cc	cc	FFFFFFFF	cc
005000	mp	to	to	to	to	to	to
010000	cc	to	to	to	to	to	to
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	FTFT?FFT	T----FFT	T----FFT	-----FFT	T----FFT	cc	cc
10	T	-T----TF	-T----TF	-T----TF	-T----TF	to	cc
20	mp	to	to	to	to	to	cc
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	nc	---F--FF	---F--FF	---F--FF	---F--FF	cc	cc
010	nc	T-TT---T	T-TT---T	---T---T	T-TT---T	FFFFFFFF	cc
020	nc	-T-T-TTT	-T-T-TTT	-T-T-TTT	to	to	cc
050	nc	T-FF--T-	T-FF--T-	to	to	to	cc
100	nc	------FF	------FF	------FF	to	to	cc
RessAllocation (P/T)
instances	greatSPN	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
R002C002	nc	-TT--F-F	-TT--F-F	-T---F-F	-TT----F	FFFFTFFF	cc
R003C002	nc	---T--F-	---T--F-	---T--F-	------F-	FFFFFFFF	------T-
R003C003	nc	-T-T-F-T	-T-T-F-T	-T-T-F-T	-T-T-F-T	FFFTTFFF	cc
R003C005	nc	-F---F--	-F---F--	-F------	-F------	FFFFTFFF	cc
R003C010	nc	-----T--	-----T--	cc	cc	cc	cc
R003C015	nc	---F-FT-	---F-FT-	---F-FT-	---F-FT-	FFFFFFFF	cc
R003C020	nc	---T-T-T	---T-T-T	to	---T-T-T	FFFTFFFF	cc
R003C050	nc	--FF-T--	--FF-T--	to	to	FFTTTFFF	cc
R003C100	nc	---T----	---T----	---T----	---T----	FFFFFFFF	cc
R005C002	nc	---T-T-T	---T-T-T	---T-T-T	---T-T-T	cc	cc
R010C002	nc	F----F-T	F----F-T	-------T	F----F-T	FFFTTFFT	cc
R015C002	nc	T-F--F-F	T-F--F-F	--F--F-F	T-F--F-F	FFTTFFFF	cc
R020C002	nc	TF-F--F-	TF-F--F-	------F-	TF-F--F-	cc	cc
R050C002	nc	F-----T-	F-----T-	F-----T-	F-----T-	FFFFFFFF	cc
R100C002	nc	------TF	------TF	to	to	FFFFFFFT	cc
Ring (P/T)
instances	greatSPN	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
none	nc	-T----FT	-T----FT	-T----FT	------FT	FFFTTFFF	------T-
RwMutex (P/T)
instances	greatSPN	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
r0010w0010	nc	FT-T-FTT	FT-T-FTT	FT-T--T-	-T-T--T-	FFFFFFFF	cc
r0010w0020	nc	--FFTF-T	--FFTF-T	---FT--T	---FTF--	FFFFFFFF	cc
r0010w0050	nc	TF---T--	TF---T--	-F------	TF---T--	cc	cc
r0010w0100	nc	T-T--TT-	T-T--TT-	-----TT-	cc	cc	-----FF-
r0010w0500	nc	---F--F-	---F--F-	---F--F-	---F--F-	FFFFFFFF	cc
r0010w1000	nc	-F----TF	-F----TF	------T-	-F----TF	cc	cc
r0010w2000	nc	F--F--T-	F--F--T-	---F--T-	F--F--T-	cc	------F-
r0020w0010	nc	-F---FT-	-F---FT-	-F---FT-	-F----T-	to	cc
r0100w0010	nc	--TF-TTF	--TF-TTF	------T-	cc	cc	cc
r0500w0010	nc	-T---TTF	-T---TTF	-T---TTF	to	cc	-----TTF
r1000w0010	nc	-F-F-F-F	-F-F-F-F	cc	cc	cc	cc
r2000w0010	nc	FFFT--F-	FFFT--F-	-F-T----	to	cc	cc
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	FTTFTFFF	T-FT-FF-	T-FT-FF-	------F-	cc	FFFFTFFF	cc
000010	FFFF?FTF	-----T-T	-----T-T	cc	cc	cc	cc
000020	mp	T-TT-TFT	T-TT-TFT	T-TT-TFT	to	cc	cc
000050	mp	cc	cc	cc	cc	to	cc
000100	mp	cc	cc	cc	cc	cc	cc
000200	cc	cc	cc	cc	cc	cc	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	-T----TF	-T----TF	------T-	-T----TF	FFFFFFFF	cc
05	nc	-F---TF-	-F---TF-	-F----F-	-F------	FFFFTFFF	cc
10	nc	to	to	to	to	FFFFFFFF	cc
15	nc	to	to	to	to	to	cc
20	nc	to	to	to	to	cc	cc
TokenRing (Colored)
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
200	nf	nf	nf	nf	nf	nf	nf
500	nf	nf	nf	nf	nf	nf	nf
TokenRing (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