Figure¶

Source code¶

model beyer_henzinger_majumdar_rybalchenko_pldi07_03 {

  var n, i, a, b;

  states q1, q4, q2, q3;

  transition t5 := {
    from   := q1;
    to     := q4;
    guard  := i >= n;
    action := ;
  };

  transition t1 := {
    from   := q1;
    to     := q2;
    guard  := i < n;
    action := ;
  };

  transition t3 := {
    from   := q2;
    to     := q3;
    guard  := true;
    action := a' = a + 2, b' = b + 1;
  };

  transition t2 := {
    from   := q2;
    to     := q3;
    guard  := true;
    action := a' = a + 1, b' = b + 2;
  };

  transition t4 := {
    from   := q3;
    to     := q1;
    guard  := true;
    action := i' = i + 1;
  };

}

strategy beyer_henzinger_majumdar_rybalchenko_pldi07_03_s {

  Region init := {state = q1 && n >= 0 && i = 0 && a = 0 && b = 0};

}

Expected invariant¶

{ q4[v1, v2, v3, 3v1 - v3] }

Results¶

• With Aspic: { q2[n, i, a, 3i - a] : a >= i and a <= 2i and i <= -1 + n; q3[n, i, a, 3 + 3i - a] : i >= 0 and a >= 1 + i and a <= 2 + 2i and i <= -1 + n; q1[n, i, a, 3i - a] : a <= 2i and a >= i and n >= 0 and i <= n; q4[n, n, a, 3n - a] : n >= 0 and a <= 2n and a >= n } (0.06s), OK.
• With ISL: { q2[n__1, i__1, a__1, 3i__1 - a__1] : n__1 >= 0 and a__1 >= i__1 and i__1 <= -1 + n__1 and a__1 <= 2i__1; q4[n__1, n__1, a__1, 3n__1 - a__1] : n__1 >= 1 and a__1 <= -1 + 2n__1 and a__1 >= 1 + n__1; q4[n__1, n__1, n__1, 2n__1] : n__1 >= 1; q4[n__1, n__1, 2n__1, n__1] : n__1 >= 1; q4[0, 0, 0, 0]; q3[n__1, i__1, a__1, 3 + 3i__1 - a__1] : (n__1 >= 0 and a__1 >= 1 + i__1 and i__1 <= -1 + n__1 and a__1 <= 1 + 2i__1) or (n__1 >= 0 and a__1 >= 3 + i__1 and i__1 <= -1 + n__1 and a__1 <= 2 + 2i__1); q3[n__1, 0, 2, 1] : n__1 >= 1; q1[n__1, i__1, a__1, 3i__1 - a__1] : n__1 >= 1 and i__1 <= n__1 and a__1 >= 1 - n__1 + 2i__1 and a__1 <= -1 + 2i__1 and a__1 >= 1 + i__1; q1[n__1, i__1, i__1, 2i__1] : n__1 >= 1 and i__1 >= 1 and i__1 <= n__1; q1[n__1, i__1, 2i__1, i__1] : n__1 >= 1 and i__1 >= 1 and i__1 <= n__1; q1[n, 0, 0, 0] : n >= 0 } (0.22s), OK.