Figure¶

Source code¶

model main {

  var N, j, k, m, tmp, tmp_1, tmp_2, tmp_3, tmp_4;

  states start, lbl_7_1, lbl_4_3, stop, lbl_10_1, lbl_11_1, lbl_12_1, lbl_12_3;

  transition t_36 := {
    from   := start;
    to     := lbl_7_1;
    guard  := 3 <= N;
    action := j' = 1, k' = 1, tmp' = ?;
  };

  transition t_28 := {
    from   := start;
    to     := stop;
    guard  := N <= 2;
    action := ;
  };

  transition t_32 := {
    from   := lbl_7_1;
    to     := lbl_4_3;
    guard  := j <= 2 * tmp + 2 && 2 * tmp + 1 <= j;
    action := k' = k + 1, tmp_4' = k;
  };

  transition t_31 := {
    from   := lbl_7_1;
    to     := lbl_10_1;
    guard  := j <= 2 * tmp + 2 && 2 * tmp + 1 <= j && 1 <= j;
    action := tmp_3' = ?;
  };

  transition t_34 := {
    from   := lbl_4_3;
    to     := lbl_7_1;
    guard  := k + 1 <= N;
    action := j' = k, tmp' = ?;
  };

  transition t_33 := {
    from   := lbl_4_3;
    to     := stop;
    guard  := N <= k;
    action := ;
  };

  transition t_23 := {
    from   := lbl_10_1;
    to     := lbl_11_1;
    guard  := j <= 2 * tmp_3 + 2 && 2 * tmp_3 + 1 <= j;
    action := tmp_2' = ?;
  };

  transition t_21 := {
    from   := lbl_11_1;
    to     := lbl_12_1;
    guard  := j <= 2 * tmp_2 + 2 && 2 * tmp_2 + 1 <= j;
    action := tmp_1' = ?;
  };

  transition t_19 := {
    from   := lbl_12_1;
    to     := lbl_12_3;
    guard  := j <= 2 * tmp_1 + 2 && 2 * tmp_1 + 1 <= j;
    action := j' = tmp_1;
  };

  transition t_29 := {
    from   := lbl_12_3;
    to     := lbl_7_1;
    guard  := true;
    action := tmp' = ?;
  };

}

strategy main_s {

  Region init := {state = start};

}

Expected invariant¶

{ lbl_11_1[v1, v2, v3, v4, v5, v6, v7, v8, v9] : v1 >= 3 and v3 <= -1 + v1 and v2 >= 1 and 2v8 <= -1 + v2 and 2v5 <= -1 + v2 and v3 >= v2 and 2v5 >= -2 + v2 and 2v8 >= -2 + v2; lbl_4_3[v1, v2, v3, v4, v5, v6, v7, v8, -1 + v3] : 2v5 >= -2 + v2 and v3 >= 1 + v2 and v1 >= 3 and v3 <= v1 and 2v5 <= -1 + v2 and v3 >= 2; lbl_12_1[v1, v2, v3, v4, v5, v6, v7, v8, v9] : v1 >= 3 and v3 <= -1 + v1 and v2 >= 1 and 2v8 <= -1 + v2 and 2v7 <= -1 + v2 and 2v5 <= -1 + v2 and v3 >= v2 and 2v5 >= -2 + v2 and 2v7 >= -2 + v2 and 2v8 >= -2 + v2; lbl_10_1[v1, v2, v3, v4, v5, v6, v7, v8, v9] : v1 >= 3 and v3 <= -1 + v1 and v2 >= 1 and 2v5 <= -1 + v2 and v3 >= v2 and 2v5 >= -2 + v2; lbl_7_1[v1, v2, v3, v4, v5, v6, v7, v8, v9] : v3 >= 1 and v3 <= -1 + v1 and v1 >= 3 and v3 >= v2; lbl_12_3[v1, v2, v3, v4, v2, v2, v2, v2, v9] : v3 <= -1 + v1 and v1 >= 3 and v3 >= 1 + 2v2 and v2 >= 0 }

Results¶

• With Aspic: { lbl_7_1[N, j, k, m, tmp, tmp_1, tmp_2, tmp_3, tmp_4] : k >= 1 and k <= -1 + N and N >= 3 and k >= j; stop[N, j, k, m, tmp, tmp_1, tmp_2, tmp_3, tmp_4]; lbl_4_3[N, j, k, m, tmp, tmp_1, tmp_2, tmp_3, -1 + k] : N >= 3 and k <= N and 2tmp <= -1 + j and k >= 2 and 2tmp >= -2 + j and k >= 1 + j; lbl_10_1[N, j, k, m, tmp, tmp_1, tmp_2, tmp_3, tmp_4] : N >= 3 and k <= -1 + N and j >= 1 and 2tmp <= -1 + j and k >= j and 2tmp >= -2 + j; start[N, j, k, m, tmp, tmp_1, tmp_2, tmp_3, tmp_4]; lbl_12_1[N, j, k, m, tmp, tmp_1, tmp_2, tmp_3, tmp_4] : N >= 3 and k <= -1 + N and j >= 1 and 2tmp_3 <= -1 + j and 2tmp_2 <= -1 + j and 2tmp <= -1 + j and k >= j and 2tmp >= -2 + j and 2tmp_2 >= -2 + j and 2tmp_3 >= -2 + j; lbl_11_1[N, j, k, m, tmp, tmp_1, tmp_2, tmp_3, tmp_4] : N >= 3 and k <= -1 + N and j >= 1 and 2tmp_3 <= -1 + j and 2tmp <= -1 + j and k >= j and 2tmp >= -2 + j and 2tmp_3 >= -2 + j; lbl_12_3[N, j, k, m, j, j, j, j, tmp_4] : k >= 1 and k >= 1 + 2j and j >= 0 and k <= -1 + N and N >= 3 } (0.09s), OK.
• With ISL: { lbl_11_1[N__1, j__1, j__1, m__1, tmp__1, tmp_1__1, tmp_2__1, tmp_3__1, -1 + j__1] : 2tmp_3__1 >= -2 + j__1 and 2tmp_3__1 <= -1 + j__1 and 2tmp__1 >= -2 + j__1 and 2tmp__1 <= -1 + j__1 and j__1 <= -1 + N__1 and j__1 >= 3; lbl_11_1[N__1, j__1, k__1, m__1, tmp__1, j__1, tmp_2__1, tmp_3__1, -1 + k__1] : 2tmp_3__1 <= -1 + j__1 and 2tmp__1 >= -2 + j__1 and k__1 >= 1 + 2j__1 and 2tmp__1 <= -1 + j__1 and k__1 <= -1 + N__1 and j__1 >= 1 and 2tmp_3__1 >= -2 + j__1; lbl_11_1[N__1, 1, 1, m__1, 0, tmp_1__1, tmp_2__1, 0, tmp_4__1] : N__1 >= 3; lbl_11_1[N__1, 2, 2, m__1, 0, tmp_1__1, tmp_2__1, 0, 1] : N__1 >= 3; lbl_11_1[N__1, 2, 2, m__1, 0, 0, tmp_2__1, 0, 1] : N__1 >= 3; lbl_4_3[N__1, j__1, 1 + j__1, m__1, tmp__1, tmp_1__1, tmp_2__1, tmp_3__1, j__1] : j__1 <= -1 + N__1 and 2tmp__1 <= -1 + j__1 and 2tmp__1 >= -2 + j__1 and j__1 >= 2; lbl_4_3[N__1, j__1, k__1, m__1, tmp__1, j__1, tmp_2__1, tmp_3__1, -1 + k__1] : 2tmp_2__1 >= -3 + k__1 and k__1 <= 3 + 2j__1 and 2tmp_2__1 <= -2 + k__1 and k__1 >= 3 and k__1 <= N__1 and 2tmp__1 >= -2 + j__1 and 2tmp__1 <= -1 + j__1 and k__1 >= 2 + 2j__1 and 2tmp_3__1 >= -3 + k__1 and 2tmp_3__1 <= -2 + k__1; lbl_4_3[N__1, 1, 2, m__1, 0, tmp_1__1, tmp_2__1, tmp_3__1, 1] : N__1 >= 3; lbl_4_3[N__1, j__1, k__1, m__1, tmp__1, j__1, j__1, j__1, -1 + k__1] : j__1 >= 0 and 2tmp__1 <= -1 + j__1 and 2tmp__1 >= -2 + j__1 and k__1 >= 4 + 2j__1 and k__1 <= N__1; lbl_4_3[N__1, 0, 2, m__1, -1, 0, 0, 0, 1] : N__1 >= 3; lbl_12_1[N__1, j__1, k__1, m__1, tmp__1, tmp_1__1, tmp_2__1, tmp_3__1, -1 + k__1] : k__1 >= 1 + 2j__1 and 2tmp_2__1 >= -2 + j__1 and 2tmp__1 >= -2 + j__1 and 2tmp_3__1 <= -1 + j__1 and k__1 <= -1 + N__1 and 2tmp_3__1 >= -2 + j__1 and 2tmp_2__1 <= -1 + j__1 and j__1 >= 1 and 2tmp__1 <= -1 + j__1; lbl_12_1[N__1, j__1, j__1, m__1, tmp__1, tmp_1__1, tmp_2__1, tmp_3__1, -1 + j__1] : 2tmp_2__1 <= -1 + j__1 and 2tmp__1 <= -1 + j__1 and 2tmp__1 >= -2 + j__1 and 2tmp_3__1 >= -2 + j__1 and j__1 <= -1 + N__1 and 2tmp_3__1 <= -1 + j__1 and 2tmp_2__1 >= -2 + j__1 and j__1 >= 2; lbl_12_1[N__1, 1, 1, m__1, 0, tmp_1__1, 0, 0, tmp_4__1] : N__1 >= 3; lbl_12_1[N__1, 2, 2, m__1, 0, tmp_1__1, 0, 0, 1] : N__1 >= 3; stop[N__1, j__1, k__1, m__1, tmp__1, tmp_1__1, tmp_2__1, tmp_3__1, tmp_4__1] : N__1 <= 2; stop[N__1, -1 + N__1, N__1, m__1, tmp__1, tmp_1__1, tmp_2__1, tmp_3__1, -1 + N__1] : N__1 >= 3 and 2tmp__1 <= -2 + N__1 and 2tmp__1 >= -3 + N__1; stop[N__1, j__1, N__1, m__1, tmp__1, j__1, tmp_2__1, tmp_3__1, -1 + N__1] : 2tmp_2__1 >= -3 + N__1 and 2j__1 >= -3 + N__1 and 2tmp_2__1 <= -2 + N__1 and N__1 >= 3 and 2tmp_3__1 <= -2 + N__1 and 2tmp__1 >= -2 + j__1 and 2tmp__1 <= -1 + j__1 and 2j__1 <= -2 + N__1 and 2tmp_3__1 >= -3 + N__1; stop[N__1, j__1, N__1, m__1, tmp__1, j__1, j__1, j__1, -1 + N__1] : j__1 >= 0 and 2tmp__1 <= -1 + j__1 and 2tmp__1 >= -2 + j__1 and 2j__1 <= -4 + N__1; start[N, j, k, m, tmp, tmp_1, tmp_2, tmp_3, tmp_4]; lbl_10_1[N__1, j__1, j__1, m__1, tmp__1, tmp_1__1, tmp_2__1, tmp_3__1, -1 + j__1] : j__1 <= -1 + N__1 and 2tmp__1 <= -1 + j__1 and 2tmp__1 >= -2 + j__1 and j__1 >= 3; lbl_10_1[N__1, j__1, k__1, m__1, tmp__1, j__1, tmp_2__1, tmp_3__1, -1 + k__1] : 2tmp_2__1 <= -1 + k__1 and k__1 <= 2 + 2j__1 and 2tmp__1 >= -2 + j__1 and j__1 >= 1 and k__1 <= -1 + N__1 and 2tmp__1 <= -1 + j__1 and 2tmp_2__1 >= -2 + k__1 and k__1 >= 1 + 2j__1; lbl_10_1[N__1, 1, 1, m__1, 0, tmp_1__1, tmp_2__1, tmp_3__1, tmp_4__1] : N__1 >= 3; lbl_10_1[N__1, j__1, k__1, m__1, tmp__1, j__1, j__1, tmp_3__1, -1 + k__1] : k__1 >= 3 + 2j__1 and 2tmp__1 <= -1 + j__1 and 2tmp__1 >= -2 + j__1 and j__1 >= 1 and k__1 <= -1 + N__1; lbl_10_1[N__1, 2, 2, m__1, 0, tmp_1__1, tmp_2__1, tmp_3__1, 1] : N__1 >= 3; lbl_10_1[N__1, 2, 2, m__1, 0, 0, 0, tmp_3__1, 1] : N__1 >= 3; lbl_7_1[N__1, 1, 1, m__1, tmp__1, tmp_1__1, tmp_2__1, tmp_3__1, tmp_4__1] : N__1 >= 3; lbl_7_1[N__1, j__1, j__1, m__1, tmp__1, tmp_1__1, tmp_2__1, tmp_3__1, -1 + j__1] : j__1 >= 3 and j__1 <= -1 + N__1; lbl_7_1[N__1, j__1, k__1, m__1, tmp__1, j__1, tmp_2__1, tmp_3__1, -1 + k__1] : 2tmp_2__1 <= -1 + k__1 and k__1 >= 1 + 2j__1 and k__1 <= 2 + 2j__1 and 2tmp_3__1 >= -2 + k__1 and k__1 <= -1 + N__1 and 2tmp_3__1 <= -1 + k__1 and 2tmp_2__1 >= -2 + k__1 and k__1 >= 2; lbl_7_1[N__1, 2, 2, m__1, tmp__1, tmp_1__1, tmp_2__1, tmp_3__1, 1] : N__1 >= 3; lbl_7_1[N__1, j__1, k__1, m__1, tmp__1, j__1, j__1, j__1, -1 + k__1] : k__1 <= -1 + N__1 and j__1 >= 0 and k__1 >= 3 + 2j__1; lbl_7_1[N__1, 0, 1, m__1, tmp__1, 0, 0, 0, tmp_4__1] : N__1 >= 3; lbl_7_1[N__1, 2, 2, m__1, tmp__1, 0, 0, 0, 1] : N__1 >= 3; lbl_12_3[N__1, j__1, k__1, m__1, tmp__1, j__1, tmp_2__1, tmp_3__1, -1 + k__1] : 2tmp__1 <= -1 + k__1 and 2tmp_3__1 >= -2 + k__1 and 2tmp_3__1 <= -1 + k__1 and 2tmp_2__1 >= -2 + k__1 and k__1 <= -1 + N__1 and 2tmp_2__1 <= -1 + k__1 and k__1 <= 2 + 2j__1 and k__1 >= 2 and k__1 >= 1 + 2j__1 and 2tmp__1 >= -2 + k__1; lbl_12_3[N__1, j__1, k__1, m__1, j__1, j__1, j__1, j__1, -1 + k__1] : k__1 <= -1 + N__1 and j__1 >= 0 and k__1 >= 3 + 2j__1; lbl_12_3[N__1, 0, 1, m__1, 0, 0, 0, 0, tmp_4__1] : N__1 >= 3; lbl_12_3[N__1, 0, 2, m__1, 0, 0, 0, 0, 1] : N__1 >= 3 } (4.13s), OK.