Termination Analyser for SCNP (The NP subset of SCT)

Brief User Guide

This program searches for ranking functions that prove the termination of SCT programs. This page gives information about the usage of the program. Theoretical background can be found in this draft paper.

Input

Input can be entered via the analyser page (choose Analyzer from the menu bar) or you can select an instance from our example base (choose Examples).
The input is an abstract program and is a list of abstract transitions. The format is best illustrated by an example:

f(x1, x2, x3) :- [x1>=y1, x3>y2, x2>=y3] ; g(y1, y2, y3).
g(x1, x2, x3) :- [x3>=y1, x2>y2, x1>=y3] ; f(y1, y2, y3).

Remarks:

  1. The list of constraints may be empty (the brackets are mandatory). The argument lists may not be empty.
  2. The current demo program provides not graceful handling of incorrectly formatted input.

Output

The output from the analysis consists of a few parts, of which the most important is headed Ranking. This part gives a list of expressions (called level mappings in our paper). Unless the list ends with the line none, the list constitutes a lexicographic ranking function for the subject program. Each entry in the list is an expression that denotes a mapping of program states into a (quasi) ordered set. The form and meaning of each is explained below.

Output conventions

  1. The program does not use the identifiers used for arguments in the input. Instead, an argument is identified by the program-point id and its position in the argument list, in the form id:num. For example, the y argument in p(x,y) is displayed as p:2.
  2. In a few examples in our benchmark, a certain id is used for two different program points, only distinguished by having different number of arguments (arity). In such a case, the program appends the suffix _ar_ and the arity to the identifier for disambiguation in the output.

Level-mapping expressions

Numeric level mapping

This type of level mapping might as well be called "constant" because it assigns a constant level to each program point. What matters is the ordering of these constants, not their values, and the program displays the information in the form numeric-[[a1, a2,...], [b1,b2,...], ...] which means that points a1, a2,... are all assigned the lowest level; b1, b2,... are assigned the next (higher) level and so forth. Note that any program point not mentioned explicitly in the representation is implicitly assigned the lowest level.

Set-valued mappings

Set-valued mappings are displayed as <order>-<set> where order is one of max, min, ms and dms; and set is a list of arguments.

These are interpreted as follows:

Tagged set-valued mappings

Tagged set-valued mappings differ from plain set-valued mappings in that the set consists of argument values paired with integer constants, such as (f:2, 1), and the underlying order is therefore lexicographic ordering of pairs. Otherwise the expressions is constructed as for plain set-valued mappings.
For a program that necessitates such a ranking function see a12.pl in our example list.