fond
Model Checking Contest @ Petri Nets 2013
Milano, Italy, June 25, 2013
Results summary for the LTLMix Examination
Last Updated
Apr. 26, 2013

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:

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