Skip to content

Commit

Permalink
Added a fast -- list based -- version of tictactoe.
Browse files Browse the repository at this point in the history
The standard version of tictactoe uses functions and
function updates and is rather slow. This model is
remarkably fast.
  • Loading branch information
jgroote committed May 2, 2021
1 parent dec0b63 commit ce8020d
Showing 1 changed file with 54 additions and 0 deletions.
54 changes: 54 additions & 0 deletions examples/games/tictactoe/tictactoe_fast.mcrl2
Original file line number Diff line number Diff line change
@@ -0,0 +1,54 @@
% This file shows the game tic-tac-toe modelled using
% functions.
%
% This example is used to generate the state space of this game
% to which a reference is made in the Coursera specialisation on System
% validation made in 2015.
%
% Jan Friso Groote, March 2015.

sort Piece = struct empty | naught | cross;
Row = List(Piece);
Board = List(Row);

map empty_board:Board;
other:Piece->Piece;
get:Nat#Nat#Board -> Piece;
get:Nat#Row -> Piece;
set:Nat#Nat#Piece#Board -> Board;
set:Nat#Piece#Row -> Row;
did_win:Piece#Board->Bool;

var b:Board;
r:Row;
p,p':Piece;
i,j:Nat;
eqn empty_board=[[empty, empty, empty],
[empty, empty, empty],
[empty, empty, empty]];
other(naught)=cross;
other(cross)=naught;
get(i,j,b)=get(i,b.j);
get(i,r)=r.i;
j==0 -> set(i,j,p,r|>b)=set(i,p,r)|>b;
j>0 -> set(i,j,p,r|>b)=r|>set(i,max(0,j-1),p,b);
i==0 -> set(i,p,p'|>r)=p|>r;
i>0 -> set(i,p,p'|>r)=p'|>set(max(0,i-1),p,r);
var b:Board;
p:Piece;
eqn did_win(p,b)=(exists i:Nat.(i<3 && get(i,0,b)==p && get(i,1,b)==p && get(i,2,b)==p)) ||
(exists j:Nat.(j<3 && get(0,j,b)==p && get(1,j,b)==p && get(2,j,b)==p)) ||
(get(0,0,b)==p && get(1,1,b)==p && get(2,2,b)==p) ||
(get(0,2,b)==p && get(1,1,b)==p && get(2,0,b)==p);


act win:Piece;
put:Piece#Nat#Nat;
proc TicTacToe(board:Board, player:Piece)=
did_win(other(player),board)
-> win(other(player)).delta
<> ( sum i,j:Nat.(i<3 && j<3 && get(i,j,board)==empty)->
put(player,i,j).
TicTacToe(set(i,j,player,board),other(player)));

init TicTacToe(empty_board,cross);

0 comments on commit ce8020d

Please sign in to comment.