Beyond Dependency Graphs
Below we report on the experiments we performed with TTT2 on the 1331
TRSs of the full termination category and the 358 TRSs of the innermost
termination category in version 5.0 of the
TPDB
that fulfill the variable condition. All tests were performed on
a workstation equipped with an Intel® Pentium™ M processor
running at a CPU rate of 2 GHz and 1 GB of system memory. For all
experiments we used a 60 seconds time limit.
Full Termination
Besides the recursive SCC algorithm and linear polynomial orderings with 0/1
coefficients we use the following DP processors:
|
t |
A simple and fast approximation of the dependency graph processor of
Theorem 4 using root comparisons to estimate the dependency graph. |
e |
The dependency graph processor with the estimation DGe(P,R)
described in Section 5. |
s |
The dependency graph processor with the estimation DGs(P,R)
described in Section 5. |
nv |
The dependency graph processor with the estimation DGnv(P,R)
described in Section 5. |
g |
The dependency graph processor with the estimation DGg(P,R)
described in Section 5. |
c |
The dependency graph processor with DGc(P,R) of
Definition 8. |
r |
The improved dependency graph processor of Theorem 16 with
IDGc(P,R) (DGc(P,R)) for (non-)right-linear P U R. |
* |
The composition of t, e, c and
r with a time limit of 500 milliseconds each for the latter
three. |
|
Experimental Results:
Innermost Termination
Besides the recursive SCC algorithm and linear polynomial orderings with 0/1
coefficients we use the following DP processors:
|
t |
A simple and fast approximation of the innermost dependency graph processor
using root comparisons to estimate the innermost dependency graph. |
e |
The innermost dependency graph processor with the estimation described
in [24]. |
c |
The innermost dependency graph processor with
DGci(P,R) of Definition 28. |
r |
The improved innermost dependency graph processor with
IDGci(P,R) (DGci(P,R)) for
(non-)right-linear P U R. |
tec |
The composition of t, e, and c
with a time limit of 500 milliseconds each for the latter two. |
ter |
The composition of t, e, and r
with a time limit of 500 milliseconds each for the latter two. |
|
Experimental Results: