# Model exmini¶

Cited in: [AliasDFG10].

Tag: complexity.

## Source code¶

```model main {

var i, j, k, tmp;

states start, lbl_7_1, stop;

transition t_17 := {
from   := start;
to     := lbl_7_1;
guard  := i <= 100 && j <= k;
action := i' = j, j' = i + 1, k' = k - 1, tmp' = i;
};

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

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

transition t_15 := {
from   := lbl_7_1;
to     := lbl_7_1;
guard  := i <= 100 && j <= k;
action := i' = j, j' = i + 1, k' = k - 1, tmp' = i;
};

}

strategy main_s {

Region init := {state = start};

}```

## Expected invariant¶

```{ lbl_7_1[v1, v2, v3, -1 + v2] : v2 <= 101 and v3 >= -1 + v1 }
```

## Results¶

• With Aspic: { start[i, j, k, tmp]; lbl_7_1[i, j, k, -1 + j] : j <= 101 and k >= -1 + i; stop[i, j, k, tmp] } (0.05s), OK.
• With ISL: { lbl_7_1[i__1, j__1, k__1, -1 + j__1] : (j__1 <= 101 and k__1 >= -1 + i__1) or (k__1 >= -1 + i__1 and j__1 <= 101); stop[i__1, j__1, k__1, tmp__1] : k__1 <= -1 + j__1 or i__1 >= 101; stop[i__1, j__1, k__1, -1 + j__1] : (j__1 <= 101 and k__1 >= -1 + i__1 and k__1 <= -1 + j__1) or (j__1 <= 101 and k__1 >= -1 + i__1 and k__1 <= -1 + j__1) or (j__1 <= 101 and k__1 >= -1 + i__1 and i__1 >= 101) or (j__1 <= 101 and k__1 >= -1 + i__1 and i__1 >= 101); start[i, j, k, tmp] } (0.03s), OK.