blob: fd0513743721c45c2b3acb9b2b6f9b0a04eac8d7 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
SPECIFICATION Spec
\* Add statements after this line.
CONSTANTS READERS = {r1, r2}
WRITERS = {w1, w2}
INTERRUPTS = FALSE \* Liveness properties not guaranteed
TRYLOCK = FALSE \* when testing interrupts or trylock
\*SYMMETRY Perms \* Disable for liveness properties
\* Safety
INVARIANTS TypeInv
RWExcl
WWExcl
\* Liveness
PROPERTIES LockAll \* Not satisfied with interrupts or trylock
\*LockAny \* Unnecessary if testing LockAll
|
