Gaston

    Back to Gaston
  1. STRAND
    2.
  2. UABE
    3.
  3. Generated formulae
    4.

About benchmarks and experiments

We compared Gaston's performance on collective of parametric families of formulae designed to stress-test WS1S decision procedures used to evaluate some of the related works. The first set of families comes from the work of D'Antoni et al. [5], artificially enhanced by added quantifier alternations, the second benchmark consists of formulae used to evaluate the Toss tool as presented in [3] and the last set of benchmarks form evaluation of our previous approach implemented in the dWiNA tool [2].

Machine Specifications

Operating system: Debian GNU/Linux
Processor Intel Core i7-4770@3.4GHz Intel Core i7-2600@3.4GHz
Memory 32 GiB RAM 16 GiB RAM

Discussion

In this set of experiments, Gaston managed to win over the other tools on many of their own benchmark formulae.

Used notations

∞ the running time exceeded 2 minutes
oom the tool ran out of memory
k k quantifier alternations were added to the original benchmark
N/A benchmark required some feature or atomic predicate unsupported by the given tool
All Overall number of generated unique terms (e.g. DAG nodes)
Fixpoint Overall number of terms inside computed fixpoint
MONA State space generated by MONA on the leaf levels of the terms

HornLeq Families

Experimental results

benchmark MONA Gaston (Heuristic II) dWiNA Toss Coalg SFA
Time [s] Space [states] Time [s] Space [states] Time [s] Time [s] Time [s] Time [s]
All Fixpoint MONA non-TNF TNF
HornLeq
horn_leq02.mona 0.01 18 0.01 31 7 22 0.01 0.01 0.01 0.01 0.01
horn_leq03.mona 0.01 35 0.01 78 26 44 0.01 0.01 0.01 0.01 0.01
horn_leq04.mona 0.01 66 0.01 145 56 66 0.01 0.008 0.008 0.008 0.01
horn_leq05.mona 0.01 123 0.01 224 97 88 0.01 0.012 0.012 0.104 0.01
horn_leq06.mona 0.01 230 0.01 314 149 110 0.01 0.016 0.016 1.096 0.01
horn_leq07.mona 0.01 328 0.01 416 212 132 0.01 0.016 0.016 0 0.01
horn_leq08.mona 0.01 834 0.01 530 286 154 0.01 0.02 0.02 101.484 0.01
horn_leq09.mona 0.01 1619 0.01 656 371 176 0.01 0.024 0.028 ∞ 0.01
horn_leq10.mona 0.01 3174 0.01 794 467 198 0.01 0.032 0.036 ∞ 0.016
horn_leq11.mona 0.05 6267 0.01 944 574 220 0.01 0.032 0.036 ∞ 0.017
horn_leq12.mona 0.09 12434 0.01 1106 692 242 0.01 0.04 0.04 ∞ 0.019
horn_leq13.mona 0.19 24747 0.01 1280 821 264 0.01 0.04 0.044 ∞ 0.02
horn_leq14.mona 0.45 49350 0.01 1466 961 286 0.01 0.044 0.044 ∞ 0.021
horn_leq15.mona 1.19 98531 0.01 1664 1112 308 0.02 0.048 0.048 ∞ 0.031
horn_leq16.mona 3.35 196866 0.01 1874 1274 330 0.02 0.052 0.052 ∞ 0.035
horn_leq17.mona 9.07 393507 0.01 2096 1447 352 0.02 0.052 0.056 ∞ 0.034
horn_leq18.mona 22.89 786758 0.01 2330 1631 374 0.02 0.06 0.06 ∞ 0.033
horn_leq19.mona oom 0.01 2576 1826 396 0.03 0.064 0.076 ∞ 0.032
horn_leq20.mona oom 0.01 2834 2032 418 0.03 0.076 0.1 ∞ 0.032
HornLeq (+1)
horn_leq02_1alts.mona 0.01 18 0.01 30 0 28 0.01 0.01 0.01 0.01 0.01
horn_leq03_1alts.mona 0.01 35 0.01 69 13 56 0.01 0.01 0.01 0.01 0.01
horn_leq04_1alts.mona 0.01 65 0.01 113 35 84 0.01 0.008 0.008 0.008 0.01
horn_leq05_1alts.mona 0.01 120 0.01 166 66 112 0.01 0.024 0.008 0.056 0.015
horn_leq06_1alts.mona 0.01 224 0.01 214 106 140 0.02 0.016 0.008 0.412 0.024
horn_leq07_1alts.mona 0.01 425 0.01 264 155 168 0.11 0.02 0.008 3.152 0.067
horn_leq08_1alts.mona 0.01 819 0.01 316 213 196 0.42 0.028 0.012 22.556 0.134
horn_leq09_1alts.mona 0.01 1598 0.01 370 280 224 2.27 0.032 0.012 ∞ 0.47
horn_leq10_1alts.mona 0.02 3146 0.01 426 356 252 14.43 0.044 0.016 ∞ 1.823
horn_leq11_1alts.mona 0.04 6231 0.01 484 441 280 95.61 0.048 0.016 ∞ 9.398
horn_leq12_1alts.mona 0.1 12389 0.01 544 535 308 ∞ 0.064 0.016 ∞ 58.985
horn_leq13_1alts.mona 0.15 24692 0.01 606 638 336 ∞ 0.068 0.016 ∞ ∞
horn_leq14_1alts.mona 0.4 49284 0.01 670 750 364 ∞ 0.084 0.016 ∞ ∞
horn_leq15_1alts.mona 1.09 98453 0.01 736 871 392 ∞ 0.1 0.02 ∞ ∞
horn_leq16_1alts.mona 3.05 196775 0.01 804 1001 420 ∞ 0.112 0.02 ∞ ∞
horn_leq17_1alts.mona 8.18 393402 0.01 874 1140 448 ∞ 0.128 0.02 ∞ ∞
horn_leq18_1alts.mona 20.55 786638 0.01 946 1288 476 ∞ 0.144 0.02 ∞ ∞
horn_leq19_1alts.mona oom 0.01 1020 1445 504 ∞ 0.16 0.024 ∞ ∞
horn_leq20_1alts.mona oom 0.01 1096 1611 532 ∞ 0.176 0.024 ∞ ∞
HornLeq (+2)
horn_leq02_2alts.mona 0.01 18 0.01 30 0 28 0.01 0.01 0.01 0.01 0.01
horn_leq03_2alts.mona 0.01 35 0.01 88 28 56 0.01 0.01 0.01 0.01 0.01
horn_leq04_2alts.mona 0.01 65 0.01 95 0 84 0.01 0.012 0.012 0.028 0.031
horn_leq05_2alts.mona 0.01 120 0.01 123 0 106 0.01 0.016 0.016 0.208 0.019
horn_leq06_2alts.mona 0.01 224 0.01 151 0 128 0.01 0.02 0.016 1.42 0.044
horn_leq07_2alts.mona 0.01 425 0.01 179 0 150 0.04 0.024 0.02 9.616 0.14
horn_leq08_2alts.mona 0.01 819 0.01 207 0 172 0.1 0.028 0.024 62.828 0.319
horn_leq09_2alts.mona 0.01 1598 0.01 235 0 194 0.23 0.028 0.028 ∞ 1.109
horn_leq10_2alts.mona 0.01 3146 0.01 263 0 216 0.68 0.036 0.032 ∞ 4.157
horn_leq11_2alts.mona 0.03 6231 0.01 291 0 238 2.19 0.04 0.036 ∞ 21.02
horn_leq12_2alts.mona 0.1 12389 0.01 319 0 260 7.61 0.044 0.044 ∞ 146.711
horn_leq13_2alts.mona 0.19 24692 0.01 347 0 282 28.6 0.048 0.048 ∞ ∞
horn_leq14_2alts.mona 0.36 49284 0.01 375 0 304 113.64 0.048 0.052 ∞ ∞
horn_leq15_2alts.mona 1.14 98453 0.01 403 0 326 ∞ 0.048 0.052 ∞ ∞
horn_leq16_2alts.mona 3.06 196775 0.01 431 0 348 ∞ 0.056 0.056 ∞ ∞
horn_leq17_2alts.mona 8.03 393402 0.01 459 0 370 ∞ 0.06 0.056 ∞ ∞
horn_leq18_2alts.mona 20.49 786638 0.01 487 0 392 ∞ 0.064 0.064 ∞ ∞
horn_leq19_2alts.mona oom 0.01 515 0 414 ∞ 0.068 0.064 ∞ ∞
horn_leq20_2alts.mona oom 0.01 543 0 436 ∞ 0.08 0.072 ∞ ∞
HornLeq (+3)
horn_leq03_3alts.mona 0.01 35 0.01 88 28 56 0.01 0.01 0.01 0.008 0.01
horn_leq04_3alts.mona 0.01 65 0.01 122 40 67 0.01 0.016 0.016 0.152 0.058
horn_leq05_3alts.mona 0.01 120 0.01 108 0 95 0.01 0.008 0.008 1.092 0.073
horn_leq06_3alts.mona 0.01 224 0.01 184 53 140 0.02 0.016 0.008 7.36 0.15
horn_leq07_3alts.mona 0.01 425 0.01 239 94 168 0.12 0.016 0.012 47.648 0.382
horn_leq08_3alts.mona 0.01 819 0.01 289 144 196 0.35 0.024 0.012 ∞ 0.726
horn_leq09_3alts.mona 0.01 1598 0.01 341 203 224 1.4 0.032 0.012 ∞ 2.353
horn_leq10_3alts.mona 0.02 3146 0.01 395 271 252 6.06 0.036 0.012 ∞ 13.616
horn_leq11_3alts.mona 0.04 6231 0.01 451 348 280 29.53 0.048 0.012 ∞ 39.229
horn_leq12_3alts.mona 0.1 12389 0.01 509 434 308 ∞ 0.052 0.016 ∞ ∞
horn_leq13_3alts.mona 0.2 24692 0.01 569 529 336 ∞ 0.064 0.016 ∞ ∞
horn_leq14_3alts.mona 0.43 49284 0.01 631 633 364 ∞ 0.076 0.02 ∞ ∞
horn_leq15_3alts.mona 1.1 98453 0.01 695 746 392 ∞ 0.088 0.024 ∞ ∞
horn_leq16_3alts.mona 3.05 196775 0.01 761 868 420 ∞ 0.096 0.024 ∞ ∞
horn_leq17_3alts.mona 8.04 393402 0.01 829 999 448 ∞ 0.112 0.024 ∞ ∞
horn_leq18_3alts.mona 20.55 786638 0.01 899 1139 476 ∞ 0.128 0.024 ∞ ∞
horn_leq19_3alts.mona oom 0.01 971 1288 504 ∞ 0.148 0.024 ∞ ∞
horn_leq20_3alts.mona oom 0.01 1045 1446 532 ∞ 0.16 0.028 ∞ ∞
HornLeq (+4)
horn_leq04_4alts.mona 0.01 65 0.01 122 40 67 0.01 0.016 0.016 0.464 0.06
horn_leq05_4alts.mona 0.01 120 0.01 222 157 95 0.01 0.016 0.02 7.3 0.143
horn_leq06_4alts.mona 0.01 224 0.01 141 0 126 0.02 0.02 0.024 51.2 0.227
horn_leq07_4alts.mona 0.01 425 0.01 173 0 151 0.06 0.016 0.016 ∞ 0.665
horn_leq08_4alts.mona 0.01 819 0.01 216 0 184 0.15 0.02 0.016 ∞ 1.87
horn_leq09_4alts.mona 0.01 1598 0.01 244 0 206 0.36 0.024 0.02 ∞ 4.494
horn_leq10_4alts.mona 0.01 3146 0.01 272 0 228 0.89 0.024 0.016 ∞ 21.617
horn_leq11_4alts.mona 0.04 6231 0.01 300 0 250 2.73 0.024 0.024 ∞ 64.341
horn_leq12_4alts.mona 0.1 12389 0.01 328 0 272 8.71 0.024 0.024 ∞ ∞
horn_leq13_4alts.mona 0.19 24692 0.01 356 0 294 29.98 0.024 0.024 ∞ ∞
horn_leq14_4alts.mona 0.43 49284 0.01 384 0 316 ∞ 0.028 0.024 ∞ ∞
horn_leq15_4alts.mona 1.13 98453 0.01 412 0 338 ∞ 0.028 0.024 ∞ ∞
horn_leq16_4alts.mona 3.07 196775 0.01 440 0 360 ∞ 0.036 0.028 ∞ ∞
horn_leq17_4alts.mona 7.99 393402 0.01 468 0 382 ∞ 0.032 0.028 ∞ ∞
horn_leq18_4alts.mona 20.52 786638 0.01 496 0 404 ∞ 0.036 0.028 ∞ ∞
horn_leq19_4alts.mona oom 0.01 524 0 426 ∞ 0.04 0.032 ∞ ∞
horn_leq20_4alts.mona oom 0.01 552 0 448 ∞ 0.04 0.028 ∞ ∞

HornIn Family

benchmark MONA Gaston (Heuristic II) dWiNA Toss Coalg SFA
Time [s] Space [states] Time [s] Space [states] Time [s] Time [s] Time [s] Time [s]
All Fixpoint MONA non-TNF TNF
Horn In
horn_in02.mona 0.01 23 0.01 48 3 40 0.01 0.012 0.01 0.01 0.035
horn_in03.mona 0.01 52 0.01 93 6 80 0.01 0.008 0.008 0.01 0.068
horn_in04.mona 0.01 117 0.01 137 8 120 0.01 0.012 0.016 0.02 0.265
horn_in05.mona 0.01 261 0.01 185 10 160 0.03 0.012 0.02 0.136 0.758
horn_in06.mona 0.01 576 0.01 229 12 200 0.13 0.016 0.032 1.068 2.645
horn_in07.mona 0.01 1258 0.01 273 14 240 0.29 0.024 0.04 8.5 8.31
horn_in08.mona 0.01 2723 0.01 317 16 280 1.16 0.024 0.044 68.048 32.436
horn_in09.mona 0.03 5851 0.01 361 18 320 3.42 0.028 0.06 ∞ ∞
horn_in10.mona 0.09 12498 0.01 405 20 360 18.4 0.036 0.068 ∞ ∞
horn_in11.mona 0.2 26568 0.01 449 22 400 54.74 0.036 0.08 ∞ ∞
horn_in12.mona 0.48 56253 0.01 493 24 440 ∞ 0.04 0.096 ∞ ∞
horn_in13.mona 1.2 118705 0.01 537 26 480 ∞ 0.044 0.112 ∞ ∞
horn_in14.mona 2.95 249764 0.01 581 28 520 ∞ 0.048 0.124 ∞ ∞
horn_in15.mona 7.26 524182 0.01 625 30 560 ∞ 0.052 0.144 ∞ ∞
horn_in16.mona oom 0.01 669 32 600 ∞ 0.056 0.16 ∞ ∞
horn_in17.mona oom 0.01 713 34 640 ∞ 0.06 0.176 ∞ ∞
horn_in18.mona oom 0.01 757 36 680 ∞ 0.064 0.196 ∞ ∞
horn_in19.mona oom 0.01 801 38 720 ∞ 0.068 0.22 ∞ ∞
horn_in20.mona oom 0.01 845 40 760 ∞ 0.072 0.24 ∞ ∞

Antichain Families

benchmark MONA Gaston (Heuristic II) dWiNA Toss Coalg SFA
Time [s] Space [states] Time [s] Space [states] Time [s] Time [s] Time [s] Time [s]
All Fixpoint MONA non-TNF TNF
Horn Trans
horn_trans03.mona 0.01 0 0.01 161 0 108 0 N/A N/A 0.01
horn_trans04.mona 0.01 0 0.01 648 0 368 0.01 0.058
horn_trans05.mona 0.01 0 0.01 1315 0 880 0.03 0.103
horn_trans06.mona 0.01 0 0.02 2654 0 1728 0.09 0.172
horn_trans07.mona 0.03 0 0.05 5265 0 2996 0.24 0.276
horn_trans08.mona 0.07 0 0.08 10517 0 4768 0.63 0.607
horn_trans09.mona 0.14 0 0.09 10675 0 7128 1.68 0.847
horn_trans10.mona 0.28 0 0.16 21269 0 10160 4.08 0.995
horn_trans11.mona 0.71 0 0.1 21343 0 13948 9.69 1.388
horn_trans12.mona 1.53 0 0.27 42776 0 18576 21.45 2.514
horn_trans13.mona 3.08 0 0.3 42889 0 24128 44.71 4.152
horn_trans14.mona 5.93 0 0.5 85662 0 30688 88.9 6.985
horn_trans15.mona 6.39 0 0.53 86358 0 38340 ∞ 9.308
horn_trans16.mona 11.15 0 0.56 86259 0 47168 ∞ 14.317
horn_trans17.mona 19.48 0 0.58 85843 0 57256 ∞ 16.968
horn_trans18.mona 32.87 0 0.99 173533 0 68688 ∞ 16.09
horn_trans19.mona 53.83 0 1.07 173710 0 81548 ∞ 25.285
horn_trans20.mona 86.43 0 1.06 173060 0 95920 ∞ 38.56
Set Closed
set_closed01.mona 0.01 77 0.01 185 125 85 0 0.016 0.016 0.04 0.01
set_closed02.mona 0.01 104 0.01 517 1050 170 0 0.024 0.06 ∞ 0.128
set_closed03.mona 0.01 155 0.01 1087 9127 255 0 0.184 0.704 ∞ 0.142
set_closed04.mona 0.34 266 0.06 3779 80386 340 0 ∞ ∞ 13.956
set_closed05.mona oom 1.86 14412 707806 425 0 ∞ ∞ ∞
set_closed06.mona oom 87.64 67976 5915136 510 0.01 ∞ ∞ ∞
set_closed07.mona oom ∞ 0 0 0 0.01 ∞ ∞ ∞
set_closed08.mona oom ∞ 0 0 0 0.03 ∞ ∞ ∞
set_closed09.mona oom ∞ 0 0 0 0.1 ∞ ∞ ∞
set_closed10.mona oom ∞ 0 0 0 0.27 ∞ ∞ ∞
set_closed11.mona oom ∞ 0 0 0 0.95 ∞ ∞ ∞
set_closed12.mona oom ∞ 0 0 0 3.61 ∞ ∞ ∞
set_closed13.mona oom ∞ 0 0 0 14.3 ∞ ∞ ∞
set_closed14.mona oom ∞ 0 0 0 69.08 ∞ ∞ ∞
set_closed15.mona oom ∞ 0 0 0 ∞ ∞ ∞ ∞
set_closed16.mona oom ∞ 0 0 0 ∞ ∞ ∞ ∞
set_closed17.mona oom ∞ 0 0 0 ∞ ∞ ∞ ∞
set_closed18.mona oom ∞ 0 0 0 ∞ ∞ ∞ ∞
set_closed19.mona oom ∞ 0 0 0 ∞ ∞ ∞ ∞
set_closed20.mona oom ∞ 0 0 0 ∞ ∞ ∞ ∞
Set Singletons
set_singletons01.mona 0.01 45 0.01 61 9 51 0 0.008 0.004 N/A 0.01
set_singletons02.mona 0.01 67 0.01 127 23 102 0 0.012 0.012 0.011
set_singletons03.mona 0.01 105 0.01 190 40 153 0.02 0.012 0.016 40.27
set_singletons04.mona 1.49 175 0.01 256 61 204 0.08 0.02 0.02 ∞
set_singletons05.mona oom 0.01 319 86 255 0.28 0.028 0.024 ∞
set_singletons06.mona oom 0.01 382 115 306 1.33 0.032 0.032 ∞
set_singletons07.mona oom 0.01 445 148 357 7.32 0.036 0.036 ∞
set_singletons08.mona oom 0.01 508 185 408 38.99 0.04 0.04 ∞
set_singletons09.mona oom 0.01 571 226 459 ∞ 0.048 0.044 ∞
set_singletons10.mona oom 0.01 634 271 510 ∞ 0.052 0.052 ∞
set_singletons11.mona oom 0.01 697 320 561 ∞ 0.056 0.06 ∞
set_singletons12.mona oom 0.01 760 373 612 ∞ 0.06 0.06 ∞
set_singletons13.mona oom 0.01 823 430 663 ∞ 0.068 0.072 ∞
set_singletons14.mona oom 0.01 886 491 714 ∞ 0.068 0.072 ∞
set_singletons15.mona oom 0.01 949 556 765 ∞ 0.076 0.084 ∞
set_singletons16.mona oom 0.01 1012 625 816 ∞ 0.08 0.084 ∞
set_singletons17.mona oom 0.01 1075 698 867 ∞ 0.088 0.092 ∞
set_singletons18.mona oom 0.01 1138 775 918 ∞ 0.088 0.096 ∞
set_singletons19.mona oom 0.01 1201 856 969 ∞ 0.096 0.1 ∞
set_singletons20.mona oom 0.01 1264 941 1020 ∞ 0.104 0.104 ∞

Acknowledgement

We thank authors of benchmarks used to evaluate tools of Toss (Ganzow, T. and Kaiser, L.) and SFA (D'Antoni, L. and Veanes, M.), which we were able to recreate in order to measure all of the tools and decision procedures.

  1. Elgaard, J., Klarlund, N., Møller, A.: MONA 1.x: new techniques for WS1S and WS2S
  2. Fiedor, T., Holik, L., Lengal, O., Vojnar, T.: Nested antichains for WS1S
  3. Ganzow, T., Kaiser, L.: New algorithm for weak monadic second-order logic on inductive structures.
  4. Traytel, D.: A coalgebraic decision procedure for WS1S
  5. D'Antoni, L., Veanes, M.: Minimization of symbolic automata
  6. Madhusudan, P., Qiu, X.: Efficient decision procedures for heaps using STRAND.
  7. Klarlund, N., Møller, A., Schwartzbach, M.I.: MONA implementation secrets