Model halbwachs1¶
Cited in: [Gonnord_thesis] fig. 2.12 p. 31, [Halbwachs_thesis].
Tag: fixpoint.
Figure¶
Source code¶
model gonnord_thesis_031 {
var i, j;
states k1, k2;
transition t3 := {
from := k1;
to := k2;
guard := i > 100;
action := ;
};
transition t2 := {
from := k1;
to := k1;
guard := i <= 100;
action := i' = i + 2, j' = j + 1;
};
transition t1 := {
from := k1;
to := k1;
guard := i <= 100;
action := i' = i + 4;
};
}
strategy gonnord_thesis_031_s {
Region init := {state = k1 && i = 0 && j = 0};
}
Expected invariant¶
{ k2[v1, v2] : 2v2 <= v1 and v2 >= 0; k1[v1, v2] : 2v2 <= v1 and v2 >= 0 }
Results¶
- With Aspic: { k2[i, j] : i >= 101 and 2j <= i and j >= 0 and i <= 104 and 2j <= 204 - i; k1[i, j] : 2j <= i and j >= 0 and i <= 104 and 2j <= 204 - i } (0.05s), OK.
- With ISL: { k2[i__1, j__1] : (2j__1 = i__1 and i__1 >= 101 and i__1 <= 102) or (exists (e0 = [(i__1)/2], e1 = [(-i__1 + 2j__1)/4]: 2e0 = i__1 and 4e1 = -i__1 + 2j__1 and i__1 >= 101 and j__1 <= 50 and j__1 >= 1 and 2j__1 <= -4 + i__1 and i__1 <= 104)); k2[i__1, 0] : exists (e0 = [(i__1)/4]: 4e0 = i__1 and i__1 >= 101 and i__1 <= 104); k1[i__1, j__1] : (2j__1 = i__1 and i__1 >= 2 and i__1 <= 102) or (exists (e0 = [(i__1)/2], e1 = [(-i__1 + 2j__1)/4]: 2e0 = i__1 and 4e1 = -i__1 + 2j__1 and i__1 <= 104 and j__1 <= 50 and j__1 >= 1 and 2j__1 <= -4 + i__1)); k1[0, 0]; k1[i__1, 0] : exists (e0 = [(i__1)/4]: 4e0 = i__1 and i__1 >= 4 and i__1 <= 104) } (0.00s), OK.