Model halbwachs5¶
Cited in: [Halbwachs_misc10] p. 23.
Tag: fixpoint.
Figure¶
Source code¶
model halbwachs_aussois10_23 {
var b0, b1, ok, x, y;
states k;
transition t12 := {
from := k;
to := k;
guard := b0 != b1 && b0 = 1 && b1 = 0 && x < y;
action := b0' = 1 - b1, b1' = b0, y' = y + 1, ok' = 0;
};
transition t11 := {
from := k;
to := k;
guard := b0 != b1 && b0 = 1 && b1 = 0 && ok = 0;
action := b0' = 1 - b1, b1' = b0, y' = y + 1, ok' = 0;
};
transition t10 := {
from := k;
to := k;
guard := b0 != b1 && b0 = 1 && b1 = 0 && ok = 1 && x >= y;
action := b0' = 1 - b1, b1' = b0, y' = y + 1, ok' = 1;
};
transition t9 := {
from := k;
to := k;
guard := b0 != b1 && b0 = 0 && b1 = 1 && x < y;
action := b0' = 1 - b1, b1' = b0, y' = y + 1, ok' = 0;
};
transition t8 := {
from := k;
to := k;
guard := b0 != b1 && b0 = 0 && b1 = 1 && ok = 0;
action := b0' = 1 - b1, b1' = b0, y' = y + 1, ok' = 0;
};
transition t7 := {
from := k;
to := k;
guard := b0 != b1 && b0 = 0 && b1 = 1 && ok = 1 && x >= y;
action := b0' = 1 - b1, b1' = b0, y' = y + 1, ok' = 1;
};
transition t6 := {
from := k;
to := k;
guard := b0 = b1 && b0 = 1 && b1 = 1 && x < y;
action := b0' = 1 - b1, b1' = b0, x' = x + 1, ok' = 0;
};
transition t5 := {
from := k;
to := k;
guard := b0 = b1 && b0 = 1 && b1 = 1 && ok = 0;
action := b0' = 1 - b1, b1' = b0, x' = x + 1, ok' = 0;
};
transition t4 := {
from := k;
to := k;
guard := b0 = b1 && b0 = 1 && b1 = 1 && ok = 1 && x >= y;
action := b0' = 1 - b1, b1' = b0, x' = x + 1, ok' = 1;
};
transition t3 := {
from := k;
to := k;
guard := b0 = b1 && b0 = 0 && b1 = 0 && x < y;
action := b0' = 1 - b1, b1' = b0, x' = x + 1, ok' = 0;
};
transition t2 := {
from := k;
to := k;
guard := b0 = b1 && b0 = 0 && b1 = 0 && ok = 0;
action := b0' = 1 - b1, b1' = b0, x' = x + 1, ok' = 0;
};
transition t1 := {
from := k;
to := k;
guard := b0 = b1 && b0 = 0 && b1 = 0 && ok = 1 && x >= y;
action := b0' = 1 - b1, b1' = b0, x' = x + 1, ok' = 1;
};
}
strategy halbwachs_aussois10_23_s {
Region init := {state = k && b0 = 0 && b1 = 0 && x = 0 && y = 0 && ok = 1};
}
Expected invariant¶
{ k[v1, v2, v3, v4, v5] : v3 <= -1 or v3 >= 1 }
Results¶
- With Aspic: { k[b0, b1, 1, x, y] : y >= b1 and y <= -b0 + b1 + x and y <= b0 - b1 + x } (0.07s), OK.
- With ISL: { k[1, 1, 1, x__1, x__1] : (exists (e0 = [(-1 + x__1)/2]: 2e0 = -1 + x__1 and x__1 >= 3)) or (exists (e0, e1 = [(-1 + x__1 - 2e0)/2]: 2e1 = -1 + x__1 - 2e0 and e0 >= 1 and 2e0 <= -3 + x__1)) or (exists (e0, e1, e2 = [(-1 + x__1 - 2e0 - 2e1)/2]: 2e2 = -1 + x__1 - 2e0 - 2e1 and e1 >= 1 and 2e1 <= -3 + x__1 - 2e0 and e0 >= 1)); k[1, 0, 1, 1, 0]; k[0, 0, 1, 0, 0]; k[1, 0, 1, x__1, -1 + x__1] : (exists (e0 = [(-1 + x__1)/2]: 2e0 = -1 + x__1 and x__1 >= 3)) or (exists (e0, e1 = [(-1 + x__1 - 2e0)/2]: 2e1 = -1 + x__1 - 2e0 and e0 >= 1 and 2e0 <= -3 + x__1)) or (exists (e0, e1, e2 = [(-1 + x__1 - 2e0 - 2e1)/2]: 2e2 = -1 + x__1 - 2e0 - 2e1 and e1 >= 1 and 2e1 <= -3 + x__1 - 2e0 and e0 >= 1)); k[0, 1, 1, 2, 1]; k[1, 1, 1, 1, 1]; k[0, 0, 1, x__1, x__1] : exists (e0 = [(x__1)/2]: 2e0 = x__1 and x__1 >= 2); k[0, 1, 1, x__1, -1 + x__1] : (exists (e0 = [(-2 + x__1)/2]: 2e0 = -2 + x__1 and x__1 >= 4)) or (exists (e0, e1 = [(-2 + x__1 - 2e0)/2]: 2e1 = -2 + x__1 - 2e0 and e0 >= 1 and 2e0 <= -4 + x__1)) or (exists (e0, e1, e2 = [(-2 + x__1 - 2e0 - 2e1)/2]: 2e2 = -2 + x__1 - 2e0 - 2e1 and e1 >= 1 and 2e1 <= -4 + x__1 - 2e0 and e0 >= 1)) } (0.92s), OK.