# Model loops¶

Cited in: [PodelskiR04].

Tag: complexity.

## Source code¶

```model main {

var n, x, y;

states start, lbl_10_1, lbl_12_1, stop;

transition t_35 := {
from   := start;
to     := lbl_10_1;
guard  := 2 <= n;
action := x' = n, y' = 2;
};

transition t_34 := {
from   := start;
to     := lbl_12_1;
guard  := n <= 1 && 0 <= n;
action := x' = n - 1, y' = 1;
};

transition t_22 := {
from   := start;
to     := stop;
guard  := n + 1 <= 0;
action := x' = n;
};

transition t_26 := {
from   := lbl_10_1;
to     := lbl_12_1;
guard  := x <= y;
action := x' = x - 1;
};

transition t_25 := {
from   := lbl_10_1;
to     := lbl_10_1;
guard  := y + 1 <= x;
action := y' = 2 * y;
};

transition t_31 := {
from   := lbl_12_1;
to     := lbl_10_1;
guard  := 2 <= x;
action := y' = 2;
};

transition t_29 := {
from   := lbl_12_1;
to     := stop;
guard  := x + 1 <= 0;
action := ;
};

transition t_30 := {
from   := lbl_12_1;
to     := lbl_12_1;
guard  := x <= 1 && 0 <= x;
action := x' = x - 1, y' = 1;
};

}

strategy main_s {

Region init := {state = start};

}```

## Expected invariant¶

`{ lbl_12_1[v1, v2, v3] : v3 >= 1 and v2 >= -1 and v2 <= -1 + v1 and v3 >= 1 + v2; stop[v1, v2, v3] : v2 <= v1 and v2 <= -1; lbl_10_1[v1, v2, v3] : v3 >= 2 and v3 <= -2 + 2v2 and v2 <= v1 }`

## Results¶

• With Aspic: { start[n, x, y]; lbl_12_1[n, x, y] : y >= 1 and x >= -1 and x <= -1 + n and y >= 1 + x; lbl_10_1[n, x, y] : y >= 2 and y <= -2 + 2x and x <= n; stop[n, x, y] : x <= n and x <= -1 } (0.05s), OK.
• With ISL: { stop[n__1, n__1, y__1] : n__1 <= -1; stop[n__1, -1, 1] : n__1 >= 3; stop[2, -1, 1]; stop[1, -1, 1]; stop[0, -1, 1]; lbl_12_1[n__1, x__1, y__1] : exists (e0 = [(y__1)/2]: 2e0 = y__1 and n__1 >= 2 and x__1 >= 2 and y__1 >= 1 + x__1 and y__1 <= 2x__1 and x__1 <= -2 + n__1); lbl_12_1[n__1, x__1, 1] : n__1 >= 3 and x__1 >= -1 and x__1 <= 0; lbl_12_1[n__1, -1 + n__1, y__1] : exists (e0 = [(y__1)/2]: 2e0 = y__1 and n__1 >= 3 and y__1 >= n__1 and y__1 <= -2 + 2n__1); lbl_12_1[n__1, 1, 2] : n__1 >= 3; lbl_12_1[2, x__1, 1] : x__1 >= -1 and x__1 <= 0; lbl_12_1[n__1, -1 + n__1, 1] : n__1 <= 1 and n__1 >= 0; lbl_12_1[2, 1, 2]; lbl_12_1[1, -1, 1]; lbl_10_1[n__1, x__1, y__1] : exists (e0 = [(y__1)/2]: 2e0 = y__1 and n__1 >= 2 and x__1 <= -1 + n__1 and x__1 >= 3 and y__1 <= -2 + 2x__1); lbl_10_1[n__1, x__1, 2] : n__1 >= 2 and x__1 <= -1 + n__1 and x__1 >= 2; lbl_10_1[n__1, n__1, y__1] : exists (e0 = [(y__1)/2]: 2e0 = y__1 and n__1 >= 3 and y__1 <= -2 + 2n__1); lbl_10_1[n__1, n__1, 2] : n__1 >= 2; start[n, x, y] } (0.02s), failed.