Figure¶

Source code¶

model popeea_chin_asian06_02 {

  var x, l, upd, N;

  states q1, q4, q2, q3;

  transition t5 := {
    from   := q1;
    to     := q4;
    guard  := x >= N;
    action := ;
  };

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

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

  transition t2 := {
    from   := q2;
    to     := q3;
    guard  := true;
    action := l' = x, upd' = 1;
  };

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

}

strategy popeea_chin_asian06_02_s {

  Region init := {state = q1 && x = 0 && upd = 0};

}

Expected invariant¶

{ q4[v1, v2, v3, v4] : v3 <= 0 or v3 >= 2; q4[v1, v2, 1, v4] : v2 >= 0 and v4 >= 1 + v2 }

Results¶

• With Aspic: { q2[x, l, upd, N] : upd >= 0 and upd <= x and N >= 1 + x; q3[x, l, upd, N] : N >= 1 + x and upd >= 0 and upd <= 1 + x and x >= 0; q1[x, l, upd, N] : upd >= 0 and upd <= x; q4[x, l, upd, N] : N <= x and upd >= 0 and upd <= x } (0.05s), failed.
• With ISL: { q2[x__1, l__1, upd__1, N__1] : x__1 >= 1 and N__1 >= 1 + x__1; q2[0, l__1, 0, N__1] : N__1 >= 1; q4[x__1, l__1, upd__1, x__1] : x__1 >= 1; q4[x__1, l__1, 0, x__1] : x__1 >= 1; q4[0, l__1, 0, N__1] : N__1 <= 0; q3[x__1, l__1, upd__1, N__1] : x__1 >= 1 and N__1 >= 1 + x__1; q3[0, l__1, 0, N__1] : N__1 >= 1; q3[0, 0, 1, N__1] : N__1 >= 1; q1[x__1, l__1, upd__1, N__1] : N__1 >= 1 and N__1 >= x__1 and x__1 >= 1; q1[x__1, l__1, 0, N__1] : N__1 >= 1 and N__1 >= x__1 and x__1 >= 1; q1[0, l, 0, N] } (0.02s), failed.