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.
- An abstract transition has the form:
source state :- constraints; target state. - A state has an identifier (also known as "program point") and a list of arguments (also known as "parameters").
- constraints relate source arguments to target arguments by either ">" or "&ge".
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:
- The list of constraints may be empty (the brackets are mandatory). The argument lists may not be empty.
- 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
- 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.
- 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:
- Regardless of order, the level mapping assigns to each
program state a (multi-)set of values. The values are taken from the arguments
that appear in the set.
Example: if the set is [p:1,p:2,q:2], then the value in abstract state p(x,y) is a two-element multiset {x,y}, in q(z,w) it is {w}, and in a state r(u,v) it is empty. - The order label indicates what ordering is applied to the set of values. Sets may be ordered according to their maximum, their minimum, or according to multiset and dual multiset orders. See the paper for more information.
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.