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

Please find enclosed the brute results for the CTLMix 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 FTFTFFFF ---T---F ---T---F ---T---F cc FFFTTFFF cc
03 FFFTFTTT FF-T-FTF FF-T-FTF FF-T--T- TF-T---- FFFTFFTF cc
04 to -F-T---- -F-T---- -F-T---- to to cc
05 to -FT----- -FT----- -FT----- to to -F------
07 mp cc cc cc cc to cc
10 mp cc cc cc cc to cc
Dekker (P/T)
instances greatSPN lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
010 nc FTTT---T FTTT---T -T-T---T FTTT---T FFFFTFFT cc
015 nc T----FFT T----FFT ------FT T----FFT FFFFFFFF cc
020 nc -FTT-FT- -FTT-FT- -F-T-FT- to cc cc
050 nc FFTT--F- FFTT--F- FFTT--F- to cc cc
100 nc T-T---F- T-T---F- T-T---F- 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 -----FTF -----FTF cc -----FTF FFFTFFFF cc
10 nc cc cc cc cc to cc
Echo (P/T)
instances greatSPN lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
d02r09 nc T--T---F T--T---F to T--T---F to cc
d02r11 nc -F---T-- -F---T-- -F---T-- -F------ cc cc
d02r15 nc ---F---- ---F---- to -T-F---- cc cc
d02r19 nc -T---FT- -T---FT- to -T---FT- to -----TF-
d03r03 nc --F----- --F----- --F----- --F----- to cc
d03r05 nc ---F---- ---F---- to ---F---- cc cc
d03r07 nc ---T-TF- ---T-TF- ---T-TF- to to to
d04r03 nc -F-F-FFT -F-F-FFT -F-F-FFT -F-F-FFT to cc
d05r03 nc ---F---- ---F---- ---F---- ---F---- to to
Eratosthenes (P/T)
instances greatSPN lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
010 nc TTTT-F-F TTTT-F-F TTTT---- TTTT-F-F FTFTFFTF -----F-F
020 nc F--T---- F--T---- F--T---- F--T---- FFFFFFFF cc
050 nc --TT-TT- --TT-TT- --TT-TT- --TT-TT- FFFFTFFF cc
100 nc ---F---- ---F---- ---F---- ---F---- FFFFTFTF cc
200 nc --TF---F --TF---F --TF---F to FFTTFFTF -------T
500 nc ---F-TF- ---F-TF- to to to cc
FMS (P/T)
instances greatSPN lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
002 TTFTTFTF T-----T- T-----T- T-----T- T-----T- FFFFTFTF ------F-
005 FFFTTTTF -F-T---T -F-T---T -F-T---- -F-T---- FFFTFFTF cc
010 TTTTFFFF FF---FF- FF---FF- -----FF- cc FFFTTFFF cc
020 FFTFTTTF -FT--TT- -FT--TT- -FT--TT- -FT---T- FFFFTFTF cc
050 TFFFTFFF TFFF--F- TFFF--F- TFFF--F- TFFF--F- FFFFFFFF ------T-
100 F F--T--T- F--T--T- F--T--T- F--T---- FFFTFFTF cc
200 to FT---F-F FT---F-F FT---F-F -T-----F cc -----T--
500 to -T-T-FT- -T-T-FT- -T-T-FT- -T-T---- 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 FFFTTFFF F-TF-FF- F-TF-FF- -----FF- to FTFTTFFF -----TT-
05 cc to to to cc to cc
Kanban (P/T)
instances greatSPN lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
0005 FTTTTTTT -TT--T-T -TT--T-T -TT--T-T -----T-- FTTTFFFF cc
0010 FTFT?FTF TT----TF TT----TF -T----TF cc cc ------F-
0020 FTTTFFFT ------FT ------FT ------FT ------FT FFFFFFFT cc
0050 FTTTFTTF --T--TT- --T--TT- --T--TT- --T----- FTFTFTTF -----TT-
0100 to -----F-F -----F-F -----F-F cc FFFTFFFF cc
0200 mp cc cc cc cc to cc
0500 FTTF T------- T------- T------- cc to cc
1000 to -F-T---T -F-T---T -F-T---T -F-T---- to -------F
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 FFFFTFTF cc
3 nc cc cc cc cc FFFFTFFF cc
4 nc cc cc cc cc FFFTFFFF cc
5 nc cc cc cc cc cc 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 FFTFFTTF -FTF---- -FTF---- -FTF---- -FTF---- FFTTTFFF cc
020 TTFTTFFF -T-T--F- -T-T--F- -T-T--F- -T-T--F- FFFTFFFF cc
040 to ------T- ------T- ------T- ------T- FFFFFFFF cc
080 to -TFF---- -TFF---- -TFF---- to FFTTFFFF cc
160 to ---F--F- ---F--F- ---F--F- to to cc
320 to -------T -------T -------T -------T 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 FTFT---- FTFT---- cc FTFT---- FFFFTFFF cc
3 nc ---T--F- ---T--F- ---T--F- ------F- cc cc
4 nc cc cc cc cc to cc
5 nc ------T- ------T- to to cc cc
6 nc cc cc cc cc cc cc
7 nc cc cc cc cc to cc
8 nc to to to to to to
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 TTFF--F- TTFF--F- TTFF--F- TTFF---- FTFFTFFF cc
02 FTFTTTTF -F-F---F -F-F---F to to to cc
05 ?????FFT cc cc to to to cc
10 FTFTFFTT FFTF--T- FFTF--T- FFTF--T- FFTF--T- to ------T-
20 FFFT?FTF ---T---- ---T---- to to cc cc
50 FFTFFTFT ------TT ------TT to to to 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 --F--TT- --F--TT- --F---T- --T----- FFFFFFTF cc
3 nc -----T-- -----T-- -----T-- cc FFFTFFFF cc
4 nc -T----TF -T----TF -T----TF -T----TF cc cc
5 nc -T------ -T------ to to cc cc
6 nc --F----T --F----T --F----T --F----T to to
7 nc ------FF ------FF to -------F 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 FFFTTFTF -F----T- -F----T- -F----T- -F----T- FFTTTFTF ------F-
000010 FTFFFTTT ---F-T-T ---F-T-T ---F-T-T ---F-T-T FTFFFFFF cc
000020 TTFF?FTF T--F---- T--F---- T--F---- to cc cc
000050 mp cc cc cc cc FTFTFFFF cc
000100 mp -T-T---- -T-T---- -T-T---- to cc cc
000200 mp cc cc cc cc FFFTFFFF cc
000500 to cc cc cc cc FFFFFFFF cc
001000 mp cc cc cc cc to cc
002000 mp ---F---- ---F---- ---F---- to cc cc
005000 mp to to to to to to
010000 cc to to to to to to
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 FTFTTFFF -----F-- -----F-- -----F-- -----F-- FFFFFFFF cc
10 FTTT -----FFF -----FFF ------F- cc to cc
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--F- --TF--F- ------F- --TF--F- FFFFFFFF cc
010 nc -F---T-T -F---T-T -F------ -----T-T cc cc
020 nc -F----TT -F----TT -F----TT to to ------FF
050 nc -----T-F -----T-F -----T-F to to -----F-T
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 F--T-TFT F--T-TFT ---T-TFT F--T-TFT FFFFTFFF -----FT-
R003C002 nc -FTT--F- -FTT--F- -FTT--F- -FTT--F- FFFTFFFF cc
R003C003 nc F----TTF F----TTF -----TTF ------T- cc cc
R003C005 nc -F------ -F------ -F------ -F------ cc cc
R003C010 nc FFFF--F- FFFF--F- -F-F--F- -F-F--F- FFFFTFFF cc
R003C015 nc --FF---T --FF---T --FF---T --FF---- FFFFFFFF --FF----
R003C020 nc ---F---- ---F---- to ---F---- FFFFTFTF cc
R003C050 nc ---F--F- ---F--F- to to FFFTFFFF cc
R003C100 nc TT-----F TT-----F TT-----F TT-----F to -------T
R005C002 nc FF-F-T-- FF-F-T-- -F-F-T-- -F-F-T-- cc cc
R010C002 nc -FTT-TTT -FTT-TTT -F-T-TTT -FTT-TTT FFFTFFFF cc
R015C002 nc FTTF-F-T FTTF-F-T FTTF-F-T FTTF-F-T FTTTTFFT cc
R020C002 nc T-F-F-F- T-F-F-F- T-F-F-F- T-F-F-F- FFFFTFFF cc
R050C002 nc cc cc cc to FFFTTFFF cc
R100C002 nc FFF----- FFF----- FFF----- to to FFF-----
Ring (P/T)
instances greatSPN lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
none nc -F----F- -F----F- -F----F- to FFFFFFFF cc
RwMutex (P/T)
instances greatSPN lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
r0010w0010 nc TFTT-T-F TFTT-T-F TFTT---- TFTT---- FFFTFFFF cc
r0010w0020 nc F----TTT F----TTT -----TTT cc FFFTTFTF cc
r0010w0050 nc -T-F-T-- -T-F-T-- -T-F-T-- cc FTFFFFFF cc
r0010w0100 nc -----FTT -----FTT ------T- cc cc cc
r0010w0500 nc F-TF-F-- F-TF-F-- cc F-TF-F-- FFFFFFFF cc
r0010w1000 nc -FTT-T-- -FTT-T-- -F-T---- -FTT-T-- FFFTFFFF cc
r0010w2000 nc -FT--T-F -FT--T-F -------F to to cc
r0020w0010 nc -TF---FT -TF---FT -TF---F- -T----F- to cc
r0100w0010 nc ---T---- ---T---- ---T---- ---T---- cc cc
r0500w0010 nc ------T- ------T- ------T- to cc ------F-
r1000w0010 nc FT-T-FFT FT-T-FFT ---T-FFT ---T--FT cc -------F
r2000w0010 nc ---TFT-- ---TFT-- ---TF--- 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 FTTT?FFT -F-F-TFF -F-F-TFF -F-F--F- -F-F---- cc cc
000010 FFFF?FTF --TF---T --TF---T ---F---- cc cc cc
000020 mp TFT----- TFT----- TFT----- to FFFFFFFF cc
000050 mp cc cc cc cc cc cc
000100 mp -----TFT -----TFT -----TFT -----TFT cc ------FT
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 -----FT- -----FT- ------T- ------T- FFFFFFTF cc
05 nc ------F- ------F- ------F- ------F- cc cc
10 nc -F---FF- -F---FF- -F---FF- -F------ cc to
15 nc to to to to to cc
20 nc to to to to to cc
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 FTFTFFTF TF---T-T TF---T-T -F------ -F------ FTFTFFTF T----T-T
010 to F-T--TT- F-T--TT- ------T- ------T- FTFTFFTF cc
020 mp to to to to cc cc
050 cc cc cc cc cc to cc