Monte Carlo Tree Search Game Play - Revision history

Michael Leuschel at 09:01, 3 December 2024

2024-12-03T09:01:22Z

← Older revision		Revision as of 09:01, 3 December 2024
Line 45:		Line 45:
	You can also trigger MCTS play in VisB.		You can also trigger MCTS play in VisB.
	Here MCTS_AUTO_PLAY is available as special event name.		Here MCTS_AUTO_PLAY is available as special event name.


			=== MCTS Game Play for XTL Files ===

			You can also use MCTS game play for XTL specifications, i.e., where you use Prolog facts start, trans and prop to define a system. The MCTS definitions should be provided as <tt>prob_game_info/3</tt> facts.
			Below is a small example of Nim using an XTL specification:

			<pre>
			% a version of Nim using ProB's new MCTS API

			% definitions for the XTL interface
			start(pos(max,9)). % e.g., we start with 9 sticks
			trans(Act,S1,S2) :- move(S1,Act,S2).
			prop(S,'='(sticks,V)) :- S=pos(_,V).
			prop(S,'='(utility,V)) :- utility(S,V).
			prop(S,'='(player,V)) :- player(S,V).

			% Game rules proper:

			% a player can either remove 1 or 2 sticks
			move(pos(P1,M),take1,pos(P2,M1)) :- M>0, M1 is M-1, other_player(P1,P2).
			move(pos(P1,M),take2,pos(P2,M1)) :- M>1, M1 is M-2, other_player(P1,P2).

			end(pos(_,X)) :- X<1. % the game is over when no sticks are left

			utility(pos(max,_),1). % other player took last stick; we won
			utility(pos(min,_),-1). % max lost

			player(pos(P,_),P).


			% definitions for the MCTS API:
			prob_game_info('GAME_PLAYER',S,V) :- player(S,V).
			prob_game_info('GAME_VALUE',S,V) :- utility(S,V).
			prob_game_info('GAME_OVER',S,V) :- (end(S) -> V=true ; V=false).
			prob_game_info('GAME_MCTS_RUNS',_,V) :- V=100.

			</pre>

Michael Leuschel at 14:57, 6 January 2024

2024-01-06T14:57:31Z

← Older revision		Revision as of 14:57, 6 January 2024
Line 38:		Line 38:


	MCTS tree can be visualised graphically.		MCTS Auto Game Play command is available in ProB Tcl/Tk by right-clicking in the operations view.
	~~MCTS commands are available~~ by right-clicking in ~~Tk operations~~ view.
	MCTS_AUTO_PLAY ~~and RANDOM_ANIMATE are~~ available as special event ~~names for VisB~~.		The last MCTS tree can be visualised graphically.
			In ProB Tcl/Tk by right-clicking in the "Operations" pane and selecting "Show last MCTS tree". In ProB2-UI you can view the MCTS tree via the "Graph Visualisation" dialog in the Visualisation menu.

			You can also trigger MCTS play in VisB.
			Here MCTS_AUTO_PLAY is available as special event name.

Michael Leuschel at 13:01, 6 January 2024

2024-01-06T13:01:45Z

← Older revision		Revision as of 13:01, 6 January 2024
Line 39:		Line 39:

	MCTS tree can be visualised graphically.		MCTS tree can be visualised graphically.
	MCTS commands are available by right-clicking in Tk operations view.		MCTS commands are available by right-clicking in Tk operations view.
	MCTS_AUTO_PLAY and RANDOM_ANIMATE are available as special event names for VisB.		MCTS_AUTO_PLAY and RANDOM_ANIMATE are available as special event names for VisB.

Michael Leuschel at 13:01, 6 January 2024

2024-01-06T13:01:36Z

← Older revision		Revision as of 13:01, 6 January 2024
Line 39:		Line 39:

	MCTS tree can be visualised graphically.		MCTS tree can be visualised graphically.
	MCTS commands are available by right-clicking in Tk operations view.		MCTS commands are available by right-clicking in Tk operations view.
	MCTS_AUTO_PLAY and RANDOM_ANIMATE are available as special event names for VisB.		MCTS_AUTO_PLAY and RANDOM_ANIMATE are available as special event names for VisB.

Michael Leuschel at 13:01, 6 January 2024

2024-01-06T13:01:25Z

← Older revision		Revision as of 13:01, 6 January 2024
Line 36:		Line 36:
	END		END
	</pre>		</pre>


			MCTS tree can be visualised graphically.
			MCTS commands are available by right-clicking in Tk operations view.
			MCTS_AUTO_PLAY and RANDOM_ANIMATE are available as special event names for VisB.

Michael Leuschel: Created page with "As of January 2024 ProB has a built-in algorithm for Monte Carlo Tree Search (MCTS). This can for example be used to perform game playing. In order to make use of MCTS one needs to provide information about the game state of a model by providing DEFINITIONS for: * GAME_OVER: must be TRUE when the game is finished; for a deadlock the game is also considered over (and by default drawn) * GAME_VALUE: must evaluate to a number if GAME_OVER is true. 0 is considered a draw, a..."

2024-01-06T13:00:34Z

Created page with "As of January 2024 ProB has a built-in algorithm for Monte Carlo Tree Search (MCTS). This can for example be used to perform game playing. In order to make use of MCTS one needs to provide information about the game state of a model by providing DEFINITIONS for: * GAME_OVER: must be TRUE when the game is finished; for a deadlock the game is also considered over (and by default drawn) * GAME_VALUE: must evaluate to a number if GAME_OVER is true. 0 is considered a draw, a..."

New page

As of January 2024 ProB has a built-in algorithm for Monte Carlo Tree Search (MCTS).
This can for example be used to perform game playing.

In order to make use of MCTS one needs to provide information about the game state of a model by providing DEFINITIONS for:
* GAME_OVER: must be TRUE when the game is finished; for a deadlock the game is also considered over (and by default drawn)
* GAME_VALUE: must evaluate to a number if GAME_OVER is true. 0 is considered a draw, a positive value a win for the max player and a negative value a win for the min player
* GAME_PLAYER: must evaluate to either "min" or "max", depending on which player has to move

The following definitions are optional and influence the MCTS algorithm:
* GAME_MCTS_RUNS
* GAME_MCTS_TIMEOUT
* GAME_MCTS_CACHE_LAST_TREE
* GAME_MCTS_MAX_SIMULATION_LENGTH

A simple example is the Nim game of sticks:

<pre>
MACHINE Nim_MCTS
CONSTANTS Players, other
PROPERTIES
Players = {"min","max"} &
other = {"min"|->"max", "max"|->"min"}
DEFINITIONS
GAME_OVER == bool(sticks < 1);
GAME_VALUE == {"max"|->1, "min"|->-1}(player);
GAME_PLAYER == player;
GAME_MCTS_RUNS == 100
VARIABLES sticks, player
INVARIANT
sticks:NATURAL &
player:Players
INITIALISATION sticks := 5 || player := "max"
OPERATIONS
Take1 = SELECT sticks>=1 THEN sticks := sticks-1 || player := other(player) END;
Take2 = SELECT sticks>=2 THEN sticks := sticks-2 || player := other(player) END
END
</pre>