CONSTANT defaultInitValue = defaultInitValue
\* Add statements after this line.

SPECIFICATION PreemptSpec

CONSTANTS PROCS = {p1, p2}
	  TASKS = {t1, t2, t3}
	  MMS = {m1, m2}

INVARIANTS TypeInv
	   SchedInv
	   MMInv

SYMMETRY Perms