# Model jeannet1¶

Cited in: [Jeannet_thesis] fig. 2.1 p. 16.

Tag: fixpoint.

## Source code¶

```model jeannet_thesis_016 {

var i, j;

states k1, k3, k2;

transition t2 := {
from   := k1;
to     := k3;
guard  := i + j > 20;
action := ;
};

transition t1 := {
from   := k1;
to     := k2;
guard  := i + j <= 20;
action := ;
};

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

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

}

strategy jeannet_thesis_016_s {

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

}```

## Expected invariant¶

`{ k2[v1, v2] : 2v2 <= -2 + v1 and v2 <= 4 }`

## Results¶

• With Aspic: { k2[i, j] : 2j <= -2 + i and j <= 4 and j <= 20 - i; k3[i, j] : j <= 4 and j >= 21 - i; k1[i, j] : j <= 4 and 2j <= -2 + i } (0.05s), OK.
• With ISL: { k3[i__1, 4] : exists (e0 = [(-2 + i__1)/4]: 4e0 = -2 + i__1 and i__1 <= 20 and i__1 >= 17); k2[i__1, j__1] : 2j__1 = -2 + i__1 and i__1 <= 11 and i__1 >= 4; k2[i__1, 4] : (exists (e0 = [(-2 + i__1)/4]: 4e0 = -2 + i__1 and i__1 >= 14 and i__1 <= 16)) or (exists (e0, e1 = [(10 - i__1 + 4e0)/4]: 4e1 = 10 - i__1 + 4e0 and 4e0 <= -14 + i__1 and e0 >= 1 and i__1 <= 16)) or (exists (e0 = [(-2 + i__1)/4]: 4e0 = -2 + i__1 and i__1 <= 16 and i__1 >= 14)) or (exists (e0 = [(-2 + i__1)/4]: 4e0 = -2 + i__1 and i__1 >= 14 and i__1 <= 16)) or (exists (e0, e1 = [(-10 + i__1 - 4e0)/4]: 4e1 = -10 + i__1 - 4e0 and i__1 <= 16 and 4e0 <= -14 + i__1 and e0 >= 1)) or (exists (e0 = [(-2 + i__1)/4]: 4e0 = -2 + i__1 and i__1 <= 16 and i__1 >= 14)) or (exists (e0, e1 = [(10 - i__1 + 4e0)/4]: 4e1 = 10 - i__1 + 4e0 and 4e0 <= -14 + i__1 and i__1 <= 16 and e0 >= 1)) or (exists (e0, e1, e2 = [(10 - i__1 + 4e0 + 4e1)/4]: 4e2 = 10 - i__1 + 4e0 + 4e1 and e0 >= 1 and e1 >= 1 and i__1 <= 16 and 4e1 <= -14 + i__1 - 4e0)); k2[2, 0]; k1[i__1, j__1] : 2j__1 = -2 + i__1 and i__1 <= 11 and i__1 >= 4; k1[i__1, 4] : exists (e0 = [(-2 + i__1)/4]: 4e0 = -2 + i__1 and i__1 <= 20 and i__1 >= 14); k1[2, 0] } (0.02s), OK.