ALICe documentation

Model gopan_reps

«  Model gonnord6   ::   Contents   ::   Model gopan_reps_alt1  »

Model gopan_reps

Cited in: [GopanR06] fig. 1 p. 3, [GopanR07] fig. 1 p. 4, [GulwaniJK09] fig. 10b p. 10, [GulwaniZ10] fig. 9 p. 12.

Tag: fixpoint.

Figure

../_images/gopan_reps.png

Source code

model gopan_cav06_03 {

  var x, y;

  states n1, n3, n4, n5, n6, n_x, 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 t5 := {
    from   := n4;
    to     := n_x;
    guard  := y <= -1;
    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_03_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; n_x[x, -1] : x >= 51 } (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; n3[x__1, 102 - x__1] : x__1 <= 102 and x__1 >= 52; n3[51, 51]; n_x[102, -1]; 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]; 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]; 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] } (0.05s), OK.

«  Model gonnord6   ::   Contents   ::   Model gopan_reps_alt1  »