MODULE phil(leftfork, rightfork)
VAR
	state: {none, left, both};
ASSIGN
	init(state) := none;
	next(state) := case
		state=none: case
			leftfork=inuse: none;
			TRUE: {none, left};
		esac;
		state=left: case
--			rightfork=inuse: left;
			rightfork=inuse: {none, left};
--			TRUE: {left, both};
			TRUE: {none, left, both};
		esac;
		TRUE: none;
	esac;
JUSTICE state=both

MODULE main
VAR
	f: array 0..6 of {free, inuse};
	ph0: phil(f[6], f[1]);
	ph1: phil(f[0], f[2]);
	ph2: phil(f[1], f[3]);
	ph3: phil(f[2], f[4]);
	ph4: phil(f[3], f[5]);
	ph5: phil(f[4], f[6]);
	ph6: phil(f[5], f[0]);
ASSIGN
	init(f[0]) := free;
	init(f[1]) := free;
	init(f[2]) := free;
	init(f[3]) := free;
	init(f[4]) := free;
	init(f[5]) := free;
	init(f[6]) := free;

	next(f[0]) := case
		next(ph6.state)=both | next(ph1.state)=left | next(ph0.state)=both: inuse;
		TRUE: free;
	esac;
	next(f[1]) := case
		next(ph0.state)=both | next(ph2.state)=left | next(ph2.state)=both: inuse;
		TRUE: free;
	esac;
	next(f[2]) := case
		next(ph1.state)=both | next(ph3.state)=left | next(ph3.state)=both: inuse;
		TRUE: free;
	esac;
	next(f[3]) := case
		next(ph2.state)=both | next(ph4.state)=left | next(ph4.state)=both: inuse;
		TRUE: free;
	esac;
	next(f[4]) := case
		next(ph3.state)=both | next(ph5.state)=left | next(ph5.state)=both: inuse;
		TRUE: free;
	esac;
	next(f[5]) := case
		next(ph4.state)=both | next(ph6.state)=left | next(ph6.state)=both: inuse;
		TRUE: free;
	esac;
	next(f[6]) := case
		next(ph5.state)=both | next(ph0.state)=left | next(ph0.state)=both: inuse;
		TRUE: free;
	esac;
--This finds a deadlock
LTLSPEC F(
	ph0.state=left &
	ph1.state=left &
	ph2.state=left &
	ph3.state=left &
	ph4.state=left &
	ph5.state=left &
	ph6.state=left)

--Checks starvation
CTLSPEC AG(
	(EF (ph0.state=both)) &
	(EF (ph1.state=both)) &
	(EF (ph2.state=both)) &
	(EF (ph3.state=both)) &
	(EF (ph4.state=both)) &
	(EF (ph5.state=both)) &
	(EF (ph6.state=both)))