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

CONSTANTS	CPUS = {p1, p2}
		TASKS = {t1, t2, t3, t4, t5, t6}
		TTU = ttu
		ASIDS = 4
		GENERATIONS = 3
		CnP = FALSE

SYMMETRY	Perms

CONSTRAINTS	Constr

INVARIANTS	TypeInv
		UniqueASIDAllCPUs
		UniqueASIDPerCPU
		SameASIDActiveTask
		UniqueASIDActiveTask
		TLBEmptyInvalPTE