gistfile1.sm

ctmc

formula blank = 0;
formula player_x = 1;
formula player_o = 2;

formula change_current_player = current_player = player_x ? player_o : player_x;

module tictactoe
	x1 : [0..2] init blank;
	x2 : [0..2] init blank;
	x3 : [0..2] init blank;
	y1 : [0..2] init blank;
	y2 : [0..2] init blank;
	y3 : [0..2] init blank;
	z1 : [0..2] init blank;
	z2 : [0..2] init blank;
	z3 : [0..2] init blank;

	// A normal player will usually mark the center if it's blank
	[player_turn] y2 = blank -> 100.0:(y2' = current_player);

	[player_turn] x1 = blank -> (x1' = current_player);
	[player_turn] x2 = blank -> (x2' = current_player);
	[player_turn] x3 = blank -> (x3' = current_player);
	[player_turn] y1 = blank -> (y1' = current_player);
	[player_turn] y3 = blank -> (y3' = current_player);
	[player_turn] z1 = blank -> (z1' = current_player);
	[player_turn] z2 = blank -> (z2' = current_player);
	[player_turn] z3 = blank -> (z3' = current_player);
endmodule

module game_state
	current_player : [player_x..player_o] init player_x;
	
	[player_turn] true -> (current_player' = change_current_player);
endmodule

label "win" =  
	(x1 = x2 & x2 = x3 & x3 != blank) |
	(y1 = y2 & y2 = y3 & y3 != blank) |
	(z1 = z2 & z2 = z3 & z3 != blank) |
	(x1 = y1 & y1 = z1 & z1 != blank) |
	(x2 = y2 & y2 = z2 & z2 != blank) |
	(x3 = y3 & y3 = z3 & z3 != blank) |
	(x1 = y2 & y2 = z3 & z3 != blank) |
	(x3 = y2 & y2 = z1 & z1 != blank);