Minor spec fix.

specs/Init.cfg

@@ -18,8 +18,14 @@ PROPERTIES
   NoShimResets
 
 CONSTANTS
+  \* Concurrent threads
   THREADS = {1, 2}
   NoThread = 0
+  \* Library functions
   FUNS = {"foo", "bar"}
+  \* Number of calls in each thread and in library ctor
   CALLS = 2
+  \* Max callstack size
   DEPTH = 2
+  \* Max number of recursive mutex locks
+  MAX_LOCK = 3

specs/Init.tla

@@ -9,7 +9,7 @@ EXTENDS
   Integers, FiniteSets, Sequences, TLC
 
 CONSTANTS
-  THREADS, FUNS, CALLS, DEPTH
+  THREADS, FUNS, CALLS, DEPTH, MAX_LOCK
 
 ASSUME
   /\ Cardinality(FUNS) > 0
@@ -46,7 +46,6 @@ StackFrame == [pc : PC, calls : 0..CALLS, callee : Callees]
 
 CallStack == UNION {[1..len -> StackFrame] : len \in 0..DEPTH}
 
-MaxLock == 3
 
 \* HELPERS
 
@@ -65,7 +64,7 @@ TypeInvariant ==
   /\ shim_table \in [FUNS -> BOOLEAN]
   /\ lib_handle_set \in BOOLEAN
   /\ lib_state \in LibraryState
-  /\ rec_lock \in [owner : THREADS \union {NoThread}, count : 0..MaxLock]
+  /\ rec_lock \in [owner : THREADS \union {NoThread}, count : 0..MAX_LOCK]
 
 LockInvariant ==
   /\