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

Please find enclosed the brute results for the ReachabilityFireability 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 ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
02 nc FFFFFFFF nc nc nc nc nc nc
03 nc FFFFFFFF nc nc nc nc nc nc
04 nc mp nc nc nc nc nc nc
05 nc mp nc nc nc nc nc nc
07 nc mp nc nc nc nc nc nc
10 nc mp nc nc nc nc nc nc
CSRepetitions (P/T)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
02 FFFFFFFF nc FFFFFFTF FFFFFFTF FFFFFF-F cc FFFFFFFF FFFFFFFF
03 FFFFFFFF nc TFTFFFTF TFTFFFTF -F-FFF-F TFTFFF-F FFFFFFFF TFTFF---
04 FFFFFTFF nc FFFFFFTF FFFFFFTF FFFFFF-F to to FFFFF---
05 to nc FF-FFF-F FF-FFF-F to to to TF--F---
07 mp nc FFFF-F-F FFFF-F-F to to to FFFFF---
10 mp nc FFFFFF-F FFFFFF-F to to to -F-F----
Dekker (P/T)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
010 nc nc TFTFFFFF TFTFFFFF -F-FFFFF TFTFFFFF FFFFFFFF cc
015 nc nc FFFFFFFF FFFFFFFF FFFFFFFF FFFFFFFF FFFFFFFF cc
020 nc nc FFFFFFFF FFFFFFFF FFFFFFFF FFFFFFFF FFFFFFFF cc
050 nc nc FFFFFFFF FFFFFFFF FFFFFFFF to to cc
100 nc nc FFFFFFFF FFFFFFFF FFFFFFFF to to cc
200 nc nc FFFFFFFF FFFFFFFF nc to to cc
DotAndBoxes (Colored)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
2 nc FFFFTTTF nc nc nc nc nc nc
3 nc FFFFF nc nc nc nc nc nc
4 nc F nc nc nc nc nc nc
5 nc mp nc nc nc nc nc nc
DrinkVendingMachine (Colored)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
02 nc FFFFFFFF nc nc nc nc nc nc
10 nc cc nc nc nc nc nc nc
DrinkVendingMachine (P/T)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
02 nc nc FFTFFTTF FFTFFTTF FF-FF--F FF-FF--F FFFFFTFF TFFF---T
10 nc nc cc cc cc cc FFFFFFFF to
Echo (P/T)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
d02r09 nc nc FFFFFF-F FFFFFF-F to to to FFFFFFFF
d02r11 nc nc FFFFFFFF FFFFFFFF FFFFFFFF to to to
d02r15 nc nc FFFFFFFF FFFFFFFF FFFFFFFF to to to
d02r19 nc nc FFFFFFFF FFFFFFFF FFFFFFFF to to to
d03r03 nc nc TFTFTFFF TFTFTFFF -F-F-FFF to to TFFFTFFF
d03r05 nc nc -F-FFFFF -F-FFFFF to to to FFFFFFFF
d03r07 nc nc FFFFFFFF FFFFFFFF FFFFFFFF to to to
d04r03 nc nc FFFFFFFF FFFFFFFF FFFFFFFF to to FFFFFFFF
d05r03 nc nc -F-F-F-F -F-F-F-F to to to TFTFTFFF
Eratosthenes (P/T)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
010 nc FFFFFFFF FFFFFFFF FFFFFFFF FFFFFFFF FFFFFFFF FFFFFFFF FFTTFTTT
020 nc FFFF FFFFFFFF FFFFFFFF FFFFFFFF FFFFFFFF FFFFFFFF FFFFFFFF
050 nc FFFFFFFF FFFFFFFF FFFFFFFF FFFFFFFF FFFFFFFF FFFFFFFF FFFFFTTT
100 nc FFFFFFFF FFFFFFFF FFFFFFFF FFFFFFFF FFFFFFFF FFFFFFFF FFFFFTTT
200 nc FFFF FFFFFFFF FFFFFFFF FFFFFFFF FFFFFFFF FFFFFFFF FFFFTTTT
500 nc FFFFFFFF FFFFFFFF FFFFFFFF FFFFFFFF FFFFFFFF FFFFFFFF FFFFFTTT
FMS (P/T)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
002 FFFFFFFF nc FFFFFFFF FFFFFFFF FFFFFFFF FFFFFFTF FFFFFFFF FFFFFFFF
005 FFFFFFFF nc FFFFFFFF FFFFFFFF FFFFFFFF FFFF-FFF FFFFFFFF FFFFFFFF
010 FFFFFFFF nc FFFFFFFF FFFFFFFF FFFFFFFF -F-FF--- FFFFFFFF FFFFFFFF
020 FFFFFFFF nc FFFFFFFF FFFFFFFF FFFFFFFF FFFFFFFF FFFFFFFF FFFFFFFF
050 FFFFFFFF nc FFFFFFFF FFFFFFFF FFFFFFFF -F-FFF-F FFFFFFFF FFFFFFFF
100 FFFFFFFF FFFFFFFF FFFFFFFF FFFFFFFF FFFFFFFF -----FFF FFFFFFFF FFFFFFFF
200 to nc FFFFFFFF FFFFFFFF FFFFFFFF -----FTF to FFFFFFFF
500 to nc FFFFFFFF FFFFFFFF FFFFFFFF TFTFFFFF to FFFFFFFF
GlobalRessAlloc (Colored)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
03 nc FFFF nc nc nc nc nc nc
05 nc nc nc nc nc nc nc nc
06 nc nc nc nc nc nc nc nc
07 nc nc nc nc nc nc nc nc
09 nc nc nc nc nc nc nc nc
10 nc nc nc nc nc nc nc nc
11 nc nc nc nc nc nc nc nc
GlobalRessAlloc (P/T)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
03 FFFFFFFF nc FFFFFFTF FFFFFFTF FFFFFF-F to FFFFFFFF TTTT----
05 cc nc to to to cc to cc
Kanban (P/T)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
0005 FFFFFFFF nc FFFFFFFF FFFFFFFF FFFFFFFF -F-FFFFF FFFFFFFF FFFFFFFF
0010 FFFFFFFF nc FFFFFFFF FFFFFFFF FFFFFFFF cc FFFFFFFF FFFFFFFF
0020 FFFFFFFF nc FFFFFFFF FFFFFFFF FFFFFFFF FFFFF--- FFFFFFFF to
0050 FFFFFFFF nc FFFFFFFF FFFFFFFF FFFFFFFF FFFFF--- FFFFFFFF FFFFFFFF
0100 to nc FFFFFFFF FFFFFFFF FFFFFFFF -F-FF--- FFFFFFFF FFFFFFFF
0200 mp nc FFFFFFFF FFFFFFFF FFFFFFFF -----F-F to FFFFFFFF
0500 mp nc FFFFFFFF FFFFFFFF FFFFFFFF -F-FFFFF to FFFFFFFF
1000 to nc FFFFFFFF FFFFFFFF FFFFFFFF -F-FF--- to FFFFFFFF
LamportFastMutEx (Colored)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
2 nc FFFFFFFF nc nc nc nc nc nc
3 nc FFFFFFFF nc nc nc nc nc nc
4 nc FFFFFFFF nc nc nc nc nc nc
5 nc FFFFFFFF nc nc nc nc nc nc
6 nc mp nc nc nc nc nc nc
7 nc mp nc nc nc nc nc nc
8 nc mp nc nc nc nc nc nc
LamportFastMutEx (P/T)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
2 nc nc cc cc cc cc FFFFFFFF cc
3 nc nc cc cc cc cc FFFFFFFF cc
4 nc nc cc cc cc cc FFFFFFFF cc
5 nc nc cc cc cc cc to cc
6 nc nc cc cc cc cc to cc
7 nc nc cc cc cc cc to cc
8 nc nc cc cc cc cc to cc
MAPK (P/T)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
008 FFFFFFFF nc FFFFFFFF FFFFFFFF FFFFFFFF FFFFFFFF FFFFFFFF FFFFFFFF
020 FFFFFFFF nc FFFFFFFF FFFFFFFF FFFFFFFF -F-F-FFF FFFFFFFF FFFFFFFF
040 to nc FFFFFFFF FFFFFFFF FFFFFFFF FFFFFFTF FFFFFFFF FFFFFFFF
080 to nc FFFFFFFF FFFFFFFF FFFFFFFF to FFFFFFFF FFFFFFFF
160 to nc FFFFFFFF FFFFFFFF FFFFFFFF to to FFFFFFFF
320 to nc FFFFFFFF FFFFFFFF FFFFFFFF FFFFFFFF to to
NeoElection (Colored)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
2 nc FFFFFTTT nc nc nc nc nc nc
3 nc FFFFFTFF nc nc nc nc nc nc
4 nc nc nc nc nc nc nc nc
5 nc mp nc nc nc nc nc nc
6 nc nc nc nc nc nc nc nc
7 nc mp nc nc nc nc nc nc
8 nc nc nc nc nc nc nc nc
NeoElection (P/T)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
2 nc nc TFTFTTTT TFTFTTTT -F-F---- TFTFTTTT FFFFFTTT TTTT---T
3 nc nc TFTFFTTF TFTFFTTF -F-FF--F cc FFFFFTFF TTTTTTTT
4 nc nc to to to to to -T-T-FFT
5 nc nc to to to to to TTTTT---
6 nc nc to to to to to -T-T----
7 nc nc to to to to to TTTT----
8 nc nc to to to to to -------T
PermAdmissibility (Colored)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
01 nc FFFFFTFT nc nc nc nc nc nc
02 nc mp nc nc nc nc nc nc
05 nc mp nc nc nc nc nc nc
10 nc mp nc nc nc nc nc nc
20 nc mp nc nc nc nc nc nc
50 nc mp nc nc nc nc nc nc
PermAdmissibility (P/T)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
01 to nc TFTFFFTF TFTFFFTF -F-FFF-F TFTFFFTF FFFFFTFT TT---FFF
02 FFFFTTTT nc FFFFFFFF FFFFFFFF FFFFFFFF to to FFFF----
05 FFFFTTTT nc FFFFFFFF FFFFFFFF FFFFFFFF to to FFFF----
10 FFFFTTTT nc FFFFFFFF FFFFFFFF FFFFFFFF to to FFFFF---
20 FFTTFTTT nc FFFFFFFF FFFFFFFF FFFFFFFF to to FF--F---
50 FFFFFTTT nc FFFFFFFF FFFFFFFF FFFFFFFF to cc to
Peterson (Colored)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
2 nc FFFFFFFF nc nc nc nc nc nc
3 nc FFFFFFFF nc nc nc nc nc nc
4 nc mp nc nc nc nc nc nc
5 nc mp nc nc nc nc nc nc
6 nc mp nc nc nc nc nc nc
7 nc mp nc nc nc nc nc nc
Peterson (P/T)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
2 nc nc FFFFFTTT FFFFFTTT FFFFF--- -----TTT FFFFFFFF to
3 nc nc FFFFTTTF FFFFTTTF FFFF---F FFFFT--- FFFFFFFF to
4 nc nc FF-F---- FF-F---- to to to to
5 nc nc FFFFF--- FFFFF--- to to to to
6 nc nc FFFFF--- FFFFF--- to to to to
7 nc nc FF-FF--F FF-FF--F to FF-FF--- to to
Philosophers (Colored)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
000005 nc nc nc nc nc nc nc nc
000010 nc nc nc nc nc nc nc nc
000020 nc nc nc nc nc nc nc nc
000050 nc nc nc nc nc nc nc nc
000100 nc nc nc nc nc nc nc nc
000200 nc nc nc nc nc nc nc nc
000500 nc nc nc nc nc nc nc nc
001000 nc nc nc nc nc nc nc nc
002000 nc nc nc nc nc nc nc nc
005000 nc nc nc nc nc nc nc nc
010000 nc nc nc nc nc nc nc nc
050000 nc nc nc nc nc nc nc nc
100000 nc nc nc nc nc nc nc nc
Philosophers (P/T)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
000005 FTFFTFFF nf FFTFFFTF FFTFFFTF FF-FFF-F FFTFFFTF FFFFFFFF TFFFFFFF
000010 FTFTFFFF nf FFFFTTTF FFFFTTTF FFFF---F FFFFTTTF FFFFFFFF TFTF-FFF
000020 FTFTFFFT nf FFFF-F-F FFFF-F-F FFFF-F-F to FFFFFFFF TFTFF---
000050 mp nf FF-FFFFF FF-FFFFF FF-FFFFF to FFFFFFFF TF------
000100 mp nf FFFFFFFF FFFFFFFF FFFFFFFF FFFFFFFF FFFFFFFF -F-F----
000200 mp nf FF-FFF-F FF-FFF-F FF-FFF-F to to -F------
000500 to nf FF-FF--- FF-FF--- FF-FF--- to to -FFFF---
001000 mp nf FF-FFF-F FF-FFF-F FF-FFF-F to to cc
002000 mp nf FFFFF--- FFFFF--- to to to cc
005000 mp nf FFFFFF-F FFFFFF-F FFFFFF-F to to cc
010000 cc nf FFFFF--F FFFFF--F to to to cc
PhilosophersDyn (Colored)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
03 nc nc nc nc nc nc nc nc
10 nc nc nc nc nc nc nc nc
20 nc nc nc nc nc nc nc nc
50 nc nc nc nc nc nc nc nc
80 nc nc nc nc nc nc nc nc
PhilosophersDyn (P/T)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
03 FFFFTTFT nc TFTFFFTF TFTFFFTF -F-FFF-F TFTFFFTF FFFFTTFT TF------
10 mp nc TFTFFFTF TFTFFFTF -F-FFF-F to to -T-T----
20 mp nc to to to to to cc
Planning (P/T)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
nf nf nf nf nf nf nf nf
Railroad (P/T)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
005 nc nc TFTFFFFF TFTFFFFF -F-FFFFF TFTFFF-F FFFFFFFF to
010 nc nc TFTFFFTF TFTFFFTF -F-FFF-F ----F--- FFFFFTFT TTTTTFFF
020 nc nc -F-F-F-F -F-F-F-F to to to to
050 nc nc to to to to to to
100 nc nc to to to to to to
RessAllocation (P/T)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
R002C002 nc nc TFTFFFTF TFTFFFTF -F-FFF-F TFTFFFTF FFFFFTFT TFFFFFTF
R003C002 nc nc FFFFFFTF FFFFFFTF FFFFFF-F -----FTF FFFFFTFT FFFFFFTF
R003C003 nc nc TFTFFFTF TFTFFFTF -F-FFF-F -F-FFFTF FFFFFTFT TFTFFFTF
R003C005 nc nc FFFFFFTF FFFFFFTF FFFFFF-F FFFFFFTF FFFFFTFF FFFFFFFF
R003C010 nc nc TFTFFFFF TFTFFFFF -F-FFFFF -F-FFF-F FFFFFFFF TFTFFFFF
R003C015 nc nc FFFFFFTF FFFFFFTF FFFFFF-F -F-FFF-F FFFFFTFT FFFFFFFF
R003C020 nc nc FFFFFFFF FFFFFFFF FFFFFFFF FFFFFFTF FFFFFFFF FFFFFFFF
R003C050 nc nc FFFFFFFF FFFFFFFF FFFFFFFF to FFFFFFFF FFFFFFFF
R003C100 nc nc FFFFFFFF FFFFFFFF FFFFFFFF to FFFFFFFF FFFFFFFF
R005C002 nc nc TFTFTFFF TFTFTFFF -F-F-FFF TFTF-FTF FFFFFFFF to
R010C002 nc nc FFFFFFFF FFFFFFFF FFFFFFFF TFTFFFFF FFFFFFFF FFFFTFFF
R015C002 nc nc TFTFFFFF TFTFFFFF -F-FFFFF TFTFFFFF FFFFFFFF TFFFFFFF
R020C002 nc nc FFFFFFFF FFFFFFFF FFFFFFFF FFFFFFFF FFFFFFFF FFFFFFFF
R050C002 nc nc TFTFFFFF TFTFFFFF -F-FFFFF to FFFFFFFF TFFFFFFF
R100C002 nc nc FFFFFFFF FFFFFFFF FFFFFFFF to FFFFFFFF FFFFFFFF
Ring (P/T)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
none nc nc -F-F-FFF -F-F-FFF -F-F-FFF to FFFFFFFF TFTFTFFF
RwMutex (P/T)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
r0010w0010 nc nc TFTFFFFF TFTFFFFF -F-FFFFF TFTFFFFF FFFTFFFF TFFFFFFF
r0010w0020 nc nc TFTFFFFF TFTFFFFF -F-FFFFF TFTFFFFF FFFFFFFF TFFFTFTF
r0010w0050 nc nc TFTFTFFF TFTFTFFF -F-F-FFF TFTFTFFF FFFTFFFF TFFFTFTF
r0010w0100 nc nc TFTFTFFF TFTFTFFF -F-F-FFF cc FFFFFFFT TFTFTFTF
r0010w0500 nc nc TFTFFFTF TFTFFFTF -F-FFF-F TFTFFFTF FFFFFTFT TFTFFFFF
r0010w1000 nc nc FFFFFFTF FFFFFFTF FFFFFF-F FFFFFFTF FFFTTTFT FFTFTFFF
r0010w2000 nc nc TFTFTFTF TFTFTFTF -F-F-F-F to to TFFFTFFF
r0020w0010 nc nc TFTFTFTF TFTFTFTF -F-F-F-F -F-F-FTF to TFFFTFFF
r0100w0010 nc nc FFFFFFFF FFFFFFFF FFFFFFFF -----F-F cc FFFFFFFF
r0500w0010 nc nc FFFFFFFF FFFFFFFF FFFFFFFF FFFFF--- cc FFFFFFFF
r1000w0010 nc nc FFFFFFFF FFFFFFFF FFFFFFFF -----FFF cc FFFFFFFF
r2000w0010 nc nc FFFFFFFF FFFFFFFF FFFFFFFF to cc FFFFFFFF
SharedMemory (Colored)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
000005 nc nc nc nc nc nc nc nc
000010 nc nc nc nc nc nc nc nc
000020 nc nc nc nc nc nc nc nc
000050 nc nc nc nc nc nc nc nc
000100 nc nc nc nc nc nc nc nc
000200 nc nc nc nc nc nc nc nc
000500 nc nc nc nc nc nc nc nc
001000 nc nc nc nc nc nc nc nc
002000 nc nc nc nc nc nc nc nc
005000 nc nc nc nc nc nc nc nc
010000 nc nc nc nc nc nc nc nc
020000 nc nc nc nc nc nc nc nc
050000 nc nc nc nc nc nc nc nc
100000 nc nc nc nc nc nc nc nc
SharedMemory (P/T)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
000005 FTFTFFFT nc FFFFTFTF FFFFTFTF FFFF-F-F -----F-F FFFFFFFF TFTFTTTT
000010 TTFFFFFF nc FFTFTFTF FFTFTFTF FF-F-F-F to FFFFFTFT TFFFF---
000020 mp nc FFFFFF-F FFFFFF-F FFFFFF-F to FFFFFFFF TFTFF---
000050 mp nc FFFFFF-F FFFFFF-F to to to FFFFF---
000100 mp nc to to to to to cc
000200 cc nc cc cc cc cc to to
SimpleLoadBal (Colored)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
02 nc FFFFFFFF nc nc nc nc nc nc
05 nc FFFFFFFF nc nc nc nc nc nc
10 nc FFFFFFFF nc nc nc nc nc nc
15 nc mp nc nc nc nc nc nc
20 nc mp nc nc nc nc nc nc
SimpleLoadBal (P/T)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
02 nc nc FFFFFFTF FFFFFFTF FFFFFF-F FFFFFTTF FFFFFFFF to
05 nc nc FFFFFFTF FFFFFFTF FFFFFF-F -----FTF FFFFFFFF to
10 nc nc to to to to FFFFFFFF to
15 nc nc to to to to to to
20 nc nc to to to to to to
TokenRing (Colored)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
005 nc nc nc nc nc nc nc nc
010 nc nc nc nc nc nc nc nc
020 nc nc nc nc nc nc nc nc
050 nc nc nc nc nc nc nc nc
100 nc nc nc nc nc nc nc nc
200 nc nc nc nc nc nc nc nc
500 nc nc nc nc nc nc nc nc
TokenRing (P/T)
instances greatSPN ITS-Tools lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
005 FTFTFTFF nc TFTFTTTF TFTFTTTF -F-F---F -F-F---- FTFTFTFF to
010 to nc TFTFTTTF TFTFTTTF -F-F---F -F------ FTFFFTFF cc
020 mp nc to to to to to cc
050 cc nc cc cc cc cc to cc