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].
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 |
In this set of experiments, Gaston managed to win over the other tools on many of their own benchmark formulae.
∞ | 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 |
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 | ∞ | ∞ |
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 | ∞ | ∞ |
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 | ∞ |
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.