# Model terminate¶

Cited in: [ColonS01].

Tags: complexity, termination.

## Source code¶

```model main {

var ell, i, j, k;

states start, lbl_7_2, stop;

transition t_16 := {
from   := start;
to     := lbl_7_2;
guard  := i <= 100 && j <= k;
action := ell' = i, i' = j, j' = i + 1, k' = k - 1;
};

transition t_15 := {
from   := start;
to     := stop;
guard  := 101 <= i || k + 1 <= j;
action := ;
};

transition t_13 := {
from   := lbl_7_2;
to     := stop;
guard  := 101 <= i || k + 1 <= j;
action := ;
};

transition t_14 := {
from   := lbl_7_2;
to     := lbl_7_2;
guard  := i <= 100 && j <= k;
action := ell' = i, i' = j, j' = i + 1, k' = k - 1;
};

}

strategy main_s {

Region init := {state = start};

}```

## Expected invariant¶

```{ lbl_7_2[v1, v2, 1 + v1, v4] : v4 >= -1 + v2 and v1 <= 100 }
```

## Results¶

• With Aspic: { lbl_7_2[ell, i, 1 + ell, k] : k >= -1 + i and ell <= 100; start[ell, i, j, k]; stop[ell, i, j, k] } (0.21s), OK.
• With ISL: { start[ell, i, j, k]; lbl_7_2[ell__1, i__1, 1 + ell__1, k__1] : (ell__1 <= 100 and k__1 >= -1 + i__1) or (k__1 >= -1 + i__1 and ell__1 <= 100); stop[ell__1, i__1, j__1, k__1] : k__1 <= -1 + j__1 or i__1 >= 101; stop[ell__1, i__1, 1 + ell__1, k__1] : (ell__1 <= 100 and k__1 >= -1 + i__1 and k__1 <= ell__1) or (ell__1 <= 100 and k__1 >= -1 + i__1 and k__1 <= ell__1) or (ell__1 <= 100 and k__1 >= -1 + i__1 and i__1 >= 101) or (ell__1 <= 100 and k__1 >= -1 + i__1 and i__1 >= 101) } (0.04s), OK.