MODULE main
VAR
	turn : {p,q};
	wantp : boolean;
	wantq : boolean;
  procp : process user(turn, wantp, wantq, p, q);
  procq : process user(turn, wantq, wantp, q, p);
ASSIGN
	init(turn) := p;
	init(wantp) := FALSE;
	init(wantq) := FALSE;
--SPEC
  --AG (proc1.state = entering -> AF proc1.state = critical)

MODULE user(turn, wantp, wantq, myid, otherid)
VAR
  state : {p1,p2,p3,p4,p5,p6,p7,p8,p9,p10};
ASSIGN
  init(state) := p1;
  next(state) := 
    case 
      state = p1 : {p1,p2};
      state = p2 : p3;
      state = p3 & wantq = TRUE : p4;
			state = p3 & wantq = FALSE : p8;
      state = p4 & turn = otherid: p5;
			state = p4 & turn = myid: p3;
			state = p5 : p6;
			state = p6 & turn = myid : p7;
			state = p7 : p3;
			state = p8 : p9;
			state = p9 : p10;
			state = p10 : p1;
      TRUE : state;
    esac;
		
	next(turn) :=
		case
			next(state) = p10 : otherid;
			TRUE : turn;
		esac;
		
  next(wantp) := 
    case
      next(state) = p3 & state != p4 : TRUE;
			next(state) = p6 : FALSE;
			next(state) = p1 & state = p10 : FALSE;
      TRUE : wantp;
    esac;
FAIRNESS
  running