Model realshellsort¶
Cited in: [AliasDFG10].
Tag: complexity.
Figure¶
Source code¶
model main {
var array_size, i, increment, j, temp, tmp, tmp_1, tmp_2;
states start, lbl_2_1, lbl_7_1, lbl_5_3, lbl_12_1, lbl_12_3, stop, lbl_10_1;
transition t_7 := {
from := start;
to := lbl_2_1;
guard := true;
action := tmp_2' = ?;
};
transition t_39 := {
from := lbl_2_1;
to := lbl_7_1;
guard := array_size <= 2 * tmp_2 + 1 && 2 * tmp_2 <= array_size && 1 <= tmp_2;
action := i' = 0, increment' = tmp_2, j' = 0, temp' = ?;
};
transition t_28 := {
from := lbl_2_1;
to := stop;
guard := array_size <= 2 * tmp_2 + 1 && 2 * tmp_2 <= array_size && tmp_2 <= 0;
action := increment' = tmp_2;
};
transition t_33 := {
from := lbl_7_1;
to := lbl_5_3;
guard := true;
action := i' = i + 1, tmp_1' = i;
};
transition t_32 := {
from := lbl_7_1;
to := lbl_10_1;
guard := increment <= j;
action := j' = j - increment;
};
transition t_35 := {
from := lbl_5_3;
to := lbl_7_1;
guard := i + 1 <= array_size;
action := j' = i, temp' = ?;
};
transition t_34 := {
from := lbl_5_3;
to := lbl_12_1;
guard := array_size <= i;
action := tmp' = ?;
};
transition t_16 := {
from := lbl_12_1;
to := lbl_12_3;
guard := increment <= 2 * tmp + 1 && 2 * tmp <= increment;
action := increment' = tmp;
};
transition t_37 := {
from := lbl_12_3;
to := lbl_7_1;
guard := 1 <= array_size && 1 <= increment;
action := i' = 0, j' = 0, temp' = ?;
};
transition t_36 := {
from := lbl_12_3;
to := lbl_12_1;
guard := array_size <= 0 && 1 <= increment;
action := i' = 0, tmp' = ?;
};
transition t_26 := {
from := lbl_12_3;
to := stop;
guard := increment <= 0;
action := ;
};
transition t_31 := {
from := lbl_10_1;
to := lbl_5_3;
guard := true;
action := i' = i + 1, tmp_1' = i;
};
transition t_30 := {
from := lbl_10_1;
to := lbl_10_1;
guard := increment <= j;
action := j' = j - increment;
};
}
strategy main_s {
Region init := {state = start};
}
Expected invariant¶
{ lbl_12_3[v1, v2, v3, v4, v5, v3, -1 + v2, v8] : v2 >= v1 and 2v8 >= -1 + v1 and v8 >= 1 and v8 >= 2v3 and 2v8 <= v1 and v4 <= -1 + v1 and v4 >= 0 and v3 >= 0; lbl_7_1[v1, v2, v3, v2, v5, v6, v7, v8] : 2v8 >= -1 + v1 and v8 >= v3 and v3 >= 1 and v2 >= 0 and v2 <= -1 + v1 and 2v8 <= v1; lbl_12_1[v1, v2, v3, v4, v5, v6, -1 + v2, v8] : v4 >= 0 and v3 >= 1 and v4 <= -1 + v1 and 2v8 <= v1 and v8 >= v3 and 2v8 >= -1 + v1 and v2 >= v1; lbl_5_3[v1, v2, v3, v4, v5, v6, -1 + v2, v8] : v8 >= v3 and 2v8 >= -1 + v1 and 2v8 <= v1 and v4 <= -1 + v1 and v4 <= -1 + v2 and v3 >= 1 and v4 >= 0; stop[v1, v2, v3, v4, v5, v6, v7, v8] : v8 >= v3 and 2v8 >= -1 + v1 and 2v8 <= v1 and v3 <= 0; lbl_10_1[v1, v2, v3, v4, v5, v6, v7, v8] : v3 >= 1 and v4 <= v2 - v3 and v4 >= 0 and v4 <= -1 + v1 and 2v8 <= v1 and 2v8 >= -1 + v1 and v8 >= v3 }
Results¶
- With Aspic: { lbl_7_1[array_size, i, increment, i, temp, tmp, tmp_1, tmp_2] : increment >= 1 and i >= 0 and i <= -1 + array_size and 2tmp_2 <= array_size and 2tmp_2 >= -1 + array_size and tmp_2 >= increment; lbl_5_3[array_size, i, increment, j, temp, tmp, -1 + i, tmp_2] : 2tmp_2 <= array_size and j <= -1 + array_size and j <= -1 + i and increment >= 1 and j >= 0 and tmp_2 >= increment and 2tmp_2 >= -1 + array_size; lbl_2_1[array_size, i, increment, j, temp, tmp, tmp_1, tmp_2]; lbl_12_1[array_size, i, increment, j, temp, tmp, -1 + i, tmp_2] : j <= -1 + array_size and 2tmp_2 <= array_size and tmp_2 >= increment and 2tmp_2 >= -1 + array_size and i >= array_size and j >= 0 and increment >= 1; lbl_12_3[array_size, i, increment, j, temp, increment, -1 + i, tmp_2] : 2tmp_2 <= array_size and j <= -1 + array_size and j >= 0 and increment >= 0 and tmp_2 >= 1 and tmp_2 >= 2increment and i >= array_size and 2tmp_2 >= -1 + array_size; stop[array_size, i, increment, j, temp, tmp, tmp_1, tmp_2] : tmp_2 >= increment and 2tmp_2 >= -1 + array_size and 2tmp_2 <= array_size and increment <= 0; lbl_10_1[array_size, i, increment, j, temp, tmp, tmp_1, tmp_2] : increment >= 1 and j <= i - increment and j >= 0 and j <= -1 + array_size and 2tmp_2 <= array_size and 2tmp_2 >= -1 + array_size and tmp_2 >= increment; start[array_size, i, increment, j, temp, tmp, tmp_1, tmp_2] } (0.12s), OK.
- With ISL: timeout.