Please find enclosed the brute results for the LTLMix 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	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	neco	sara
02	nc	nc	nc	nc	nc	nc
03	nc	nc	nc	nc	nc	nc
04	nc	nc	nc	nc	nc	nc
05	nc	nc	nc	nc	nc	nc
07	nc	nc	nc	nc	nc	nc
10	nc	nc	nc	nc	nc	nc
CSRepetitions (P/T)
instances	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	neco	sara
02	cc	cc	cc	cc	FFFFTFFF	cc
03	cc	cc	cc	cc	FFFTTTTT	cc
04	cc	cc	cc	cc	to	cc
05	cc	cc	cc	cc	cc	cc
07	cc	cc	cc	cc	cc	cc
10	cc	cc	cc	cc	cc	cc
Dekker (P/T)
instances	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	neco	sara
010	cc	cc	cc	cc	FFFFFFTF	cc
015	cc	cc	cc	cc	FTFTTTTT	cc
020	cc	cc	cc	cc	FFFTFFFF	cc
050	cc	cc	cc	cc	cc	cc
100	cc	cc	cc	cc	cc	cc
200	cc	nc	cc	cc	cc	cc
DotAndBoxes (Colored)
instances	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	neco	sara
2	nc	nc	nc	nc	nc	nc
3	nc	nc	nc	nc	nc	nc
4	nc	nc	nc	nc	nc	nc
5	nc	nc	nc	nc	nc	nc
DrinkVendingMachine (Colored)
instances	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	neco	sara
02	nc	nc	nc	nc	nc	nc
10	nc	nc	nc	nc	nc	nc
DrinkVendingMachine (P/T)
instances	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	neco	sara
02	cc	cc	cc	cc	nc	cc
10	cc	cc	cc	cc	nc	cc
Echo (P/T)
instances	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	neco	sara
d02r09	cc	cc	cc	cc	nc	cc
d02r11	cc	cc	cc	cc	nc	cc
d02r15	cc	cc	cc	cc	nc	cc
d02r19	cc	cc	cc	cc	nc	cc
d03r03	cc	cc	cc	cc	nc	cc
d03r05	cc	cc	cc	cc	nc	cc
d03r07	cc	cc	cc	cc	nc	cc
d04r03	cc	cc	cc	cc	nc	cc
d05r03	cc	cc	cc	cc	nc	cc
Eratosthenes (P/T)
instances	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	neco	sara
010	cc	cc	cc	cc	FTFTFFTF	cc
020	cc	cc	cc	cc	FTTTFFTF	cc
050	cc	cc	cc	cc	TTFTTFTF	cc
100	cc	cc	cc	cc	cc	cc
200	cc	cc	cc	cc	cc	cc
500	cc	cc	cc	cc	cc	cc
FMS (P/T)
instances	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	neco	sara
002	cc	cc	cc	cc	FTFTFFFF	cc
005	cc	cc	cc	cc	FTFTTFFF	cc
010	cc	cc	cc	cc	FFFTTFTF	cc
020	cc	cc	cc	cc	FFFFFFFF	cc
050	cc	cc	cc	cc	cc	cc
100	cc	cc	cc	cc	cc	cc
200	cc	cc	cc	cc	cc	cc
500	cc	cc	cc	cc	cc	cc
GlobalRessAlloc (Colored)
instances	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	neco	sara
03	nc	nc	nc	nc	nc	nc
05	nc	nc	nc	nc	nc	nc
06	nc	nc	nc	nc	nc	nc
07	nc	nc	nc	nc	nc	nc
09	nc	nc	nc	nc	nc	nc
10	nc	nc	nc	nc	nc	nc
11	nc	nc	nc	nc	nc	nc
GlobalRessAlloc (P/T)
instances	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	neco	sara
03	cc	cc	cc	cc	nc	cc
05	cc	cc	cc	cc	nc	cc
Kanban (P/T)
instances	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	neco	sara
0005	cc	cc	cc	cc	TTTTFTTT	cc
0010	cc	cc	cc	cc	FFFTTFFF	cc
0020	cc	cc	cc	cc	FFFTFFFF	cc
0050	cc	cc	cc	cc	cc	cc
0100	cc	cc	cc	cc	cc	cc
0200	cc	cc	cc	cc	cc	cc
0500	cc	cc	cc	cc	cc	cc
1000	cc	cc	cc	cc	cc	cc
LamportFastMutEx (Colored)
instances	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	neco	sara
2	nc	nc	nc	nc	nc	nc
3	nc	nc	nc	nc	nc	nc
4	nc	nc	nc	nc	nc	nc
5	nc	nc	nc	nc	nc	nc
6	nc	nc	nc	nc	nc	nc
7	nc	nc	nc	nc	nc	nc
8	nc	nc	nc	nc	nc	nc
LamportFastMutEx (P/T)
instances	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	neco	sara
2	cc	cc	cc	cc	FFFFTFFF	cc
3	cc	cc	cc	cc	FFFFTFFF	cc
4	cc	cc	cc	cc	to	cc
5	cc	cc	cc	cc	FFFFTTTF	cc
6	cc	cc	cc	cc	FTFTFFFF	cc
7	cc	cc	cc	cc	to	cc
8	cc	cc	cc	cc	to	cc
MAPK (P/T)
instances	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	neco	sara
008	cc	cc	cc	cc	FFFFFFFF	cc
020	cc	cc	cc	cc	FTFTFFFF	cc
040	cc	cc	cc	cc	cc	cc
080	cc	cc	cc	cc	cc	cc
160	cc	cc	cc	cc	cc	cc
320	cc	cc	cc	cc	cc	cc
NeoElection (Colored)
instances	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	neco	sara
2	nc	nc	nc	nc	nc	nc
3	nc	nc	nc	nc	nc	nc
4	nc	nc	nc	nc	nc	nc
5	nc	nc	nc	nc	nc	nc
6	nc	nc	nc	nc	nc	nc
7	nc	nc	nc	nc	nc	nc
8	nc	nc	nc	nc	nc	nc
NeoElection (P/T)
instances	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	neco	sara
2	cc	cc	cc	cc	FFFFTFFF	cc
3	cc	cc	cc	cc	cc	cc
4	cc	cc	cc	cc	cc	cc
5	cc	cc	cc	cc	cc	cc
6	cc	cc	cc	cc	cc	cc
7	cc	cc	cc	cc	cc	cc
8	to	to	to	to	cc	to
PermAdmissibility (Colored)
instances	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	neco	sara
01	nc	nc	nc	nc	nc	nc
02	nc	nc	nc	nc	nc	nc
05	nc	nc	nc	nc	nc	nc
10	nc	nc	nc	nc	nc	nc
20	nc	nc	nc	nc	nc	nc
50	nc	nc	nc	nc	nc	nc
PermAdmissibility (P/T)
instances	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	neco	sara
01	cc	cc	cc	cc	nc	cc
02	cc	cc	cc	cc	nc	cc
05	cc	cc	cc	cc	nc	cc
10	cc	cc	cc	cc	nc	cc
20	cc	cc	cc	cc	nc	cc
50	cc	cc	cc	cc	nc	cc
Peterson (Colored)
instances	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	neco	sara
2	nc	nc	nc	nc	nc	nc
3	nc	nc	nc	nc	nc	nc
4	nc	nc	nc	nc	nc	nc
5	nc	nc	nc	nc	nc	nc
6	nc	nc	nc	nc	nc	nc
7	nc	nc	nc	nc	nc	nc
Peterson (P/T)
instances	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	neco	sara
2	cc	cc	cc	cc	FFFTTFFF	cc
3	cc	cc	cc	cc	to	cc
4	cc	cc	cc	cc	cc	cc
5	cc	cc	cc	cc	cc	cc
6	cc	cc	cc	cc	cc	cc
7	cc	cc	cc	cc	cc	cc
Philosophers (Colored)
instances	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	neco	sara
000005	nc	nc	nc	nc	nc	nc
000010	nc	nc	nc	nc	nc	nc
000020	nc	nc	nc	nc	nc	nc
000050	nc	nc	nc	nc	nc	nc
000100	nc	nc	nc	nc	nc	nc
000200	nc	nc	nc	nc	nc	nc
000500	nc	nc	nc	nc	nc	nc
001000	nc	nc	nc	nc	nc	nc
002000	nc	nc	nc	nc	nc	nc
005000	nc	nc	nc	nc	nc	nc
010000	nc	nc	nc	nc	nc	nc
050000	nc	nc	nc	nc	nc	nc
100000	nc	nc	nc	nc	nc	nc
Philosophers (P/T)
instances	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	neco	sara
000005	cc	cc	cc	cc	TTFTFFFF	cc
000010	cc	cc	cc	cc	FTFFTFFF	cc
000020	cc	cc	cc	cc	FFFFFFFF	cc
000050	cc	cc	cc	cc	cc	cc
000100	cc	cc	cc	cc	cc	cc
000200	cc	cc	cc	cc	cc	cc
000500	cc	cc	cc	cc	cc	cc
001000	cc	cc	cc	cc	cc	cc
002000	cc	cc	cc	cc	cc	cc
005000	to	to	to	to	cc	to
010000	cc	cc	cc	cc	cc	cc
PhilosophersDyn (Colored)
instances	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	neco	sara
03	nc	nc	nc	nc	nc	nc
10	nc	nc	nc	nc	nc	nc
20	nc	nc	nc	nc	nc	nc
50	nc	nc	nc	nc	nc	nc
80	nc	nc	nc	nc	nc	nc
PhilosophersDyn (P/T)
instances	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	neco	sara
03	cc	cc	cc	cc	FTFTFFFF	cc
10	cc	cc	cc	cc	cc	cc
20	cc	cc	cc	cc	cc	cc
Planning (P/T)
instances	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	neco	sara
nf	nf	nf	nf	nf	nf
Railroad (P/T)
instances	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	neco	sara
005	cc	cc	cc	cc	FFFTTFFF	cc
010	cc	cc	cc	cc	FTFTFFFF	cc
020	cc	cc	cc	cc	FTFTTFFF	cc
050	cc	cc	cc	cc	cc	cc
100	cc	cc	cc	cc	cc	cc
RessAllocation (P/T)
instances	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	neco	sara
R002C002	cc	cc	cc	cc	FTTTFFFF	cc
R003C002	cc	cc	cc	cc	FFFTFFTF	cc
R003C003	cc	cc	cc	cc	TTFTTTTF	cc
R003C005	cc	cc	cc	cc	FFFFFFFF	cc
R003C010	cc	cc	cc	cc	FFFFFTTF	cc
R003C015	cc	cc	cc	cc	FTTTFFTF	cc
R003C020	cc	cc	cc	cc	FFFFFFTF	cc
R003C050	cc	cc	cc	cc	FTFFTFFF	cc
R003C100	cc	cc	cc	cc	FFFFTFFF	cc
R005C002	cc	cc	cc	cc	FTFTTFFF	cc
R010C002	cc	cc	cc	cc	TTFTFFTF	cc
R015C002	cc	cc	cc	cc	FTFTTFFF	cc
R020C002	cc	cc	cc	cc	FTTTFFFF	cc
R050C002	cc	cc	cc	cc	FTFFTFFF	cc
R100C002	cc	cc	cc	cc	FTFTTFFF	cc
Ring (P/T)
instances	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	neco	sara
none	cc	cc	cc	cc	nc	cc
RwMutex (P/T)
instances	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	neco	sara
r0010w0010	cc	cc	cc	cc	FTFTTFTF	cc
r0010w0020	cc	cc	cc	cc	FFFFTTTT	cc
r0010w0050	cc	cc	cc	cc	FTFTFTTT	cc
r0010w0100	cc	cc	cc	cc	FFFTFFTF	cc
r0010w0500	cc	cc	cc	cc	cc	cc
r0010w1000	cc	cc	cc	cc	cc	cc
r0010w2000	cc	cc	cc	cc	cc	cc
r0020w0010	cc	cc	cc	cc	TTTTTFFF	cc
r0100w0010	cc	cc	cc	cc	FTTTFTTF	cc
r0500w0010	cc	cc	cc	cc	cc	cc
r1000w0010	cc	cc	cc	cc	cc	cc
r2000w0010	cc	cc	cc	cc	cc	cc
SharedMemory (Colored)
instances	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	neco	sara
000005	nc	nc	nc	nc	nc	nc
000010	nc	nc	nc	nc	nc	nc
000020	nc	nc	nc	nc	nc	nc
000050	nc	nc	nc	nc	nc	nc
000100	nc	nc	nc	nc	nc	nc
000200	nc	nc	nc	nc	nc	nc
000500	nc	nc	nc	nc	nc	nc
001000	nc	nc	nc	nc	nc	nc
002000	nc	nc	nc	nc	nc	nc
005000	nc	nc	nc	nc	nc	nc
010000	nc	nc	nc	nc	nc	nc
020000	nc	nc	nc	nc	nc	nc
050000	nc	nc	nc	nc	nc	nc
100000	nc	nc	nc	nc	nc	nc
SharedMemory (P/T)
instances	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	neco	sara
000005	cc	cc	cc	cc	FFFTFFFF	cc
000010	cc	cc	cc	cc	FFFTTFFF	cc
000020	cc	cc	cc	cc	cc	cc
000050	cc	cc	cc	cc	cc	cc
000100	cc	cc	cc	cc	cc	cc
000200	cc	cc	cc	cc	cc	cc
SimpleLoadBal (Colored)
instances	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	neco	sara
02	nc	nc	nc	nc	nc	nc
05	nc	nc	nc	nc	nc	nc
10	nc	nc	nc	nc	nc	nc
15	nc	nc	nc	nc	nc	nc
20	nc	nc	nc	nc	nc	nc
SimpleLoadBal (P/T)
instances	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	neco	sara
02	cc	cc	cc	cc	FFFFFFFF	cc
05	cc	cc	cc	cc	FTFTTFTF	cc
10	cc	cc	cc	cc	to	cc
15	cc	cc	cc	cc	FFFFTFFF	cc
20	cc	cc	cc	cc	cc	cc
TokenRing (Colored)
instances	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	neco	sara
005	nc	nc	nc	nc	nc	nc
010	nc	nc	nc	nc	nc	nc
020	nc	nc	nc	nc	nc	nc
050	nc	nc	nc	nc	nc	nc
100	nc	nc	nc	nc	nc	nc
200	nc	nc	nc	nc	nc	nc
500	nc	nc	nc	nc	nc	nc
TokenRing (P/T)
instances	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	neco	sara
005	cc	cc	cc	cc	to	cc
010	cc	cc	cc	cc	cc	cc
020	cc	cc	cc	cc	cc	cc
050	cc	cc	cc	cc	cc	cc