Next2 ==
/\ turn' = turn + 1 \* A
/\ current' = Opponent \* B
/\ ∃i,j∈1..N: \* C
/\board[i,j] = Empty \* C.1
/\ board'[i,j] = current \* C.2
For `Next2` to be true, the square [i, j] has to be empty AND in the following state, that same square must have whichever mark was `current` in it. Since `current` switches between the two each step of the behavior, this forces each player to wait until their turn comes around.
Comments
In the TicTacToe spec, we have
For `Next2` to be true, the square [i, j] has to be empty AND in the following state, that same square must have whichever mark was `current` in it. Since `current` switches between the two each step of the behavior, this forces each player to wait until their turn comes around.