model determinant {

  var i, j, k, n;

  states start, a, d, halt, b, c;

  transition t0 := {
    from   := start;
    to     := a;
    guard  := n >= 1;
    action := ;
  };

  transition t1 := {
    from   := a;
    to     := d;
    guard  := true;
    action := k' = 1;
  };

  transition t3 := {
    from   := d;
    to     := halt;
    guard  := k >= n;
    action := i' = i;
  };

  transition t2 := {
    from   := d;
    to     := b;
    guard  := k < n;
    action := i' = k + 1;
  };

  transition t5 := {
    from   := b;
    to     := c;
    guard  := i <= n;
    action := j' = n;
  };

  transition t4 := {
    from   := b;
    to     := d;
    guard  := i > n;
    action := k' = k + 1;
  };

  transition t7 := {
    from   := c;
    to     := b;
    guard  := j <= k;
    action := i' = i + 1;
  };

  transition t6 := {
    from   := c;
    to     := c;
    guard  := j > k;
    action := j' = j - 1;
  };

}

strategy determinant_s {

  Region init := {state = start};

}

{ d[v1, v2, v3, v4] : v4 >= v3 and v3 >= 1; a[v1, v2, v3, v4] : v4 >= 1; halt[v1, v2, v3, v3] : v3 >= 1; b[v1, v2, v3, v4] : v4 >= -1 + v1 and v3 <= -1 + v1 and v4 >= 1 + v3 and v3 >= 1; c[v1, v2, v3, v4] : v4 >= v1 and v4 >= v2 and v3 >= 1 and v3 <= v2 and v3 <= -1 + v1 }