Please find enclosed the brute results for the ReachabilityDeadlock 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	cunf	greatSPN	ITS-Tools	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
02	nc	nc	F	nc	nc	nc	nc	nc	nc
03	nc	nc	F	nc	nc	nc	nc	nc	nc
04	nc	nc	mp	nc	nc	nc	nc	nc	nc
05	nc	nc	mp	nc	nc	nc	nc	nc	nc
07	nc	nc	mp	nc	nc	nc	nc	nc	nc
10	nc	nc	mp	nc	nc	nc	nc	nc	nc
CSRepetitions (P/T)
instances	cunf	greatSPN	ITS-Tools	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
02	FF	FF	nc	FF	FF	FF	FF	FT	F-
03	F?	FF	nc	FF	FF	FF	FF	FT	F-
04	to	FF	nc	FF	FF	FF	FF	to	F-
05	to	to	nc	FF	FF	FF	FF	to	F-
07	to	mp	nc	FF	FF	FF	FF	to	F-
10	to	mp	nc	FF	FF	FF	FF	to	F-
Dekker (P/T)
instances	cunf	greatSPN	ITS-Tools	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
010	FT	nc	nc	FT	FT	F-	FT	FT	F-
015	FT	nc	nc	FT	FT	F-	FT	FT	F-
020	FT	nc	nc	FT	FT	F-	to	FT	F-
050	FT	nc	nc	to	to	to	to	to	F-
100	FT	nc	nc	to	to	to	to	to	F-
200	nc	nc	nc	to	nc	to	to	to	F-
DotAndBoxes (Colored)
instances	cunf	greatSPN	ITS-Tools	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
2	nc	nc	F	nc	nc	nc	nc	nc	nc
3	nc	nc	F	nc	nc	nc	nc	nc	nc
4	nc	nc	F	nc	nc	nc	nc	nc	nc
5	nc	nc	mp	nc	nc	nc	nc	nc	nc
DrinkVendingMachine (Colored)
instances	cunf	greatSPN	ITS-Tools	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
02	nc	nc	F	nc	nc	nc	nc	nc	nc
10	nc	nc	F	nc	nc	nc	nc	nc	nc
DrinkVendingMachine (P/T)
instances	cunf	greatSPN	ITS-Tools	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
02	FT	nc	nc	FT	FT	F-	FT	FT	F-
10	nc	nc	nc	F-	F-	F-	F-	FT	F-
Echo (P/T)
instances	cunf	greatSPN	ITS-Tools	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
d02r09	nc	nc	nc	FF	FF	FF	FF	to	F-
d02r11	nc	nc	nc	FF	FF	FF	FF	to	F-
d02r15	nc	nc	nc	FF	FF	FF	FF	to	F-
d02r19	nc	nc	nc	FF	FF	FF	FF	to	F-
d03r03	nc	nc	nc	FF	FF	FF	FF	to	F-
d03r05	nc	nc	nc	FF	FF	FF	FF	to	F-
d03r07	nc	nc	nc	FF	FF	FF	FF	to	F-
d04r03	nc	nc	nc	FF	FF	FF	FF	to	F-
d05r03	nc	nc	nc	FF	FF	FF	FF	to	F-
Eratosthenes (P/T)
instances	cunf	greatSPN	ITS-Tools	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
010	FF	nc	nc	FF	FF	FF	FF	FT	F-
020	FF	nc	nc	FF	FF	FF	FF	FT	F-
050	FF	nc	nc	FF	FF	FF	FF	FT	F-
100	FF	nc	nc	FF	FF	FF	FF	FT	F-
200	FF	nc	nc	FF	FF	FF	FF	FT	F-
500	nc	nc	nc	FF	FF	FF	to	FT	F-
FMS (P/T)
instances	cunf	greatSPN	ITS-Tools	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
002	nc	FT	nc	FT	FT	F-	FT	FT	F-
005	nc	FT	nc	FT	FT	F-	FT	FT	F-
010	nc	FT	nc	FT	FT	F-	FT	FT	F-
020	nc	FT	nc	FT	FT	F-	FT	FT	F-
050	nc	FT	nc	FT	FT	F-	FT	FT	F-
100	nc	FT	nc	FT	FT	F-	FT	FT	F-
200	nc	to	nc	FT	FT	F-	FT	to	F-
500	nc	to	nc	FT	FT	F-	FT	to	F-
GlobalRessAlloc (Colored)
instances	cunf	greatSPN	ITS-Tools	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
03	nc	nc	F	nc	nc	nc	nc	nc	nc
05	nc	nc	F	nc	nc	nc	nc	nc	nc
06	nc	nc	F	nc	nc	nc	nc	nc	nc
07	nc	nc	mp	nc	nc	nc	nc	nc	nc
09	nc	nc	mp	nc	nc	nc	nc	nc	nc
10	nc	nc	mp	nc	nc	nc	nc	nc	nc
11	nc	nc	mp	nc	nc	nc	nc	nc	nc
GlobalRessAlloc (P/T)
instances	cunf	greatSPN	ITS-Tools	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
03	F?	FT	nc	FT	FT	F-	FT	FT	F-
05	nc	cc	nc	to	to	to	F-	to	F-
Kanban (P/T)
instances	cunf	greatSPN	ITS-Tools	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
0005	nc	FT	nc	FT	FT	F-	FT	FT	F-
0010	nc	FT	nc	FT	FT	F-	FT	FT	F-
0020	nc	FT	nc	FT	FT	F-	FT	FT	F-
0050	nc	FT	nc	FT	FT	F-	FT	FT	F-
0100	nc	FT	nc	F-	F-	F-	FT	FT	F-
0200	nc	T	nc	F-	F-	F-	FT	to	F-
0500	nc	T	nc	F-	F-	F-	FT	to	F-
1000	nc	to	nc	F-	F-	F-	FT	to	F-
LamportFastMutEx (Colored)
instances	cunf	greatSPN	ITS-Tools	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
2	nc	nc	F	nc	nc	nc	nc	nc	nc
3	nc	nc	F	nc	nc	nc	nc	nc	nc
4	nc	nc	F	nc	nc	nc	nc	nc	nc
5	nc	nc	F	nc	nc	nc	nc	nc	nc
6	nc	nc	mp	nc	nc	nc	nc	nc	nc
7	nc	nc	mp	nc	nc	nc	nc	nc	nc
8	nc	nc	mp	nc	nc	nc	nc	nc	nc
LamportFastMutEx (P/T)
instances	cunf	greatSPN	ITS-Tools	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
2	FT	nc	nc	FT	FT	F-	FT	FT	F-
3	FT	nc	nc	FT	FT	F-	FT	FT	F-
4	F?	nc	nc	FT	FT	F-	FT	FT	F-
5	to	nc	nc	F-	F-	to	FT	to	F-
6	to	nc	nc	F-	F-	to	to	to	F-
7	to	nc	nc	F-	F-	to	to	to	F-
8	to	nc	nc	to	to	to	to	to	F-
MAPK (P/T)
instances	cunf	greatSPN	ITS-Tools	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
008	nc	FT	nc	FT	FT	F-	FT	FT	F-
020	nc	FT	nc	F-	F-	F-	FT	FT	F-
040	nc	FT	nc	F-	F-	F-	FT	FT	F-
080	nc	to	nc	F-	F-	F-	to	FT	F-
160	nc	to	nc	F-	F-	F-	to	to	F-
320	nc	to	nc	F-	F-	F-	to	to	F-
NeoElection (Colored)
instances	cunf	greatSPN	ITS-Tools	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
2	nc	nc	F	nc	nc	nc	nc	nc	nc
3	nc	nc	F	nc	nc	nc	nc	nc	nc
4	nc	nc	F	nc	nc	nc	nc	nc	nc
5	nc	nc	mp	nc	nc	nc	nc	nc	nc
6	nc	nc	mp	nc	nc	nc	nc	nc	nc
7	nc	nc	mp	nc	nc	nc	nc	nc	nc
8	nc	nc	mp	nc	nc	nc	nc	nc	nc
NeoElection (P/T)
instances	cunf	greatSPN	ITS-Tools	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
2	FF	nc	nc	FF	FF	FF	FF	FT	F-
3	FF	nc	nc	FF	FF	FF	FF	FT	F-
4	nc	nc	nc	FF	FF	FF	FF	to	F-
5	nc	nc	nc	FF	FF	FF	FF	to	F-
6	nc	nc	nc	FF	FF	FF	FF	to	F-
7	nc	nc	nc	FF	FF	FF	FF	to	F-
8	nc	nc	nc	FF	FF	FF	FF	to	F-
PermAdmissibility (Colored)
instances	cunf	greatSPN	ITS-Tools	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
01	nc	nc	F	nc	nc	nc	nc	nc	nc
02	nc	nc	mp	nc	nc	nc	nc	nc	nc
05	nc	nc	mp	nc	nc	nc	nc	nc	nc
10	nc	nc	mp	nc	nc	nc	nc	nc	nc
20	nc	nc	mp	nc	nc	nc	nc	nc	nc
50	nc	nc	mp	nc	nc	nc	nc	nc	nc
PermAdmissibility (P/T)
instances	cunf	greatSPN	ITS-Tools	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
01	FF	FF	nc	FF	FF	FF	FF	FT	F-
02	nc	TF	nc	FF	FF	FF	FF	to	F-
05	nc	TF	nc	FF	FF	FF	FF	to	F-
10	nc	TF	nc	FF	FF	FF	FF	to	F-
20	nc	TF	nc	FF	FF	FF	FF	to	F-
50	nc	TF	nc	FF	FF	FF	FF	to	F-
Peterson (Colored)
instances	cunf	greatSPN	ITS-Tools	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
2	nc	nc	F	nc	nc	nc	nc	nc	nc
3	nc	nc	F	nc	nc	nc	nc	nc	nc
4	nc	nc	mp	nc	nc	nc	nc	nc	nc
5	nc	nc	mp	nc	nc	nc	nc	nc	nc
6	nc	nc	mp	nc	nc	nc	nc	nc	nc
7	nc	nc	mp	nc	nc	nc	nc	nc	nc
Peterson (P/T)
instances	cunf	greatSPN	ITS-Tools	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
2	FT	nc	nc	FT	FT	F-	FT	FT	F-
3	FT	nc	nc	FT	FT	F-	FT	FT	F-
4	nc	nc	nc	F-	F-	F-	to	to	F-
5	to	nc	nc	F-	F-	to	to	to	F-
6	to	nc	nc	F-	F-	to	F-	to	F-
7	to	nc	nc	F-	F-	to	F-	to	F-
Philosophers (Colored)
instances	cunf	greatSPN	ITS-Tools	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
000005	nc	nc	nc	nc	nc	nc	nc	nc	nc
000010	nc	nc	nc	nc	nc	nc	nc	nc	nc
000020	nc	nc	nc	nc	nc	nc	nc	nc	nc
000050	nc	nc	nc	nc	nc	nc	nc	nc	nc
000100	nc	nc	nc	nc	nc	nc	nc	nc	nc
000200	nc	nc	nc	nc	nc	nc	nc	nc	nc
000500	nc	nc	nc	nc	nc	nc	nc	nc	nc
001000	nc	nc	nc	nc	nc	nc	nc	nc	nc
002000	nc	nc	nc	nc	nc	nc	nc	nc	nc
005000	nc	nc	nc	nc	nc	nc	nc	nc	nc
010000	nc	nc	nc	nc	nc	nc	nc	nc	nc
050000	nc	nc	nc	nc	nc	nc	nc	nc	nc
100000	nc	nc	nc	nc	nc	nc	nc	nc	nc
Philosophers (P/T)
instances	cunf	greatSPN	ITS-Tools	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
000005	FF	FF	nf	FF	FF	FF	FF	FT	F-
000010	FF	FF	nf	FF	FF	FF	FF	FT	F-
000020	FF	FF	nf	FF	FF	FF	FF	FT	F-
000050	FF	FF	nf	FF	FF	FF	FF	FT	F-
000100	FF	to	nf	FF	FF	FF	FF	FT	F-
000200	FF	to	nf	FF	FF	FF	FF	FT	F-
000500	FF	to	nf	FF	FF	FF	to	FT	F-
001000	FF	mp	nf	FF	FF	FF	to	FT	F-
002000	FF	mp	nf	FF	FF	FF	to	to	F-
005000	nc	mp	nf	FF	FF	FF	to	to	F-
010000	nc	cc	nf	FF	FF	FF	to	to	F-
PhilosophersDyn (Colored)
instances	cunf	greatSPN	ITS-Tools	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
03	nc	nc	nc	nc	nc	nc	nc	nc	nc
10	nc	nc	nc	nc	nc	nc	nc	nc	nc
20	nc	nc	nc	nc	nc	nc	nc	nc	nc
50	nc	nc	nc	nc	nc	nc	nc	nc	nc
80	nc	nc	nc	nc	nc	nc	nc	nc	nc
PhilosophersDyn (P/T)
instances	cunf	greatSPN	ITS-Tools	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
03	to	FF	nc	FF	FF	FF	FF	FT	F-
10	nc	mp	nc	FF	FF	FF	FF	to	F-
20	to	mp	nc	FF	FF	FF	FF	to	F-
Planning (P/T)
instances	cunf	greatSPN	ITS-Tools	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
nf	nf	nf	nf	nf	nf	nf	nf	nf
Railroad (P/T)
instances	cunf	greatSPN	ITS-Tools	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
005	FT	nc	nc	FT	FT	F-	FT	FT	F-
010	FT	nc	nc	FT	FT	F-	FT	FT	F-
020	to	nc	nc	F-	F-	to	to	to	F-
050	to	nc	nc	to	to	to	to	to	F-
100	nc	nc	nc	to	to	to	to	to	F-
RessAllocation (P/T)
instances	cunf	greatSPN	ITS-Tools	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
R002C002	FF	nc	nc	FF	FF	FF	FF	FT	F-
R003C002	FF	nc	nc	FF	FF	FF	FF	FT	F-
R003C003	FF	nc	nc	FF	FF	FF	FF	FT	F-
R003C005	FF	nc	nc	FF	FF	FF	FF	FT	F-
R003C010	FF	nc	nc	FF	FF	FF	FF	FT	F-
R003C015	FF	nc	nc	FF	FF	FF	FF	FT	F-
R003C020	FF	nc	nc	FF	FF	FF	FF	FT	F-
R003C050	FF	nc	nc	FF	FF	FF	FF	FT	F-
R003C100	FF	nc	nc	FF	FF	FF	FF	FT	F-
R005C002	FF	nc	nc	FF	FF	FF	FF	FT	F-
R010C002	FF	nc	nc	FF	FF	FF	FF	FT	F-
R015C002	FF	nc	nc	FF	FF	FF	FF	FT	F-
R020C002	FF	nc	nc	FF	FF	FF	FF	FT	F-
R050C002	FF	nc	nc	FF	FF	FF	FF	FT	F-
R100C002	F?	nc	nc	FF	FF	FF	FF	FT	F-
Ring (P/T)
instances	cunf	greatSPN	ITS-Tools	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
none	nc	nc	nc	F-	F-	F-	to	FT	F-
RwMutex (P/T)
instances	cunf	greatSPN	ITS-Tools	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
r0010w0010	FT	nc	nc	FT	FT	F-	FT	FT	F-
r0010w0020	FT	nc	nc	FT	FT	F-	FT	FT	F-
r0010w0050	FT	nc	nc	FT	FT	F-	FT	FT	F-
r0010w0100	FT	nc	nc	FT	FT	F-	FT	FT	F-
r0010w0500	FT	nc	nc	FT	FT	F-	FT	FT	F-
r0010w1000	FT	nc	nc	FT	FT	F-	FT	FT	F-
r0010w2000	FT	nc	nc	FT	FT	F-	FT	to	F-
r0020w0010	FT	nc	nc	FT	FT	F-	FT	FT	F-
r0100w0010	FT	nc	nc	FT	FT	F-	FT	cc	F-
r0500w0010	FT	nc	nc	FT	FT	F-	FT	cc	F-
r1000w0010	FT	nc	nc	FT	FT	F-	FT	cc	F-
r2000w0010	FT	nc	nc	FT	FT	F-	FT	cc	F-
SharedMemory (Colored)
instances	cunf	greatSPN	ITS-Tools	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
000005	nc	nc	nc	nc	nc	nc	nc	nc	nc
000010	nc	nc	nc	nc	nc	nc	nc	nc	nc
000020	nc	nc	nc	nc	nc	nc	nc	nc	nc
000050	nc	nc	nc	nc	nc	nc	nc	nc	nc
000100	nc	nc	nc	nc	nc	nc	nc	nc	nc
000200	nc	nc	nc	nc	nc	nc	nc	nc	nc
000500	nc	nc	nc	nc	nc	nc	nc	nc	nc
001000	nc	nc	nc	nc	nc	nc	nc	nc	nc
002000	nc	nc	nc	nc	nc	nc	nc	nc	nc
005000	nc	nc	nc	nc	nc	nc	nc	nc	nc
010000	nc	nc	nc	nc	nc	nc	nc	nc	nc
020000	nc	nc	nc	nc	nc	nc	nc	nc	nc
050000	nc	nc	nc	nc	nc	nc	nc	nc	nc
100000	nc	nc	nc	nc	nc	nc	nc	nc	nc
SharedMemory (P/T)
instances	cunf	greatSPN	ITS-Tools	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
000005	FT	FT	nc	FT	FT	F-	FT	FT	F-
000010	FT	FT	nc	FT	FT	F-	FT	FT	F-
000020	FT	mp	nc	F-	F-	to	to	FT	F-
000050	FT	mp	nc	F-	F-	to	to	to	F-
000100	FT	mp	nc	F-	F-	to	to	to	F-
000200	FT	cc	nc	F-	F-	F-	F-	to	F-
SimpleLoadBal (Colored)
instances	cunf	greatSPN	ITS-Tools	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
02	nc	nc	F	nc	nc	nc	nc	nc	nc
05	nc	nc	F	nc	nc	nc	nc	nc	nc
10	nc	nc	F	nc	nc	nc	nc	nc	nc
15	nc	nc	mp	nc	nc	nc	nc	nc	nc
20	nc	nc	mp	nc	nc	nc	nc	nc	nc
SimpleLoadBal (P/T)
instances	cunf	greatSPN	ITS-Tools	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
02	FT	nc	nc	FT	FT	F-	FT	FT	F-
05	FT	nc	nc	FT	FT	F-	FT	FT	F-
10	to	nc	nc	FT	FT	F-	FT	FT	F-
15	to	nc	nc	to	to	to	to	to	F-
20	to	nc	nc	to	to	to	to	to	F-
TokenRing (Colored)
instances	cunf	greatSPN	ITS-Tools	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
005	nc	nc	nc	nc	nc	nc	nc	nc	nc
010	nc	nc	nc	nc	nc	nc	nc	nc	nc
020	nc	nc	nc	nc	nc	nc	nc	nc	nc
050	nc	nc	nc	nc	nc	nc	nc	nc	nc
100	nc	nc	nc	nc	nc	nc	nc	nc	nc
200	nc	nc	nc	nc	nc	nc	nc	nc	nc
500	nc	nc	nc	nc	nc	nc	nc	nc	nc
TokenRing (P/T)
instances	cunf	greatSPN	ITS-Tools	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
005	FT	FT	nc	FT	FT	F-	FT	FT	F-
010	FT	to	nc	FT	FT	F-	FT	FT	F-
020	nc	mp	nc	to	to	to	to	to	F-
050	nc	cc	nc	to	to	to	to	to	F-