From 28731a9c0279d6e9339ee30d9caa53bb162c7e2d Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@uni-duesseldorf.de>
Date: Tue, 2 Jan 2024 17:40:19 +0100
Subject: [PATCH] add TicTacToe TLA+ version
---
TicTacToe/tictactoe_grid.svg | 18 +++
TicTacToe/tictactoe_v2.tla | 101 +++++++++++++++++
TicTacToe/tictactoe_visb.json | 207 ++++++++++++++++++++++++++++++++++
3 files changed, 326 insertions(+)
create mode 100644 TicTacToe/tictactoe_grid.svg
create mode 100644 TicTacToe/tictactoe_v2.tla
create mode 100644 TicTacToe/tictactoe_visb.json
diff --git a/TicTacToe/tictactoe_grid.svg b/TicTacToe/tictactoe_grid.svg
new file mode 100644
index 0000000..50bf42f
--- /dev/null
+++ b/TicTacToe/tictactoe_grid.svg
@@ -0,0 +1,18 @@
+<?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>
diff --git a/TicTacToe/tictactoe_v2.tla b/TicTacToe/tictactoe_v2.tla
new file mode 100644
index 0000000..7b7760b
--- /dev/null
+++ b/TicTacToe/tictactoe_v2.tla
@@ -0,0 +1,101 @@
+---------------------------- 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
+=============================================================================
diff --git a/TicTacToe/tictactoe_visb.json b/TicTacToe/tictactoe_visb.json
new file mode 100644
index 0000000..c0128dd
--- /dev/null
+++ b/TicTacToe/tictactoe_visb.json
@@ -0,0 +1,207 @@
+{
+ "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"}]
+ }
+ ]
+}
--
GitLab