The source code of the translation to automata is available as a tar file source_solver.tar or you can browse directly the directory source_solver
The sources of the prototype can be found in the folder gen. The interesting files of this folder are:
The directory intersect contains an algorithm that takes two automata in the standard input and prints out "EMPTY" when the two automata contain no common tree and it prints out "NON EMPTY" followed by an example tree otherwise.
The directory forms contains some examples formulae.
The directory example contains an automaton example.auto that accepts any tree. This automaton is used by the script get_example.sh to print an example solution for a formula (see manual).
The directory translateXPath contains the benchmark that tests the lineage of n 'tr' elements against the xhtml dtd.
φ = φ & φ̩ | φ | φ̩ | let $var = φ, …, $var = φ in $var | mu $var . φ | mu var . φ | <1> φ | <2> φ | <-1> φ | <-2> φ | $var | atom | (φ) | T | ~φWarning: the let with more than one variable is still beta.
solver FILEwill output the automaton for the formula in FILE. The solver commands accepts several arguments:
let $x = <1> $x | <2> $x | φ in $x
The solver output starts by a line containing an integer n followed by n strings corresponding of the n labels used by the automaton. _other is a special label. When compression is used, it indicates any other label than those appearing in the formula. When the compression is not used it indicates that a transition where no atomics are true. The second line contains 5 integers T s1 s2 f R. States of the automaton are integers between 0 and T. si is the state representing a i-leaf. f is the unique final state. Finally, R is the number of transitions. In the current version we have si=i-1. Each of the R following lines contains a string l (the label) and tree integers e1 e2 r. This represents a transition where ei is the i-child, r is the parent state and l is the label of the transition.
./solver ../forms/multi compress | cat ../example/example.auto - | ./intersect/interIntersecting with the automaton that accepts anything is a fast way to get example solutions for a formula so we have bundled it into the script example/get_example.sh. Our previous example become:
./solver ../forms/multi compress | ../example/get_example.sh