We evaluated these formulae in Mode (II), i.e. we used VATA library to generate non-deterministic automaton corresponding to the matrix of the formulae and run our algorithm to deal with whole formulae. We chose this approach to show the power of nondeterministic automata and also in Mode (I) the translation from MONA to VATA representation took considerable amount of time resulting into numerous timeouts. All the generated formulae are in prenex form.
Our experiments show that not only are nondeterministic automata efficient when handling certain class of formulae, but our tool handles most of these generated formulae more efficiently than MONA, which runs out of memory for some 1 < k < n. However, for one kind of formulae, our approach fails on timeout due to excessive time needed to build nondeterministic base automaton.
Note that we are using notation
&_{1 <= i <= n} to denote conjuction over the i ranging
from 1 to n. Further we use the following notation i, j, k in perm(3)to denote that i, j, k are ranging over all of the permutations of choices of three indexes.
horn_sub_n_k ::= ex2 Y: ~ex2 X1,...,~ex2 Xk,...,Xn: &_{1 <= i <= n} (Xi sub Y & Xi sub Xi+1 & Xi ~= Xi+1) => Xi+1 sub Y;
| benchmark | MONA | dWiNA | |||
|---|---|---|---|---|---|
| Time [s] | Space [states] | Time [s] | Space [states] | ||
| DecProc | Overall | DecProc | Overall eval | Overall gen | |
| horn_sub10_1alts.mona | 0.11 | 10718 | 0.0 | 39 | 39 |
| horn_sub11_2alts.mona | 0.2 | 25517 | 0.0 | 44 | 45 |
| horn_sub12_3alts.mona | 0.57 | 60924 | 0.0 | 50 | 85 |
| horn_sub13_4alts.mona | 1.79 | 145765 | 0.02 | 58 | 320 |
| horn_sub14_5alts.mona | 4.98 | 349314 | 0.02 | 70 | 2415 |
| horn_sub15_6alts.mona | insufficient memory | insufficient memory | 0.47 | 90 | 24614 |
horn_trans_n: all2 Y: ex2 X1,...Xn: ~ &_{i, j, k in perm(3)} Xi sub Y & (Xi sub Xj & Xj sub Xk) => Xi sub Xk;
| benchmark | MONA | dWiNA | |||
|---|---|---|---|---|---|
| Time [s] | Space [states] | Time [s] | Space [states] | ||
| DecProc | Overall | DecProc | Overall eval | Overall gen | |
| horn_trans03.mona | 0.0 | 84 | 0.0 | 15 | 15 |
| horn_trans04.mona | 0.0 | 126 | 0.0 | 35 | 35 |
| horn_trans05.mona | 0.0 | 204 | 0.0 | 73 | 73 |
| horn_trans06.mona | 0.0 | 330 | 0.0 | 135 | 135 |
| horn_trans07.mona | 0.01 | 516 | 0.0 | 227 | 227 |
| horn_trans08.mona | 0.04 | 774 | 0.0 | 355 | 355 |
| horn_trans09.mona | 0.12 | 1116 | 0.0 | 525 | 525 |
| horn_trans10.mona | 0.24 | 1554 | 0.0 | 743 | 743 |
| horn_trans11.mona | 0.51 | 2100 | 0.01 | 1015 | 1015 |
| horn_trans12.mona | 1.02 | 2766 | 0.01 | 1347 | 1347 |
| horn_trans13.mona | 1.98 | 3564 | 0.02 | 1745 | 1745 |
| horn_trans14.mona | 3.7 | 4506 | 0.04 | 2215 | 2215 |
| horn_trans15.mona | 6.66 | 5604 | 0.06 | 2763 | 2763 |
| horn_trans16.mona | 11.75 | 6870 | 0.1 | 3395 | 3395 |
| horn_trans17.mona | 19.97 | 8316 | 0.15 | 4117 | 4117 |
| horn_trans18.mona | 32.89 | 9954 | 0.23 | 4935 | 4935 |
| horn_trans19.mona | 53.5 | 11796 | 0.32 | 5855 | 5855 |
| horn_trans20.mona | 85.39 | 13854 | 0.46 | 6883 | 6883 |
set_obvious_n: ex2 X1,...,Xn: all2 Y: &_{1 <= i <= n} (Y sub Xi & Xi ~= y) => ~Xi sub X;
| benchmark | MONA | dWiNA | |||
|---|---|---|---|---|---|
| Time [s] | Space [states] | Time [s] | Space [states] | ||
| DecProc | Overall | DecProc | Overall eval | Overall gen | |
| set_obvious01.mona | 0.0 | 16 | 0.0 | 5 | 6 |
| set_obvious02.mona | 0.0 | 46 | 0.0 | 7 | 10 |
| set_obvious03.mona | 0.0 | 267 | 0.0 | 9 | 16 |
| set_obvious04.mona | 0.09 | 7436 | 0.0 | 11 | 26 |
| set_obvious05.mona | insufficient memory | insufficient memory | 0.0 | 13 | 44 |
| set_obvious06.mona | insufficient memory | insufficient memory | 0.01 | 15 | 78 |
| set_obvious07.mona | insufficient memory | insufficient memory | 0.05 | 17 | 144 |
| set_obvious08.mona | insufficient memory | insufficient memory | 0.23 | 19 | 274 |
| set_obvious09.mona | insufficient memory | insufficient memory | 1.09 | 21 | 532 |
| set_obvious10.mona | insufficient memory | insufficient memory | 5.13 | 23 | 1046 |
| set_obvious11.mona | insufficient memory | insufficient memory | 23.92 | 25 | 2072 |
| set_obvious12.mona | insufficient memory | insufficient memory | timeout | timeout | timeout |
set_closed_n: ex2 X1,...,Xn: all1 x: ex1 y, z: ~&_{1 <= i <= n} (x in Xi & x <= y & y <= z & z in Xi) => y in Xi;
| benchmark | MONA | dWiNA | |||
|---|---|---|---|---|---|
| Time [s] | Space [states] | Time [s] | Space [states] | ||
| DecProc | Overall | DecProc | Overall eval | Overall gen | |
| set_closed01.mona | 0.0 | 104 | 0.0 | 12 | 26 |
| set_closed02.mona | 0.0 | 195 | 0.0 | 16 | 118 |
| set_closed03.mona | 0.0 | 1376 | 0.0 | 20 | 1488 |
| set_closed04.mona | 0.25 | 52697 | timeout | timeout | timeout |
| set_closed05.mona | insufficient memory | insufficient memory | timeout | timeout | timeout |
set_singletons_n: ex2 X1,...,Xn: all1 x, y: &_{1 <= i <= n} (x in Xi & y in Xi) => x = y;
| benchmark | MONA | dWiNA | |||
|---|---|---|---|---|---|
| Time [s] | Space [states] | Time [s] | Space [states] | ||
| DecProc | Overall | DecProc | Overall eval | Overall gen | |
| set_singletons01.mona | 0.0 | 57 | 0.0 | 24 | 26 |
| set_singletons02.mona | 0.0 | 108 | 0.0 | 45 | 53 |
| set_singletons03.mona | 0.0 | 443 | 0.0 | 66 | 92 |
| set_singletons04.mona | 1.43 | 66024 | 0.03 | 87 | 167 |
| set_singletons05.mona | insufficient memory | insufficient memory | 0.15 | 108 | 350 |
| set_singletons06.mona | insufficient memory | insufficient memory | 0.82 | 129 | 857 |
| set_singletons07.mona | insufficient memory | insufficient memory | timeout | timeout | timeout |