dWiNA is an implementation of backward decision procedure for WS*k*S logic (weak second-order theory of *k* successors). The tool is using *libvata* a highly optimised non-deterministic finite tree automata library that supports semi-symbolic encoding using *multi-terminal binary decision diagrams* (MTBDDs) for storing transition table of the automaton. Procedure generates state space on-the-fly and prunes the states using the antichain-based approach. State space is represented by downward and upward closed represenation of states. The tool computes the representation of final states and test if initial states are included in final states and thus (dis)prove validity.

It is highly recommended to use a recent Linux distribution and *g++-4.8* or higher for experimenting with *dWiNA*.
A zip archive with the library is here.

Or you can clone the `git` repository with the library (the repository is available on github).
For this you need to have the `git` version control system installed.
To clone the repository, run

$ git clone git://github.com/Raph-Stash/dWiNA.git

Follow the instructions in the `README` file in the root directory of the downloaded repository for compiling and running the command-line interface.

See the `README` file in the root directory of the downloaded repository for instructions about usage.

dWiNA takes as an input formulae in `.mona` files corresponding to the MONA syntax (for full description of syntax consult MONA manual). We present the basic syntax as follows:

program ::= (header;)? (declaration;)+ header ::= ws1s | ws2s declaration ::= formula | var0 (varname)+ | var1 (varname)+ | var2 (varname)+ | 'pred' varname (params)? = formula | 'macro' varname (params)? = formula formula ::= 'true' | 'false' | (formula) | '~' formula | formula '|' formula | formula '&' formula | formula '=>' formula | formula '<=>' formula | first-order-term '=' first-order-term | first-order-term '~=' first-order-term | first-order-term '<' first-order-term | first-order-term '>' first-order-term | first-order-term '<=' first-order-term | first-order-term '>=' first-order-term | second-order-term '=' second-order-term | second-order-term '=' '{' (int)+ '}' | second-order-term '~=' second-order-term | second-order-term 'sub' second-order-term | first-order-term 'in' second-order-term | first-order-term 'notin' second-order-term | 'ex1' (varname)+ ':' formula | 'all1' (varname)+ ':' formula | 'ex2' (varname)+ ':' formula | 'all2' (varname)+ ':' formula first-order-term ::= varname | (first-order-term) | int | first-order-term '+' int second-order-term ::= varname | (second-order-term) | second-order-term + intAn example could look like this:

ws1s; all1 x, y, z: (x <= y & y <= z) => x <= z;

We evaluated our approach in a benchmark of both practical and generated formulae in two following ways. The first uses MONA to generate the deterministic automaton corresponding to the matrix of the formula, translates it to libvata representation and run our algoritm for dealing with the prefix. The other approach translates the formula into prenex normal form with negations only at literals and constructs the nondeterministic automaton directly by libvata.

The practical formulae for our experiments were obtained from the shape analysis by STRAND tool (see STRAND experiments) and several ones that were used to evaluated tool RegSy (Regular Synthesis) (see RegSy experiments). The rest of the experiments were performed on our own generated formulae encoding various interesting relations among subsets (see Experiments with generated formulae).

If you have further questions, do not hesitate to contact authors (Tomas Fiedor, Lukas Holik, Ondrej Lengal and Tomas Vojnar).