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.
| 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 | |
| addition.mona | 0.0 | 0.0 | 6 | 251 | 214 | 0.0 | 5 | 5 |
| approximation.mona | 0.0 | -1 | 70 | -1 | 5481 | 0.0 | 24 | 24 |
| company-production.mona | 0.0 | -1 | 298 | -1 | 239903 | 0.0 | 14 | 19 |
| four-weights.mona | 0.0 | -1 | 91 | -1 | 34731 | 0.0 | 234 | 234 |
| christmas.mona | 0.03 | -1 | 2463 | -1 | 4924 | 0.0 | 28 | 28 |
| six-modulo-test.mona | 0.0 | -1 | 16 | -1 | 753 | 0.0 | 11 | 11 |
| smoothing.mona | 0.01 | -1 | 545 | -1 | 1668152 | 0.0 | 22 | 29 |
| syracuse-unfolding.mona | 0.0 | -1 | 67 | -1 | 2126 | 0.0 | 22 | 29 |
| three-weigths-minimisation.mona | 0.0 | -1 | 83 | -1 | 257779 | 0.0 | 56 | 56 |
We thank authors of RegSy tool (J. Hamza, B. Jobstmann, and V. Kuncak) for publication of their experiments with WSkS formulae.