« Model jeannet6 :: Contents :: Model loops »

Model leeyannakis_bad¶

Cited in: [GulavaniHKNR06] fig. 6 p. 7.

Tag: termination.

Figure¶

../_images/leeyannakis_bad.png

Source code¶

model gulavani_henzinger_kannan_nori_rajamani_sigsoft06_07 {

  var y;

  states q;

  transition t := {
    from   := q;
    to     := q;
    guard  := y > 0;
    action := y' = y - 1;
  };

}

strategy gulavani_henzinger_kannan_nori_rajamani_sigsoft06_07_s {

  Region init := {state = q};

}

Expected invariant¶

{  }

Results¶

With Aspic: { q[y] } (0.06s), OK.
With ISL: { q[y] } (0.00s), OK.

« Model jeannet6 :: Contents :: Model loops »