ACABAR is a prototype implementation of a termination analyzed as descibed 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 some examples that you can start from, including all those that appear in the paper. The help section has all you need to start using the tool.
Click on one of the examples below, it will be automatically loaded into the input loop text area in the analyzer section.
This section includes all example that appeared in the paper.
# 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.