// ------------------------------------------------------------------
// 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 b win local board b?
pred winsLocal(b:Local, p:Player) 
  requires p ≠ none;
⇔ // sample solution: 4 lines
  ⊥
;

// does player p win global board b?
pred wins(b:Board, p:Player) 
  requires p ≠ none;
⇔ // sample solution: 4 lines 
  ⊥
;

// is choice c0 legal for board b and previous choice c?
pred legal(b:Board, c:Choice, c0:Choice) ⇔ 
  // sample solution: 5 lines
  ⊥
;

// ------------------------------------------------------------------
// play the game
// ------------------------------------------------------------------

// set to true to print all winning games
val all = false;

// if "all" is true, set "trace" to true to print trace to winning situation
val trace = true;

shared system UltimateTicTacToe
{
  var board: Board = binit;
  var player: Player = first;
  var choice: Choice = cinit;

  // prints winning situation
  invariant wins(board, player) => 
    print "******************************************************************" in
    print "WINNER: player {1} wins with board {2}", player, board in 
    print "*****************************************************************" in
    if ¬trace then all else printtrace in all;

  action play(choice0:Choice) with legal(board, choice, choice0);
  {
    board[choice0.global][choice0.local] = player;
    if player = first then player := second; else player := first;
    choice := choice0;
  }
}

// ------------------------------------------------------------------
// end of file
// ------------------------------------------------------------------