Model disj¶
Cited in: [BeyerHMR07] fig. 4 p. 7, [GulwaniZ10] fig. 9 p. 12.
Tag: fixpoint.
Figure¶
Source code¶
model beyer_henzinger_majumdar_rybalchenko_pldi07_07 {
var x, y;
states q1, q3, q2;
transition t4 := {
from := q1;
to := q3;
guard := x >= 100;
action := ;
};
transition t1 := {
from := q1;
to := q2;
guard := x < 100;
action := ;
};
transition t3 := {
from := q2;
to := q1;
guard := x >= 50;
action := x' = x + 1, y' = y + 1;
};
transition t2 := {
from := q2;
to := q1;
guard := x < 50;
action := x' = x + 1;
};
}
strategy beyer_henzinger_majumdar_rybalchenko_pldi07_07_s {
Region init := {state = q1 && x = 0 && y = 50};
}
Expected invariant¶
{ q1[v1, v2] : v2 >= v1 and v2 >= 50; q2[v1, v2] : v2 >= 50 and v2 >= v1 and v1 <= 99; q3[v1, v2] : v2 >= v1 and v1 >= 100 }
Results¶
- With Aspic: { q1[x, y] : y >= x and y >= 50; q2[x, y] : y >= 50 and y >= x and x <= 99; q3[x, y] : y >= x and x >= 100 } (0.06s), OK.
- With ISL: { q1[x__1, 50] : x__1 >= 1 and x__1 <= 50; q1[x__1, x__1] : x__1 >= 51 and x__1 <= 100; q1[0, 50]; q3[100, 100]; q2[x__1, 50] : x__1 >= 1 and x__1 <= 50; q2[x__1, x__1] : x__1 >= 51 and x__1 <= 99; q2[0, 50] } (0.02s), OK.