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
dartes_1.fsa 662 1.03886e+13 257 1557 40 170296 74 38230
dp_12.fsa 144 531440 48 373 5 21367 10 4821
elevator_1 126 163 99 525 15 131175 28 75661
elevator_2 292 1092 299 1605 ?? ?? ?? ??
elevator_3 654 7276 783 4175 ?? ?? ?? ??
elevator_4 ?? ?? ?? ?? ?? ?? ?? ??
hartstone_25.fsa 254 1.67772e+08 77 508 13 29302 26 11822
hartstone_50.fsa 504 5.6295e+15 152 1008 ?? ?? ?? ??
hartstone_75.fsa 754 1.88895e+23 227 1508 ?? ?? ?? ??
hartstone_100.fsa 1004 6.33825e+30 302 2008 ?? ?? ?? ??
key_2 188 536 92 487 16 72753 27 32982
key_3 258 4923 133 686 23 637956 41 225151
key_4 328 44819 174 882 28 18955007 52 626592
mmgt_2.fsa 172 816 114 429 ?? ?? ?? ??
mmgt_3.fsa 244 7702 172 630 ?? ?? ?? ??
mmgt_4.fsa 316 66308 232 847 ?? ?? ?? ??
q_1.fsa 326 123596 194 1043 33 335343 57 66993
sentest_100.fsa 658 1238 130 965 16 53088 25 18069
speed_1.fsa 66 44344 39 208 3 14904 9 2489


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