# Model forward¶

Cited in: [BeyerHMR07] fig. 1 p. 3.

Tag: fixpoint.

## Source code¶

```model beyer_henzinger_majumdar_rybalchenko_pldi07_03 {

var n, i, a, b;

states q1, q4, q2, q3;

transition t5 := {
from   := q1;
to     := q4;
guard  := i >= n;
action := ;
};

transition t1 := {
from   := q1;
to     := q2;
guard  := i < n;
action := ;
};

transition t3 := {
from   := q2;
to     := q3;
guard  := true;
action := a' = a + 2, b' = b + 1;
};

transition t2 := {
from   := q2;
to     := q3;
guard  := true;
action := a' = a + 1, b' = b + 2;
};

transition t4 := {
from   := q3;
to     := q1;
guard  := true;
action := i' = i + 1;
};

}

strategy beyer_henzinger_majumdar_rybalchenko_pldi07_03_s {

Region init := {state = q1 && n >= 0 && i = 0 && a = 0 && b = 0};

}```

## Expected invariant¶

`{ q4[v1, v2, v3, 3v1 - v3] }`

## Results¶

• With Aspic: { q2[n, i, a, 3i - a] : a >= i and a <= 2i and i <= -1 + n; q3[n, i, a, 3 + 3i - a] : i >= 0 and a >= 1 + i and a <= 2 + 2i and i <= -1 + n; q1[n, i, a, 3i - a] : a <= 2i and a >= i and n >= 0 and i <= n; q4[n, n, a, 3n - a] : n >= 0 and a <= 2n and a >= n } (0.06s), OK.
• With ISL: { q2[n__1, i__1, a__1, 3i__1 - a__1] : n__1 >= 0 and a__1 >= i__1 and i__1 <= -1 + n__1 and a__1 <= 2i__1; q4[n__1, n__1, a__1, 3n__1 - a__1] : n__1 >= 1 and a__1 <= -1 + 2n__1 and a__1 >= 1 + n__1; q4[n__1, n__1, n__1, 2n__1] : n__1 >= 1; q4[n__1, n__1, 2n__1, n__1] : n__1 >= 1; q4[0, 0, 0, 0]; q3[n__1, i__1, a__1, 3 + 3i__1 - a__1] : (n__1 >= 0 and a__1 >= 1 + i__1 and i__1 <= -1 + n__1 and a__1 <= 1 + 2i__1) or (n__1 >= 0 and a__1 >= 3 + i__1 and i__1 <= -1 + n__1 and a__1 <= 2 + 2i__1); q3[n__1, 0, 2, 1] : n__1 >= 1; q1[n__1, i__1, a__1, 3i__1 - a__1] : n__1 >= 1 and i__1 <= n__1 and a__1 >= 1 - n__1 + 2i__1 and a__1 <= -1 + 2i__1 and a__1 >= 1 + i__1; q1[n__1, i__1, i__1, 2i__1] : n__1 >= 1 and i__1 >= 1 and i__1 <= n__1; q1[n__1, i__1, 2i__1, i__1] : n__1 >= 1 and i__1 >= 1 and i__1 <= n__1; q1[n, 0, 0, 0] : n >= 0 } (0.22s), OK.