------------------------------------------------------------------------------- -- NuSMV model implementing the "tris" (tic-tac-toe) puzzle -- -- X | | -- ____|___|____ -- | X | -- ____|___|____ -- O | | O -- | | -- -- Numbering of the board squares: -- -- 1 | 2 | 3 -- ____|___|____ -- 4 | 5 | 6 -- ____|___|____ -- 7 | 8 | 9 -- | | ------------------------------------------------------------------------------- MODULE main -- players VAR player : 1..2; -- Let us assume that the player 1 is starting -- Players then move alternatively ASSIGN init(player) := 1; next(player) := case GameOver : player; player = 1 : 2; player = 2 : 1; esac; -- Move counter and Possible moves VAR -- MV_Count = 0 when the game finishes MV_Count : 0..9; move : array 1..9 of 0..9; -- the board -- "0" means empty, "1" filled by player 1, "2" filled by player 2 B1 : Board(1,MV_Count,move,player); B2 : Board(2,MV_Count,move,player); B3 : Board(3,MV_Count,move,player); B4 : Board(4,MV_Count,move,player); B5 : Board(5,MV_Count,move,player); B6 : Board(6,MV_Count,move,player); B7 : Board(7,MV_Count,move,player); B8 : Board(8,MV_Count,move,player); B9 : Board(9,MV_Count,move,player); ASSIGN init(MV_Count) := 1; next(MV_Count) := case GameOver: MV_Count; MV_Count < 9 & ! Win1 & ! Win2: MV_Count + 1; 1 : 0; esac; -- The initial moves are are set to zero apart from move[1] init(move[1]) := 1..9; init(move[2]) := 0; init(move[3]) := 0; init(move[4]) := 0; init(move[5]) := 0; init(move[6]) := 0; init(move[7]) := 0; init(move[8]) := 0; init(move[9]) := 0; -- move changes only at its turn next(move[1]) := move[1]; next(move[2]) := case next(MV_Count) = 2 : 1..9; 1 : move[2]; esac; next(move[3]) := case next(MV_Count) = 3 : 1..9; 1 : move[3]; esac; next(move[4]) := case next(MV_Count) = 4 : 1..9; 1 : move[4]; esac; next(move[5]) := case next(MV_Count) = 5 : 1..9; 1 : move[5]; esac; next(move[6]) := case GameOver : move[6]; next(MV_Count) = 6 : 1..9; 1 : move[6]; esac; next(move[7]) := case GameOver : move[7]; next(MV_Count) = 7 : 1..9; 1 : move[7]; esac; next(move[8]) := case GameOver : move[8]; next(MV_Count) = 8 : 1..9; 1 : move[8]; esac; next(move[9]) := case GameOver : move[9]; next(MV_Count) = 9 : 1..9; 1 : move[9]; esac; -- Successive moves must avoid occupied cells TRANS next(MV_Count) = 2 -> !(next(move[2]) = move[1]); TRANS next(MV_Count) = 3 -> !(next(move[3]) = move[1])& !(next(move[3]) = move[2]); TRANS next(MV_Count) = 4 -> !(next(move[4]) = move[3])& !(next(move[4]) = move[2])& !(next(move[4]) = move[1]); TRANS next(MV_Count) = 5 -> !(next(move[5]) = move[4])& !(next(move[5]) = move[3])& !(next(move[5]) = move[2])& !(next(move[5]) = move[1]); TRANS next(MV_Count) = 6 -> !(next(move[6]) = move[5])& !(next(move[6]) = move[4])& !(next(move[6]) = move[3])& !(next(move[6]) = move[2])& !(next(move[6]) = move[1]); TRANS next(MV_Count) = 7 -> !(next(move[7]) = move[6])& !(next(move[7]) = move[5])& !(next(move[7]) = move[4])& !(next(move[7]) = move[3])& !(next(move[7]) = move[2])& !(next(move[7]) = move[1]); TRANS next(MV_Count) = 8 -> !(next(move[8]) = move[7])& !(next(move[8]) = move[6])& !(next(move[8]) = move[5])& !(next(move[8]) = move[4])& !(next(move[8]) = move[3])& !(next(move[8]) = move[2])& !(next(move[8]) = move[1]); TRANS next(MV_Count) = 9 -> !(next(move[9]) = move[8])& !(next(move[9]) = move[7])& !(next(move[9]) = move[6])& !(next(move[9]) = move[5])& !(next(move[9]) = move[4])& !(next(move[9]) = move[3])& !(next(move[9]) = move[2])& !(next(move[9]) = move[1]); -- "Win1" means player 1 wins -- "Win2" means player 2 wins DEFINE Win1 := (B1.value=1 & B2.value=1 & B3.value=1) | (B4.value=1 & B5.value=1 & B6.value=1) | (B7.value=1 & B8.value=1 & B9.value=1) | (B1.value=1 & B4.value=1 & B7.value=1) | (B2.value=1 & B5.value=1 & B8.value=1) | (B3.value=1 & B6.value=1 & B9.value=1) | (B1.value=1 & B5.value=1 & B9.value=1) | (B3.value=1 & B5.value=1 & B7.value=1); Win2 := (B1.value=2 & B2.value=2 & B3.value=2) | (B4.value=2 & B5.value=2 & B6.value=2) | (B7.value=2 & B8.value=2 & B9.value=2) | (B1.value=2 & B4.value=2 & B7.value=2) | (B2.value=2 & B5.value=2 & B8.value=2) | (B3.value=2 & B6.value=2 & B9.value=2) | (B1.value=2 & B5.value=2 & B9.value=2) | (B3.value=2 & B5.value=2 & B7.value=2); GameOver := (Win1 | Win2); -- SPECIFICATIONS -- PLAYER 2 -- player 2 does not have a "winning" strategy -- SPEC -- !(EX (AX (EX (AX (EX (AX (EX (AX Win2)))))))) -- player 2 has a "non-losing" strategy -- SPEC -- EX (AX (EX (AX (EX (AX (EX (AX !Win1))))))) -- player 2 has also a "non-winning" strategy -- SPEC -- EX (AX (EX (AX (EX (AX (EX (AX !Win2))))))) -- player 2 does not have a "losing" strategy -- SPEC -- !(EX (AX (EX (AX (EX (AX (EX (AX Win1)))))))) -- PLAYER 1 -- player 1 does not have a "winning" strategy --SPEC --!(AX (EX (AX (EX (AX (EX (AX (EX Win1)))))))) -- player 1 has a "non-losing" strategy -- SPEC -- AX (EX (AX (EX (AX (EX (AX (EX !Win2))))))) -- player 1 has also a "non-winning" strategy --SPEC -- player 1 does not have a "losing" strategy -- SPEC -- player 1 has a possibility to win LTLSPEC F Win2 -------------------------------------------- -- THE BOARD MODULE -------------------------------------------- MODULE Board(cell,MV_Count,move,player) -- initially, all squares are empty apart from -- the square denoted by the current move VAR value : 0..2; ASSIGN init(value) := case move[1] = cell : player; 1 : 0; esac; next(value) := case next(MV_Count) = 2 : case next(move[2]) = cell : next(player); 1 : value; esac; next(MV_Count) = 3 : case next(move[3]) = cell : next(player); 1 : value; esac; next(MV_Count) = 4 : case next(move[4]) = cell : next(player); 1 : value; esac; next(MV_Count) = 5 : case next(move[5]) = cell : next(player); 1 : value; esac; next(MV_Count) = 6 : case next(move[6]) = cell : next(player); 1 : value; esac; next(MV_Count) = 7 : case next(move[7]) = cell : next(player); 1 : value; esac; next(MV_Count) = 8 : case next(move[8]) = cell : next(player); 1 : value; esac; next(MV_Count) = 9 : case next(move[9]) = cell : next(player); 1 : value; esac; 1 : value; esac;