dWiNA

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

About

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.

Experimental results

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