// ------------------------------------------------------------------ // Ultimate Tic-Tac-Toe // https://en.wikipedia.org/wiki/Ultimate_tic-tac-toe // ------------------------------------------------------------------ // the various dimensions val N = 3; // the size of each board val N2 = N⋅N; // the number of positions on it val M = N2⋅N2; // the maximum number of moves required // a player type Player = ℕ[2]; val none:Player = 0; val first:Player = 1; val second:Player = 2; // choices of global/local position type Choice = Record[global:ℕ[N2-1],local:ℕ[N2-1]]; type Local = Array[N2,Player]; // a local board type Board = Array[N2,Local]; // a global board // initial values val linit:Local = Array[N2,Player](0); val binit:Board = Array[N2,Local](linit); val cinit:Choice = ⟨global:0,local:0⟩; // ------------------------------------------------------------------ // the core predicates // ------------------------------------------------------------------ // does player p win board b? pred wins(b:Board,p:Player) requires p ≠ none; // sample solution: 4 lines using another predicate // whose definition also requires 4 lines ⇔ ⊥ ; // is choice c0 legal for board b and previous choice c? pred legal(b:Board, c:Choice, c0:Choice) ⇔ // sample solution: 4 lines ⊥ ; // ------------------------------------------------------------------ // play the game // ------------------------------------------------------------------ // compute next state of board b for choice c of player p fun next(b:Board, p:Player, c:Choice):Board = b with [c.global] = (b[c.global] with [c.local] = p); // play the game proc play(): Player { var board:Board = binit; var winner: Player = none; var player: Player = first; var choice: Choice = cinit; var choices:Array[M,Choice] = Array[M,Choice](choice); var blocked:Bool = ⊥; var i:ℕ[M] = 0; while winner = none ∧ ¬blocked ∧ i < M do { choose choice0:Choice with legal(board,choice,choice0) then { board ≔ next(board,player,choice0); if wins(board,player) then winner ≔ player; player ≔ if player = first then second else first; choice ≔ choice0; choices[i] ≔ choice; i ≔ i+1; } else blocked ≔ ⊤; } if winner ≠ none then print ⟨winner,i,choices⟩; return winner; } // ------------------------------------------------------------------ // end of file // ------------------------------------------------------------------