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

Please find enclosed the brute results for the StateSpace 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:

Please note that, for some models/instances, we could not reformat the number of the state space (apparently over 10**239 states) and then provide "∞ (ovf)" as an answer.

CSRepetitions (Colored)
instances alpina greatSPN ITS-Tools lola pessimistic marcie neco pnxdd
02 7424 nc 7424 nc nc nc nc
03 1.341E+08 nc 1.341E+08 nc nc nc nc
04 to nc mp nc nc nc nc
05 to nc mp nc nc nc nc
07 cc nc mp nc nc nc nc
10 cc nc mp nc nc nc nc
CSRepetitions (P/T)
instances alpina greatSPN ITS-Tools lola pessimistic marcie neco pnxdd
02 7424 1872 1872 nc 1872 1872 1872
03 1.341E+08 3.952E+06 3.952E+06 nc 3.952E+06 3.952E+06 3.952E+06
04 to 6.417E+10 6.417E+10 nc to cc 6.417E+10
05 to to 6.668E+15 nc to nc 6.668E+15
07 cc mp 1.308E+28 nc to nc to
10 cc mp mp nc to nc to
Dekker (P/T)
instances alpina greatSPN ITS-Tools lola pessimistic marcie neco pnxdd
010 to nc 6144 nc 6144 6144 6144
015 to nc 278528 nc 278528 278528 278528
020 to nc mp nc 1.153E+07 1.153E+07 1.153E+07
050 cc nc mp nc to cc nc
100 cc nc mp nc to nc to
200 to nc mp nc to nc to
DotAndBoxes (Colored)
instances alpina greatSPN ITS-Tools lola pessimistic marcie neco pnxdd
2 11 nc 11 nc nc nc nc
3 cc nc 383 nc nc nc nc
4 cc nc 270156 nc nc nc nc
5 cc nc mp nc nc nc nc
DrinkVendingMachine (Colored)
instances alpina greatSPN ITS-Tools lola pessimistic marcie neco pnxdd
02 1024 nc 1024 nc nc nc nc
10 cc nc 1.153E+18 nc nc nc nc
DrinkVendingMachine (P/T)
instances alpina greatSPN ITS-Tools lola pessimistic marcie neco pnxdd
02 1024 nc 1024 nc 1024 nc 1024
10 cc nc to nc 1.153E+18 nc to
Echo (P/T)
instances alpina greatSPN ITS-Tools lola pessimistic marcie neco pnxdd
d02r09 cc nc mp nc to nc to
d02r11 cc nc mp nc to nc to
d02r15 cc nc mp nc to nc to
d02r19 cc nc mp nc to nc to
d03r03 to nc mp nc to nc mp
d03r05 cc nc mp nc to nc mp
d03r07 cc nc mp nc to nc to
d04r03 cc nc mp nc to nc mp
d05r03 cc nc mp nc to nc to
Eratosthenes (P/T)
instances alpina greatSPN ITS-Tools lola pessimistic marcie neco pnxdd
010 32 nc 32 nc 32 32 32
020 2048 nc 2048 nc 2048 2048 2048
050 1.718E+10 nc 1.718E+10 nc 1.718E+10 cc 1.718E+10
100 1.889E+22 nc 1.889E+22 nc 1.889E+22 nc 1.889E+22
200 cc nc 1.142E+46 nc 1.142E+46 nc 1.142E+46
500 cc nc 4.13E+121 nc 4.13E+121 nc 4.13E+121
FMS (P/T)
instances alpina greatSPN ITS-Tools lola pessimistic marcie neco pnxdd
002 3444 3444 3444 nc 3444 3444 3444
005 2.895E+06 2.895E+06 2.895E+06 nc 2.895E+06 2.895E+06 2.895E+06
010 to 2.501E+09 2.501E+09 nc 2.501E+09 cc 2.501E+09
020 to 6.029E+12 6.029E+12 nc 6.029E+12 cc 6.029E+12
050 to 4.240E+17 4.240E+17 nc 4.240E+17 nc 4.240E+17
100 to 2.703E+21 2.703E+21 nc 2.703E+21 nc to
200 to to 1.954E+25 nc to nc to
500 to to to nc to nc to
GlobalRessAlloc (Colored)
instances alpina greatSPN ITS-Tools lola pessimistic marcie neco pnxdd
03 to nc 6320 nc nc nc nc
05 to nc 1.066E+08 nc nc nc nc
06 to nc 2.572E+10 nc nc nc nc
07 to nc mp nc nc nc nc
09 to nc mp nc nc nc nc
10 to nc mp nc nc nc nc
11 to nc mp nc nc nc nc
GlobalRessAlloc (P/T)
instances alpina greatSPN ITS-Tools lola pessimistic marcie neco pnxdd
03 to 6320 6320 nc 6320 nc 6320
05 to cc to nc to nc to
Kanban (P/T)
instances alpina greatSPN ITS-Tools lola pessimistic marcie neco pnxdd
0005 2.546E+06 2.546E+06 2.546E+06 nc 2.546E+06 2.546E+06 2.546E+06
0010 1.006E+09 1.006E+09 1.006E+09 nc 1.006E+09 cc 1.006E+09
0020 to 8.054E+11 8.054E+11 nc 8.054E+11 cc 8.054E+11
0050 to 1.043E+16 1.043E+16 nc 1.043E+16 nc to
0100 to 1.726E+19 1.726E+19 nc 1.726E+19 nc to
0200 to cc 3.173E+22 nc to nc to
0500 to cc to nc to nc to
1000 to to to nc to nc to
LamportFastMutEx (Colored)
instances alpina greatSPN ITS-Tools lola pessimistic marcie neco pnxdd
2 380 nc 1370 nc nc nc nc
3 19742 nc 34529 nc nc nc nc
4 to nc 3.978E+07 nc nc nc nc
5 to nc 1.585E+09 nc nc nc nc
6 to nc mp nc nc nc nc
7 to nc mp nc nc nc nc
8 to nc mp nc nc nc nc
LamportFastMutEx (P/T)
instances alpina greatSPN ITS-Tools lola pessimistic marcie neco pnxdd
2 380 nc 380 nc 380 380 380
3 19742 nc 19742 nc 19742 19742 19742
4 to nc 1.915E+06 nc 1.915E+06 1.915E+06 1.915E+06
5 to nc 5.307E+08 nc to cc 5.307E+08
6 to nc mp nc to cc mp
7 to nc mp nc to to mp
8 to nc mp nc to to mp
MAPK (P/T)
instances alpina greatSPN ITS-Tools lola pessimistic marcie neco pnxdd
008 to 6.111E+06 6.111E+06 nc 6.111E+06 6.111E+06 6.111E+06
020 to 8.813E+10 8.813E+10 nc 8.813E+10 cc 8.813E+10
040 to 4.783E+14 4.783E+14 nc 4.783E+14 nc 4.783E+14
080 to to 5.635E+18 nc 5.635E+18 nc to
160 to to to nc to nc to
320 to to mp nc to nc to
NeoElection (Colored)
instances alpina greatSPN ITS-Tools lola pessimistic marcie neco pnxdd
2 241 nc 241 nc nc nc nc
3 29024 nc 974325 nc nc nc nc
4 to nc 2.919E+11 nc nc nc nc
5 to nc mp nc nc nc nc
6 to nc mp nc nc nc nc
7 to nc mp nc nc nc nc
8 to nc mp nc nc nc nc
NeoElection (P/T)
instances alpina greatSPN ITS-Tools lola pessimistic marcie neco pnxdd
2 241 nc 241 nc 241 241 241
3 29024 nc 974325 nc 974325 nc 974325
4 to nc 2.919E+11 nc to nc 2.919E+11
5 to nc mp nc to nc nc
6 to nc mp nc to nc to
7 to nc to nc to nc to
8 to nc to nc to nc to
PermAdmissibility (Colored)
instances alpina greatSPN ITS-Tools lola pessimistic marcie neco pnxdd
01 52537 nc 52537 nc nc nc nc
02 to nc mp nc nc nc nc
05 to nc mp nc nc nc nc
10 to nc mp nc nc nc nc
20 to nc mp nc nc nc nc
50 to nc mp nc nc nc nc
PermAdmissibility (P/T)
instances alpina greatSPN ITS-Tools lola pessimistic marcie neco pnxdd
01 52537 52537 52537 nc 52537 nc 52537
02 to cc mp nc to nc to
05 to cc mp nc to nc to
10 to cc mp nc to nc mp
20 to cc mp nc to nc mp
50 to cc mp nc to nc mp
Peterson (Colored)
instances alpina greatSPN ITS-Tools lola pessimistic marcie neco pnxdd
2 20754 nc 20754 nc nc nc nc
3 3.408E+06 nc 3.408E+06 nc nc nc nc
4 to nc mp nc nc nc nc
5 cc nc mp nc nc nc nc
6 cc nc mp nc nc nc nc
7 cc nc mp nc nc nc nc
Peterson (P/T)
instances alpina greatSPN ITS-Tools lola pessimistic marcie neco pnxdd
2 20754 nc 20754 nc 20754 20754 20754
3 3.408E+06 nc 3.408E+06 nc 3.408E+06 to 3.408E+06
4 to nc 6.299E+08 nc to cc 6.299E+08
5 cc nc 1.366E+11 nc to nc nc
6 cc nc mp nc to nc nc
7 cc nc mp nc to nc nc
Philosophers (Colored)
instances alpina greatSPN ITS-Tools lola pessimistic marcie neco pnxdd
000005 243 nc 243 nc nc nc nc
000010 59049 nc 59049 nc nc nc nc
000020 3.487E+09 nc 3.487E+09 nc nc nc nc
000050 7.179E+23 nc 7.179E+23 nc nc nc nc
000100 5.154E+47 nc 5.154E+47 nc nc nc nc
000200 cc nc 2.656E+95 nc nc nc nc
000500 cc nc 3.64E+238 nc nc nc nc
001000 cc nc +∞ (ovf) nc nc nc nc
002000 cc nc +∞ (ovf) nc nc nc nc
005000 cc nc +∞ (ovf) nc nc nc nc
010000 cc nc +∞ (ovf) nc nc nc nc
050000 cc nc +∞ (ovf) nc nc nc nc
100000 cc nc +∞ (ovf) nc nc nc nc
Philosophers (P/T)
instances alpina greatSPN ITS-Tools lola pessimistic marcie neco pnxdd
000005 243 243 243 nc 243 243 243
000010 59049 59049 59049 nc 59049 59049 59049
000020 3.487E+09 3.487E+09 3.487E+09 nc 3.487E+09 cc 3.487E+09
000050 7.179E+23 7.179E+23 7.179E+23 nc 7.179E+23 nc 7.179E+23
000100 5.154E+47 5.154E+47 5.154E+47 nc 5.154E+47 nc 5.154E+47
000200 cc 2.656E+95 2.656E+95 nc 2.656E+95 nc 2.656E+95
000500 cc to 3.64E+238 nc 3.64E+238 nc 3.64E+238
001000 cc mp +∞ (ovf) nc +∞ (ovf) nc +∞ (ovf)
002000 cc mp +∞ (ovf) nc +∞ (ovf) nc +∞ (ovf)
005000 cc mp +∞ (ovf) nc to nc to
010000 cc cc +∞ (ovf) nc to nc to
PhilosophersDyn (Colored)
instances alpina greatSPN ITS-Tools lola pessimistic marcie neco pnxdd
03 325 nc nc nc nc nc nc
10 cc nc nc nc nc nc nc
20 to nc nc nc nc nc nc
50 to nc nc nc nc nc nc
80 to nc nc nc nc nc nc
PhilosophersDyn (P/T)
instances alpina greatSPN ITS-Tools lola pessimistic marcie neco pnxdd
03 325 7251 7251 nc 7251 7251 7251
10 cc 199051 mp nc to cc 199051
20 to mp mp nc to nc to
Planning (P/T)
instances alpina greatSPN ITS-Tools lola pessimistic marcie neco pnxdd
cc nc nc nc cc nc nc nc
Railroad (P/T)
instances alpina greatSPN ITS-Tools lola pessimistic marcie neco pnxdd
005 1838 nc 1838 nc 1838 1838 1838
010 to nc 2.038E+06 nc 2.038E+06 2.038E+06 2.038E+06
020 to nc mp nc to cc nc
050 cc nc mp nc to nc nc
100 cc nc to nc to nc to
RessAllocation (P/T)
instances alpina greatSPN ITS-Tools lola pessimistic marcie neco pnxdd
R002C002 8 nc 8 nc 8 8 8
R003C002 20 nc 20 nc 20 20 20
R003C003 92 nc 92 nc 92 92 92
R003C005 1200 nc 1200 nc 1200 1200 1200
R003C010 to nc 823552 nc 823552 823552 823552
R003C015 to nc 5.789E+08 nc 5.789E+08 cc 5.789E+08
R003C020 to nc 4.065E+11 nc 4.065E+11 cc 4.065E+11
R003C050 to nc 4.872E+28 nc 4.872E+28 to 4.872E+28
R003C100 cc nc 1.420E+57 nc 1.420E+57 to 1.420E+57
R005C002 112 nc 112 nc 112 112 112
R010C002 6144 nc 6144 nc 6144 6144 6144
R015C002 to nc 278528 nc 278528 278528 278528
R020C002 to nc mp nc 1.153E+07 1.153E+07 1.153E+07
R050C002 to nc mp nc 2.927E+16 cc 2.927E+16
R100C002 to nc mp nc 6.465E+31 to 6.465E+31
Ring (P/T)
instances alpina greatSPN ITS-Tools lola pessimistic marcie neco pnxdd
none to nc 9.027E+11 nc 9.027E+11 nc 9.027E+11
RwMutex (P/T)
instances alpina greatSPN ITS-Tools lola pessimistic marcie neco pnxdd
r0010w0010 1034 nc 1034 nc 1034 1034 1034
r0010w0020 1044 nc 1044 nc 1044 1044 1044
r0010w0050 1074 nc 1074 nc 1074 1074 1074
r0010w0100 1124 nc 1124 nc 1124 1124 1124
r0010w0500 cc nc 1524 nc 1524 cc 1524
r0010w1000 cc nc 2024 nc 2024 cc 2024
r0010w2000 cc nc 3024 nc to cc to
r0020w0010 to nc mp nc 1048586 1048586 1048590
r0100w0010 to nc mp nc cc to nc
r0500w0010 cc nc mp nc cc cc nc
r1000w0010 cc nc mp nc cc cc nc
r2000w0010 cc nc to nc cc cc to
SharedMemory (Colored)
instances alpina greatSPN ITS-Tools lola pessimistic marcie neco pnxdd
000005 1863 nc 1863 nc nc nc nc
000010 1.831E+06 nc 1.831E+06 nc nc nc nc
000020 cc nc 4.451E+11 nc nc nc nc
000050 cc nc 5.870E+26 nc nc nc nc
000100 cc nc 1.701E+51 nc nc nc nc
000200 to nc 3.524E+99 nc nc nc nc
000500 cc nc 3.02E+243 nc nc nc nc
001000 cc nc +∞ (ovf) nc nc nc nc
002000 cc nc +∞ (ovf) nc nc nc nc
005000 cc nc +∞ (ovf) nc nc nc nc
010000 cc nc +∞ (ovf) nc nc nc nc
020000 cc nc +∞ (ovf) nc nc nc nc
050000 cc nc +∞ (ovf) nc nc nc nc
100000 cc nc +∞ (ovf) nc nc nc nc
SharedMemory (P/T)
instances alpina greatSPN ITS-Tools lola pessimistic marcie neco pnxdd
000005 1863 1863 1863 nc 1863 1863 1863
000010 1.831E+06 1.831E+06 1.831E+06 nc 1.831E+06 1.831E+06 1.831E+06
000020 cc mp 4.451E+11 nc 4.451E+11 cc 4.451E+11
000050 cc mp 5.870E+26 nc to nc to
000100 cc mp 1.701E+51 nc to nc to
000200 to cc 3.524E+99 nc to nc to
SimpleLoadBal (Colored)
instances alpina greatSPN ITS-Tools lola pessimistic marcie neco pnxdd
02 832 nc 832 nc nc nc nc
05 832 nc 116176 nc nc nc nc
10 cc nc 4.060E+08 nc nc nc nc
15 cc nc mp nc nc nc nc
20 cc nc mp nc nc nc nc
SimpleLoadBal (P/T)
instances alpina greatSPN ITS-Tools lola pessimistic marcie neco pnxdd
02 832 nc 832 nc 832 832 832
05 832 nc 116176 nc 116176 116176 116176
10 cc nc nc nc 4.060E+08 cc 4.060E+08
15 cc nc nc nc to cc 1.374E+12
20 cc nc nc nc to cc 4.583E+15
TokenRing (Colored)
instances alpina greatSPN ITS-Tools lola pessimistic marcie neco pnxdd
005 65 nc nc nc nc nc nc
010 cc nc nc nc nc nc nc
020 cc nc nc nc nc nc nc
050 cc nc nc nc nc nc nc
100 cc nc nc nc nc nc nc
200 to nc nc nc nc nc nc
500 cc nc nc nc nc nc nc
TokenRing (P/T)
instances alpina greatSPN ITS-Tools lola pessimistic marcie neco pnxdd
005 65 166 166 nc 166 166 166
010 cc 58905 58905 nc 58905 58905 58905
020 cc mp nc nc to nc 2.447E+10
050 cc cc nc nc to nc to