Jars/DieHard_tla.json

 {
   "svg":"Jars.svg",
+  "svg_box": {"height":200, "width":360},
   "comment": "VisB Visualization for Jars by Jonas Erdmann",
   "definitions":[
     {"name":"level",

Jars/Jars.svg

 <!--svg for Jars by Jonas Erdmann-->
-<svg width="360" height="360"
+<svg width="360" height="200"
   xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink">
   
 <g id="jar_3" transform="rotate(180 25 100)">
@@ -10,6 +10,7 @@
 	<line id="left_3" x1="50" y1="0" x2="50" y2="60" style="stroke:#000000;stroke-width:4"/>
 	<line id="right_3" x1="0" y1="0" x2="0" y2="60" style="stroke:#000000;stroke-width:4"/>
 	<line x1="50" y1="0" x2="0" y2="0" style="stroke:#000000;stroke-width:4"/>
+	</g>
 	</svg>
 </g>
 <text id="jar_3_text" opacity="1" x="20" y="95">0</text>
@@ -22,6 +23,7 @@
 	<line id="left_5" x1="50" y1="0" x2="50" y2="100" style="stroke:#000000;stroke-width:4"/>
 	<line id="right_5" x1="0" y1="0" x2="0" y2="100" style="stroke:#000000;stroke-width:4"/>
 	<line x1="50" y1="0" x2="0" y2="0" style="stroke:#000000;stroke-width:4"/>
+	</g>
 	</svg>
 </g>
 <text id="jar_5_text" opacity="1" x="125" y="95">0</text>
@@ -40,3 +42,4 @@
 <polyline id="transfer_right" points="85,45 79,41 79,49" fill="#00000"/>
 <rect id="transfer_sym3" x="76" y="43.5" height="3" width="3"/>
 <text id="goal_achieved" opacity="0" x="165" y="125" fill="purple" font-size="12" font-weight="bold">goal achieved!</text>
+</svg>
\ No newline at end of file

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