blob: cddcb1d471cd97e46a73462b41466bcb05b55951 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
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
|