See MutualExclusionSpec.tla

	Any processes may take arbitrarily long to execute its noncritical
	section, and may even halt there.  Other processes must be able to enter the
	critical section without having to wait for those processes to complete the
	noncritical section.