Announcements

I was notified that there is some problem with the "winning condition" in the file I handed out. After some inspection, I've indeed identified/corrected the following errors:

• The invariant should actually state that the other (prevously selected) player has won the game:

  invariant let player = other(player) in wins(board, player) ⇒ ...

• Also the action should not be allowed any more if the other player has already won the game:

  action play(choice0:Choice) with 
    ¬wins(board, other(player)) ∧ legal(board, choice, choice0);
  {
    board[choice0.global][choice0.local] = player;
    player := other(player);
    choice := choice0;
  }

The definition of the new function "other" is:

// the other player
fun other(player:Player):Player 
  requires player ≠ none;
= if player = first then second else first;

Thank you for pointing out the problem; I've uploaded a new version of "UltimateTicTacToe.txt" in the assignment.