iRankFinder is a tool for inferring linear, lexicographic-linear and multiphase-linear ranking functions for multipath linear-constraint loops, with variables ranging over the rationals, reals, or integers. It is a prototype implementation of the algorithms presented in:

• Amir M. Ben-Amram and Samir Genaim. Ranking Functions for Linear-Constraint Loops. [arXiv]
• Amir M. Ben-Amram and Samir Genaim. On Multiphase-Linear Ranking Functionss. [arXiv]
• Amir M. Ben-Amram, Jesús J. Doménech Samir Genaim. Multiphase-Linear Ranking Functions and their Relation to Recurrent Sets. [arXiv]

You can start using it from the analyzer section, where you will be asked to provide a loop and choose an appropriate setting. In the examples section you will find many examples that you can start from, including all those that appear in the paper(s). The help section has all you need to start using the tool.

The name iRankFinder is obtained by adding i (for integers) to RankFinder of Andreas Podelski and Andrey Rybalchenko.

Comments, suggestions, and BUG reports are very welcome!

Click on one of the examples below, it will be automatically loaded into the input loop text area in the analyzer section.

Nonterminating SLC loops

Nonterminating SLC loops

Examples from the POPL'13 paper

This section includes all example that appeared in the POPL'13 paper.

Examples for LLRF

This section includes examples for the lexicographic-linear ranking fuctions.

Various examples

This section includes various examples.

Summary of Special Cases

Summary of special PTIME cases of LinRF(Z): Q is the set of constraints that define the loop; C is the set of constraints that define the loop condition; and N-dimensional means at most N variables for a fixed N (below we assume N=2).

Examples for MΦRF

This section includes examples for multi-phase ranking functions ranking fuctions.

Examples taken from ACABAR

Examples of ACABAR, orginating from other papers.

Options

Enter the loop in the corresponding text area, set the required options, and click on Analyze. The result will be displayed at the bottom of this page.

---

algorithm Select LinRF(Q) or LinRF(Z) for synthesizing a linear ranking function over the rationals or integers respectively. Select LexLinRF(Q) or LexLinRF(Z) for synthesizing a lexicographic-linear ranking function over the rational or integers respectively. LinRF(Q) LinRF(Z) LexLinRF(Q) LexLinRF(Z) MΦRF(Q) MΦRF(Z) Nested MΦRF(Q) Nested MΦRF(Z) options Check PTIME cases When computing the integer hull of a polyhedron, for LinRF(Z) and LexLinRF(Z), first check if it belongs to one of the special cases that can be computed in polynomial time. Use closure for octagons instead of integer hull Instead of computing the integer hull of an octagonal relation, compute the tight closure. Note that completeness of LinRF(Z) and LexLinRF(Z) is not guaranteed then. Compute the integer hull if PTIME cases fail Always compute the integer hull, for LinRF(Z) and LexLinRF(Z). Disable this option, and enable the PTIME cases option, if you want to only check PTIME case. Use the generators algorithm for LRFs Use the algorithm that works on the generators representation for synthesizing LRFs, instead of the Podelski and Rybalchenko procedure. Generate LRFs/LLRFs with integer coefficients Multiply the function by an integer big enough to make its coefficients integer. Consolidate (weak) LLRFs Turn weak LLRFs to LLRFs. Note that weak LLRFs are enough to claim termination, but consolidated ones are useful for complexity bounds. Verbose mode • The maximum MΦRF depth is 1 2 3 4 5 6 7 8 9

---

---

Result

Not applied yet ...

• Syntax of multi-path linear constraints loop
• Understanding the different options
• References

# variables section
!vars
x1 x2

# primed variables section
!pvars
x1' x2'
    
!path # 1st path
-x1+x2 <= 0
-x1-x2 <= -1
x1'=x1
x2'=x2-2*x1+1

!path # 2nd path
4*x1>=x2
x2>=1
2*x1-5*x1'=<3
-2x1+5*x1'<=1
x2'=x2

First, note that anything after # is a comment. The loop is defined by several sections.

The first section defines the loop variables: the keyword !vars followed by a sequence of variables (separated with white spaces). The second section defines the loop primed variables: the keyword !pvars followed by a sequence of variables (separated with white spaces). The variables and the primed variables must be different. The i-th variable in the !pvars section is the primed version of the i-th variables in the !vars section. Variable names are like in Java or C. Optionally they can end with '. Note that the primed variables do not have to end with ' but rather can have any valid name.

After the !vars and !pvars sections we can have several !path sections which define the loop's paths. Such section starts with the keyword !path followed by a sequence of linear constraints (in separated lines). A linear constraint is defined by the following grammar:

See the above loop for some examples of linear constraints. Note that we do not distinguish between the constraints of the condition and the constraints of the update, they are automatically separated by the parser. A path can be disabled by changing !path by !ipath. This is useful for experimenting.

In principle, you have to select between

• LinRF(Q): Inference of a linear ranking function, where all variables range over the rational or real
• LinRF(Z): Inference of a linear ranking function, where all variables range over the integers
• LexLinRF(Q): Inference of a lexicographic-linear ranking function, where all variables range over the rational or real
• LexLinRF(Z): Inference of a lexicographic-linear ranking function, where all variables range over the integers

LinRF(Q) applies the Podelski-Rybalchenko procedure [PR04] (extended for multi-path loops). LinRF(Z) computes the integer hull of the transition polyhedra and then applies of the Podelski-Rybalchenko procedure. Optionally, the Podelski-Rybalchenko procedure can be replaced by the algorithm that is based on the generator representation, by selecting the appropriate option. LexLinRF(Q) applies the algorithm that appears in the paper, and LexLinRF(Z) computes the integer-hull and then applies LexLinRF(Q).

When computing the integer hulls, if the corresponding paths is linear with integer coefficients it computes the integer hull of the condition only, otherwise it computes the integer hull of the transition polyhedra.

The integer hull is computed as follows: first the polyhedron is divided into independent components (i.e., inequalities that do not share variables), the integer hull of each component is computed, and finally all integer hulls are merged into a single polyhedron again. The integer hull of each component is computed by applying the following steps in the given order:

1. If the PTIME cases option is enabled (it is by default), we check for one of the PTIME cases. The supported cases so far are: DBMs, Cones, and two-dimensional polyhedra. For DBMs we just tighten the constants, for Cones we do nothing as it they are integral already, and for two-dimensional polyhedra we use Harvey's algorithm [H99].
2. If the polyhedron is defined by octagonal inequalities, and the tight closure option is enabled (it is off by default), we compute the tight closure instead of the integer hull. Note that completeness is not guaranteed if this option is selected.
3. If the integer hull option is enabled (it is by default), then we compute the integer hull using Hartman's algorithm [H88] as explained by Charles et al. [CHA09]. This algorithm supports only bounded polyhedra, the integer hull of unbounded polyhedra is computed by computing the integer hull of a corresponding bounded one [SCH86].
4. If we are at this point, the integer hull has not been computed, and thus completeness is not guaranteed.

The Parma Polyhedra Library [BHZ08] is used for converting between generator and constraints representations, as well as for solving LP problems, eliminating variables, etc.

Download

Drop us an email, and we will email you the code.