Figure¶

Source code¶

model main {

  var array_size, i, j, mn, temp, tmp, tmp_1;

  states start, lbl_5_3, lbl_9_1, lbl_1_3, stop;

  transition t_41 := {
    from   := start;
    to     := lbl_5_3;
    guard  := 2 <= array_size;
    action := i' = 0, j' = 2, mn' = 1, tmp' = 1;
  };

  transition t_40 := {
    from   := start;
    to     := lbl_5_3;
    guard  := 2 <= array_size;
    action := i' = 0, j' = 2, mn' = 0, tmp' = 1;
  };

  transition t_31 := {
    from   := start;
    to     := stop;
    guard  := array_size <= 1;
    action := i' = 0;
  };

  transition t_33 := {
    from   := lbl_5_3;
    to     := lbl_9_1;
    guard  := array_size <= j;
    action := temp' = ?;
  };

  transition t_35 := {
    from   := lbl_5_3;
    to     := lbl_5_3;
    guard  := j + 1 <= array_size;
    action := j' = j + 1, mn' = j, tmp' = j;
  };

  transition t_34 := {
    from   := lbl_5_3;
    to     := lbl_5_3;
    guard  := j + 1 <= array_size;
    action := j' = j + 1, tmp' = j;
  };

  transition t_24 := {
    from   := lbl_9_1;
    to     := lbl_1_3;
    guard  := true;
    action := i' = i + 1, tmp_1' = i;
  };

  transition t_38 := {
    from   := lbl_1_3;
    to     := lbl_5_3;
    guard  := i + 2 <= array_size;
    action := j' = i + 2, mn' = i + 1, tmp' = i + 1;
  };

  transition t_37 := {
    from   := lbl_1_3;
    to     := lbl_5_3;
    guard  := i + 2 <= array_size;
    action := j' = i + 2, mn' = i, tmp' = i + 1;
  };

  transition t_29 := {
    from   := lbl_1_3;
    to     := stop;
    guard  := array_size <= i + 1;
    action := ;
  };

}

strategy main_s {

  Region init := {state = start};

}

Expected invariant¶

{ lbl_5_3[v1, v2, v3, v4, v5, -1 + v3, v7] : v2 >= 0 and v3 <= v1 and v4 >= v2 and v3 >= 2 + v2 and v4 <= -1 + v3; lbl_1_3[v1, v2, v1, v4, v5, -1 + v1, -1 + v2] : v2 >= 1 and v4 >= -1 + v2 and v4 <= -1 + v1 and v2 <= -1 + v1; stop[v1, v2, v3, v4, v5, v6, v7] : v2 >= 0 and v2 >= -1 + v1; lbl_9_1[v1, v2, v1, v4, v5, -1 + v1, v7] : v2 <= -2 + v1 and v4 >= v2 and v2 >= 0 and v4 <= -1 + v1 }

Results¶

• With Aspic: { stop[array_size, i, j, mn, temp, tmp, tmp_1] : i >= 0 and i >= -1 + array_size; start[array_size, i, j, mn, temp, tmp, tmp_1]; lbl_5_3[array_size, i, j, mn, temp, -1 + j, tmp_1] : mn >= i and j >= 2 + i and mn <= -1 + j and i >= 0 and j <= array_size; lbl_1_3[array_size, i, array_size, mn, temp, -1 + array_size, -1 + i] : mn <= -1 + array_size and i <= -1 + array_size and i >= 1 and mn >= -1 + i; lbl_9_1[array_size, i, array_size, mn, temp, -1 + array_size, tmp_1] : i >= 0 and mn <= -1 + array_size and i <= -2 + array_size and mn >= i } (0.10s), OK.
• With ISL: { lbl_5_3[array_size__1, i__1, j__1, mn__1, temp__1, -1 + j__1, tmp_1__1] : array_size__1 >= 3 and i__1 >= 1 and j__1 <= array_size__1; lbl_5_3[array_size__1, 0, j__1, mn__1, temp__1, -1 + j__1, tmp_1__1] : j__1 <= array_size__1 and j__1 >= 3; lbl_5_3[array_size__1, 0, 2, mn__1, temp__1, 1, tmp_1__1] : array_size__1 >= 2 and mn__1 <= 1 and mn__1 >= 0; lbl_1_3[array_size__1, i__1, array_size__1, mn__1, temp__1, -1 + array_size__1, -1 + i__1] : (i__1 >= 2 and array_size__1 >= 3) or (array_size__1 >= 3 and i__1 >= 1); lbl_1_3[2, 1, 2, mn__1, temp__1, 1, 0] : mn__1 >= 0 and mn__1 <= 1; start[array_size, i, j, mn, temp, tmp, tmp_1]; lbl_9_1[array_size__1, i__1, array_size__1, mn__1, temp__1, -1 + array_size__1, tmp_1__1] : (array_size__1 >= 3 and i__1 >= 1) or (i__1 >= 1 and array_size__1 >= 3); lbl_9_1[2, 0, 2, mn__1, temp__1, 1, tmp_1__1] : mn__1 >= 0 and mn__1 <= 1; lbl_9_1[array_size__1, 0, array_size__1, mn__1, temp__1, -1 + array_size__1, tmp_1__1] : array_size__1 >= 3; stop[array_size__1, 0, j__1, mn__1, temp__1, tmp__1, tmp_1__1] : array_size__1 <= 1; stop[array_size__1, i__1, array_size__1, mn__1, temp__1, -1 + array_size__1, -1 + i__1] : (i__1 >= 2 and array_size__1 >= 3 and i__1 >= -1 + array_size__1) or (array_size__1 >= 3 and i__1 >= 1 and i__1 >= -1 + array_size__1); stop[2, 1, 2, mn__1, temp__1, 1, 0] : mn__1 >= 0 and mn__1 <= 1 } (0.19s), failed.