module tictactoe
open std/ord


// Player can be either X, or O
sig Content {}
static part sig X, O, Nobody extends Content {}

sig Idx {}

sig Board {
	contents : Idx->Idx->Content,
	// OSquares is the set of Squares which has a O type of Player
	oSquares: Idx->Idx,
	// XSquares is the set of Squares which has a X type of Player 
	xSquares: Idx->Idx
}{
	// for everyboard, the square in oSquares should be shown in contents for some r and c and its element should be OSquare = Idx.Idx.(this.contents)
	all r,c:Idx | r->c in oSquares <=> contents[r][c] = O
	// for everyboard, the square in xSquares should be shown in contents for some r and c and its element should be X
	all r,c:Idx | r->c in xSquares <=> contents[r][c] = X  	
}


// this function is a helper function to visualize board contents - used during testing
fun boardContent () {
	Board = univ [Board]
}

// Make sure that it's possible to generate at least 10 boards.
run boardContent for 3 Idx, 3 Content, 10 Board


fun Same (b1,b2:Board) {
  all r,c:Idx | b1.contents[r][c] = b2.contents[r][c]
}

assert Reflexive { all b : Board | Same(b,b) }
assert Commutative { all b,b2 : Board | Same(b,b2) <=> Same(b2,b) }
assert Transitive { all b,b2,b3: Board | Same(b,b2) && Same(b2,b3) => Same(b,b3) }

check Reflexive for 5 Board, 3 Idx, 3 Content
check Commutative for 5 Board, 3 Idx, 3 Content
check Transitive for 5 Board, 3 Idx, 3 Content


// this function is evaluated true when the number of X and the number of O differ by 1
// this function prevents empty relations of contents, oSquares, xSquares
fun isLegal (b:Board) {
	noTwoWinner(b) &&
	#(b.oSquares) > 0 &&
	#(b.xSquares) > 0 &&
	(
		#(b.oSquares) = (#(b.xSquares) + 1 ) || 
		#(b.xSquares) = (#(b.oSquares) + 1 ) ||
		#(b.xSquares) =  #(b.oSquares)
	)
}

// this function is evaluated true if boardContPent b has tictactoe of a Player e 
fun tictactoe (b:Board, e:Content) {
	(some r:Idx | all c:Idx | b.contents[r][c] = e ) || 
	(some c:Idx | all r:Idx | b.contents[r][c] = e ) ||
	(all  r:Idx | some c:Idx | #OrdPrevs(r) = #OrdPrevs(c) && b.contents[r][c] =e) ||
	(all  r:Idx | some c:Idx | #OrdPrevs(r) = #OrdNexts(c) && b.contents[r][c] =e) 	

}
// this function is evaluated as true if the board does not have two winners
fun noTwoWinner (b:Board) {
	( tictactoe(b,O) => !tictactoe(b,X) )&&
	( tictactoe(b,X) => !tictactoe(b,O) ) 	
}
// this function is evaluated as true if x wins tictactoe on a legal board
fun xWins (b:Board) { 
	wins(b,X) 
}

// this function is evaluated as true is o wins tictactoe on a legal board 
fun oWins (b:Board) {
	wins(b,O) 
}

// this function is a helper function used for xWins and oWins 
fun wins(b:Board, w:Content) {
	isLegal (b) && tictactoe (b, w) && !tictactoe(b,Content-Nobody-w) 
}
// this function is evaluated as true when the boardcontent does not have tictactoe of any kind
fun isTie(b:Board) {
	isLegal (b) && !tictactoe (b,O) && !tictactoe(b,X)
}
// ********************************************************************************************************** /
//these test functions force boardcontents to be different from each other 
fun findIlegalBoards() {
	some disj b1, b2, b3:Board | 
	!Same(b1,b2) && !Same(b2,b3) && !Same(b1,b3) &&
	!isLegal(b1)&& !isLegal(b2) && !isLegal(b3) 
}
fun findXWinningBoards () {
	some disj b1, b2, b3, b4: Board | 
	!Same(b1,b2) && !Same(b1,b3) && !Same(b1,b4) && !Same(b2,b3) && !Same(b2,b4) && !Same(b3,b4) &&
	xWins(b1) && xWins(b2) && xWins(b3) && xWins(b4)
}
fun findTieBoards () {
	some disj b1, b2, b3:Board | 
	!Same(b1,b2) && !Same(b2,b3) && !Same(b1,b3) &&
	isTie(b1) && isTie(b2) && isTie(b3) 
}
run findIlegalBoards for 3 Idx, 3 Content, 3 Board
run findXWinningBoards for 3 Idx, 3 Content, 4 Board
run findTieBoards for 3 Idx, 3 Content, 3 Board