next up previous
Next: Fixed variable order results Up: Evaluating Symbolic Traversal Algorithms Previous: Benchmark Description

General benchmark data


General Transyt NuSMV VIS
Name Vars Reachable TR parts TR size TR parts TR size TR parts TR size
c-arbiter 98 3.33813e+09 70 280 4 50216 8 3854
c-arbiter-xl 126 5.46918e+13 98 342 6 53859 12 5563
gals 84 1232 15 369 2 5437 5 1788
muller_5 50 20 10 100 2 2081 2 1155
muller_10 100 420 20 200 3 4198 5 2364
muller_15 150 6006 30 300 4 7640 10 4191
muller_20 200 251940 40 400 5 10309 9 4873
muller_25 250 4 50 500 6 15398 11 6103
muller_30 300 6.009e+07 60 600 7 27668 ?? ??
muller_40 400 4.64139e+10 80 800 ?? ?? ?? ??
muller_50 500 3.61071e+13 100 1000 ?? ?? ?? ??
muller_60 600 8.38369e+15 120 1200 ?? ?? ?? ??
muller_70 700 7.01713e+18 140 1400 ?? ?? ?? ??
muller_80 800 5.82061e+21 160 1600 ?? ?? ?? ??
muller_90 900 1.34627e+24 180 1800 ?? ?? ?? ??
muller_100 1000 1.16143e+27 200 2000 ?? ?? ?? ??
pcc 68 989184 30 221 3 25972 5 2158
pipeline1 26 2516 21 71 1 8378 2 795
pipeline2 42 372368 35 121 2 6361 4 1130
pipeline4 74 372368 63 220 4 8649 4 1103
pipelineabs1 52 532 16 107 2 1959 3 1070
pipelineabs2 80 14896 24 165 2 24478 5 1446
pipelineabs4 136 1 40 281 3 45314 7 3077
pipelineabs8 248 7.17824e+12 72 513 5 95867 11 6336
pipelineabs16 472 2.71195e+24 136 977 ?? ?? ?? ??
stari4 56 5 56 182 4 7327 5 3403
stari8 104 1.07225e+12 104 358 6 43982 9 6806
stari12 152 2.12662e+17 152 535 ?? ?? ?? ??
stari16 200 4.21776e+22 200 707 ?? ?? ?? ??
tree5 74 1620 24 159 3 7878 4 2886
tree10 134 492075 44 294 5 45714 9 14226
tree15 194 1.43489e+08 64 429 6 389779 11 334233
tree20 254 4.06792e+10 84 565 ?? ?? ?? ??
tree30 374 3.08837e+15 124 834 ?? ?? ?? ??
tree40 494 2.22891e+20 164 1105 ?? ?? ?? ??
tree50 614 1.55545e+25 204 1372 ?? ?? ?? ??
tree60 734 1.05978e+30 244 1642 ?? ?? ?? ??
tree70 854 7.09227e+34 284 1915 ?? ?? ?? ??


next up previous
Next: Fixed variable order results Up: Evaluating Symbolic Traversal Algorithms Previous: Benchmark Description
Enric Pastor 2004-05-28