From 7f58d86d3493286e8cf27a5714d0eb884d637d91 Mon Sep 17 00:00:00 2001 From: Aditya Naik Date: Fri, 8 Dec 2017 19:06:57 -0500 Subject: initial --- xnos.tla | 52 ++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 52 insertions(+) create mode 100644 xnos.tla diff --git a/xnos.tla b/xnos.tla new file mode 100644 index 0000000..a0587a2 --- /dev/null +++ b/xnos.tla @@ -0,0 +1,52 @@ +-------------------------------- MODULE xnos -------------------------------- +EXTENDS Integers +VARIABLES board, row1, row2, row3, curr + +Init == /\ row1 = <<0,0,0>> +/\ row2 = <<0,0,0>> +/\ row3 = <<0,0,0>> +/\ curr = 1 +/\ board = <> + + +Move(row, col, player) == +/\ board[row][col] = 0 +/\ curr = player +/\ IF row = 1 THEN + /\ row1' = [i \in 1..3 |-> IF i = col THEN player ELSE row1[i]] + /\ UNCHANGED <> + ELSE IF row = 2 THEN + /\ row2' = [i \in 1..3 |-> IF i = col THEN player ELSE row2[i]] + /\ UNCHANGED <> + ELSE + /\ row3' = [i \in 1..3 |-> IF i = col THEN player ELSE row3[i]] + /\ UNCHANGED <> +/\ IF player = 1 THEN curr' = 2 ELSE curr' = 1 +/\ board' = <> + +\* p1: 1, p2: 2 +Next == \E row \in 1..3 : \E col \in 1..3: + Move(row,col,1) \/ Move(row,col,2) + +\* P1 or P2 victory invariants +P1NotWinning == +/\ \neg (\E i \in 1..3 : + /\ (board[1][i] = 1 /\ board[2][i] = 1 /\ board[3][i] = 1) + /\ (board[i][1] = 1 /\ board[i][2] = 1 /\ board[i][3] = 1) + ) +/\ \neg (board[1][1] = 1 /\ board[2][2] = 1 /\ board[3][3] = 1) +/\ \neg (board[1][3] = 1 /\ board[2][2] = 1 /\ board[3][3] = 1) + +P2NotWinning == +/\ \neg (\E i \in 1..3 : + /\ (board[1][i] = 2 /\ board[2][i] = 2 /\ board[3][i] = 2) + /\ (board[i][1] = 2 /\ board[i][2] = 2 /\ board[i][3] = 2) + ) +/\ \neg (board[1][1] = 2 /\ board[2][2] = 2 /\ board[3][3] = 2) +/\ \neg (board[1][3] = 2 /\ board[2][2] = 2 /\ board[3][3] = 2) + + +============================================================================= +\* Modification History +\* Last modified Fri Dec 08 18:53:10 EST 2017 by aditya +\* Created Thu Dec 07 21:45:57 EST 2017 by aditya -- cgit v1.2.3