SPECIFICATION Spec
\* Add statements after this line.

CONSTANTS	READERS = {r1, r2}
		WRITERS = {w1, w2}
		INTERRUPTS = FALSE	\* Liveness properties not guaranteed
		TRYLOCK = FALSE		\* when testing interrupts or trylock

\*SYMMETRY	Perms			\* Disable for liveness properties

\* Safety
INVARIANTS	TypeInv
		RWExcl
		WWExcl

\* Liveness
PROPERTIES	LockAll			\* Not satisfied with interrupts or trylock
		\*LockAny		\* Unnecessary if testing LockAll