Gaston

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

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