# Model gonnord2¶

Cited in: [Gonnord_thesis] fig. 4.7 p. 55.

Tag: fixpoint.

## 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.