model gonnord_thesis_096a {

  var s, t, d;

  states q;

  transition t2 := {
    from   := q;
    to     := q;
    guard  := true;
    action := s' = 0, t' = t + 1;
  };

  transition t1 := {
    from   := q;
    to     := q;
    guard  := s <= 3;
    action := d' = d + 1, s' = s + 1;
  };

}

strategy gonnord_thesis_096a_s {

  Region init := {state = q && s = 0 && t = 0 && d = 0};

}

{ q[v1, v2, v3] : v2 >= 0 and v1 >= 0 and v1 <= 4 and v3 >= 0 and v3 <= v1 + 4v2 }