Model realheapsort¶
Cited in: [AliasDFG10].
Tag: complexity.
Figure¶
Source code¶
model main {
var N, j, k, m, tmp, tmp_1, tmp_2, tmp_3, tmp_4, tmp_5;
states start, lbl_7_1, lbl_4_3, lbl_27_1, lbl_28_1, lbl_13_3, stop, lbl_10_1, lbl_11_1, lbl_12_1, lbl_12_3;
transition t_89 := {
from := start;
to := lbl_7_1;
guard := 3 <= N;
action := j' = 1, k' = 1, tmp_1' = ?;
};
transition t_71 := {
from := start;
to := stop;
guard := N <= 2;
action := ;
};
transition t_77 := {
from := lbl_7_1;
to := lbl_4_3;
guard := j <= 2 * tmp_1 + 2 && 2 * tmp_1 + 1 <= j;
action := k' = k + 1, tmp_5' = k;
};
transition t_76 := {
from := lbl_7_1;
to := lbl_10_1;
guard := j <= 2 * tmp_1 + 2 && 2 * tmp_1 + 1 <= j && 1 <= j;
action := tmp_4' = ?;
};
transition t_111 := {
from := lbl_4_3;
to := lbl_27_1;
guard := N <= k && 4 <= N;
action := j' = 2, k' = 0, m' = 2;
};
transition t_110 := {
from := lbl_4_3;
to := lbl_28_1;
guard := N <= k && 4 <= N;
action := j' = N, k' = 0, m' = 2;
};
transition t_109 := {
from := lbl_4_3;
to := lbl_27_1;
guard := N <= k && 3 <= N;
action := j' = 1, k' = 0, m' = 1;
};
transition t_108 := {
from := lbl_4_3;
to := lbl_28_1;
guard := N <= k && 3 <= N;
action := j' = N, k' = 0, m' = 1;
};
transition t_107 := {
from := lbl_4_3;
to := lbl_13_3;
guard := 2 = N && 2 <= k;
action := j' = 0, k' = 1, m' = 0, tmp' = 0;
};
transition t_87 := {
from := lbl_4_3;
to := stop;
guard := N <= k && N <= 1;
action := k' = 0;
};
transition t_86 := {
from := lbl_4_3;
to := lbl_7_1;
guard := k + 1 <= N;
action := j' = k, tmp_1' = ?;
};
transition t_95 := {
from := lbl_27_1;
to := lbl_28_1;
guard := 2 * j + k + 4 <= N;
action := j' = N, m' = 2 * j + 2;
};
transition t_93 := {
from := lbl_27_1;
to := lbl_28_1;
guard := 2 * j + k + 3 <= N;
action := j' = N, m' = 2 * j + 1;
};
transition t_92 := {
from := lbl_27_1;
to := lbl_13_3;
guard := N <= 2 * j + k + 2;
action := k' = k + 1, tmp' = k;
};
transition t_96 := {
from := lbl_27_1;
to := lbl_27_1;
guard := 2 * j + k + 4 <= N;
action := j' = 2 * j + 2, m' = 2 * j + 2;
};
transition t_94 := {
from := lbl_27_1;
to := lbl_27_1;
guard := 2 * j + k + 3 <= N;
action := j' = 2 * j + 1, m' = 2 * j + 1;
};
transition t_101 := {
from := lbl_28_1;
to := lbl_27_1;
guard := 2 * j + k + 4 <= N;
action := j' = 2 * j + 2, m' = 2 * j + 2;
};
transition t_99 := {
from := lbl_28_1;
to := lbl_27_1;
guard := 2 * j + k + 3 <= N;
action := j' = 2 * j + 1, m' = 2 * j + 1;
};
transition t_97 := {
from := lbl_28_1;
to := lbl_13_3;
guard := N <= 2 * j + k + 2;
action := k' = k + 1, tmp' = k;
};
transition t_100 := {
from := lbl_28_1;
to := lbl_28_1;
guard := 2 * j + k + 4 <= N;
action := j' = N, m' = 2 * j + 2;
};
transition t_98 := {
from := lbl_28_1;
to := lbl_28_1;
guard := 2 * j + k + 3 <= N;
action := j' = N, m' = 2 * j + 1;
};
transition t_106 := {
from := lbl_13_3;
to := lbl_27_1;
guard := k + 4 <= N;
action := j' = 2, m' = 2;
};
transition t_105 := {
from := lbl_13_3;
to := lbl_28_1;
guard := k + 4 <= N;
action := j' = N, m' = 2;
};
transition t_104 := {
from := lbl_13_3;
to := lbl_27_1;
guard := k + 3 <= N;
action := j' = 1, m' = 1;
};
transition t_103 := {
from := lbl_13_3;
to := lbl_28_1;
guard := k + 3 <= N;
action := j' = N, m' = 1;
};
transition t_82 := {
from := lbl_13_3;
to := stop;
guard := N <= k + 1;
action := ;
};
transition t_102 := {
from := lbl_13_3;
to := lbl_13_3;
guard := k + 2 = N;
action := j' = 0, k' = k + 1, m' = 0, tmp' = k;
};
transition t_66 := {
from := lbl_10_1;
to := lbl_11_1;
guard := j <= 2 * tmp_4 + 2 && 2 * tmp_4 + 1 <= j;
action := tmp_3' = ?;
};
transition t_64 := {
from := lbl_11_1;
to := lbl_12_1;
guard := j <= 2 * tmp_3 + 2 && 2 * tmp_3 + 1 <= j;
action := tmp_2' = ?;
};
transition t_62 := {
from := lbl_12_1;
to := lbl_12_3;
guard := j <= 2 * tmp_2 + 2 && 2 * tmp_2 + 1 <= j;
action := j' = tmp_2;
};
transition t_74 := {
from := lbl_12_3;
to := lbl_7_1;
guard := true;
action := tmp_1' = ?;
};
}
strategy main_s {
Region init := {state = start};
}
Expected invariant¶
{ lbl_11_1[v1, v2, v3, v4, v5, v6, v7, v8, v9, v10] : v1 >= 3 and v3 <= -1 + v1 and v2 >= 1 and 2v9 <= -1 + v2 and 2v6 <= -1 + v2 and v3 >= v2 and 2v6 >= -2 + v2 and 2v9 >= -2 + v2; lbl_27_1[v1, v2, v3, v2, v5, v6, v7, v8, v9, -1 + v1] : v3 <= -2 + v1 - v2 and 2v6 <= -2 + v1 and v2 >= 1 and v3 >= 0 and v6 >= -1; lbl_12_1[v1, v2, v3, v4, v5, v6, v7, v8, v9, v10] : v1 >= 3 and v3 <= -1 + v1 and v2 >= 1 and 2v9 <= -1 + v2 and 2v8 <= -1 + v2 and 2v6 <= -1 + v2 and v3 >= v2 and 2v6 >= -2 + v2 and 2v8 >= -2 + v2 and 2v9 >= -2 + v2; lbl_4_3[v1, v2, v3, v4, v5, v6, v7, v8, v9, -1 + v3] : 2v6 >= -2 + v2 and v3 >= 1 + v2 and v1 >= 3 and v3 <= v1 and v2 >= 0 and 2v6 <= -1 + v2 and v3 >= 2; lbl_28_1[v1, v1, v3, v4, v5, v6, v7, v8, v9, -1 + v1] : v4 <= -2 + v1 - v3 and 2v6 <= -2 + v1 and v4 >= 1 and v6 >= -1 and v3 >= 0; lbl_7_1[v1, v2, v3, v4, v5, v6, v7, v8, v9, v10] : v3 >= 1 and v2 >= 0 and v3 <= -1 + v1 and v1 >= 3 and v3 >= v2; lbl_10_1[v1, v2, v3, v4, v5, v6, v7, v8, v9, v10] : v1 >= 3 and v3 <= -1 + v1 and v2 >= 1 and 2v6 <= -1 + v2 and v3 >= v2 and 2v6 >= -2 + v2; lbl_12_3[v1, v2, v3, v4, v5, v2, v2, v2, v2, v10] : v3 <= -1 + v1 and v1 >= 3 and v3 >= 1 + 2v2 and v2 >= 0; lbl_13_3[v1, v2, v3, v4, -1 + v3, v6, v7, v8, v9, -1 + v1] : v4 <= -1 + v1 - v3 and 2v6 <= -2 + v1 and 3v4 >= 3 - v1 + v2 and v3 <= -1 + v1 and v4 >= -1 + v1 - v2 - v3 and v6 >= -1 and v3 >= 1 and v4 <= v2 and v2 <= v1 }
Results¶
- With Aspic: { lbl_12_1[N, j, k, m, tmp, tmp_1, tmp_2, tmp_3, tmp_4, tmp_5] : N >= 3 and k <= -1 + N and j >= 1 and 2tmp_4 <= -1 + j and 2tmp_3 <= -1 + j and 2tmp_1 <= -1 + j and k >= j and 2tmp_1 >= -2 + j and 2tmp_3 >= -2 + j and 2tmp_4 >= -2 + j; lbl_28_1[N, N, k, m, tmp, tmp_1, tmp_2, tmp_3, tmp_4, -1 + N] : k >= 0 and m >= 1 and tmp_1 >= -1 and m <= -2 + N - k and 2tmp_1 <= -2 + N; lbl_10_1[N, j, k, m, tmp, tmp_1, tmp_2, tmp_3, tmp_4, tmp_5] : N >= 3 and k <= -1 + N and j >= 1 and 2tmp_1 <= -1 + j and k >= j and 2tmp_1 >= -2 + j; lbl_7_1[N, j, k, m, tmp, tmp_1, tmp_2, tmp_3, tmp_4, tmp_5] : k >= 1 and j >= 0 and k <= -1 + N and N >= 3 and k >= j; start[N, j, k, m, tmp, tmp_1, tmp_2, tmp_3, tmp_4, tmp_5]; lbl_4_3[N, j, k, m, tmp, tmp_1, tmp_2, tmp_3, tmp_4, -1 + k] : N >= 3 and k <= N and j >= 0 and 2tmp_1 <= -1 + j and k >= 2 and 2tmp_1 >= -2 + j and k >= 1 + j; lbl_11_1[N, j, k, m, tmp, tmp_1, tmp_2, tmp_3, tmp_4, tmp_5] : N >= 3 and k <= -1 + N and j >= 1 and 2tmp_4 <= -1 + j and 2tmp_1 <= -1 + j and k >= j and 2tmp_1 >= -2 + j and 2tmp_4 >= -2 + j; lbl_12_3[N, j, k, m, tmp, j, j, j, j, tmp_5] : k >= 1 + 2j and k >= 1 and j >= 0 and k <= -1 + N and N >= 3; stop[N, j, k, m, tmp, tmp_1, tmp_2, tmp_3, tmp_4, tmp_5]; lbl_27_1[N, j, k, j, tmp, tmp_1, tmp_2, tmp_3, tmp_4, -1 + N] : tmp_1 >= -1 and j >= 1 and k >= 0 and k <= -2 + N - j and 2tmp_1 <= -2 + N; lbl_13_3[N, j, k, m, -1 + k, tmp_1, tmp_2, tmp_3, tmp_4, -1 + N] : m >= -1 + N - j - k and tmp_1 >= -1 and k >= 1 and m >= 2 - k and m <= j and j <= N and 3m >= 3 - N + j and k <= -1 + N and m <= -1 + N - k and 2tmp_1 <= -2 + N } (0.30s), OK.
- With ISL: timeout.