Figure¶

Source code¶

model gulwani_zuleger_pldi10_04b {

  var flag, n, n0, i;

  states q1, q2;

  transition t1 := {
    from   := q1;
    to     := q2;
    guard  := flag = 1;
    action := flag' = 0, i' = i + 1;
  };

  transition t3 := {
    from   := q2;
    to     := q1;
    guard  := true;
    action := ;
  };

  transition t2 := {
    from   := q2;
    to     := q2;
    guard  := n > 0;
    action := n' = n - 1, flag' = 1;
  };

}

strategy gulwani_zuleger_pldi10_04b_s {

  Region init := {state = q1 && n >= 0 && n = n0 && flag = 1 && i = 0};

}

Expected invariant¶

{ q2[v1, v2, v3, v4] : v4 <= 1 + v3; q1[v1, v2, v3, v4] : v4 <= 1 + v3 }

Results¶

• With Aspic: { q2[flag, n, n0, 1 - flag - n + n0] : n0 >= 0 and n >= 0 and flag >= 0 and n0 >= flag + n; q1[flag, n, n0, 1 - flag - n + n0] : n >= 0 and n0 >= -1 + flag + n and n0 >= -1 + flag and n0 >= n and n0 >= 0 } (0.04s), failed.
• With ISL: { q2[flag__1, n__1, n0__1, i__1] : n0__1 >= 0 and i__1 >= 2 - flag__1 and n0__1 >= 1 + n__1 and flag__1 <= 1 and flag__1 >= 0 and n__1 >= 0; q2[0, n__1, n0__1, i__1] : n0__1 >= 1 and i__1 >= 1 and n0__1 >= 1 + n__1; q2[0, n__1, n__1, 1] : n__1 >= 0; q1[1, n__1, n0__1, i__1] : n0__1 >= 0 and i__1 >= 1 and n__1 >= 0 and n0__1 >= 1 + n__1; q1[0, n__1, n0__1, i__1] : n0__1 >= 1 and i__1 >= 1 and n0__1 >= 1 + n__1; q1[0, n__1, n__1, 1] : n__1 >= 0; q1[1, n, n, 0] : n >= 0 } (0.23s), failed.