model ack {

  var m, n;

  states start, cont1, a, b, stop3, stop2, stop1;

  transition t0bis := {
    from   := start;
    to     := cont1;
    guard  := m > 0;
    action := ;
  };

  transition t0 := {
    from   := start;
    to     := stop1;
    guard  := m <= 0;
    action := ;
  };

  transition t2 := {
    from   := cont1;
    to     := a;
    guard  := n > 0;
    action := n' = n - 1;
  };

  transition t1 := {
    from   := cont1;
    to     := stop2;
    guard  := n <= 0;
    action := m' = m - 1, n' = 1;
  };

  transition t3 := {
    from   := a;
    to     := b;
    guard  := true;
    action := m' = m - 1, n' = ?;
  };

  transition t4bis := {
    from   := b;
    to     := stop3;
    guard  := n < 0;
    action := ;
  };

  transition t4 := {
    from   := b;
    to     := start;
    guard  := n >= 0;
    action := ;
  };

}

strategy ack_s {

  Region init := {state = start && n >= 0 && m >= 0};

}

{ b[v1, v2] : v1 >= 0; stop1[0, v2] : v2 >= 0; cont1[v1, v2] : v1 >= 1 and v2 >= 0; start[v1, v2] : v1 >= 0 and v2 >= 0; a[v1, v2] : v2 >= 0 and v1 >= 1; stop2[v1, 1] : v1 >= 0; stop3[v1, v2] : v2 <= -1 and v1 >= 0 }