dWiNA

    Back to dWiNA
  1. STRAND
  2. Regsy
  3. Generated formulae

About

We evaluated these formulae in Mode (I), i.e. we used MONA to generate determinsitic automaton corresponding to the matrix of the formula, translate it to the libvata representation and then we run our algorithm to deal only with the prefix of formulae. We chose this approach, because the other Mode (II) took too long to generate base automaton (missing reduction technique in libvata is one of the sources of time consumption). We further tried to force MONA to work with formulae in existential prenex normal form (denoted ExPNF) to show the exponential blow-up problem with deterministic automata.

Experiments show that dWiNA generated considerably less states when handling prefix (denoted Prefix Only). However, out of the generated states (Prefix Only gen) most of them were evaluated (Prefix Only eval) and thus pruning of the states based on subsumption relation did not have great impact on these formulae.

Experimental results

benchmark MONA dWiNA
Time [s] Space [states] Time [s] Space [states]
DecProc DecProc ExPNF Prefix Only Prefix Only ExPNF Overall DecProc Prefix Only eval Prefix Only gen
bubblesort-else.mona 0.01 0.45 1285 12071 15163 0.01 14 19
bubblesort-if-else.mona 0.02 2.17 4260 116760 63444 0.23 234 234
bubblesort-if-if.mona 0.12 5.29 8390 233372 130555 1.14 28 28
sorted-list-insert-after-loop.mona 0.0 0.0 167 686 2584 0.0 28 36
sorted-list-insert-before-head.mona 0.0 0.0 43 152 645 0.0 38 45
sorted-list-insert-before-loop.mona 0.0 0.01 103 1021 1415 0.0 38 47
sorted-list-insert-error-error.mona 0.0 0.0 103 1021 1415 0.0 38 47
sorted-list-insert-in-loop.mona 0.01 0.07 463 5015 5963 0.0 59 59
sorted-list-reverse-after-loop.mona 0.0 0.0 179 1326 1886 0.0 100 110
sorted-list-reverse-before-loop.mona 0.0 0.0 179 1326 1886 0.0 1782 1782
sorted-list-reverse-in-loop.mona 0.02 0.47 1311 70287 24210 0.02 260 271
sorted-list-search-after-loop.mona 0.0 0.0 90 278 1012 0.0 262 274
sorted-list-search-before-loop.mona 0.0 0.0 90 426 1119 0.0 262 274
sorted-list-search-in-loop.mona 0.01 0.48 1311 70287 24210 0.02 84 84
Note: For commented versions of these formulae consult the site of the STRAND original experiments.

Acknowledgement

We thank authors of STRAND tool (P. Madhusudan, X. Qiu and G. Parlato) for publication of their experiments with WSkS formulae.