Figure¶

Source code¶

model main {

  var i, j, length, temp, test, tmp;

  states start, lbl_5_3, lbl_7_1, lbl_1_3, stop;

  transition t_52 := {
    from   := start;
    to     := lbl_5_3;
    guard  := 2 <= length;
    action := i' = length - 1, j' = 1, test' = 0, tmp' = 0;
  };

  transition t_51 := {
    from   := start;
    to     := lbl_7_1;
    guard  := 2 <= length;
    action := i' = length - 1, j' = 0, temp' = ?, test' = 0;
  };

  transition t_39 := {
    from   := start;
    to     := stop;
    guard  := length <= 1;
    action := i' = length - 1;
  };

  transition t_43 := {
    from   := lbl_5_3;
    to     := lbl_7_1;
    guard  := j + 1 <= i;
    action := temp' = ?;
  };

  transition t_42 := {
    from   := lbl_5_3;
    to     := lbl_1_3;
    guard  := i <= j && test + 1 <= 0 || i <= j && 1 <= test;
    action := i' = i - 1;
  };

  transition t_41 := {
    from   := lbl_5_3;
    to     := stop;
    guard  := i <= j && 0 = test;
    action := ;
  };

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

  transition t_35 := {
    from   := lbl_7_1;
    to     := lbl_5_3;
    guard  := true;
    action := j' = j + 1, test' = 1, tmp' = j;
  };

  transition t_48 := {
    from   := lbl_1_3;
    to     := lbl_5_3;
    guard  := 1 <= i;
    action := j' = 1, test' = 0, tmp' = 0;
  };

  transition t_47 := {
    from   := lbl_1_3;
    to     := lbl_7_1;
    guard  := 1 <= i;
    action := j' = 0, temp' = ?, test' = 0;
  };

  transition t_37 := {
    from   := lbl_1_3;
    to     := stop;
    guard  := i <= 0;
    action := ;
  };

}

strategy main_s {

  Region init := {state = start};

}

Expected invariant¶

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

Results¶

• With Aspic: { stop[i, j, length, temp, test, tmp] : length >= 1 + i; start[i, j, length, temp, test, tmp]; lbl_1_3[i, 1 + i, length, temp, test, i] : length >= 2 + i and test >= 1 and i >= 0; lbl_5_3[i, j, length, temp, test, -1 + j] : test >= 0 and j >= 1 and j <= i and length >= 1 + i; lbl_7_1[i, j, length, temp, test, tmp] : length >= 1 + i and j >= 0 and test >= 0 and j <= -1 + i } (0.17s), OK.
• With ISL: { lbl_5_3[i__1, j__1, length__1, temp__1, test__1, -1 + j__1] : (length__1 >= 3 and j__1 <= i__1 and j__1 >= 1 and test__1 <= 1 and test__1 >= 0 and test__1 >= 3 + i__1 - length__1) or (length__1 >= 2 and length__1 >= 3 + i__1 and j__1 <= i__1 and test__1 <= 1 and test__1 >= 0 and j__1 >= 1); lbl_5_3[i__1, 1, 1 + i__1, temp__1, 1, 0] : i__1 >= 1; lbl_5_3[i__1, j__1, 2 + i__1, temp__1, test__1, -1 + j__1] : i__1 >= 1 and j__1 >= 1 and j__1 <= i__1 and test__1 >= 0 and test__1 <= 1; lbl_5_3[i__1, j__1, 1 + i__1, temp__1, 1, -1 + j__1] : (i__1 >= 1 and j__1 <= i__1 and j__1 >= 2) or (i__1 >= 1 and j__1 >= 2 and j__1 <= i__1); lbl_5_3[i__1, 1, 1 + i__1, temp__1, 0, 0] : i__1 >= 1; lbl_5_3[i__1, j__1, 2 + i__1, temp__1, 0, -1 + j__1] : i__1 >= 1 and j__1 >= 1 and j__1 <= i__1; lbl_5_3[i__1, j__1, 1 + i__1, temp__1, 0, -1 + j__1] : i__1 >= 1 and j__1 >= 2 and j__1 <= i__1; stop[i__1, j__1, 1 + i__1, temp__1, test__1, tmp__1] : i__1 <= 0; stop[i__1, i__1, length__1, temp__1, 0, -1 + i__1] : (length__1 >= 3 and length__1 >= 3 + i__1 and i__1 >= 1) or (length__1 >= 2 and length__1 >= 3 + i__1 and i__1 >= 1); stop[i__1, i__1, 1 + i__1, temp__1, 0, -1 + i__1] : i__1 >= 2; stop[0, 1, length__1, temp__1, 1, 0] : length__1 >= 3 or length__1 >= 3; stop[0, 1, 2, temp__1, 1, 0]; stop[i__1, i__1, 2 + i__1, temp__1, 0, -1 + i__1] : i__1 >= 1 or i__1 >= 1; stop[1, 1, 2, temp__1, 0, 0]; start[i, j, length, temp, test, tmp]; lbl_7_1[i__1, j__1, length__1, temp__1, test__1, -1 + j__1] : (length__1 >= 3 and test__1 <= 1 and test__1 >= 0 and j__1 >= 1 and length__1 >= 2 + i__1 and j__1 <= -1 + i__1) or (length__1 >= 2 and length__1 >= 2 + i__1 and j__1 <= -1 + i__1 and test__1 <= 1 and test__1 >= 0 and j__1 >= 1); lbl_7_1[i__1, j__1, 1 + i__1, temp__1, 0, -1 + j__1] : i__1 >= 1 and j__1 >= 2 and j__1 <= -1 + i__1; lbl_7_1[i__1, 0, length__1, temp__1, 0, i__1] : (length__1 >= 3 and i__1 >= 1 and length__1 >= 2 + i__1) or (length__1 >= 2 and i__1 >= 1 and length__1 >= 3 + i__1); lbl_7_1[i__1, 0, 2 + i__1, temp__1, 0, i__1] : i__1 >= 1; lbl_7_1[i__1, 0, 1 + i__1, temp__1, 0, tmp__1] : i__1 >= 1; lbl_7_1[i__1, j__1, 1 + i__1, temp__1, 1, -1 + j__1] : (i__1 >= 1 and j__1 <= -1 + i__1 and j__1 >= 2) or (i__1 >= 1 and j__1 >= 1 and j__1 <= -1 + i__1); lbl_7_1[i__1, 1, 1 + i__1, temp__1, 0, 0] : i__1 >= 2; lbl_1_3[i__1, 1 + i__1, length__1, temp__1, 1, i__1] : (length__1 >= 3 and i__1 >= 0 and length__1 >= 3 + i__1) or (length__1 >= 2 and i__1 >= 0 and length__1 >= 3 + i__1); lbl_1_3[0, 1, 2, temp__1, 1, 0]; lbl_1_3[i__1, 1 + i__1, 2 + i__1, temp__1, 1, i__1] : i__1 >= 1 or i__1 >= 1 } (0.61s), OK.