gistfile1.sm

ctmc

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

global next : [player_x..player_o] init player_x;
formula change_next = next = 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
	[] y2 = blank -> 100.0:(y2' = next)&(next' = change_next);

	[] x1 = blank -> (x1' = next)&(next' = change_next);
	[] x2 = blank -> (x2' = next)&(next' = change_next);
	[] x3 = blank -> (x3' = next)&(next' = change_next);
	[] y1 = blank -> (y1' = next)&(next' = change_next);
	[] y3 = blank -> (y3' = next)&(next' = change_next);
	[] z1 = blank -> (z1' = next)&(next' = change_next);
	[] z2 = blank -> (z2' = next)&(next' = change_next);
	[] z3 = blank -> (z3' = next)&(next' = change_next);
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);