diff --git a/TicTacToe/tictactoe_v2.tla b/TicTacToe/tictactoe_v2.tla index 7b7760bdc66c05fe1f9ab75b6a418c7b62797bed..f45be8782acd7a04e0bff52eca3c9a2d3a50880e 100644 --- a/TicTacToe/tictactoe_v2.tla +++ b/TicTacToe/tictactoe_v2.tla @@ -94,7 +94,7 @@ GOAL == Won("O") \* the following Invariant is violated by this model INVARIANT == ~Won("O") \/ ~Won("X") \* additions for ProB so that we can apply MCTS auto play: -GAME_MCTS_RUNS == 100 +GAME_MCTS_RUNS == 400 GAME_PLAYER == IF nextTurn = "X" THEN "max" ELSE "min" GAME_OVER == IF Won("X") \/ Won("O") THEN TRUE ELSE FALSE GAME_VALUE == IF Won("X") THEN 1 ELSE 0