diff --git a/Algorithms/MCTS/Bucket_Game.def b/Algorithms/MCTS/Bucket_Game.def
new file mode 100644
index 0000000000000000000000000000000000000000..bd06b262f2b3f357db9e4f82fb362f8ead0e30c7
--- /dev/null
+++ b/Algorithms/MCTS/Bucket_Game.def
@@ -0,0 +1,8 @@
+DEFINITIONS
+ /* a particular game tree : simple bucket example */
+ GAME_DEFINITIONS ==
+ min_node = 1 & max_node = 10 &
+ root = 1 &
+ moves = [{2,3,4}, {5,6}, {7,8}, {9,10}, {},{},{},{},{},{}] &
+ utility = {5 |-> -50, 6|-> 50, 7|->1, 8|->3, 9|->10, 10 |->-5} &
+ maxplayer_nodes = {1, 5,6, 7,8, 9,10}
diff --git a/Algorithms/MCTS/CustomGraph.def b/Algorithms/MCTS/CustomGraph.def
new file mode 100644
index 0000000000000000000000000000000000000000..9e79745c2c2c7c80a2ce2bbf9ddfca953c330f30
--- /dev/null
+++ b/Algorithms/MCTS/CustomGraph.def
@@ -0,0 +1,32 @@
+DEFINITIONS
+ "LibraryStrings.def";
+ perc_wins(s) == IF number_of_visits(s)=0 THEN 0.0 ELSE real(number_of_wins(s)) / real(number_of_visits(s)) END;
+ node_string(s) == (IF n:terminal_nodes THEN FORMAT_TO_STRING("~w (val=~w)",[n,utility(n)]) ELSE TO_STRING(n) END)
+ ^
+ (IF n=state THEN "*" ELSE "" END);
+ CUSTOM_GRAPH_NODES1 ==
+ ran(%n.(n:terminal_nodes | rec(color:IF utility(n)>0 THEN "green3" ELSE "burlywood" END,
+ value:n,shape:"box",label:node_string(n))));
+ CUSTOM_GRAPH_NODES2 ==
+ ran(%n.(n:expanded_nodes | rec(color:IF perc_wins(n) > 0.5 THEN "green3" ELSE "burlywood" END,
+ value:n,
+ shape:"record",
+ style:IF n=state THEN "bold" ELSE "rounded" END,
+ label:FORMAT_TO_STRING("|{~w\\n|w=~w\\n|n=~w\\n|exp=~w\\n|ucb=~w}|",
+ [node_string(n),TO_STRING(number_of_wins(n)),
+ TO_STRING(number_of_visits(n)),
+ REAL_TO_DEC_STRING(Exploration(n),2),
+ REAL_TO_DEC_STRING(UCBtot(n),2)]))));
+ CUSTOM_GRAPH_NODES3 ==
+ ran(%n.(n:nodes\terminal_nodes\expanded_nodes | rec(color:"gray",
+ value:n,shape:"box",
+ label:TO_STRING(n))));
+ CUSTOM_GRAPH_EDGES1 ==
+ rec(label:"",
+ style:"dotted",
+ value:{x,y|x:nodes & y:(moves(x)) & IsBestMove(x,y)=FALSE});
+
+ CUSTOM_GRAPH_EDGES2 ==
+ rec(label:"best",
+ style:"bold",
+ value:{x,y|x:nodes & y:(moves(x)) & IsBestMove(x,y)=TRUE});
diff --git a/Algorithms/MCTS/MCTS.mch b/Algorithms/MCTS/MCTS.mch
new file mode 100644
index 0000000000000000000000000000000000000000..1fcc9f136d6cc6b8f01b3bab1e3ec268136eed0d
--- /dev/null
+++ b/Algorithms/MCTS/MCTS.mch
@@ -0,0 +1,138 @@
+MACHINE MCTS
+// an attempt at modelling Monte-Carlo Tree Search in B for ProB
+// by Michael Leuschel (c) 2022
+DEFINITIONS
+ VISB_JSON_FILE == "MCTS_visb.json";
+ terminal_nodes == dom(utility);
+ "Bucket_Game.def";
+ "LibraryStrings.def";
+ "LibraryRandom.def";
+ "LibraryReals.def";
+ "CustomGraph.def";
+ IsBestMove(from,to) == bool(to:expanded_nodes & to:(moves(from)) &
+ number_of_visits(to) = max(number_of_visits[(moves(from))]));
+ UpdateState(s,SimValue) == // update state after a simulation with value SimValue
+ BEGIN
+ number_of_visits(s) := number_of_visits(s) + 1;
+ IF (s/:maxplayer_nodes & SimValue >0 ) or
+ (s:maxplayer_nodes & SimValue <0 ) THEN // we adapt the value for the parent node !
+ number_of_wins(s) := number_of_wins(s) + 1 // TO DO: treat value 0 as 0.5 for wins
+ END
+ END;
+ UCBtot(s) == IF s:expanded_nodes & s/= root THEN UCB(s) ELSE 0.0 END; // total version of UCB
+ INFINITY == 10000.0;
+ Exploration(s) == IF number_of_visits(s) = 0 or s=root THEN
+ INFINITY
+ ELSE RSQRT(2.0 * RLOGe(real(number_of_visits(parent(s))))
+ /
+ real(number_of_visits(s)))
+ END;
+ UCB(s) == // Upper Confidence Bound Formula
+ LET ni BE ni = number_of_visits(s) IN
+ IF ni=0 THEN
+ INFINITY
+ ELSE
+ real(number_of_wins(s)) / real(ni) // Exploitation
+ +
+ RSQRT(2.0 * RLOGe(real(number_of_visits(parent(s))))
+ /
+ real(ni))
+ END // IF
+ END;
+ABSTRACT_CONSTANTS rollout
+CONSTANTS root, nodes, min_node, max_node, moves, utility, parent, maxplayer_nodes
+PROPERTIES
+ root : nodes &
+ max_node : NATURAL1 &
+ nodes = min_node..max_node &
+ moves: nodes --> POW(nodes) &
+ utility: nodes +-> INTEGER &
+ !s.(s:nodes => (moves(s)={} => s:terminal_nodes)) &
+
+ parent: nodes \ {root} --> nodes &
+ !(p,c).(p:nodes & c:(moves(p)) => c|->p : parent) &
+
+ rollout = %n.(n:nodes | IF n:terminal_nodes THEN
+ utility(n)
+ ELSE
+ rollout(random_element(moves(n)))
+ END ) &
+
+ /* a particular game tree : simple bucket example*/
+ !(p,c).(p:nodes & c:(moves(p)) => p<c) /*@desc "Ensures we have no cycles" */ &
+
+ GAME_DEFINITIONS
+
+VARIABLES cur_root,
+ state,
+ selected,
+ expanded_nodes,
+ number_of_visits,
+ number_of_wins
+INVARIANT
+ cur_root:nodes &
+ state:nodes &
+ selected:BOOL /*@desc "TRUE if state has been selected" */ &
+ expanded_nodes <: nodes &
+ number_of_visits : expanded_nodes --> NATURAL &
+ number_of_wins : expanded_nodes --> NATURAL
+INITIALISATION cur_root := root ||
+ state := root ||
+ selected := TRUE ||
+ expanded_nodes := {root} ||
+ number_of_visits := {root} * {0} ||
+ number_of_wins := {root} * {0}
+OPERATIONS
+
+ // PHASE 1: Select children from cur_root with best UCB value
+ Select(ucb,child) = SELECT selected=FALSE &
+ state : expanded_nodes &
+ ucb = %(i).(i:(moves(state)) | UCB(i)) &
+ child: moves(state) &
+ // ucb(nr) = max(ran(ucb))
+ !o.(o:ran(ucb) => ucb(child) >= o)
+ THEN
+ state := child ||
+ selected := bool(number_of_visits(child) = 0 or child:terminal_nodes)
+ END;
+
+ // PHASE 2: Expand the selected node
+ Expand(newchildren) = SELECT selected=TRUE &
+ newchildren = (moves(state)) \ expanded_nodes & newchildren /= {} THEN
+ expanded_nodes := expanded_nodes \/ newchildren ||
+ number_of_visits := number_of_visits <+ (newchildren*{0}) ||
+ number_of_wins := number_of_wins <+ (newchildren*{0})
+ END;
+
+ // PHASE 3: Run a simulation and backpropagate result back to cur_root
+ Simulate(value) = SELECT selected=TRUE &
+ (moves(state)) <: expanded_nodes &
+ value = rollout(state) /* perform random simulation */
+ THEN
+ UpdateState(state,value);
+ VAR backstate IN
+ BEGIN
+ backstate := state;
+ WHILE backstate : dom(parent) DO
+ backstate := parent(backstate);
+ UpdateState(backstate,value)
+ INVARIANT backstate:nodes
+ VARIANT backstate
+ END // WHILE
+ END // BEGIN
+ END; //VAR
+ state,selected := cur_root, FALSE // Restart selecting nodes at the root
+ END; //SELECT
+
+ ChooseBestMove(To) = SELECT 1=2 & state=cur_root & IsBestMove(cur_root,To)=TRUE THEN
+ cur_root := To || // refocus on new root state of game
+ state := To
+ END
+ // Query operations to inspect state:
+ /*
+ ;
+ res <-- GameOver = SELECT state:terminal_nodes THEN
+ res := utility(state)
+ END
+ */
+END
diff --git a/Algorithms/MCTS/MCTS_visb.json b/Algorithms/MCTS/MCTS_visb.json
new file mode 100644
index 0000000000000000000000000000000000000000..17aa8a997363f20dff3bb70a068eed02e4f8f3e5
--- /dev/null
+++ b/Algorithms/MCTS/MCTS_visb.json
@@ -0,0 +1,58 @@
+{
+ "svg":"MCTS_visb.svg",
+ "comment": "VisB Visualization for MCTS",
+ "items": [
+ {
+ "id": "w_%0",
+ "attr": "text",
+ "value": "\"w=\"^IF %0:dom(number_of_wins) THEN TO_STRING(number_of_wins(%0)) ELSE \"-\" END",
+ "for": {"from":1, "to":10}
+ },
+ {
+ "id": "n_%0",
+ "attr": "text",
+ "value": "\"n=\"^IF %0:dom(number_of_visits) THEN TO_STRING(number_of_visits(%0)) ELSE \"-\" END",
+ "for": {"from":1, "to":10}
+ },
+ {
+ "id": "exp_%0",
+ "attr": "text",
+ "value": "\"exp=\"^IF %0:dom(number_of_visits) THEN REAL_TO_DEC_STRING(Exploration(%0),2) ELSE \"-\" END",
+ "for": {"from":1, "to":10}
+ },
+ {
+ "id": "ucb_%0",
+ "attr": "text",
+ "value": "\"ucb=\"^IF %0:dom(number_of_visits) THEN REAL_TO_DEC_STRING(UCBtot(%0),2) ELSE \"-\" END",
+ "for": {"from":1, "to":10}
+ },
+ {
+ "id": "node%0",
+ "attr": "stroke-width",
+ "value": "IF %0=state THEN 3 ELSE 1 END",
+ "for": {"from":1, "to":10}
+ },
+ {
+ "id": "feedback_text",
+ "attr": "text",
+ "value": "\"Next: \"^IF GET_IS_ENABLED(\"Simulate\")=TRUE THEN \"SIMULATE\" ELSIF GET_IS_ENABLED(\"Select\")=TRUE THEN \"SELECT\" ELSE \"EXPAND\" END"
+ }
+
+],
+ "events": [
+
+ {
+ "id": "feedback_text",
+ "event": "Select"
+ },
+ {
+ "id": "feedback_text",
+ "event": "Expand"
+ },
+ {
+ "id": "feedback_text",
+ "event": "Simulate"
+ }
+
+ ]
+}
diff --git a/Algorithms/MCTS/MCTS_visb.svg b/Algorithms/MCTS/MCTS_visb.svg
new file mode 100644
index 0000000000000000000000000000000000000000..ed4a921d8b8a918433f1afb2a67dc3a21e18b8ed
--- /dev/null
+++ b/Algorithms/MCTS/MCTS_visb.svg
@@ -0,0 +1,238 @@
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN"
+ "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd">
+<!-- Generated by graphviz version 2.50.0 (20211204.2007)
+ -->
+<!-- Title: prob_graph Pages: 1 -->
+<svg width="540pt" height="718pt"
+ viewBox="0.00 0.00 542.00 720.04" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink">
+
+<g id="graph0" class="graph" transform="scale(0.74 0.74) rotate(0) translate(4 972)">
+<title>prob_graph</title>
+<polygon fill="white" stroke="transparent" points="-4,4 -4,-972 730,-972 730,4 -4,4"/>
+<!-- 0 -->
+<g id="node10" class="node">
+<title>0</title>
+<path fill="none" stroke="#00cd00" d="M264,-70.5C264,-70.5 350,-70.5 350,-70.5 356,-70.5 362,-76.5 362,-82.5 362,-82.5 362,-163.5 362,-163.5 362,-169.5 356,-175.5 350,-175.5 350,-175.5 264,-175.5 264,-175.5 258,-175.5 252,-169.5 252,-163.5 252,-163.5 252,-82.5 252,-82.5 252,-76.5 258,-70.5 264,-70.5"/>
+<polyline fill="none" stroke="#00cd00" points="272,-70.5 272,-175.5 "/>
+<text id="node_10" text-anchor="middle" x="307" y="-161.9" font-family="Times,serif" font-size="12.00">10 (val=-5)</text>
+<polyline fill="none" stroke="#00cd00" points="272,-154.5 342,-154.5 "/>
+<text id="w_10" text-anchor="middle" x="307" y="-140.9" font-family="Times,serif" font-size="12.00">w=2</text>
+<polyline fill="none" stroke="#00cd00" points="272,-133.5 342,-133.5 "/>
+<text id="n_10" text-anchor="middle" x="307" y="-119.9" font-family="Times,serif" font-size="12.00">n=2</text>
+<polyline fill="none" stroke="#00cd00" points="272,-112.5 342,-112.5 "/>
+<text id="exp_10" text-anchor="middle" x="307" y="-98.9" font-family="Times,serif" font-size="12.00">exp=1.18</text>
+<polyline fill="none" stroke="#00cd00" points="272,-91.5 342,-91.5 "/>
+<text id="ucb_10" text-anchor="middle" x="307" y="-77.9" font-family="Times,serif" font-size="12.00">ucb=2.18</text>
+<polyline fill="none" stroke="#00cd00" points="342,-70.5 342,-175.5 "/>
+</g>
+<!-- 1 -->
+<g id="node5" class="node">
+<title>1</title>
+<path fill="none" stroke="#00cd00" d="M12,-70.5C12,-70.5 98,-70.5 98,-70.5 104,-70.5 110,-76.5 110,-82.5 110,-82.5 110,-163.5 110,-163.5 110,-169.5 104,-175.5 98,-175.5 98,-175.5 12,-175.5 12,-175.5 6,-175.5 0,-169.5 0,-163.5 0,-163.5 0,-82.5 0,-82.5 0,-76.5 6,-70.5 12,-70.5"/>
+<polyline fill="none" stroke="#00cd00" points="20,-70.5 20,-175.5 "/>
+<text id="node_5" text-anchor="middle" x="55" y="-161.9" font-family="Times,serif" font-size="12.00">5 (val=-50)</text>
+<polyline fill="none" stroke="#00cd00" points="20,-154.5 90,-154.5 "/>
+<text id="w_5" text-anchor="middle" x="55" y="-140.9" font-family="Times,serif" font-size="12.00">w=2</text>
+<polyline fill="none" stroke="#00cd00" points="20,-133.5 90,-133.5 "/>
+<text id="n_5" text-anchor="middle" x="55" y="-119.9" font-family="Times,serif" font-size="12.00">n=2</text>
+<polyline fill="none" stroke="#00cd00" points="20,-112.5 90,-112.5 "/>
+<text id="exp_5" text-anchor="middle" x="55" y="-98.9" font-family="Times,serif" font-size="12.00">exp=1.18</text>
+<polyline fill="none" stroke="#00cd00" points="20,-91.5 90,-91.5 "/>
+<text id="ucb_5" text-anchor="middle" x="55" y="-77.9" font-family="Times,serif" font-size="12.00">ucb=2.18</text>
+<polyline fill="none" stroke="#00cd00" points="90,-70.5 90,-175.5 "/>
+</g>
+<!-- 2 -->
+<g id="node6" class="node">
+<title>2</title>
+<path fill="none" stroke="burlywood" d="M140,-70.5C140,-70.5 222,-70.5 222,-70.5 228,-70.5 234,-76.5 234,-82.5 234,-82.5 234,-163.5 234,-163.5 234,-169.5 228,-175.5 222,-175.5 222,-175.5 140,-175.5 140,-175.5 134,-175.5 128,-169.5 128,-163.5 128,-163.5 128,-82.5 128,-82.5 128,-76.5 134,-70.5 140,-70.5"/>
+<polyline fill="none" stroke="burlywood" points="148,-70.5 148,-175.5 "/>
+<text id="node_6" text-anchor="middle" x="181" y="-161.9" font-family="Times,serif" font-size="12.00">6 (val=50)</text>
+<polyline fill="none" stroke="burlywood" points="148,-154.5 214,-154.5 "/>
+<text id="w_6" text-anchor="middle" x="181" y="-140.9" font-family="Times,serif" font-size="12.00">w=0</text>
+<polyline fill="none" stroke="burlywood" points="148,-133.5 214,-133.5 "/>
+<text id="n_6" text-anchor="middle" x="181" y="-119.9" font-family="Times,serif" font-size="12.00">n=1</text>
+<polyline fill="none" stroke="burlywood" points="148,-112.5 214,-112.5 "/>
+<text id="exp_6" text-anchor="middle" x="181" y="-98.9" font-family="Times,serif" font-size="12.00">exp=1.67</text>
+<polyline fill="none" stroke="burlywood" points="148,-91.5 214,-91.5 "/>
+<text id="ucb_6" text-anchor="middle" x="181" y="-77.9" font-family="Times,serif" font-size="12.00">ucb=1.67</text>
+<polyline fill="none" stroke="burlywood" points="214,-70.5 214,-175.5 "/>
+</g>
+<!-- 3 -->
+<g id="node7" class="node">
+<title>3</title>
+<path fill="none" stroke="#00cd00" d="M516,-70.5C516,-70.5 594,-70.5 594,-70.5 600,-70.5 606,-76.5 606,-82.5 606,-82.5 606,-163.5 606,-163.5 606,-169.5 600,-175.5 594,-175.5 594,-175.5 516,-175.5 516,-175.5 510,-175.5 504,-169.5 504,-163.5 504,-163.5 504,-82.5 504,-82.5 504,-76.5 510,-70.5 516,-70.5"/>
+<polyline fill="none" stroke="#00cd00" points="524,-70.5 524,-175.5 "/>
+<text id="node_7" text-anchor="middle" x="555" y="-161.9" font-family="Times,serif" font-size="12.00">7 (val=1)</text>
+<polyline fill="none" stroke="#00cd00" points="524,-154.5 586,-154.5 "/>
+<text id="w_7" text-anchor="middle" x="555" y="-140.9" font-family="Times,serif" font-size="12.00">w=0</text>
+<polyline fill="none" stroke="#00cd00" points="524,-133.5 586,-133.5 "/>
+<text id="n_7" text-anchor="middle" x="555" y="-119.9" font-family="Times,serif" font-size="12.00">n=4</text>
+<polyline fill="none" stroke="#00cd00" points="524,-112.5 586,-112.5 "/>
+<text id="exp_7" text-anchor="middle" x="555" y="-98.9" font-family="Times,serif" font-size="12.00">exp=1.05</text>
+<polyline fill="none" stroke="#00cd00" points="524,-91.5 586,-91.5 "/>
+<text id="ucb_7" text-anchor="middle" x="555" y="-77.9" font-family="Times,serif" font-size="12.00">ucb=1.05</text>
+<polyline fill="none" stroke="#00cd00" points="586,-70.5 586,-175.5 "/>
+</g>
+<!-- 4 -->
+<g id="node8" class="node">
+<title>4</title>
+<path fill="none" stroke="#00cd00" d="M636,-70.5C636,-70.5 714,-70.5 714,-70.5 720,-70.5 726,-76.5 726,-82.5 726,-82.5 726,-163.5 726,-163.5 726,-169.5 720,-175.5 714,-175.5 714,-175.5 636,-175.5 636,-175.5 630,-175.5 624,-169.5 624,-163.5 624,-163.5 624,-82.5 624,-82.5 624,-76.5 630,-70.5 636,-70.5"/>
+<polyline fill="none" stroke="#00cd00" points="644,-70.5 644,-175.5 "/>
+<text id="node_8" text-anchor="middle" x="675" y="-161.9" font-family="Times,serif" font-size="12.00">8 (val=3)</text>
+<polyline fill="none" stroke="#00cd00" points="644,-154.5 706,-154.5 "/>
+<text id="w_8" text-anchor="middle" x="675" y="-140.9" font-family="Times,serif" font-size="12.00">w=0</text>
+<polyline fill="none" stroke="#00cd00" points="644,-133.5 706,-133.5 "/>
+<text id="n_8" text-anchor="middle" x="675" y="-119.9" font-family="Times,serif" font-size="12.00">n=4</text>
+<polyline fill="none" stroke="#00cd00" points="644,-112.5 706,-112.5 "/>
+<text id="exp_8" text-anchor="middle" x="675" y="-98.9" font-family="Times,serif" font-size="12.00">exp=1.05</text>
+<polyline fill="none" stroke="#00cd00" points="644,-91.5 706,-91.5 "/>
+<text id="ucb_8" text-anchor="middle" x="675" y="-77.9" font-family="Times,serif" font-size="12.00">ucb=1.05</text>
+<polyline fill="none" stroke="#00cd00" points="706,-70.5 706,-175.5 "/>
+</g>
+<!-- 5 -->
+<g id="node9" class="node">
+<title>5</title>
+<path fill="none" stroke="burlywood" d="M392,-70.5C392,-70.5 474,-70.5 474,-70.5 480,-70.5 486,-76.5 486,-82.5 486,-82.5 486,-163.5 486,-163.5 486,-169.5 480,-175.5 474,-175.5 474,-175.5 392,-175.5 392,-175.5 386,-175.5 380,-169.5 380,-163.5 380,-163.5 380,-82.5 380,-82.5 380,-76.5 386,-70.5 392,-70.5"/>
+<polyline fill="none" stroke="burlywood" points="400,-70.5 400,-175.5 "/>
+<text id="node_9" text-anchor="middle" x="433" y="-161.9" font-family="Times,serif" font-size="12.00">9 (val=10)</text>
+<polyline fill="none" stroke="burlywood" points="400,-154.5 466,-154.5 "/>
+<text id="w_9" text-anchor="middle" x="433" y="-140.9" font-family="Times,serif" font-size="12.00">w=0</text>
+<polyline fill="none" stroke="burlywood" points="400,-133.5 466,-133.5 "/>
+<text id="n_9" text-anchor="middle" x="433" y="-119.9" font-family="Times,serif" font-size="12.00">n=1</text>
+<polyline fill="none" stroke="burlywood" points="400,-112.5 466,-112.5 "/>
+<text id="exp_9" text-anchor="middle" x="433" y="-98.9" font-family="Times,serif" font-size="12.00">exp=1.67</text>
+<polyline fill="none" stroke="burlywood" points="400,-91.5 466,-91.5 "/>
+<text id="ucb_9" text-anchor="middle" x="433" y="-77.9" font-family="Times,serif" font-size="12.00">ucb=1.67</text>
+<polyline fill="none" stroke="burlywood" points="466,-70.5 466,-175.5 "/>
+</g>
+<!-- 6 -->
+<g id="node1" class="node">
+<title>6</title>
+<path fill="none" stroke="burlywood" d="M310,-792.5C310,-792.5 412,-792.5 412,-792.5 418,-792.5 424,-798.5 424,-804.5 424,-804.5 424,-885.5 424,-885.5 424,-891.5 418,-897.5 412,-897.5 412,-897.5 310,-897.5 310,-897.5 304,-897.5 298,-891.5 298,-885.5 298,-885.5 298,-804.5 298,-804.5 298,-798.5 304,-792.5 310,-792.5"/>
+<polyline fill="none" stroke="burlywood" points="318,-792.5 318,-897.5 "/>
+<text id="node_1" text-anchor="middle" x="361" y="-883.9" font-family="Times,serif" font-size="12.00">1</text>
+<polyline fill="none" stroke="burlywood" points="318,-876.5 404,-876.5 "/>
+<text id="w_1" text-anchor="middle" x="361" y="-862.9" font-family="Times,serif" font-size="12.00">w=4</text>
+<polyline fill="none" stroke="burlywood" points="318,-855.5 404,-855.5 "/>
+<text id="n_1" text-anchor="middle" x="361" y="-841.9" font-family="Times,serif" font-size="12.00">n=18</text>
+<polyline fill="none" stroke="burlywood" points="318,-834.5 404,-834.5 "/>
+<text id="exp_1" text-anchor="middle" x="361" y="-820.9" font-family="Times,serif" font-size="12.00">exp=10000.00</text>
+<polyline fill="none" stroke="burlywood" points="318,-813.5 404,-813.5 "/>
+<text id="ucb_1" text-anchor="middle" x="361" y="-799.9" font-family="Times,serif" font-size="12.00">ucb=0.00</text>
+<polyline fill="none" stroke="burlywood" points="404,-792.5 404,-897.5 "/>
+</g>
+<!-- 7 -->
+<g id="node2" class="node">
+<title>7</title>
+<path fill="none" stroke="burlywood" d="M142,-431.5C142,-431.5 220,-431.5 220,-431.5 226,-431.5 232,-437.5 232,-443.5 232,-443.5 232,-524.5 232,-524.5 232,-530.5 226,-536.5 220,-536.5 220,-536.5 142,-536.5 142,-536.5 136,-536.5 130,-530.5 130,-524.5 130,-524.5 130,-443.5 130,-443.5 130,-437.5 136,-431.5 142,-431.5"/>
+<polyline fill="none" stroke="burlywood" points="150,-431.5 150,-536.5 "/>
+<text id="node_2" text-anchor="middle" x="181" y="-522.9" font-family="Times,serif" font-size="12.00">2</text>
+<polyline fill="none" stroke="burlywood" points="150,-515.5 212,-515.5 "/>
+<text id="w_2" text-anchor="middle" x="181" y="-501.9" font-family="Times,serif" font-size="12.00">w=2</text>
+<polyline fill="none" stroke="burlywood" points="150,-494.5 212,-494.5 "/>
+<text id="n_2" text-anchor="middle" x="181" y="-480.9" font-family="Times,serif" font-size="12.00">n=4</text>
+<polyline fill="none" stroke="burlywood" points="150,-473.5 212,-473.5 "/>
+<text id="exp_2" text-anchor="middle" x="181" y="-459.9" font-family="Times,serif" font-size="12.00">exp=1.20</text>
+<polyline fill="none" stroke="burlywood" points="150,-452.5 212,-452.5 "/>
+<text id="ucb_2" text-anchor="middle" x="181" y="-438.9" font-family="Times,serif" font-size="12.00">ucb=1.70</text>
+<polyline fill="none" stroke="burlywood" points="212,-431.5 212,-536.5 "/>
+</g>
+<!-- 6->7 -->
+<g id="edge6" class="edge">
+<title>6->7</title>
+<path fill="none" stroke="blue" stroke-dasharray="1,5" d="M335.02,-792.18C302.27,-726.86 246.07,-614.77 211.37,-545.57"/>
+<polygon fill="blue" stroke="blue" points="214.44,-543.88 206.83,-536.51 208.18,-547.02 214.44,-543.88"/>
+</g>
+<!-- 8 -->
+<g id="node4" class="node">
+<title>8</title>
+<path fill="none" stroke="burlywood" d="M322,-431.5C322,-431.5 400,-431.5 400,-431.5 406,-431.5 412,-437.5 412,-443.5 412,-443.5 412,-524.5 412,-524.5 412,-530.5 406,-536.5 400,-536.5 400,-536.5 322,-536.5 322,-536.5 316,-536.5 310,-530.5 310,-524.5 310,-524.5 310,-443.5 310,-443.5 310,-437.5 316,-431.5 322,-431.5"/>
+<polyline fill="none" stroke="burlywood" points="330,-431.5 330,-536.5 "/>
+<text id="node_4" text-anchor="middle" x="361" y="-522.9" font-family="Times,serif" font-size="12.00">4</text>
+<polyline fill="none" stroke="burlywood" points="330,-515.5 392,-515.5 "/>
+<text id="w_4" text-anchor="middle" x="361" y="-501.9" font-family="Times,serif" font-size="12.00">w=2</text>
+<polyline fill="none" stroke="burlywood" points="330,-494.5 392,-494.5 "/>
+<text id="n_4" text-anchor="middle" x="361" y="-480.9" font-family="Times,serif" font-size="12.00">n=4</text>
+<polyline fill="none" stroke="burlywood" points="330,-473.5 392,-473.5 "/>
+<text id="exp_4" text-anchor="middle" x="361" y="-459.9" font-family="Times,serif" font-size="12.00">exp=1.20</text>
+<polyline fill="none" stroke="burlywood" points="330,-452.5 392,-452.5 "/>
+<text id="ucb_4" text-anchor="middle" x="361" y="-438.9" font-family="Times,serif" font-size="12.00">ucb=1.70</text>
+<polyline fill="none" stroke="burlywood" points="392,-431.5 392,-536.5 "/>
+</g>
+<!-- 6->8 -->
+<g id="edge7" class="edge">
+<title>6->8</title>
+<path fill="none" stroke="blue" stroke-dasharray="1,5" d="M361,-792.18C361,-727.26 361,-616.14 361,-546.84"/>
+<polygon fill="blue" stroke="blue" points="364.5,-546.51 361,-536.51 357.5,-546.51 364.5,-546.51"/>
+</g>
+<!-- 9 -->
+<g id="node3" class="node">
+<title>9</title>
+<polygon fill="none" stroke="#00cd00" points="504,-431.5 504,-536.5 606,-536.5 606,-431.5 504,-431.5"/>
+<polyline fill="none" stroke="#00cd00" points="524,-431.5 524,-536.5 "/>
+<text id="node_3" text-anchor="middle" x="555" y="-522.9" font-family="Times,serif" font-size="12.00">3</text>
+<polyline fill="none" stroke="#00cd00" points="524,-515.5 586,-515.5 "/>
+<text id="w_3" text-anchor="middle" x="555" y="-501.9" font-family="Times,serif" font-size="12.00">w=9</text>
+<polyline fill="none" stroke="#00cd00" points="524,-494.5 586,-494.5 "/>
+<text id="n_3" text-anchor="middle" x="555" y="-480.9" font-family="Times,serif" font-size="12.00">n=9</text>
+<polyline fill="none" stroke="#00cd00" points="524,-473.5 586,-473.5 "/>
+<text id="exp_3" text-anchor="middle" x="555" y="-459.9" font-family="Times,serif" font-size="12.00">exp=0.80</text>
+<polyline fill="none" stroke="#00cd00" points="524,-452.5 586,-452.5 "/>
+<text id="ucb_3" text-anchor="middle" x="555" y="-438.9" font-family="Times,serif" font-size="12.00">ucb=1.80</text>
+<polyline fill="none" stroke="#00cd00" points="586,-431.5 586,-536.5 "/>
+</g>
+<!-- 6->9 -->
+<g id="edge1" class="edge">
+<title>6->9</title>
+<path fill="none" stroke="blue" stroke-width="2" d="M389,-792.18C424.3,-726.86 484.87,-614.77 522.27,-545.57"/>
+<polygon fill="blue" stroke="blue" stroke-width="2" points="525.49,-546.97 527.16,-536.51 519.33,-543.65 525.49,-546.97"/>
+<text text-anchor="middle" x="467.5" y="-660.9" font-family="Times,serif" font-size="12.00">best</text>
+</g>
+<!-- 7->1 -->
+<g id="edge2" class="edge">
+<title>7->1</title>
+<path fill="none" stroke="blue" stroke-width="2" d="M162.81,-431.18C139.93,-365.99 100.71,-254.23 76.41,-184.99"/>
+<polygon fill="blue" stroke="blue" stroke-width="2" points="79.69,-183.79 73.08,-175.51 73.09,-186.11 79.69,-183.79"/>
+<text text-anchor="middle" x="127.5" y="-300.9" font-family="Times,serif" font-size="12.00">best</text>
+</g>
+<!-- 7->2 -->
+<g id="edge8" class="edge">
+<title>7->2</title>
+<path fill="none" stroke="blue" stroke-dasharray="1,5" d="M181,-431.18C181,-366.26 181,-255.14 181,-185.84"/>
+<polygon fill="blue" stroke="blue" points="184.5,-185.51 181,-175.51 177.5,-185.51 184.5,-185.51"/>
+</g>
+<!-- 8->0 -->
+<g id="edge5" class="edge">
+<title>8->0</title>
+<path fill="none" stroke="blue" stroke-width="2" d="M353.21,-431.18C343.42,-366.13 326.66,-254.69 316.24,-185.42"/>
+<polygon fill="blue" stroke="blue" stroke-width="2" points="319.7,-184.88 314.75,-175.51 312.77,-185.92 319.7,-184.88"/>
+<text text-anchor="middle" x="343.5" y="-300.9" font-family="Times,serif" font-size="12.00">best</text>
+</g>
+<!-- 8->5 -->
+<g id="edge9" class="edge">
+<title>8->5</title>
+<path fill="none" stroke="blue" stroke-dasharray="1,5" d="M371.39,-431.18C384.44,-366.13 406.79,-254.69 420.68,-185.42"/>
+<polygon fill="blue" stroke="blue" points="424.13,-186 422.67,-175.51 417.27,-184.63 424.13,-186"/>
+</g>
+<!-- 9->3 -->
+<g id="edge3" class="edge">
+<title>9->3</title>
+<path fill="none" stroke="blue" stroke-width="2" d="M555,-431.18C555,-366.26 555,-255.14 555,-185.84"/>
+<polygon fill="blue" stroke="blue" stroke-width="2" points="558.5,-185.51 555,-175.51 551.5,-185.51 558.5,-185.51"/>
+<text text-anchor="middle" x="564.5" y="-300.9" font-family="Times,serif" font-size="12.00">best</text>
+</g>
+<!-- 9->4 -->
+<g id="edge4" class="edge">
+<title>9->4</title>
+<path fill="none" stroke="blue" stroke-width="2" d="M572.32,-431.18C594.07,-366.13 631.32,-254.69 654.47,-185.42"/>
+<polygon fill="blue" stroke="blue" stroke-width="2" points="657.93,-186.11 657.78,-175.51 651.29,-183.89 657.93,-186.11"/>
+<text text-anchor="middle" x="624.5" y="-300.9" font-family="Times,serif" font-size="12.00">best</text>
+</g>
+</g>
+<g id="feedback" class="node">
+<title>feed</title>
+<text id="feedback_text" text-anchor="middle" x="100" y="90"
+ font-family="Times,serif" font-size="12.00">ACTION</text>
+</g>
+</svg>