dWiNA is an implementation of backward decision procedure for WS1S logic (weak second-order theory of 1 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 + int
An 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).