| SPECIFICATION Spec | |
| CONSTANT defaultInitValue = defaultInitValue | |
| \* Add statements after this line. | |
| CONSTANTS CPUS = {p1, p2} | |
| TASKS = {t1, t2, t3, t4, t5, t6} | |
| ASIDS = 4 | |
| GENERATIONS = 3 | |
| CnP = FALSE | |
| SYMMETRY Perms | |
| CONSTRAINTS Constr | |
| INVARIANTS TypeInv | |
| UniqueASIDAllCPUs | |
| UniqueASIDPerCPU | |
| SameASIDActiveTask | |
| UniqueASIDActiveTask |