WANDA is a command-line termination tool. Given a file describing a (higher-order) term rewriting system, she will return YES (the system is terminating), NO (the system is non-terminating) or MAYBE (termination status could not be determined).
In its most basic form, you invoke WANDA by typing: ./wanda.exe <benchmark>
- An input file in applicative AFSM format, listing first
function declarations, followed by an empty line, and then
example afsm input file
- An input file in the format employed in the annual termination
competition for the higher-order union beta category. These are
Algebraic Functional Systems, so systems with both
function application and application, but no meta-variables.
example xml input file
- An input file in "converted" xml format: WANDA's own
human-readable variation of the competition's XML format.
example afs input file
- A normal TRS input file in the human-readable format used in
the termination competition, which represents an
applicative TRS: there is only one binary function
symbol; everything else has arity 0.
If possible, this system is given a typing and treated as an
applicative higher-order system. Note that WANDA's answer does
not give information about termination of the original untyped
example atrs input file
Note that, internally, all these input formats are converted to the AFSM formalism, corresponding to the .afsm format.
- The input file to analyse. If no file name is given, the user is prompted to type in a system in AFSM format. If several files are given, termination is analysed for all of them.
- By default, a purely numeric input to WANDA is assumed to be the timeout. However, this number is completely ignored at this time.
- --verbose, -v
- Give additional comments during execution, such as describing what the tool is doing. When verbose is enabled, the proof output is printed during execution, rather than afterwards.
- --silent, -s
- By default WANDA prints YES/NO/MAYBE followed by an explanation (a proof, counter example or the reason why deciding was difficult). You can suppress this explanation by choosing silent mode.
- --rewrite, -r
- Rather than proving termination, the user is prompted to type in a term, and this term is rewritten following the rules.
- --format=<format>, -f <format>
- Rather than choosing the standard formalism associated with a file's extension, consider all input files in the given formalism.
- --firstorder=<file>, -i <file>
- WANDA uses a first-order termination prover, located in the resources/ directory, to prove termination of the first order part of the rules. With this argument you can indicate which file in the resources/ directory should be used. If none is indicated, WANDA will not attempt to use a first-order prover. If this is omitted, the file "firstorderprover" will be used (make sure that it is set as executable!).
- --disable=<list>, -d <list>
- You can disable certain features of WANDA; for example to
disable non-termination proving and rule removal, use
--disable=nt,rr or -d nt,rr (note that there is no space after
the comma!). The things you can disable are:
- nt: non-termination proving
- rr: rule removal
- dp: the dependency pair framework
- static: static dependency pairs
- dynamic: dynamic dependency pairs
- sc: the subterm criterion
- fr: formative rules
- ur: usable rules
- local: using tags and suchlike improvements for abstraction-simple (also sometimes called local) systems
- graph: the dependency graph
- poly: polynomial interpretations
- pprod: polynomial interpretations with products
- horpo: the recursive path ordering
- --query=<property>, -q <property>
- Query whether the system has the given property; outputs YES or
NO and does nothing else. The property must be one of the
- algebraic (no meta-variables occur below an abstraction)
- argumentfree (meta-variables do not take arguments)
- --show, -w
- Just show the system (possibly converting it to an AFSM first) and abort.
- --debug, -D
- Give additional debug information during execution. More verbose than --erbose, this is really just for debugging problems (for example, the entire formula table of HORPO is printed).
- --style=<style>, -y <style>
Creates output of the given style for the proof; default is plain.
Possible styles are:
- html: creates a single html-page (unfinished)
- plain: just ascii
- ansi: just ascii, but with ansi-colour characters
- utf: prints to the terminal using utf8-characters
- ansiutf: prints to the terminal using utf8-characters and ansi-colour
- --output=<filename>, -o <filename>
- Prints only the YES/NO/MAYBE to stdout, and the rest to the given file.
A default SAT-solver and a default first-order termination prover are supplied in the resources/ directory. Both can be replaced by other solvers, with similar input and output, provided they are given the same name. The expected input/output is that which is defined by the relevant competitions.
In addition, a non-termination prover is included in the resources/ directory. The given script is simply a placeholder which returns MAYBE. However, it can be replaced by any tool which takes a first-order TRS in standard human-readable format as input, and returns YES, NO or MAYBE, followed by a non-terminating term in the case of NO. Using this, WANDA can identify non-terminating systems if the first-order part is non-terminating. No suitable such tool is included because no open-source tools with these specifications exist at the moment.