Model gonnord2¶
Cited in: [Gonnord_thesis] fig. 4.7 p. 55.
Tag: fixpoint.
Figure¶
Source code¶
model gonnord_thesis_055 {
var i, j, k;
states k1, k2;
transition t4 := {
from := k1;
to := k2;
guard := i > 100;
action := ;
};
transition t3 := {
from := k1;
to := k1;
guard := i <= 100 && j = 9;
action := i' = i + 2, k' = k + 2, j' = 0;
};
transition t2 := {
from := k1;
to := k1;
guard := i <= 100 && j < 9;
action := i' = i + 2, j' = j + 1;
};
transition t1 := {
from := k1;
to := k1;
guard := i <= 100 && j < 9;
action := i' = i + 2, k' = k + 1, j' = j + 1;
};
}
strategy gonnord_thesis_055_s {
Region init := {state = k1 && i = 0 && j = 0 && k = 0};
}
Expected invariant¶
{ k1[v1, v2, v3] : 2v2 <= v1 and 20v3 <= 11v1 - 2v2 and 10v3 >= v1 - 2v2 and v2 >= 0; k2[v1, v2, v3] : 2v2 <= v1 and 20v3 <= 11v1 - 2v2 and 10v3 >= v1 - 2v2 and v2 >= 0 }
Results¶
- With Aspic: { k1[i, j, k] : i <= 102 and 10k >= i - 2j and 2j <= i and 20k <= 11i - 2j and j <= 9; k2[i, j, k] : i <= 102 and 10k >= i - 2j and i >= 101 and 20k <= 11i - 2j and j <= 9 } (0.05s), failed.
- With ISL: { k1[i__1, j__1, k__1] : exists (e0 = [(i__1)/2], e1 = [(-i__1 + 2j__1)/20]: 2e0 = i__1 and 20e1 = -i__1 + 2j__1 and 2j__1 <= i__1 and i__1 >= 2 and j__1 <= 9 and i__1 <= 102 and 20k__1 <= 11i__1 - 2j__1 and 10k__1 >= i__1 - 2j__1 and 2j__1 >= -9i__1); k1[0, 0, 0]; k2[i__1, j__1, k__1] : exists (e0 = [(i__1)/2], e1 = [(-i__1 + 2j__1)/20]: 2e0 = i__1 and 20e1 = -i__1 + 2j__1 and 2j__1 <= i__1 and i__1 >= 101 and j__1 <= 9 and i__1 <= 102 and 20k__1 <= 11i__1 - 2j__1 and 10k__1 >= i__1 - 2j__1 and 2j__1 >= -9i__1) } (0.02s), failed.