TCT is a tool for automatically proving (low) upper bounds on the derivational complexity and runtime complexity of terminating term rewriting systems. It is strongly based on the automatic termination prover TTT2.
Download
The following files are available for download:- A binary (native-compiled on 32-bit Linux)
- A bytecode version (also compiled on 32-bit Linux)
- The documentation (preliminary module documentation) of TCT
- An archive containing the source of TCT published under the lesser GPL. In order to compile the sources, a set of TTT2 libraries are needed. These will presumably be open sourced somewhen in 2009, in the meantime we provide a binary distribution which can be downloaded from here. These libraries include additionally the source code of the MiniSat SAT-solver. TCT furthermore relies on the Yices SMT Solver. Currently only version 1.0.11 available from here is supported.
INSTALLATION in the root directory of
the source package.
The current version was updated last on
Thu Feb 5 09:30:25 CET 2009
.
Usage
The usage of TCT is essentially the same as the usage of TTT2. It is called by./tct [options] <file>. Most options
which were allowed in TTT2 are also included in TCT (type
./tct --help for a complete list of the currently available
options). For an explanation of these options, we refer to
TTT2. The first
new option added by TCT is --answer_type <answertype>
(or -a <answertype>). This option controls what TCT
prints in the first line of its output: allowed values for <answertype>
are plain (just print YES or MAYBE),
dc, rc, idc, and irc (add an upper bound on the (innermost) derivational or
runtime complexity to a YES). The second new option is
-v (or --version), which just prints the current
version number, and then exits TCT.
Of the options inherited from TTT2, the option --strategy
(respectively, -s) deserves special mentioning.
This option takes as argument a string describing the strategy that
TCT should use in order to attempt to prove termination and complexity
bounds of the given TRS. For a description of the grammar for this
argument string (the strategy language), we refer to
TTT2
(ttt2-doc,
Section "Module Strategy").
A list of atomic strategies in TCT is available.
Here are some sample calls of TCT:
./tct -p -a irc -s 'pop* -i[60]' <trs>./tct -p -a dc -s 'poly -c dres -i -b 7' <trs>./tct -p -a dc -s 'matrix -c tri -i -b 7 -d 3' <trs>./tct -p -a rc -s 'wdp; poly -c linc' <trs>./tct -p -a rc -s 'wdprp -i -b 31; poly -c qsimpc' <trs>./tct -p -a rc -s 'widp -fwdp; poly -c qsimpc' <trs>./tct -p -a rc -s 'widprp -fdp; poly -c linc' <trs>
-s '(wdprp | wdp); poly -c linc'
tct/tests contains many complexity-specific strategy macros.
Still, it is subject to further extension.
Experimental Results for the standard strategies of TCT
Note: due to an error in Lemma 22 of of the IJCAR 2008 paper by Hirokawa and Moser, the applicability of Corollaries 35 and 36 of that paper is reduced, which makes some of TCT's results in the Termination Competition unsound. The following table contains the result of our competition strategy, after considering the implications of that error:| status | DC | DC innermost | RC | RC innermost |
|---|---|---|---|---|
| YES | 225 | 226 | 271 | 304 |
| total time | 318.99 | 389.32 | 671.02 | 945.42 |
| avg. time | 1.42 | 1.72 | 2.48 | 3.11 |
| MAYBE | 0 | 948 | 515 | 757 |
| total time | 0.00 | 51.93 | 5241.34 | 21224.76 |
| avg. time | 0.00 | 0.05 | 10.28 | 28.22 |
| TIMEOUT | 221 | 220 | 608 | 333 |
| total time | 16553.45 | 16900.81 | 36959.21 | 19985.78 |
| avg. time | 74.90 | 76.82 | 60.79 | 60.02 |