model gulwani_jain_koskinen_pldi09_05b {

  var i, j, m, n, c;

  states q;

  transition t2 := {
    from   := q;
    to     := q;
    guard  := i < n && j >= m;
    action := j' = 0, i' = i + 1, c' = c + 1;
  };

  transition t1 := {
    from   := q;
    to     := q;
    guard  := i < n && j < m;
    action := j' = j + 1, c' = c + 1;
  };

}

strategy gulwani_jain_koskinen_pldi09_05b_s {

  Region init := {state = q && 0 < m && m < n && i = 0 && j = 0 && c = 0};

}