Figure¶

Source code¶

model gulwani_mehra_chilimbi_popl09_06f {

  var x0, y0, x, y, n, m, c1, c2;

  states q1, q2;

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

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

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

}

strategy gulwani_mehra_chilimbi_popl09_06f_s {

  Region init := {state = q1 && x = x0 && y = y0 && 0 <= x0 && x0 <= n && 0 <= y0 && y0 <= m && c1 = 0 && c2 = 0 && n >= 0 && m >= 0};

}

Expected invariant¶

{ q1[v1, v2, v3, v4, v5, v6, v7, v8] : v8 <= -v1 - v2 + v5 + v6 - v7; q2[v1, v2, v3, v4, v5, v6, v7, v8] : v8 <= -v1 - v2 + v5 + v6 - v7 }

Results¶

• With Aspic: { q1[x0, y0, x, y, n, m, -y0 + y, -x0 + x] : x >= x0 and n >= x0 and n >= x and m >= y0 and m >= x0 - x + y and y >= y0 and y0 >= 0 and x0 >= 0 and m >= y; q2[x0, y0, x, y, n, m, -y0 + y, -x0 + x] : x >= x0 and y >= y0 and m >= y and m >= y0 and y0 >= 0 and x0 >= 0 and n >= 1 + x } (0.05s), OK.
• With ISL: { q1[x0__1, y0__1, x__1, y__1, n__1, m__1, -y0__1 + y__1, -x0__1 + x__1] : (x0__1 >= 0 and n__1 >= 1 + x0__1 and y0__1 >= 0 and m__1 >= 1 + y0__1 and n__1 >= 0 and m__1 >= 0 and x__1 >= 1 + x0__1 and y__1 >= -x0__1 + y0__1 + x__1 and n__1 >= x__1 and m__1 >= y__1) or (x0__1 >= 0 and n__1 >= x0__1 and y0__1 >= 0 and m__1 >= y0__1 and n__1 >= 0 and m__1 >= 0 and n__1 >= x__1 and y__1 >= 1 + y0__1 and x__1 >= 2 + x0__1 and m__1 >= y__1); q1[x0, y0, x0, y0, n, m, 0, 0] : x0 >= 0 and n >= x0 and y0 >= 0 and m >= y0 and n >= 0 and m >= 0; q1[x0__1, y0__1, x__1, y0__1, n__1, m__1, 0, -x0__1 + x__1] : x0__1 >= 0 and n__1 >= 1 + x0__1 and y0__1 >= 0 and m__1 >= y0__1 and n__1 >= 0 and m__1 >= 0 and x__1 >= 1 + x0__1 and n__1 >= x__1; q2[x0__1, y0__1, x__1, y__1, n__1, m__1, -y0__1 + y__1, -x0__1 + x__1] : x0__1 >= 0 and n__1 >= x0__1 and y0__1 >= 0 and m__1 >= y0__1 and n__1 >= 0 and m__1 >= 0 and y__1 >= 1 + y0__1 and n__1 >= 1 + x__1 and x__1 >= x0__1 and m__1 >= y__1; q2[x0__1, y0__1, x__1, y0__1, n__1, m__1, 0, -x0__1 + x__1] : x0__1 >= 0 and n__1 >= x0__1 and y0__1 >= 0 and m__1 >= y0__1 and n__1 >= 0 and m__1 >= 0 and x__1 >= x0__1 and n__1 >= 1 + x__1 } (0.12s), OK.