initial

1 files changed, 52 insertions, 0 deletions

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 = <<row1, row2, row3>>
+
+
+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 <<row2, row3>>
+    ELSE IF row = 2 THEN 
+        /\ row2' = [i \in 1..3 |-> IF i = col THEN player ELSE row2[i]]
+        /\ UNCHANGED <<row1, row3>>
+    ELSE 
+        /\ row3' = [i \in 1..3 |-> IF i = col THEN player ELSE row3[i]]
+        /\ UNCHANGED <<row1, row2>>
+/\ IF player = 1 THEN curr' = 2 ELSE curr' = 1
+/\ board' = <<row1, row2, row3>>
+
+\* 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