# Model halbwachs9¶

Cited in: [Halbwachs_thesis] p. 128.

Tag: fixpoint.

## Source code¶

```model halbwachs_thesis_60 {

var i, j, k;

states k1, k3, k2;

transition t2 := {
from   := k1;
to     := k3;
guard  := i > 100;
action := ;
};

transition t1 := {
from   := k1;
to     := k2;
guard  := i <= 100;
action := k' = k + 1;
};

transition t4 := {
from   := k2;
to     := k1;
guard  := true;
action := i' = i + 2, j' = j + 1;
};

transition t3 := {
from   := k2;
to     := k1;
guard  := true;
action := i' = i + 4;
};

}

strategy halbwachs_thesis_60_s {

Region init := {state = k1 && i = 0 && j = 0 && k = 0};

}```

## Expected invariant¶

`{ k1[v1, v2, v3] : 4v3 = v1 + 2v2 }`

## Results¶

• With Aspic: { k1[i, j, k] : 4k = i + 2j and j >= 0 and 2j <= i; k3[i, j, k] : 4k = i + 2j and i >= 101 and j >= 0 and 2j <= i; k2[i, j, k] : 4k = 4 + i + 2j and j >= 0 and i <= 100 and 2j <= i } (0.06s), OK.
• With ISL: { k1[i__1, j__1, k__1] : (4k__1 = i__1 + 2j__1 and 2j__1 <= -4 + i__1 and i__1 <= 102 and j__1 >= 1) or (4k__1 = i__1 + 2j__1 and 2j__1 <= -8 + i__1 and i__1 <= 104 and j__1 >= 0) or (2j__1 = i__1 and 2k__1 = i__1 and i__1 <= 102 and i__1 >= 4) or (2j__1 = -4 + i__1 and 2k__1 = -2 + i__1 and i__1 <= 104 and i__1 >= 6); k1[2, 1, 1]; k1[4, 0, 1]; k1[0, 0, 0]; k3[i__1, j__1, k__1] : (4k__1 = i__1 + 2j__1 and 2j__1 <= -4 + i__1 and i__1 <= 102 and j__1 >= 1 and i__1 >= 101) or (4k__1 = i__1 + 2j__1 and 2j__1 <= -8 + i__1 and i__1 <= 104 and j__1 >= 0 and i__1 >= 101) or (2j__1 = i__1 and 2k__1 = i__1 and i__1 <= 102 and i__1 >= 101) or (2j__1 = -4 + i__1 and 2k__1 = -2 + i__1 and i__1 <= 104 and i__1 >= 101); k2[i__1, j__1, k__1] : (4k__1 = 4 + i__1 + 2j__1 and 2j__1 <= -4 + i__1 and i__1 <= 100 and j__1 >= 0) or (2j__1 = i__1 and 2k__1 = 2 + i__1 and i__1 <= 100 and i__1 >= 2); k2[0, 0, 1] } (0.04s), OK.