MODULE main
VAR

turn: {0,1,2};

pr1: process prc(pr2.status, turn, 1, 2);

pr2: process prc(pr1.status, turn, 2, 1);

ASSIGN

init(turn) := 0;

-- SAFETY: Is never the case that two processes are in their critical section
-- at the same time.
SPEC
!EF((pr1.status = critical) & (pr2.status = critical))

-- LIVENESS: When pr1 is trying it will get the resourse
-- SPEC
-- AG((pr1.status = trying) -> AF (pr1.status = critical))

LTLSPEC
 G F(!(pr2.status = critical)) -> G((pr1.status=trying) -> F(pr1.status=critical))

SPEC
 AG AF (!(pr2.status = critical)) -> AG((pr1.status = trying) -> AF(pr1.status = critical))

SPEC
 AG AF (!(pr2.status = critical))

SPEC
 AG EF (!(pr2.status = critical)) -> AG((pr1.status = trying) -> AF(pr1.status = critical))



MODULE prc(other-status, turn, myturn, other-turn)
VAR

status: {noncritical, trying, critical};

ASSIGN

init(status) := noncritical;

next(status) := 
case
   (status = noncritical) : trying;
   (status = trying):
	case
		(turn = myturn): critical;
		1	       : trying;
	esac;
   (status = critical) : {critical,noncritical};
   1: status;
esac;

next(turn) :=
case
   (turn =0): myturn;
   (turn = myturn) &  
   (next(status) = noncritical):
	case
		(other-status = noncritical): 0;
   		(other-status = trying): other-turn;
	esac;
   1: turn;
esac;

FAIRNESS
running

--FAIRNESS
--!(status=critical)