1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
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
|
