This site provides supporting material for the paper AC Completion with Termination Tools by Sarah Winkler and Aart Middeldorp, accepted to CADE 2011.

Download

The tool mascott is available as a bytecode executable for Linux (32 bit), but you can also obtain the sources and compile the tool yourself. Some hints on how to call mascott are given below.

Usage

./mascott <file> <options> calls mascott on the given file. The input problem is assumed to be in TPDB format . Possible options are the following:

General

The global time limit is given by -t <seconds>. Further options are -st and -ct to output useful statistics and the completed system, respectively. -h displays the list of options.

Termination Checks

By default, termination checks are performed internally by TTT2, also specified by the option -it. The applied termination techniques can be controlled by -s <strategy> in the TTT2 strategy language. Alternatively, termination can be checked externally if an appropriate script is supplied using the option -tp <script>. The script is supposed to be executable from the current directory and it has to be compatible with the following minimal interface:
<script> <file> checks termination of the given system in TPDB format. It must print YES on the first line of standard output if termination could be established and something else otherwise. The time limit for each termination check is specified by -T <seconds>.

Experiments