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

Please find enclosed the brute results for the CTLFireability 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 FTFTTFFF FTFT--F- FTFT--F- FTFT--F- -T-T--F- FTFTTFFF TTTT--F-
03 FTTTTTTT --F---TT --F---TT ------TT --F---TT FTTTTTTT ------TF
04 to --T--FF- --T--FF- --T--FF- to to --F--TF-
05 to -F---T-- -F---T-- -F---T-- to to -F---T--
07 mp F--F---- F--F---- F--F---- cc to ---F----
10 mp -F----T- -F----T- to to cc -F----T-
Dekker (P/T)
instances greatSPN lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
010 nc F--T-T-F F--T-T-F F--T-T-F F--T-T-F FFFTTTFF cc
015 nc T-----T- T-----T- T-----T- T-----T- cc cc
020 nc -F-T-F-- -F-T-F-- -F-T-F-- -F-T-F-- FFFTTFFF cc
050 nc -TT--F-F -TT--F-F -TT--F-F to to cc
100 nc -TT--TFT -TT--TFT -TT--TFT 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 --FF---T --FF---T --FF---- --FF---T FFFFTFTF to
10 nc cc cc cc cc FFFTF to
Echo (P/T)
instances greatSPN lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
d02r09 nc FFTT-TF- FFTT-TF- FFTT-TF- cc cc FFTTFTF-
d02r11 nc --TT---- --TT---- --TT---- ---T---- to to
d02r15 nc --FT-F-- --FT-F-- --FT-F-- to to to
d02r19 nc ---T-F-F ---T-F-F ---T-F-F ---T---- to to
d03r03 nc T-TT---T T-TT---T T-TT---T to to T-TT---T
d03r05 nc TF-T-T-- TF-T-T-- TF-T-T-- to to TF-T-T--
d03r07 nc FTT--T-T FTT--T-T FTT--T-T to cc to
d04r03 nc FT-T---- FT-T---- FT-T---- -T-T---- cc FT-T----
d05r03 nc FTTT--T- FTTT--T- FTTT--T- to to to
Eratosthenes (P/T)
instances greatSPN lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
010 nc --F-TF-F --F-TF-F --F-TF-F --F-TF-F FTFTTFFF --T-TF-F
020 nc F-FF--T- F-FF--T- F-FF--T- F-FF--T- FFFFFTTF F-TT--T-
050 nc -FT--T-T -FT--T-T -FT--T-T -FT--T-T FFTTFTFT -FT--T-T
100 nc FFT---TT FFT---TT FFT---TT FFT---TT FFTTFTTT FFT---TT
200 nc -F-T-T-- -F-T-T-- -F-T-T-- -F-T-T-- TFFTTTFF -F-F-T--
500 nc FFF--F-T FFF--F-T FFF--F-T FFF--F-T FFFTFFTT FFF-TF-T
FMS (P/T)
instances greatSPN lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
002 FTFT?FFF -TFT---- -TFT---- -TFT---- -TTT---- cc -TFTF---
005 FTTTFFFT -T-----T -T-----T -T-----T -T------ FTFTTFTT -T-----T
010 FFTFTTTT F-TF-T-T F-TF-T-T F-TF-T-T cc FFTFFTTT F-TFFT-T
020 FTFT?TTF -T---TT- -T---TT- -T---TT- -T---TT- cc -T---TT-
050 TTFT?FFF T--T-FF- T--T-FF- T--T-FF- ---T--F- cc T--T-FF-
100 FFFTFTTF FF-T---F FF-T---F FF-T---F -F-T---T FFFTFFFF FF-T---F
200 to T--F---- T--F---- T--F---- ---F---- to T--FT---
500 to --F---F- --F---F- --F---F- ------F- to --F---F-
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 TFTFTFTF T-FF-FT- T-FF-FT- T--F-FT- to TTTFTFTF to
05 cc cc cc cc cc to cc
Kanban (P/T)
instances greatSPN lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
0005 FFTT?TFT -FT--TFT -FT--TFT -FT--TFT -F------ cc -FT--TFT
0010 FFFT?FFF FF---FF- FF---FF- FF---FF- FF------ cc FF--TFF-
0020 FTFTTFFF FT-T-F-- FT-T-F-- FT-T-F-- -----F-- FTFTFFTF FT-T-F--
0050 to -FF--TF- -FF--TF- -FF--TF- cc FFFFFTFT -FF-FTF-
0100 FFTT?FFF --T----- --T----- --T----- cc cc --T-----
0200 mp FF-F--TT FF-F--TT FF-F--TT -F-F---- to FF-FF-TT
0500 FFF -TTF---- -TTF---- -TTF---- cc to -TTF----
1000 to FT---TF- FT---TF- FT---TF- FT------ cc FT---TF-
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 cc cc
3 nc cc cc cc cc FFFTTFFF cc
4 nc cc cc cc cc FFTTTFTF 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 cc cc
MAPK (P/T)
instances greatSPN lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
008 FFFTFFFF --F--F-F --F--F-F --F--F-F --F--F-F FFFTFFFF --F-FF-F
020 FTTT?FTF -TT---T- -TT---T- -TT---T- -TT---T- cc -TT-T-T-
040 to TFFT--F- TFFT--F- TFFT--F- FFTT--F- TFFTFFFF to
080 to -FT---FT -FT---FT -FT---FT to FFTFTFFT -FT---FT
160 to ------TF ------TF ------TF ------TF to ------TF
320 to T---F--F T---F--F T---F--F to to T---F--F
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 --FF--T- --FF--T- ---F--T- --FF--T- cc --FTF-F-
3 nc T--F-TFF T--F-TFF ------F- T--F-TFF FFFFFFFF T--F-TTF
4 nc to to to to to -FT-T---
5 nc -T---F-- -T---F-- -T---F-- to cc -F---T--
6 nc -T---TT- -T---TT- to to to -F---FF-
7 nc to to to to cc --F-TT-F
8 nc to to to to cc ------FT
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 F--FT--T F--FT--T ---F---- F--FT--T FFTFFFTF F---T--T
02 FFFTFFFF FF---F-- FF---F-- FF---F-- to to FF---F--
05 FTFFTFTF T--F-F-T T--F-F-T T--F-F-T to to to
10 FTFT?FFF F-T--TF- F-T--TF- F-T--TF- to cc F-T--TF-
20 FFFFFFTF T-F----- T-F----- T-F----- to cc to
50 FFTFTTFF -T-T--T- -T-T--T- -T-T--T- -T-T--T- cc -T-T--T-
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 -TTF--T- -TTF--T- -T-F--T- -T-F--T- cc -TFF--T-
3 nc -F---F-F -F---F-F -F---F-F -F---T-T cc to
4 nc -----F-- -----F-- -----F-- -----F-- cc -----T--
5 nc cc cc to to to F-F-----
6 nc T--F-FT- T--F-FT- to to to to
7 nc --T--FT- --T--FT- --T--FT- --T--FT- 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 FTTF?FTF --T---T- --T---T- --T---T- --T---T- cc --F-T-T-
000010 TTTT?TTT --TT---- --TT---- --TT---- --TT---- cc --FTF---
000020 FTTF?TTF FT-F-TTF FT-F-TTF FT-F-TTF FT-F-TTF cc TT-F-FTT
000050 mp -TFF--FF -TFF--FF -TFF--FF -TFF--FF FTFFFFFF -TTF--FT
000100 mp -FF--F-- -FF--F-- -FF--F-- to to -F------
000200 mp F----T-F F----T-F F----T-F to cc cc
000500 to FFTT-FT- FFTT-FT- FFTT-FT- to to -F-T--T-
001000 mp -F---FT- -F---FT- -F---FT- to to cc
002000 mp F-TT--T- F-TT--T- F-TT--T- to cc cc
005000 mp TT-F--TF TT-F--TF TT-F--TF to to cc
010000 cc -----F-- -----F-- -----F-- 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 TTFFFFFF TT---F-- TT---F-- TT---F-- TT---F-- TTFTFFFT -T---T--
10 FFF ---T-T-- ---T-T-- ---T---- ---T-T-- to -----T--
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---T --TF---T --TF---- --TF---T cc --TF---F
010 nc FFF--F-T FFF--F-T -F---F-T cc cc to
020 nc ---F--T- ---F--T- ---F--T- cc to ---F--T-
050 nc to to to to to to
100 nc to to to to to to
RessAllocation (P/T)
instances greatSPN lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
R002C002 nc -----F-T -----F-T cc -----F-T FTFTTFTF -----F-F
R003C002 nc T-FT-TT- T-FT-TT- ---T--T- -----TT- FFTTFFTF T-TTTTT-
R003C003 nc T-FT-F-F T-FT-F-F T-FT-F-F T-FT-F-F TTFTTFTF T-FTTF-F
R003C005 nc -TFF-F-F -TFF-F-F -T-F---- -T-F-F-F FTFFTFFF to
R003C010 nc T-T--TFT T-T--TFT -----TFT T-T--TFT FFFFFTFT T-T-FTFT
R003C015 nc TTF--TF- TTF--TF- TTF--TF- FTT--TF- TTFTTTFT TTF--TF-
R003C020 nc FFTT-TFT FFTT-TFT FFTT-TFT FFTT-TFT FFTTFTFT FFTT-TFT
R003C050 nc FT-T-T-- FT-T-T-- FT-T-T-- to to FT-TTT--
R003C100 nc FFTFTFT- FFTFTFT- FFTFTFT- to FFTFTFTF FFTFTFT-
R005C002 nc ------F- ------F- ------F- ------F- FFFTTFFF ----T-F-
R010C002 nc F-TT---F F-TT---F ---T---F F-TT---F FTFTFFFF F-FT---F
R015C002 nc -FF--F-T -FF--F-T -FF--F-T -FF--F-T FFFFTFFT -FF-TF-T
R020C002 nc T-----FF T-----FF ------FF T-----FT FFFFFFFF to
R050C002 nc F-F----- F-F----- cc to cc to
R100C002 nc cc cc cc cc to ----T---
Ring (P/T)
instances greatSPN lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
none nc -T-----T -T-----T -T-----T to FTFFFFFT -T-----F
RwMutex (P/T)
instances greatSPN lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
r0010w0010 nc -TTF--TF -TTF--TF -TTF--T- -T-F--TF cc -TTF--TF
r0010w0020 nc -------T -------T cc -------T TTFTTFTF -------F
r0010w0050 nc T-FF-T-F T-FF-T-F ---F-T-F T-FF-T-F FTTFFTFF T-FF-T-F
r0010w0100 nc FF-F--FF FF-F--FF -F-F--F- cc FFFFFFFT FF-FT-FT
r0010w0500 nc F-----F- F-----F- ------F- F-----F- cc F-----F-
r0010w1000 nc T-T-FF-T T-T-FF-T cc T-T-FF-T FTFTTFFF T-T-TF-T
r0010w2000 nc F--F--F- F--F--F- ---F--F- to to F--FT-F-
r0020w0010 nc T--T---- T--T---- T--T---- T--T---- to T--T----
r0100w0010 nc -TFT-TT- -TFT-TT- -TFT-TT- -T-T--T- cc -TFTTTT-
r0500w0010 nc -F-T---- -F-T---- -F-T---- -F-T---- cc -F-TT---
r1000w0010 nc F--T-FTT F--T-FTT F--T-FTT ------T- cc F--T-FTT
r2000w0010 nc -----FTT -----FTT -----FTT cc cc ----TFTT
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 FTFT?TTT --T----F --T----F cc cc cc --T-----
000010 FTFT?TTT -TFF-F-- -TFF-F-- -TFF-F-- -T-F---- cc -TTF-T--
000020 mp -F-F--F- -F-F--F- -F-F--F- -F-F--F- cc -F-FT-F-
000050 mp TTT----- TTT----- to to to cc
000100 mp -F-----T -F-----T to to to cc
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 ---F-F-- ---F-F-- ---F-F-- ---F---- FFFFTFTT ---F-F--
05 nc TF---F-- TF---F-- TF---F-- -F---F-- cc F----T--
10 nc FT-F---- FT-F---- to FT-F---F cc to
15 nc FT-T--FT FT-T--FT FT-T--FT to to to
20 nc to to to to to to
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 FTTFTFTF -T----FT -T----FT -T----F- -T----F- FTTFTFTF to
010 to -----T-- -----T-- cc cc FTFTTFTF cc
020 mp to to to to to cc
050 cc cc cc cc cc to cc