« Model gopan_reps :: Contents :: Model gopan_reps_alt2 »

Model gopan_reps_alt1¶

Cited in: [GopanR06] fig. 3a p. 5, [GopanR07] fig. 2 p. 5.

Tag: fixpoint.

Figure¶

../_images/gopan_reps_alt1.png

Source code¶

model gopan_cav06_05a {

  var x, y;

  states n1, n2, n4, n5, n6;

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

  transition t2 := {
    from   := n2;
    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;
  };

}

strategy gopan_cav06_05a_s {

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

}

Expected invariant¶

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

Results¶

With Aspic: { n2[0, 0]; n1[0, 0]; n5[0, 1]; n4[0, 1]; n6[1, 1] } (0.05s), OK.
With ISL: { n6[1, 1]; n2[0, 0]; n5[0, 1]; n1[0, 0]; n4[0, 1] } (0.00s), OK.

« Model gopan_reps :: Contents :: Model gopan_reps_alt2 »