\* Direct-TLC check for DLV-0012 deadlock-freedom via canonical lock ordering.
\* Run from specs/: java -jar tla2tools.jar -config LockOrderModel.cfg LockOrderModel.tla
\* Deadlock detection is left ON (default): it corroborates NoWaitCycle by
\* confirming no reachable state is a total deadlock.
SPECIFICATION LockSpec
INVARIANT DeadlockFree