MODULE main

VAR

state1: {n1, t1, c1};

ASSIGN

init(state1) := n1;

next(state1) := 
case
   (state1 = n1) & ((state2 = t2)| (state3 = t3)): t1;
   (state1 = n1) & ((state2 = n2)| (state3 = n3)): t1;
   (state1 = n1) & ((state2 = c2)| (state3 = c3)): t1;
   (state1 = t1) & ((state2 = n2)| (state3 = n3)): c1;
   (state1 = t1) & ((state2 = t2)| (state3 = t3)) & (turn = 1):  c1;
   (state1 = c1): n1;
   1: state1;
esac;


VAR

state2: {n2, t2, c2};

ASSIGN

init(state2) := n2;

next(state2) := 
case
   (state2 = n2) & ((state1 = t1) | (state3 = t3)): t2;
   (state2 = n2) & ((state1 = n1) | (state3 = n3)): t2;
   (state2 = n2) & ((state1 = c1) | (state3 = c3)): t2;
   (state2 = t2) & ((state1 = n1) | (state3 = n3)): c2;
   (state2 = t2) & ((state1 = t1) | (state3 = t3)) & (turn = 2):  c2;
   (state2 = c2): n2;
   1: state2;
esac;


VAR

state3: {n3, t3, c3};

ASSIGN

init(state3) := n3;

next(state3) := 
case
   (state3 = n3) & ((state2 = t2) | (state1 = t1)): t3;
   (state3 = n3) & ((state2 = n2) | (state1 = n1)): t3;
   (state3 = n3) & ((state2 = c2) | (state1 = c1)): t3;
   (state3 = t3) & ((state2 = n2) | (state1 = n1)): c3;
   (state3 = t3) & ((state2 = t2) | (state1 = t1)) & (turn = 3):  c3;
   (state3 = c3): n3;
   1: state3;
esac;



VAR

turn: {1, 2, 3};

ASSIGN

init(turn) := 1;

next(turn) := 
case
   (state1 = n1) & (state2 = n2) & (state3 = t3): 3;
   (state1 = n1) & (state2 = t2) & (state3 = n3): 2;
   (state1 = t1) & (state2 = n2) & (state3 = n3): 1;
   1: turn;
esac;