Download Integer Set Library: Manual

R2 := [n] -> { [i,j] -> [i,j+3] : i <= 2 j
j <= 2 i
R3 := [n] -> { [i,j] -> [i+1,j+1] : i <= 2
j <= 2
(R1 . R3) - (R3 . R1);
(R2 . R3) - (R3 . R2);
j
i
1
4
-
and i
and j
1 and
1 and
<= n
<= n
i <=
j <=
and
- 3 };
n - 1 and
n - 1 };
R3 can therefore be moved forward in any path. For the other two basic relations,
we have both R2 ◦ R1 * R1 ◦ R2 and R1 ◦ R2 * R2 ◦ R1 and so R1 and R2 form a
strongly connected component. By computing the power of R3 and R1 ∪ R2 separately
and composing the results, the power of R can be computed exactly using (2.5). As
explained by Beletska et al. (2009), applying the same formula to R directly, without a
decomposition, would result in an overapproximation of the power.
2.4.5
Partitioning the domains and ranges of R
The algorithm of Section 2.4.2 assumes that the input relation R can be treated as a
union of translations. This is a reasonable assumption if R maps elements of a given
abstract domain to the same domain. However, if R is a union of relations that map
between different domains, then this assumption no longer holds. In particular, when
an entire dependence graph is encoded in a single relation, as is done by, e.g., Barthou
et al. (2000, Section 6.1), then it does not make sense to look at differences between
iterations of different domains. Now, arguably, a modified Floyd-Warshall algorithm
should be applied to the dependence graph, as advocated by Kelly et al. (1996c), with
the transitive closure operation only being applied to relations from a given domain to
itself. However, it is also possible to detect disjoint domains and ranges and to apply
Floyd-Warshall internally.
Algorithm 1: The modified Floyd-Warshall algorithm of Kelly et al. (1996c)
Input: Relations R pq , 0 ≤ p, q < n
Output: Updated relations R pq such that each relation R pq contains all indirect
paths from p to q in the input graph
1
2
3
4
5
6
for r ∈ [0, n − 1] do
Rrr B R+rr
for p ∈ [0, n − 1] do
for q ∈ [0, n − 1] do
if p , r or q , r then
R pq B R pq ∪ Rrq ◦ R pr ∪ Rrq ◦ Rrr ◦ R pr
Let the input relation R be a union of m basic relations Ri . Let D2i be the domains of
Ri and D2i+1 the ranges of Ri . The first step is to group overlapping D j until a partition
is obtained. If the resulting partition consists of a single part, then we continue with the
algorithm of Section 2.4.2. Otherwise, we apply Floyd-Warshall on the graph with as
59