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

Please find enclosed the brute results for the CTLPlaceComparison 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 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 FFFFFFFF TFT-F--- TFT-F--- -F--F--- ----F--- FFFFTFFF cc
03 FTFTFFFF --T----- --T----- cc --T----- FFFTTFFF cc
04 FFFT?FTF ---T---- ---T---- ---T---- to cc cc
05 to cc cc to to cc cc
07 mp -----FT- -----FT- to to cc cc
10 mp -F------ -F------ to to to cc
Dekker (P/T)
instances greatSPN lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
010 nc F----TFT F----TFT -----TFT F----TFT cc cc
015 nc T-T----- T-T----- --T----- T-T----- cc cc
020 nc -T-F--FT -T-F--FT -T-F--F- to FFFFTFFF cc
050 nc ---F-F-- ---F-F-- ---F-F-- ---F-F-- to cc
100 nc to to to to to cc
200 nc --TT--F- --TT--F- nf 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 TTTT---- TTTT---- cc TTTT---- FFFFFFFF cc
10 nc cc cc cc cc FFFFFFFF cc
Echo (P/T)
instances greatSPN lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
d02r09 nc -------F -------F -------F cc to cc
d02r11 nc T-F----- T-F----- to T-F----- to cc
d02r15 nc cc cc to to to cc
d02r19 nc -----T-- -----T-- to -----T-- to -----F--
d03r03 nc F----TTF F----TTF F-----T- to to cc
d03r05 nc ---T---F ---T---F ---T---F ---T---- to cc
d03r07 nc -F---TF- -F---TF- -F---TF- to to cc
d04r03 nc --F----- --F----- to --F----F cc cc
d05r03 nc --F--T-- --F--T-- --F--T-- --F--T-- cc cc
Eratosthenes (P/T)
instances greatSPN lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
010 nc F------F F------F cc cc FFFFFFFF cc
020 nc --T---F- --T---F- ------F- ------F- FFFTFFFF ------T-
050 nc FTF----- FTF----- to FTF--T-- FFFFFFFF -----T--
100 nc -------F -------F -------F -------F FFFFTFFF cc
200 nc ------T- ------T- to to FFFFFFFF -----TF-
500 nc -TT--TFF -TT--TFF to to cc cc
FMS (P/T)
instances greatSPN lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
002 FTFT?FFT -T-T---T -T-T---T -T-T---T ---T---- cc cc
005 FTFFTTTT ---T-F-F ---T-F-F cc cc FFFFFFFF cc
010 FFFTTTTF TFTT-TT- TFTT-TT- -F-T-TT- -F-T--T- FFFFFFFF cc
020 FFFFFTTF T--F---T T--F---T ---F---- ---F---- FFFTTFFF cc
050 FTFFTFTF FT----T- FT----T- FT----T- FT----T- FFTTTFFT ------F-
100 mp -----TFT -----TFT -----TFT -----TFT FFFFFFFF cc
200 to -------F -------F -------F cc cc -------T
500 to cc cc cc cc 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 FTFFFTTF ---F-TT- ---F-TT- ---F-TT- to FFFFFFFF to
05 cc to to to cc to cc
Kanban (P/T)
instances greatSPN lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
0005 FTFTTTTF T----T-F T----T-F -----T-F -----T-F FFFTTFFF cc
0010 FTFFFTFF ---F-TF- ---F-TF- ---F-TF- ---F--F- FFFFFFFF cc
0020 TTFTFTTF -----T-F -----T-F -----T-F -----T-F FFFTTFFF cc
0050 to ------T- ------T- ------T- cc FFFFFFFF cc
0100 to -F-F--F- -F-F--F- -F-F--F- ------F- cc cc
0200 TTF --TT-T-- --TT-T-- --TT-T-- ---T---- to cc
0500 mp -F------ -F------ -F------ -F------ to cc
1000 to --TT--T- --TT--T- --TT--T- --TT---- to cc
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 FFFTTFFF cc
3 nc cc cc cc cc FFFFFFFF cc
4 nc cc cc cc cc FFFFTFFF 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 to cc
MAPK (P/T)
instances greatSPN lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
008 TTFT?FTF --T---TF --T---TF ------TF ------TF cc ------F-
020 FFTTTFTF ------T- ------T- ------T- ------T- FFTTTFFT cc
040 to -T-T--F- -T-T--F- -T-T--F- ---T--F- FFTTFFFF cc
080 to FTF----- FTF----- FTF----- to FFFFFFFF cc
160 to -----TT- -----TT- -----TT- -----TT- to cc
320 to ---F--FT ---F--FT ---F--FT to 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 -TF--T-- -TF--T-- -T------ -TF----- FFFFFFFF cc
3 nc -TF--FTT -TF--FTT ------T- -TF--FTT FFFTFFFF cc
4 nc ---T-FF- ---T-FF- ---T-FF- ---T-FF- cc -----TT-
5 nc -----FFT -----FFT to to to cc
6 nc -TFT--T- -TFT--T- to to to cc
7 nc ---T---T ---T---T ---T---T ---T---T to cc
8 nc ---F--T- ---F--T- ---F--T- ---F--T- cc cc
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 cc T----FT- T----FT- T-----T- T----FT- cc cc
02 cc -----F-- -----F-- -----F-- -----F-- to cc
05 TFFFFTTF -----F-F -----F-F to to to cc
10 TFFT?TFF ---T--T- ---T--T- to to cc ------F-
20 cc -F----T- -F----T- -F----T- ------T- to cc
50 FTFFT??? -F---F-T -F---F-T to to cc 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 -----T-- -----T-- cc cc cc -----T--
3 nc -T---TFF -T---TFF -T----FF -T----F- cc cc
4 nc cc cc to to cc cc
5 nc -----TF- -----TF- to to to cc
6 nc cc cc to to to cc
7 nc ---T-F-- ---T-F-- to to 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 FTFF?FFF F--F-F-- F--F-F-- F--F---- F------- cc cc
000010 FFTTTFTF T--F--T- T--F--T- ------T- ------T- FFFFTFFF cc
000020 FFFF?FTT ------T- ------T- ------T- to cc cc
000050 to -F------ -F------ -F------ to FFFFFFFF cc
000100 to -FTF---- -FTF---- -FTF---- to FFFFFFFF cc
000200 FFFTF ------T- ------T- ------T- to FFFFTFFF cc
000500 to cc cc cc to FFFFFFFF cc
001000 mp ------T- ------T- ------T- to FFFTTFFT cc
002000 mp -------T -------T -------T to to cc
005000 mp -----TTF -----TTF to to to cc
010000 cc ------T- to to 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 FTFT?FTF -T----T- -T----T- -T----T- -T----T- cc cc
10 mp T-FT-T-T T-FT-T-T ---T---- T-FT-T-T to cc
20 mp to to to to cc 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 ---F-T-- ---F-T-- ---F-T-- ---F-T-- FFFFTFFF cc
010 nc -----T-T -----T-T cc cc FFFFFFFF cc
020 nc -----T-- -----T-- -----T-- to to cc
050 nc ---F-FT- ---F-FT- to to to cc
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 ------T- ------T- ------T- ------T- FFFTFFFF cc
R003C002 nc FT-T-F-F FT-T-F-F -T-T-F-F FT-T---F FFFFFFFT -----T--
R003C003 nc --F----- --F----- cc cc FFFFTFFF cc
R003C005 nc --F---TT --F---TT ------TT --F---TT cc cc
R003C010 nc -T-T---- -T-T---- cc cc FFFFFFFT cc
R003C015 nc --FT-F-- --FT-F-- ---T-F-- ---T-F-- FFFTTFFF cc
R003C020 nc cc cc cc cc FFFTTFFF cc
R003C050 nc cc cc to to cc cc
R003C100 nc -------F -------F to to FFFTFFFF cc
R005C002 nc T-FF-F-T T-FF-F-T -----F-T -----F-T FFFFTFFF cc
R010C002 nc -F-F-FTF -F-F-FTF -F-F---- -F-F---F FFTTTFFF cc
R015C002 nc FT-F-TT- FT-F-TT- FT-F-TT- FT-F-TT- cc cc
R020C002 nc T-----F- T-----F- ------F- T-----F- cc cc
R050C002 nc --TT--T- --TT--T- --TT--T- --TT--T- FFFFFFFF cc
R100C002 nc cc cc to cc cc cc
Ring (P/T)
instances greatSPN lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
none nc -F---F-T -F---F-T -F---F-T to cc cc
RwMutex (P/T)
instances greatSPN lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
r0010w0010 nc F--T-F-- F--T-F-- F--T---- F--T---- FFFFFFFF cc
r0010w0020 nc ---F-T-F ---F-T-F ---F-T-F ---F-T-- FFTTFFFF cc
r0010w0050 nc --F--FFF --F--FFF -----FFF --F--FFF FFFFFFFF cc
r0010w0100 nc F-F--T-T F-F--T-T cc cc FFFFTFFF cc
r0010w0500 nc --TT--F- --TT--F- --TT---- --TT--F- FFTTFFFF cc
r0010w1000 nc -F-F-F-T -F-F-F-T -F-F-F-T -F-F-F-T FFFFTFFF cc
r0010w2000 nc --T---T- --T---T- cc to to cc
r0020w0010 nc -FF---T- -FF---T- ------T- cc FFFFFFFF cc
r0100w0010 nc -T---TFT -T---TFT -T---TFT -T----F- cc -----FTF
r0500w0010 nc TFTF---T TFTF---T -------T cc cc cc
r1000w0010 nc F-T--FT- F-T--FT- ------T- ------T- cc cc
r2000w0010 nc ---T-FFT ---T-FFT ---T-FFT 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 FFFTTFFF TF-T-TT- TF-T-TT- -F-T---- cc FFFFFFFF cc
000010 FTFFTFTT --FF---T --FF---T ---F---T ---F---- FFFFTFFF cc
000020 mp cc cc to to cc cc
000050 mp cc cc to to cc -----F--
000100 mp to to to to to cc
000200 cc cc cc cc cc to -------F
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--T-FT- F--T-FT- ---T-FT- F--T-FT- FFTTFFFF cc
05 nc --TT--T- --TT--T- ---T--T- --TT---- FFFFFFFF cc
10 nc to to to to FFFFFFFF cc
15 nc to to to to to cc
20 nc T----TFF T----TFF T----TFF T------- to cc
TokenRing (Colored)
instances greatSPN lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
005 nf nf nf nf nf nf nf
010 nf nf nf nf nf nf nf
020 nf nf nf nf nf nf nf
050 nf nf nf nf nf nf nf
100 nf nf nf nf nf nf nf
200 nf nf nf nf nf nf nf
500 nf nf nf nf nf nf nf
TokenRing (P/T)
instances greatSPN lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
005 nf nf nf nf nf nf nf
010 nf nf nf nf nf nf nf
020 nf nf nf nf nf nf nf
050 nf nf nf nf nf nf nf