Please find enclosed the brute results for the CTLFireability 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	FTFTTFFF	FTFT--F-	FTFT--F-	FTFT--F-	-T-T--F-	FTFTTFFF	TTTT--F-
03	FTTTTTTT	--F---TT	--F---TT	------TT	--F---TT	FTTTTTTT	------TF
04	to	--T--FF-	--T--FF-	--T--FF-	to	to	--F--TF-
05	to	-F---T--	-F---T--	-F---T--	to	to	-F---T--
07	mp	F--F----	F--F----	F--F----	cc	to	---F----
10	mp	-F----T-	-F----T-	to	to	cc	-F----T-
Dekker (P/T)
instances	greatSPN	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
010	nc	F--T-T-F	F--T-T-F	F--T-T-F	F--T-T-F	FFFTTTFF	cc
015	nc	T-----T-	T-----T-	T-----T-	T-----T-	cc	cc
020	nc	-F-T-F--	-F-T-F--	-F-T-F--	-F-T-F--	FFFTTFFF	cc
050	nc	-TT--F-F	-TT--F-F	-TT--F-F	to	to	cc
100	nc	-TT--TFT	-TT--TFT	-TT--TFT	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	--FF---T	--FF---T	--FF----	--FF---T	FFFFTFTF	to
10	nc	cc	cc	cc	cc	FFFTF	to
Echo (P/T)
instances	greatSPN	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
d02r09	nc	FFTT-TF-	FFTT-TF-	FFTT-TF-	cc	cc	FFTTFTF-
d02r11	nc	--TT----	--TT----	--TT----	---T----	to	to
d02r15	nc	--FT-F--	--FT-F--	--FT-F--	to	to	to
d02r19	nc	---T-F-F	---T-F-F	---T-F-F	---T----	to	to
d03r03	nc	T-TT---T	T-TT---T	T-TT---T	to	to	T-TT---T
d03r05	nc	TF-T-T--	TF-T-T--	TF-T-T--	to	to	TF-T-T--
d03r07	nc	FTT--T-T	FTT--T-T	FTT--T-T	to	cc	to
d04r03	nc	FT-T----	FT-T----	FT-T----	-T-T----	cc	FT-T----
d05r03	nc	FTTT--T-	FTTT--T-	FTTT--T-	to	to	to
Eratosthenes (P/T)
instances	greatSPN	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
010	nc	--F-TF-F	--F-TF-F	--F-TF-F	--F-TF-F	FTFTTFFF	--T-TF-F
020	nc	F-FF--T-	F-FF--T-	F-FF--T-	F-FF--T-	FFFFFTTF	F-TT--T-
050	nc	-FT--T-T	-FT--T-T	-FT--T-T	-FT--T-T	FFTTFTFT	-FT--T-T
100	nc	FFT---TT	FFT---TT	FFT---TT	FFT---TT	FFTTFTTT	FFT---TT
200	nc	-F-T-T--	-F-T-T--	-F-T-T--	-F-T-T--	TFFTTTFF	-F-F-T--
500	nc	FFF--F-T	FFF--F-T	FFF--F-T	FFF--F-T	FFFTFFTT	FFF-TF-T
FMS (P/T)
instances	greatSPN	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
002	FTFT?FFF	-TFT----	-TFT----	-TFT----	-TTT----	cc	-TFTF---
005	FTTTFFFT	-T-----T	-T-----T	-T-----T	-T------	FTFTTFTT	-T-----T
010	FFTFTTTT	F-TF-T-T	F-TF-T-T	F-TF-T-T	cc	FFTFFTTT	F-TFFT-T
020	FTFT?TTF	-T---TT-	-T---TT-	-T---TT-	-T---TT-	cc	-T---TT-
050	TTFT?FFF	T--T-FF-	T--T-FF-	T--T-FF-	---T--F-	cc	T--T-FF-
100	FFFTFTTF	FF-T---F	FF-T---F	FF-T---F	-F-T---T	FFFTFFFF	FF-T---F
200	to	T--F----	T--F----	T--F----	---F----	to	T--FT---
500	to	--F---F-	--F---F-	--F---F-	------F-	to	--F---F-
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	TFTFTFTF	T-FF-FT-	T-FF-FT-	T--F-FT-	to	TTTFTFTF	to
05	cc	cc	cc	cc	cc	to	cc
Kanban (P/T)
instances	greatSPN	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
0005	FFTT?TFT	-FT--TFT	-FT--TFT	-FT--TFT	-F------	cc	-FT--TFT
0010	FFFT?FFF	FF---FF-	FF---FF-	FF---FF-	FF------	cc	FF--TFF-
0020	FTFTTFFF	FT-T-F--	FT-T-F--	FT-T-F--	-----F--	FTFTFFTF	FT-T-F--
0050	to	-FF--TF-	-FF--TF-	-FF--TF-	cc	FFFFFTFT	-FF-FTF-
0100	FFTT?FFF	--T-----	--T-----	--T-----	cc	cc	--T-----
0200	mp	FF-F--TT	FF-F--TT	FF-F--TT	-F-F----	to	FF-FF-TT
0500	FFF	-TTF----	-TTF----	-TTF----	cc	to	-TTF----
1000	to	FT---TF-	FT---TF-	FT---TF-	FT------	cc	FT---TF-
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	FFFTTFFF	cc
4	nc	cc	cc	cc	cc	FFTTTFTF	cc
5	nc	cc	cc	cc	cc	to	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	FFFTFFFF	--F--F-F	--F--F-F	--F--F-F	--F--F-F	FFFTFFFF	--F-FF-F
020	FTTT?FTF	-TT---T-	-TT---T-	-TT---T-	-TT---T-	cc	-TT-T-T-
040	to	TFFT--F-	TFFT--F-	TFFT--F-	FFTT--F-	TFFTFFFF	to
080	to	-FT---FT	-FT---FT	-FT---FT	to	FFTFTFFT	-FT---FT
160	to	------TF	------TF	------TF	------TF	to	------TF
320	to	T---F--F	T---F--F	T---F--F	to	to	T---F--F
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	--FF--T-	--FF--T-	---F--T-	--FF--T-	cc	--FTF-F-
3	nc	T--F-TFF	T--F-TFF	------F-	T--F-TFF	FFFFFFFF	T--F-TTF
4	nc	to	to	to	to	to	-FT-T---
5	nc	-T---F--	-T---F--	-T---F--	to	cc	-F---T--
6	nc	-T---TT-	-T---TT-	to	to	to	-F---FF-
7	nc	to	to	to	to	cc	--F-TT-F
8	nc	to	to	to	to	cc	------FT
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	F--FT--T	F--FT--T	---F----	F--FT--T	FFTFFFTF	F---T--T
02	FFFTFFFF	FF---F--	FF---F--	FF---F--	to	to	FF---F--
05	FTFFTFTF	T--F-F-T	T--F-F-T	T--F-F-T	to	to	to
10	FTFT?FFF	F-T--TF-	F-T--TF-	F-T--TF-	to	cc	F-T--TF-
20	FFFFFFTF	T-F-----	T-F-----	T-F-----	to	cc	to
50	FFTFTTFF	-T-T--T-	-T-T--T-	-T-T--T-	-T-T--T-	cc	-T-T--T-
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	-TTF--T-	-TTF--T-	-T-F--T-	-T-F--T-	cc	-TFF--T-
3	nc	-F---F-F	-F---F-F	-F---F-F	-F---T-T	cc	to
4	nc	-----F--	-----F--	-----F--	-----F--	cc	-----T--
5	nc	cc	cc	to	to	to	F-F-----
6	nc	T--F-FT-	T--F-FT-	to	to	to	to
7	nc	--T--FT-	--T--FT-	--T--FT-	--T--FT-	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	FTTF?FTF	--T---T-	--T---T-	--T---T-	--T---T-	cc	--F-T-T-
000010	TTTT?TTT	--TT----	--TT----	--TT----	--TT----	cc	--FTF---
000020	FTTF?TTF	FT-F-TTF	FT-F-TTF	FT-F-TTF	FT-F-TTF	cc	TT-F-FTT
000050	mp	-TFF--FF	-TFF--FF	-TFF--FF	-TFF--FF	FTFFFFFF	-TTF--FT
000100	mp	-FF--F--	-FF--F--	-FF--F--	to	to	-F------
000200	mp	F----T-F	F----T-F	F----T-F	to	cc	cc
000500	to	FFTT-FT-	FFTT-FT-	FFTT-FT-	to	to	-F-T--T-
001000	mp	-F---FT-	-F---FT-	-F---FT-	to	to	cc
002000	mp	F-TT--T-	F-TT--T-	F-TT--T-	to	cc	cc
005000	mp	TT-F--TF	TT-F--TF	TT-F--TF	to	to	cc
010000	cc	-----F--	-----F--	-----F--	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	TTFFFFFF	TT---F--	TT---F--	TT---F--	TT---F--	TTFTFFFT	-T---T--
10	FFF	---T-T--	---T-T--	---T----	---T-T--	to	-----T--
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---T	--TF---T	--TF----	--TF---T	cc	--TF---F
010	nc	FFF--F-T	FFF--F-T	-F---F-T	cc	cc	to
020	nc	---F--T-	---F--T-	---F--T-	cc	to	---F--T-
050	nc	to	to	to	to	to	to
100	nc	to	to	to	to	to	to
RessAllocation (P/T)
instances	greatSPN	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
R002C002	nc	-----F-T	-----F-T	cc	-----F-T	FTFTTFTF	-----F-F
R003C002	nc	T-FT-TT-	T-FT-TT-	---T--T-	-----TT-	FFTTFFTF	T-TTTTT-
R003C003	nc	T-FT-F-F	T-FT-F-F	T-FT-F-F	T-FT-F-F	TTFTTFTF	T-FTTF-F
R003C005	nc	-TFF-F-F	-TFF-F-F	-T-F----	-T-F-F-F	FTFFTFFF	to
R003C010	nc	T-T--TFT	T-T--TFT	-----TFT	T-T--TFT	FFFFFTFT	T-T-FTFT
R003C015	nc	TTF--TF-	TTF--TF-	TTF--TF-	FTT--TF-	TTFTTTFT	TTF--TF-
R003C020	nc	FFTT-TFT	FFTT-TFT	FFTT-TFT	FFTT-TFT	FFTTFTFT	FFTT-TFT
R003C050	nc	FT-T-T--	FT-T-T--	FT-T-T--	to	to	FT-TTT--
R003C100	nc	FFTFTFT-	FFTFTFT-	FFTFTFT-	to	FFTFTFTF	FFTFTFT-
R005C002	nc	------F-	------F-	------F-	------F-	FFFTTFFF	----T-F-
R010C002	nc	F-TT---F	F-TT---F	---T---F	F-TT---F	FTFTFFFF	F-FT---F
R015C002	nc	-FF--F-T	-FF--F-T	-FF--F-T	-FF--F-T	FFFFTFFT	-FF-TF-T
R020C002	nc	T-----FF	T-----FF	------FF	T-----FT	FFFFFFFF	to
R050C002	nc	F-F-----	F-F-----	cc	to	cc	to
R100C002	nc	cc	cc	cc	cc	to	----T---
Ring (P/T)
instances	greatSPN	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
none	nc	-T-----T	-T-----T	-T-----T	to	FTFFFFFT	-T-----F
RwMutex (P/T)
instances	greatSPN	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
r0010w0010	nc	-TTF--TF	-TTF--TF	-TTF--T-	-T-F--TF	cc	-TTF--TF
r0010w0020	nc	-------T	-------T	cc	-------T	TTFTTFTF	-------F
r0010w0050	nc	T-FF-T-F	T-FF-T-F	---F-T-F	T-FF-T-F	FTTFFTFF	T-FF-T-F
r0010w0100	nc	FF-F--FF	FF-F--FF	-F-F--F-	cc	FFFFFFFT	FF-FT-FT
r0010w0500	nc	F-----F-	F-----F-	------F-	F-----F-	cc	F-----F-
r0010w1000	nc	T-T-FF-T	T-T-FF-T	cc	T-T-FF-T	FTFTTFFF	T-T-TF-T
r0010w2000	nc	F--F--F-	F--F--F-	---F--F-	to	to	F--FT-F-
r0020w0010	nc	T--T----	T--T----	T--T----	T--T----	to	T--T----
r0100w0010	nc	-TFT-TT-	-TFT-TT-	-TFT-TT-	-T-T--T-	cc	-TFTTTT-
r0500w0010	nc	-F-T----	-F-T----	-F-T----	-F-T----	cc	-F-TT---
r1000w0010	nc	F--T-FTT	F--T-FTT	F--T-FTT	------T-	cc	F--T-FTT
r2000w0010	nc	-----FTT	-----FTT	-----FTT	cc	cc	----TFTT
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	FTFT?TTT	--T----F	--T----F	cc	cc	cc	--T-----
000010	FTFT?TTT	-TFF-F--	-TFF-F--	-TFF-F--	-T-F----	cc	-TTF-T--
000020	mp	-F-F--F-	-F-F--F-	-F-F--F-	-F-F--F-	cc	-F-FT-F-
000050	mp	TTT-----	TTT-----	to	to	to	cc
000100	mp	-F-----T	-F-----T	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	---F-F--	---F-F--	---F-F--	---F----	FFFFTFTT	---F-F--
05	nc	TF---F--	TF---F--	TF---F--	-F---F--	cc	F----T--
10	nc	FT-F----	FT-F----	to	FT-F---F	cc	to
15	nc	FT-T--FT	FT-T--FT	FT-T--FT	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	FTTFTFTF	-T----FT	-T----FT	-T----F-	-T----F-	FTTFTFTF	to
010	to	-----T--	-----T--	cc	cc	FTFTTFTF	cc
020	mp	to	to	to	to	to	cc
050	cc	cc	cc	cc	cc	to	cc