Experiments
Currently Tct does not support analysis of cTRSs.
Therefore we restrict our experiments to size-measurements relating the number of bytecode instructions with the number of nodes in the graph.
The examples can be downloaded here.
Note that in most examples methods usually are invoked only once, ie., if there would be no overhead the number of nodes in the graph would correspond to the number of bytecode instructions.
This measurement should give an intuition about the size (in terms of the number of rules) of the resulting problems.
The examples are taken from the Termination Problem Data Base} (TPDB).
and we compare our results with the AProVE tool.
For AProVE the numbers are extracted from the bytecode of the examples and the proof output.
For our tool the examples have been rewritten to Jinja bytecode.
Since the handled languages are different, the tools are difficult to compare directly.
Furthermore, it seems that there is some additional overhead, due to the initialisation procedure in Java, which effects smaller programs especially.
| | Jat | AProVE |
| AG313 | 1.1 | 4.3 |
| costa09-example\_1 | 1.7 | 2.0 |
| costa09-example\_4 | 1.2 | 6.2 |
| CyclicList | 1.7 | 3.1 |
| CyclicPair | 0.9 | 2.1 |
| DivMinus2 | 1.1 | 3.5 |
| DivWithoutMinus | 1.1 | 4.3 |
| FlattenRTA | 2.5 | 3.2 |
| GCD | 1.2 | 3.4 |
| IntPath | 1.2 | 3.0 |
| IntPath2 | 1.4 | 2.8 |
| IntRTA | 1.0 | 3.5 |
| ListContentTail | 1.7 | 5.6 |
| McCarthyIterative | 1.2 | 3.0 |
| PastaA4 | 1.2 | 5.5 |
| PastaA7 | 1.1 | 6.6 |
| PastaB15 | 1.1 | 6.3 |
| PastaB16 | 1.2 | 5.2 |
| PastaB3 | 1.2 | 5.0 |
| PastaC10 | 1.1 | 7.8 |
| PastaC2 | 1.2 | 3.0 |
| PastaC9 | 1.2 | 8.8 |
| SharingPair | 3.9 | 3.8 |
| TypeSwitch | 2.2 | 2.9 |