TicTacToe/tictactoe_grid.svg

+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<svg
+   xmlns="http://www.w3.org/2000/svg"
+   height="400" width="400"
+   viewBox="-2 -2 55 40"
+   >
+       <text  text-align="left"  x="0"  y="35" font-size="2"
+        font-family="sans-serif">
+       <tspan id="visb_debug_messages_opt"> </tspan>
+
+    
+  <filter id="displacementFilter">
+    <feTurbulence type="turbulence" baseFrequency="0.05"
+        numOctaves="2" result="turbulence"/>
+    <feDisplacementMap in2="turbulence" in="SourceGraphic"
+        scale="1.2" xChannelSelector="R" yChannelSelector="G"/>
+  </filter>
+</svg>

TicTacToe/tictactoe_v2.tla

+---------------------------- MODULE tictactoe_v2 ----------------------------
+(* taken from https://elliotswart.github.io/pragmaticformalmodeling/ *)
+(* version adapted for TLA2B so that we can have B-style operations with parameters for VisB *)
+(* also contains GAME state definitions for ProB so that we can use MCTS *)
+EXTENDS Naturals
+
+VARIABLES 
+    board, \* board[1..3][1..3] A 3x3 tic-tac-toe board
+    nextTurn \* who goes next
+
+Pieces == {"X", "O", "_"} \* "_" represents a blank square
+
+Init ==
+        /\ nextTurn = "X" \* X always goes first
+        \* Every space in the board states blank
+        /\ board = [i \in 1..3 |-> [j \in 1..3 |-> "_"]]
+
+MoveO ==
+    \E i \in 1..3: \E j \in 1..3: \* There exists a position on the board
+        /\ nextTurn = "O" \* Only enabled on player's turn
+        /\ nextTurn' = "X" \* The future state of next turn is other player
+        /\ board[i][j] = "_" \* Where the board is currently empty
+        (********************************************************************)
+        (* The future state of board is the same, except a piece is in that *)
+        (* spot                                                             *)
+        (********************************************************************)
+        /\ board' = [board EXCEPT
+                        ![i][j] = "O"] 
+
+MoveX ==
+    \E i \in 1..3: \E j \in 1..3: \* There exists a position on the board
+        /\ nextTurn = "X" \* Only enabled on player's turn
+        /\ nextTurn' = "O" \* The future state of next turn is other player
+        /\ board[i][j] = "_" \* Where the board is currently empty
+        (********************************************************************)
+        (* The future state of board is the same, except a piece is in that *)
+        (* spot                                                             *)
+        (********************************************************************)
+        /\ board' = [board EXCEPT
+                        ![i][j] = "X"] 
+
+\* Every state, X will move if X's turn, O will move on O's turn
+Next == MoveX \/ MoveO
+
+\* A description of every possible game of tic-tac-toe
+\* will play until the board fills up, even if someone won
+Spec == Init /\ [][Next]_<<board,nextTurn>>
+
+(***************************************************************************)
+(* Invariants: The things we are checking for.                             *)
+(***************************************************************************)
+
+WinningPositions == {
+    \* Horizonal wins
+    {<<1,1>>, <<1,2>>, <<1,3>>},
+    {<<2,1>>, <<2,2>>, <<2,3>>},
+    {<<3,1>>, <<3,2>>, <<3,3>>},
+    \* Vertical wins
+    {<<1,1>>, <<2,1>>, <<3,1>>},
+    {<<1,2>>, <<2,2>>, <<3,2>>},
+    {<<1,3>>, <<2,3>>, <<3,3>>},
+    \* Diagonal wins
+    {<<1,1>>, <<2,2>>, <<3,3>>},
+    {<<3,1>>, <<2,2>>, <<1,3>>}
+}
+
+Won(player) == 
+    \* A player has won if there exists a winning position
+    \E winningPosition \in WinningPositions:
+        \* Where all the needed spaces
+        \A neededSpace \in winningPosition:
+            \* are occupied by one player
+            board[neededSpace[1]][neededSpace[2]] = player
+
+XHasNotWon == ~Won("X")
+OHasNotWon == ~Won("O")
+
+BoardFilled ==
+    \* There does not exist
+    ~\E i \in 1..3, j \in 1..3:
+        \* an empty space
+        LET space == board[i][j] IN
+        space = "_"
+
+\* It's not a stalemate if one player has won or the board is not filled
+NotStalemate ==
+    \/ Won("X")
+    \/ Won("O")
+    \/ ~BoardFilled
+
+\* additions for ProB:
+VISB_JSON_FILE == "tictactoe_visb.json"
+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_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
+=============================================================================

TicTacToe/tictactoe_visb.json

+{
+  "svg": "tictactoe_grid.svg",
+  "comment": "version which uses new svg object creation",
+  "definitions": [
+    { "name":"x_offset",
+      "value" : "4"
+    },
+    { "name":"center",
+      "value" : "%i.(i:INTEGER|5+10*(i-1))"
+    },
+    { "name":"vert_line_a",
+      "value":"%(i,j).(i:INTEGER & j:INTEGER | TO_STRING(center(i)+x_offset) ^ \" \" ^ TO_STRING(center(j)-x_offset)  ^ \" \" ^ TO_STRING(center(i)-x_offset) ^ \" \" ^ TO_STRING(center(j)+x_offset))"
+    },
+    { "name":"vert_line_b",
+      "value":"%(i,j).(i:INTEGER & j:INTEGER | TO_STRING(center(i)+x_offset) ^ \" \" ^ TO_STRING(center(j)+x_offset)  ^ \" \" ^ TO_STRING(center(i)-x_offset) ^ \" \" ^ TO_STRING(center(j)-x_offset))"
+    }
+  ],
+  "svg_objects":[
+    {
+      "for":{"from":1,"to":"3"}, 
+      "for":{"from":1,"to":3}, 
+      "svg_class":"rect",
+      "id":"grid%0_%1",
+      "x":"10*(%0-1)",
+      "y":"10*(%1-1)",
+      "width":"10",
+      "height" : "10",
+      "stroke":"black",
+      "stroke-width":"0.25",
+      "fill":"white"
+    },
+    {
+      "for":{"from":1,"to":"3"}, 
+      "for":{"from":1,"to":"3"}, 
+      "svg_class":"circle",
+      "id":"pieceO%0_%1",
+      "cx":"center(%0)",
+      "cy":"center(%1)",
+      "r":"4.5",
+      "stroke":"red",
+      "stroke-width":"0.5",
+      "style": "",
+      "fill":"white"
+    },
+    {
+      "for":{"from":1,"to":"3"}, 
+      "for":{"from":1,"to":"3"}, 
+      "repeat": ["a","b"],
+      "svg_class":"polyline",
+      "id":"pieceX%0_%1_%2",
+      "points":"0 0 10 10",
+      "stroke":"blue",
+      "stroke-width":"0.5",
+      "style": "",
+      "fill":"white"
+    },
+    {
+      "svg_class":"rect",
+      "id":"winnerRect",
+      "x":"10*(5-1)",
+      "y":"10*(2-1)",
+      "width":"10",
+      "height" : "10",
+      "stroke":"black",
+      "stroke-width":"0.25",
+      "fill":"white"
+    },
+    {
+      "svg_class":"rect",
+      "id":"mctsRect",
+      "x":"10*(5-1)",
+      "y":"10.0*(2.0)+2.5",
+      "width":"10",
+      "height" : "5",
+      "stroke":"black",
+      "stroke-width":"0.25",
+      "fill":"lightgray"
+    },
+    {
+      "svg_class":"text",
+      "id":"winnerTxt",
+      "x":"40",
+      "y":"8",
+      "font-size":"3.0",
+      "font-family":"sans-serif",
+      "text":"Winner: "
+    },
+    {
+      "svg_class":"circle",
+      "id":"winnerO",
+      "cx":"center(5)",
+      "cy":"center(2)",
+      "r":"4.5",
+      "stroke":"red",
+      "stroke-width":"0.5",
+      "style": "",
+      "fill":"white"
+    },
+    {
+      "repeat": ["a","b"],
+      "svg_class":"polyline",
+      "id":"winnerX_%0",
+      "points":"0 0 10 10",
+      "stroke":"blue",
+      "stroke-width":"0.5",
+      "style": "",
+      "fill":"white"
+    },
+    {
+      "svg_class":"text",
+      "id":"mctsRectTxt",
+      "x":"41.6",
+      "y":"25.9",
+      "font-size":"2.5",
+      "font-family":"sans-serif",
+      "text":"MCTS"
+    }
+    ],
+  "items": [
+    { 
+      "for":{"from":1,"to":"3"}, 
+      "for":{"from":1,"to":3}, 
+      "id":"pieceO%0_%1",
+      "attr": "visibility",
+      "value": "IF board(%0)(%1) = \"O\" THEN \"visible\" ELSE \"hidden\" END"
+    },
+    { 
+      "for":{"from":1,"to":"3"}, 
+      "for":{"from":1,"to":3}, 
+      "repeat": ["a","b"],
+      "id":"pieceX%0_%1_%2",
+      "attr": "visibility",
+      "value": "IF board(%0)(%1) = \"X\" THEN \"visible\" ELSE \"hidden\" END"
+    },
+    { 
+      "id":"winnerO",
+      "attr": "visibility",
+      "value": "IF Won(\"O\") THEN \"visible\" ELSE \"hidden\" END"
+    },
+    { 
+      "repeat": ["a","b"],
+      "id":"winnerX_%0",
+      "attr": "visibility",
+      "value": "IF Won(\"X\") THEN \"visible\" ELSE \"hidden\" END"
+    },
+    { 
+      "id":"winnerTxt",
+      "attr": "text",
+      "value": "IF ran(union(ran(board)))={\"O\",\"X\"} & not(Won(\"X\")) & not(Won(\"O\")) THEN \"Draw !\" ELSE \"Winner:\" END"
+    },
+    { 
+      "for":{"from":1,"to":"3"}, 
+      "for":{"from":1,"to":3}, 
+      "repeat": ["a"],
+      "id":"pieceX%0_%1_%2",
+      "attr": "points",
+      "value": "vert_line_a(%0,%1)"
+    },
+    { 
+      "for":{"from":1,"to":"3"}, 
+      "for":{"from":1,"to":3}, 
+      "repeat": ["b"],
+      "id":"pieceX%0_%1_%2",
+      "attr": "points",
+      "value": "vert_line_b(%0,%1)"
+    },
+    { 
+      "id":"winnerX_a",
+      "attr": "points",
+      "value": "vert_line_a(5,2)"
+    },
+    { 
+      "id":"winnerX_b",
+      "attr": "points",
+      "value": "vert_line_b(5,2)"
+    }
+    ],
+  "events":[ 
+    {
+      "for":{"from":1,"to":"3"}, 
+      "for":{"from":1,"to":3}, 
+      "id":"grid%0_%1",
+      "optional": "true",
+      "event":"MoveX",
+      "predicates": [ "i=%0", "j=%1"],
+      "hovers": [{ "attr":"fill", "enter":"gray", "leave":"white"}]
+    },
+    {
+      "for":{"from":1,"to":"3"}, 
+      "for":{"from":1,"to":3}, 
+      "id":"grid%0_%1",
+      "optional": "true",
+      "event":"MoveO",
+      "predicates": [ "i=%0", "j=%1"]
+    },
+    { 
+      "id":"mctsRect",
+      "event": "MCTS_AUTO_PLAY",
+      "hovers": [{ "attr":"fill", "enter":"green", "leave":"lightgray"}]
+    },
+    { 
+      "id":"mctsRectTxt",
+      "event": "MCTS_AUTO_PLAY",
+      "hovers": [{ "id":"mctsRect", "attr":"fill", "enter":"green", "leave":"lightgray"}]
+    }
+    ]
+}