Figure¶

Source code¶

model gulwani_cav09_06 {

  var x, y, n, i1, i2;

  states q1, q2;

  transition t1 := {
    from   := q1;
    to     := q2;
    guard  := x < n;
    action := i1' = i1 + 1, y' = x;
  };

  transition t3 := {
    from   := q2;
    to     := q1;
    guard  := true;
    action := x' = y + 1;
  };

  transition t2 := {
    from   := q2;
    to     := q2;
    guard  := y < n;
    action := i2' = i2 + 1, y' = y + 1;
  };

}

strategy gulwani_cav09_06_s {

  Region init := {state = q1 && n >= 0 && x = 0 && i1 = 0 && i2 = 0};

}

Expected invariant¶

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

Results¶

• With Aspic: { q2[x, y, n, i1, 1 + y - i1] : n >= 1 + x and y >= x and i1 >= 1 and i1 <= 1 + x and n >= y; q1[x, y, n, i1, x - i1] : i1 <= x and i1 >= 0 and i1 <= n and i1 >= x - n and n >= 0 and 2i1 >= x - n } (0.06s), OK.
• With ISL: { q1[x__1, -1 + x__1, n__1, i1__1, x__1 - i1__1] : n__1 >= 0 and i1__1 >= 2 and i1__1 <= x__1 and n__1 >= -1 + x__1; q1[0, y, n, 0, 0] : n >= 0; q1[x__1, -1 + x__1, n__1, 1, -1 + x__1] : n__1 >= 0 and n__1 >= -1 + x__1 and x__1 >= 2; q1[1, 0, n__1, 1, 0] : n__1 >= 1; q2[x__1, y__1, n__1, i1__1, 1 + y__1 - i1__1] : n__1 >= 0 and i1__1 >= 2 and i1__1 <= 1 + y__1 and n__1 >= y__1; q2[0, y__1, n__1, 1, y__1] : n__1 >= 0 and n__1 >= y__1 and y__1 >= 1; q2[0, 0, n__1, 1, 0] : n__1 >= 1 } (0.04s), OK.