iRankFinder is a tool for inferring linear and lexicographiclinear ranking functions for multipath linearconstraint loops, with variables ranging over the rationals, reals, or integers. It is a prototype implementation of the algorithms presented in:
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.
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 lexicographiclinear ranking fuctions.
loop1.mlc 
The example from the preliminaries section that shows the difference wrt ADFG10

loop2.mlc 
Ackermann like example

loop3.mlc 
The example with the weak LLRF (from Section 5.3)

loop4.mlc 
The example from the preliminaries section that shows the difference wrt BMS05

loop5.mlc 
A loop that has a LLRF over Z but not over Q, it is a combination of
two SLC loops that have LRFs over Z but not over Q.

Various examples
This section includes various examples.
loop1.mlc 
An example with a LRF over both Q and Z

loop2.mlc 
A loop that decreases a variable every other iteration. It has a LRF
both over Q and Z.

loop3.mlc 
A multi path loop that uses a boolean like variable

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 Ndimensional means at most
N variables for a fixed N (below we assume N=2).
loop1.mlc 
Q is totally unimodular (e.g., DBM). In this case
Q it is already integral.

loop2.mlc 
Q is Ndimensional. In this case we need to compute the
integer hull of Q.

loop3.mlc 
The update is affine linear with integer coefficients, and
C is a cone. In this case Q is already integral.

loop4.mlc 
The update is affine linear with integer coefficients, and
C is totally unimodular. In this case Q is
already integral.

loop5.mlc 
The update is affine linear with integer coefficients, and
C is Ndimensional. In this case we compute the integer
hull of C.

loop6.mlc 
The update is affine linear with integer coefficients, and
C can be partitioned into independent sets where each is
either a cone, totally unimodular, or
Ndimensional. In the case of Ndimensional we compute
its integer hull.

loop7.mlc 
Q can be partitioned into independent sets that are
covered by the above cases.

Examples for MΦRF
This section includes examples for multiphase ranking functions ranking fuctions.
loop1.mlc 
The classical example with 3phases, with a little change in the conditions

loop2.mlc 
An example that does not have MLRF over Z, and nonterminating over Q.

loop3.mlc 
An example that has MLRF over Z, but not over Q.

loop4.mlc 

loop5.mlc 
A loop by Matthias&Jan, has no MLRF

loop6.mlc 
A loop that demonstrates that depth depends on the coefficients of the constraints

loop7.mlc 
The classical 2phase loop, with a change in condition so it has a single ray

loop8.mlc 
Yet another loop with a MΦRF

loop9.mlc 
The classical 2phase loop, with a change in condition to make last component possibly negative 
loop10.mlc 
A loop with two phases

loop11.mlc 
A loop that has a LLRF that is not a MΦRF, but has a MΦRF as
well. 
loop12.mlc 
An MLC loop with MΦRF

Examples taken from ACABAR
Examples taken from ACABAR.
Syntax of multipath linear constraints loop
The syntax is best explained with an example (you have many in the
examples section). Here is a loop
# variables section
!vars
x1 x2
# primed variables section
!pvars
x1' x2'
!path # 1st path
x1+x2 <= 0
x1x2 <= 1
x1'=x1
x2'=x22*x1+1
!path # 2nd path
4*x1>=x2
x2>=1
2*x15*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 ith variable in the !pvars section is the primed version of the ith 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:
C 
::= 
E OP E 
OP 
::= 
>=  =>  <=  =<  = 
E 
::= 
BE  E+BE  EBE 
BE 
::= 
Num  Num*Variable  Num Variable Variable 
Num 
::= 
integer  integer/positiveinteger 
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.
Understanding the different options
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 lexicographiclinear ranking function, where all variables range over the rational or real
 LexLinRF(Z): Inference of a lexicographiclinear ranking function, where all variables range over the integers
LinRF(Q) applies the PodelskiRybalchenko procedure [PR04] (extended for multipath loops). LinRF(Z) computes the integer hull of the transition polyhedra and then applies of the PodelskiRybalchenko procedure. Optionally, the PodelskiRybalchenko 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 integerhull 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:
 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 twodimensional polyhedra. For DBMs we just tighten the constants, for Cones we do nothing as it they are integral already, and for twodimensional polyhedra we use Harvey's algorithm [H99].
 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.
 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].
 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.
References
[BHZ08] 
Roberto Bagnara, Patricia M. Hill, and Enea Zaffanella. The Parma Polyhedra Library: Toward a Complete Set of Numerical Abstractions for the Analysis and Verification of Hardware and Software Systems. Sci. Comput. Program., 72(12):3–21, 2008. 
[CHA09] 
Philip J. Charles, Jacob M. Howe, Andy King: Integer Polyhedra for Program Analysis AAIM 2009: 8599. 
[H88] 
Mark E. Hartmann.: Cutting Planes and the Complexity of the Integer Hull. PhD thesis, School of Operations Research and Industrial Engineering, Cornell University (1988); Technical Report 819. 
[H99] 
Warwick Harvey: Computing TwoDimensional Integer Hulls. SIAM J. Comput. 28(6): 22852299 (1999). 
[PR04] 
Andreas Podelski, Andrey Rybalchenko: A Complete Method for the Synthesis of Linear Ranking Functions. VMCAI 2004: 239251. 
[SCH86] 
Alexander Schrijver: Theory of Linear and Integer Programming. 