iRankFinder is a tool for inferring linear and lexicographic-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. [.pdf]

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.

loop1.mlc Example 3.6
loop2.mlc Example 3.18
loop3.mlc Example 3.20 - 1st loop
loop4.mlc Example 3.20 - 2st loop
loop5.mlc Example 3.20 - both loop
loop6.mlc Example 4.2 (the second path of Example 3.20)
loop7.mlc Example 4.12
loop8.mlc Example 4.13
loop9.mlc Example 4.14
loop10.mlc Example 4.15 - 1st loop (the first path of 3.20)
loop11.mlc Example 4.15 - 2nd loop
loop12.mlc Example 4.34
loop13.mlc The example in the conclusions regards the complexity

Examples for LLRF

This section includes examples for the lexicographic-linear 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 N-dimensional 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 N-dimensional. 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 N-dimensional. 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 N-dimensional. In the case of N-dimensional 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 multi-phase ranking functions ranking fuctions.

loop1.mlc The classical example with 3-phases, with a little change in the conditions
loop2.mlc An example that does not have MLRF over Z, and non-terminating 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 2-phase 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 2-phase 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.

loop01.mlc  
loop02.mlc  
loop03.mlc  
loop04.mlc  
loop05.mlc  
loop06.mlc  
loop07.mlc  
loop08.mlc  
loop09.mlc  
loop10.mlc  
loop11.mlc  
loop12.mlc  
loop13.mlc  
loop14.mlc  
loop15.mlc  
loop16.mlc  
loop17.mlc  
loop18.mlc  
loop19.mlc  
loop20.mlc  
loop21.mlc  
loop22.mlc  
loop23.mlc  
loop24.mlc  
loop25.mlc  
loop26.mlc  
loop27.mlc  
loop28.mlc  
loop29.mlc  
loop30.mlc  
loop31.mlc  
loop32.mlc  
loop33.mlc  
loop34.mlc  
loop35.mlc  
loop36.mlc  
loop37.mlc  
loop38.mlc  
loop39.mlc  
loop40.mlc  
loop41.mlc  

Options

Select Algorithm: LINRF(Q) LINRF(Z) LINRF(Z) by LINRF(Q)

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)
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


Result

Not applied yet ...

Syntax of multi-path 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
-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:

C  ::=  E OP E
OP  ::=  >= | => | <= | =< | =
E  ::=  BE | E+BE | E-BE
BE  ::=  Num | Num*Variable | Num Variable |-Variable
Num  ::=  integer | integer/positive-integer

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 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.

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(1-2):321, 2008.
[CHA09] Philip J. Charles, Jacob M. Howe, Andy King: Integer Polyhedra for Program Analysis AAIM 2009: 85-99.
[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 Two-Dimensional Integer Hulls. SIAM J. Comput. 28(6): 2285-2299 (1999).
[PR04] Andreas Podelski, Andrey Rybalchenko: A Complete Method for the Synthesis of Linear Ranking Functions. VMCAI 2004: 239-251.
[SCH86] Alexander Schrijver: Theory of Linear and Integer Programming.

Download