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
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.
Examples from the paper
This section includes all example that appeared in the paper.
Syntax of multi-path linear constraints loop
The syntax is best explained with an example (you have many in
section). Here is a loop
# variables section
# primed variables section
!path # 1st path
-x1+x2 <= 0
-x1-x2 <= -1
!path # 2nd path
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:
|| E OP E
|| >= | => | <= | =< | =
||BE | E+BE | E-BE
||Num | Num*Variable | Num Variable |-Variable
||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.