The LICENSE file contains the license for this release.
The program is released under GNU GPL license.

**************************************************************************
* polyrank: Tools for termination analysis.                              *
*                                                                        *
* Author: Aaron R. Bradley <arbrad {at} theory {dot} stanford {dot} edu> *
* Copyright (c) 2005 Aaron R. Bradley                                    *
**************************************************************************

1. Compiling
============

i. Caveats:
  - Compiled on Linux 2.4.2 for i386 machines.
  - Compiled with ocamlc v3.07+2.

ii. Download and install:
  - LRS v4.1 (http://cgm.cs.mcgill.ca/~avis/C/lrs.html)
  - GMP v4.1.4 (http://www.swox.com/gmp/)
  - Follow installation instructions on respective pages.

iii. Enter directory 'src'.

iv. Edit 'Makefile.globals':
  - Set OCAML to your ocaml directory (e.g., /lib/ocaml).
  - Set LRS to the directory in which LRS was installed (e.g.,
    $(HOME)/local/software/lrslib-042).
  - Set GMP to the directory containing the lib and include
    directories into which GMP was installed (e.g., $(HOME)/local).

v. Type 'make'.  Two binaries, 'linsys' and 'polysys', should result.

2. Running
==========

A. linsys
---------

Typing "linsys --help" returns:

  linsys [options] <file>
    -degree    degree (default: 1)
    -ninv      # template invariants (default: 0)
    -strategy  strategy [One | Bucket[!] | Search[!]] (default: Search)
    -verbose   (default: false)
    -depth     control variable (default: 2)
    -help   Display this list of options
    --help  Display this list of options

Options:

-degree: Maximum degree of returned polyranking function.  A ranking
 function is degree 1.

-ninv: Number of supporting invariants.

-strategy: Search for a ...
 o One: non-lexicographic function
 o Bucket: set of functions
 o Search: lexicographic tuple of functions

-depth: Maximum absolute value of coefficients of supporting
 invariants is 2^depth.

Input format:

- See examples 1-11.  
- Assertions must be linear but may include inequalities.
- Not specifying how a variable is updated means that the variable is
  updated nondeterministically.

Examples:

linsys -degree 2 example3.loop
linsys -ninv 1 -degree 2 example6.loop (in [3])
linsys -ninv 1 example8.loop  (McCarthy 91, in [2])
linsys -ninv 2 -strategy one example9.loop  (GCD, in [2])
linsys -ninv 1 example9.loop (GCD, in [2])
linsys -degree 2 example11.loop (GCD, in [3])

B. polysys
----------

Typing "polysys --help" returns:

  polysys [options] <file>
    -degree    degree (default: 1)
    -verbose   (default: true)
    -help   Display this list of options
    --help  Display this list of options

Options:

-degree: Maximum degree of returned polyranking function.

Input format:

- See example1.loop and example12.loop.
- Similar to linsys, except that assertions are polynomial equations.
- Not specifying how a variable is updated means that the variable is
  preserved.

Examples:

polysys example1.loop
polysys -degree 3 example12.loop (in [1])

**************************************************

Questions or comments?  Please email Aaron R. Bradley at
arbrad {at} theory {dot} stanford {dot} edu.

Downloaded from http://theory.stanford.edu/~arbrad

References:
----------

[1] Aaron R. Bradley, Zohar Manna, Henny B. Sipma, Termination of
Polynomial Programs, In Proc. Verification, Model-Checking, and
Abstract-Interpretation (VMCAI) January 2005, Lecture Notes in
Computer Science, Volume 3385, Springer-Verlag.

[2] Aaron R. Bradley, Zohar Manna, Henny B. Sipma, Linear Ranking with
Reachability, In submission.

[3] Aaron R. Bradley, Zohar Manna, Henny B. Sipma, The Polyranking
Principle, In submission.