MODULE proc(i, s, yme, yother)
VAR
	line: {l2, l3, l4, l7, l8};
ASSIGN
	init(line):=l2;
	next(line):=case
		line=l2: {l2,l3};
		line=l3: {l3,l4};
		line=l4: case
			!(yother=0 | s!=i) : l4;
			TRUE: {l4,l7};
		esac;
		line=l7: {l7,l8};
		line=l8: {l8,l2};
	esac;
JUSTICE line=l7

MODULE main
VAR
	y0: 0..1;
	y1: 0..1;
	s: 0..1;
	proc0: proc(0, s, y0, y1);
	proc1: proc(1, s, y1, y0);
ASSIGN
	next(y0):=case
		proc0.line=l3: 1;
		proc0.line=l8: 0;
		TRUE: y0;
	esac;
	next(y1):=case
		proc1.line=l3: 1;
		proc1.line=l8: 0;
		TRUE: y1;
	esac;
	next(s):=case
		proc0.line=l3 & proc1.line=l3: {0,1};
		proc0.line=l3: 0;
		proc1.line=l3: 1;
		TRUE: s;
	esac;

--Mutual exclusion
LTLSPEC G(!(proc0.line=l7 & proc1.line=l7))

--Absence of starvation
LTLSPEC G (F(proc0.line=l7) & F(proc1.line=l7))