Figure¶

Source code¶

model gopan_cav06_05b {

  var x, y;

  states n1, n3, n4, n5, n6, n2;

  transition t3 := {
    from   := n1;
    to     := n3;
    guard  := x >= 51;
    action := ;
  };

  transition t1 := {
    from   := n1;
    to     := n2;
    guard  := x <= 50;
    action := ;
  };

  transition t4 := {
    from   := n3;
    to     := n4;
    guard  := true;
    action := y' = y - 1;
  };

  transition t6 := {
    from   := n4;
    to     := n5;
    guard  := y >= 0;
    action := ;
  };

  transition t7 := {
    from   := n5;
    to     := n6;
    guard  := true;
    action := x' = x + 1;
  };

  transition t8 := {
    from   := n6;
    to     := n1;
    guard  := true;
    action := ;
  };

  transition t2 := {
    from   := n2;
    to     := n4;
    guard  := true;
    action := y' = y + 1;
  };

}

strategy gopan_cav06_05b_s {

  Region init := {state = n1 && x = 0 && y = 0};

}

Expected invariant¶

{ n1[v1, v2] : v2 >= 0 and v2 <= v1 }

Results¶

• With Aspic: { n2[x, y] : y <= x and y >= 0 and x <= 50; n1[x, y] : y >= 0 and y <= x; n5[x, y] : y >= 0 and y <= 1 + x and 51y >= 51 - 2x; n3[x, y] : y >= 0 and y <= x and x >= 51; n4[x, y] : 51y >= 51 - 2x and y <= 1 + x and y >= -1; n6[x, y] : y >= 0 and y <= x and 51y >= 53 - 2x } (0.05s), OK.
• With ISL: { n6[x__1, 102 - x__1] : x__1 <= 102 and x__1 >= 52; n6[x__1, x__1] : x__1 <= 51 and x__1 >= 1; n1[x__1, 102 - x__1] : x__1 <= 102 and x__1 >= 52; n1[x__1, x__1] : x__1 <= 51 and x__1 >= 1; n1[0, 0]; n2[x__1, x__1] : x__1 <= 50 and x__1 >= 1; n2[0, 0]; n5[x__1, 101 - x__1] : x__1 <= 101 and x__1 >= 52; n5[x__1, 1 + x__1] : x__1 <= 50 and x__1 >= 0; n5[51, 50]; n3[x__1, 102 - x__1] : x__1 <= 102 and x__1 >= 52; n3[51, 51]; n4[x__1, 101 - x__1] : x__1 <= 102 and x__1 >= 51; n4[x__1, 1 + x__1] : x__1 <= 50 and x__1 >= 1; n4[0, 1] } (0.05s), OK.