open util/ordering[Time]

sig Time {
	want : set Process,
	turn : one Process,
	label : Process -> one Label
}

abstract sig Process {}
one sig P1,P2 extends Process {}

abstract sig Label {}
one sig Idle, Want, Wait, Critical extends Label {}

pred want [p : Process, t,t' : Time] {
	t.label[p] = Idle
	t'.want = t.want + p
	t'.turn = t.turn
	t'.label = t.label - p->Label + p->Want
}

pred turn [p : Process, t,t' : Time] {
	t.label[p] = Want
	t'.want = t.want
	t'.turn = p
	t'.label = t.label - p->Label + p->Wait
}

pred enter [p : Process, t,t' : Time] {
	t.label[p] = Wait
	let other = Process - p | other not in t.want or t.turn = other
	t'.want = t.want
	t'.turn = t.turn
	t'.label = t.label - p->Label + p->Critical
}

pred exit [p : Process, t,t' : Time] {
	t.label[p] = Critical
	t'.want = t.want - p
	t'.turn = t.turn
	t'.label = t.label - p->Label + p->Idle
}

pred nop [p : Process, t,t' : Time] {
	t'.want = t.want
	t'.turn = t.turn
	t'.label = t.label
}

run {} for 10 Time

fact {
	no first.want
	first.label = Process->Idle

	all t : Time - last {
		some p : Process {
			want[p,t,t.next] or turn[p,t,t.next] or enter[p,t,t.next] or exit[p,t,t.next]
		}
	}
}

check MutualExclusion {
	all t : Time | lone t.label.Critical
} for 128 Time

check NoStarvation {
	all t : Time, p : Process | t.label[p] = Want implies some t' : t.*ordering/next | t'.label[p] = Critical
} for 10 Time