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

CONSTANTS	CPUS = {p1}
		THREADS = {t1, t2}
		VALS = {v1, v2}

SYMMETRY	Perms

INVARIANTS	TypeInv
		SchedInv