ticketlock.cfg


1
2
3
4
5
6
7
8
9
10
11
12
13

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

CONSTANTS	PROCS = {p1, p2, p3, p4}
		MAXVAL = 3
		TRYLOCK = FALSE

INVARIANTS	TypeInv
		ExclInv

PROPERTIES	\*LockAny
		LockAll		\* Not satisfied by trylock