val N:ℕ;
type int = ℤ[-1,N];
 
shared system Counter
{
  var x:int = 0; var y:int = 0;
  invariant 0 ≤ x ∧ x < N ∧ 0 ≤ y ∧ y < N;
  ltl □ 〚 0 <= x ∧ x < N ∧ 0 ≤ y ∧ y < N 〛;
  ltl[fairness] (◇〚 x ≥ 1 〛) ∧ (◇〚 y ≥ 1 〛); 
  action incX() fairness weak;
  { x = if x < N-1 then x+1 else 0; }
  action incY() fairness weak;
  { y = if y < N-1 then y+1 else 0; }
}