Please find enclosed the brute results for the CTLMix 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	FTFTFFFF	---T---F	---T---F	---T---F	cc	FFFTTFFF	cc
03	FFFTFTTT	FF-T-FTF	FF-T-FTF	FF-T--T-	TF-T----	FFFTFFTF	cc
04	to	-F-T----	-F-T----	-F-T----	to	to	cc
05	to	-FT-----	-FT-----	-FT-----	to	to	-F------
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	FTTT---T	FTTT---T	-T-T---T	FTTT---T	FFFFTFFT	cc
015	nc	T----FFT	T----FFT	------FT	T----FFT	FFFFFFFF	cc
020	nc	-FTT-FT-	-FTT-FT-	-F-T-FT-	to	cc	cc
050	nc	FFTT--F-	FFTT--F-	FFTT--F-	to	cc	cc
100	nc	T-T---F-	T-T---F-	T-T---F-	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	-----FTF	-----FTF	cc	-----FTF	FFFTFFFF	cc
10	nc	cc	cc	cc	cc	to	cc
Echo (P/T)
instances	greatSPN	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
d02r09	nc	T--T---F	T--T---F	to	T--T---F	to	cc
d02r11	nc	-F---T--	-F---T--	-F---T--	-F------	cc	cc
d02r15	nc	---F----	---F----	to	-T-F----	cc	cc
d02r19	nc	-T---FT-	-T---FT-	to	-T---FT-	to	-----TF-
d03r03	nc	--F-----	--F-----	--F-----	--F-----	to	cc
d03r05	nc	---F----	---F----	to	---F----	cc	cc
d03r07	nc	---T-TF-	---T-TF-	---T-TF-	to	to	to
d04r03	nc	-F-F-FFT	-F-F-FFT	-F-F-FFT	-F-F-FFT	to	cc
d05r03	nc	---F----	---F----	---F----	---F----	to	to
Eratosthenes (P/T)
instances	greatSPN	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
010	nc	TTTT-F-F	TTTT-F-F	TTTT----	TTTT-F-F	FTFTFFTF	-----F-F
020	nc	F--T----	F--T----	F--T----	F--T----	FFFFFFFF	cc
050	nc	--TT-TT-	--TT-TT-	--TT-TT-	--TT-TT-	FFFFTFFF	cc
100	nc	---F----	---F----	---F----	---F----	FFFFTFTF	cc
200	nc	--TF---F	--TF---F	--TF---F	to	FFTTFFTF	-------T
500	nc	---F-TF-	---F-TF-	to	to	to	cc
FMS (P/T)
instances	greatSPN	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
002	TTFTTFTF	T-----T-	T-----T-	T-----T-	T-----T-	FFFFTFTF	------F-
005	FFFTTTTF	-F-T---T	-F-T---T	-F-T----	-F-T----	FFFTFFTF	cc
010	TTTTFFFF	FF---FF-	FF---FF-	-----FF-	cc	FFFTTFFF	cc
020	FFTFTTTF	-FT--TT-	-FT--TT-	-FT--TT-	-FT---T-	FFFFTFTF	cc
050	TFFFTFFF	TFFF--F-	TFFF--F-	TFFF--F-	TFFF--F-	FFFFFFFF	------T-
100	F	F--T--T-	F--T--T-	F--T--T-	F--T----	FFFTFFTF	cc
200	to	FT---F-F	FT---F-F	FT---F-F	-T-----F	cc	-----T--
500	to	-T-T-FT-	-T-T-FT-	-T-T-FT-	-T-T----	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	FFFTTFFF	F-TF-FF-	F-TF-FF-	-----FF-	to	FTFTTFFF	-----TT-
05	cc	to	to	to	cc	to	cc
Kanban (P/T)
instances	greatSPN	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
0005	FTTTTTTT	-TT--T-T	-TT--T-T	-TT--T-T	-----T--	FTTTFFFF	cc
0010	FTFT?FTF	TT----TF	TT----TF	-T----TF	cc	cc	------F-
0020	FTTTFFFT	------FT	------FT	------FT	------FT	FFFFFFFT	cc
0050	FTTTFTTF	--T--TT-	--T--TT-	--T--TT-	--T-----	FTFTFTTF	-----TT-
0100	to	-----F-F	-----F-F	-----F-F	cc	FFFTFFFF	cc
0200	mp	cc	cc	cc	cc	to	cc
0500	FTTF	T-------	T-------	T-------	cc	to	cc
1000	to	-F-T---T	-F-T---T	-F-T---T	-F-T----	to	-------F
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	FFFFTFTF	cc
3	nc	cc	cc	cc	cc	FFFFTFFF	cc
4	nc	cc	cc	cc	cc	FFFTFFFF	cc
5	nc	cc	cc	cc	cc	cc	cc
6	nc	cc	cc	cc	cc	to	cc
7	nc	cc	cc	cc	cc	to	cc
8	nc	cc	cc	cc	cc	cc	cc
MAPK (P/T)
instances	greatSPN	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
008	FFTFFTTF	-FTF----	-FTF----	-FTF----	-FTF----	FFTTTFFF	cc
020	TTFTTFFF	-T-T--F-	-T-T--F-	-T-T--F-	-T-T--F-	FFFTFFFF	cc
040	to	------T-	------T-	------T-	------T-	FFFFFFFF	cc
080	to	-TFF----	-TFF----	-TFF----	to	FFTTFFFF	cc
160	to	---F--F-	---F--F-	---F--F-	to	to	cc
320	to	-------T	-------T	-------T	-------T	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	FTFT----	FTFT----	cc	FTFT----	FFFFTFFF	cc
3	nc	---T--F-	---T--F-	---T--F-	------F-	cc	cc
4	nc	cc	cc	cc	cc	to	cc
5	nc	------T-	------T-	to	to	cc	cc
6	nc	cc	cc	cc	cc	cc	cc
7	nc	cc	cc	cc	cc	to	cc
8	nc	to	to	to	to	to	to
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	TTFF--F-	TTFF--F-	TTFF--F-	TTFF----	FTFFTFFF	cc
02	FTFTTTTF	-F-F---F	-F-F---F	to	to	to	cc
05	?????FFT	cc	cc	to	to	to	cc
10	FTFTFFTT	FFTF--T-	FFTF--T-	FFTF--T-	FFTF--T-	to	------T-
20	FFFT?FTF	---T----	---T----	to	to	cc	cc
50	FFTFFTFT	------TT	------TT	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	--F--TT-	--F--TT-	--F---T-	--T-----	FFFFFFTF	cc
3	nc	-----T--	-----T--	-----T--	cc	FFFTFFFF	cc
4	nc	-T----TF	-T----TF	-T----TF	-T----TF	cc	cc
5	nc	-T------	-T------	to	to	cc	cc
6	nc	--F----T	--F----T	--F----T	--F----T	to	to
7	nc	------FF	------FF	to	-------F	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	FFFTTFTF	-F----T-	-F----T-	-F----T-	-F----T-	FFTTTFTF	------F-
000010	FTFFFTTT	---F-T-T	---F-T-T	---F-T-T	---F-T-T	FTFFFFFF	cc
000020	TTFF?FTF	T--F----	T--F----	T--F----	to	cc	cc
000050	mp	cc	cc	cc	cc	FTFTFFFF	cc
000100	mp	-T-T----	-T-T----	-T-T----	to	cc	cc
000200	mp	cc	cc	cc	cc	FFFTFFFF	cc
000500	to	cc	cc	cc	cc	FFFFFFFF	cc
001000	mp	cc	cc	cc	cc	to	cc
002000	mp	---F----	---F----	---F----	to	cc	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	FTFTTFFF	-----F--	-----F--	-----F--	-----F--	FFFFFFFF	cc
10	FTTT	-----FFF	-----FFF	------F-	cc	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	--TF--F-	--TF--F-	------F-	--TF--F-	FFFFFFFF	cc
010	nc	-F---T-T	-F---T-T	-F------	-----T-T	cc	cc
020	nc	-F----TT	-F----TT	-F----TT	to	to	------FF
050	nc	-----T-F	-----T-F	-----T-F	to	to	-----F-T
100	nc	to	to	to	to	to	cc
RessAllocation (P/T)
instances	greatSPN	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
R002C002	nc	F--T-TFT	F--T-TFT	---T-TFT	F--T-TFT	FFFFTFFF	-----FT-
R003C002	nc	-FTT--F-	-FTT--F-	-FTT--F-	-FTT--F-	FFFTFFFF	cc
R003C003	nc	F----TTF	F----TTF	-----TTF	------T-	cc	cc
R003C005	nc	-F------	-F------	-F------	-F------	cc	cc
R003C010	nc	FFFF--F-	FFFF--F-	-F-F--F-	-F-F--F-	FFFFTFFF	cc
R003C015	nc	--FF---T	--FF---T	--FF---T	--FF----	FFFFFFFF	--FF----
R003C020	nc	---F----	---F----	to	---F----	FFFFTFTF	cc
R003C050	nc	---F--F-	---F--F-	to	to	FFFTFFFF	cc
R003C100	nc	TT-----F	TT-----F	TT-----F	TT-----F	to	-------T
R005C002	nc	FF-F-T--	FF-F-T--	-F-F-T--	-F-F-T--	cc	cc
R010C002	nc	-FTT-TTT	-FTT-TTT	-F-T-TTT	-FTT-TTT	FFFTFFFF	cc
R015C002	nc	FTTF-F-T	FTTF-F-T	FTTF-F-T	FTTF-F-T	FTTTTFFT	cc
R020C002	nc	T-F-F-F-	T-F-F-F-	T-F-F-F-	T-F-F-F-	FFFFTFFF	cc
R050C002	nc	cc	cc	cc	to	FFFTTFFF	cc
R100C002	nc	FFF-----	FFF-----	FFF-----	to	to	FFF-----
Ring (P/T)
instances	greatSPN	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
none	nc	-F----F-	-F----F-	-F----F-	to	FFFFFFFF	cc
RwMutex (P/T)
instances	greatSPN	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
r0010w0010	nc	TFTT-T-F	TFTT-T-F	TFTT----	TFTT----	FFFTFFFF	cc
r0010w0020	nc	F----TTT	F----TTT	-----TTT	cc	FFFTTFTF	cc
r0010w0050	nc	-T-F-T--	-T-F-T--	-T-F-T--	cc	FTFFFFFF	cc
r0010w0100	nc	-----FTT	-----FTT	------T-	cc	cc	cc
r0010w0500	nc	F-TF-F--	F-TF-F--	cc	F-TF-F--	FFFFFFFF	cc
r0010w1000	nc	-FTT-T--	-FTT-T--	-F-T----	-FTT-T--	FFFTFFFF	cc
r0010w2000	nc	-FT--T-F	-FT--T-F	-------F	to	to	cc
r0020w0010	nc	-TF---FT	-TF---FT	-TF---F-	-T----F-	to	cc
r0100w0010	nc	---T----	---T----	---T----	---T----	cc	cc
r0500w0010	nc	------T-	------T-	------T-	to	cc	------F-
r1000w0010	nc	FT-T-FFT	FT-T-FFT	---T-FFT	---T--FT	cc	-------F
r2000w0010	nc	---TFT--	---TFT--	---TF---	cc	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	FTTT?FFT	-F-F-TFF	-F-F-TFF	-F-F--F-	-F-F----	cc	cc
000010	FFFF?FTF	--TF---T	--TF---T	---F----	cc	cc	cc
000020	mp	TFT-----	TFT-----	TFT-----	to	FFFFFFFF	cc
000050	mp	cc	cc	cc	cc	cc	cc
000100	mp	-----TFT	-----TFT	-----TFT	-----TFT	cc	------FT
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	-----FT-	-----FT-	------T-	------T-	FFFFFFTF	cc
05	nc	------F-	------F-	------F-	------F-	cc	cc
10	nc	-F---FF-	-F---FF-	-F---FF-	-F------	cc	to
15	nc	to	to	to	to	to	cc
20	nc	to	to	to	to	to	cc
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	FTFTFFTF	TF---T-T	TF---T-T	-F------	-F------	FTFTFFTF	T----T-T
010	to	F-T--TT-	F-T--TT-	------T-	------T-	FTFTFFTF	cc
020	mp	to	to	to	to	cc	cc
050	cc	cc	cc	cc	cc	to	cc