[tlaplus] Reproducing deadlock in TLA+

I'm trying to reproduce a deadlock from Herlihy's "The Art of Multiprocessor Programming" in TLA+. In the following code when a thread wants to acquire a lock it marks itself as a victim and proceed only when another thread becomes a victim. There is a deadlock here if another thread never comes.

```
class LockTwo implements Lock {
private int victim;

public void lock() {
    int i = ThreadID.get();
    victim = i; // let the other go first
    while (victim == i) {} // wait
}

public void unlock() {}
}
```

The TLA+ spec is as follows:

```
------------------------------ MODULE LockTwo ------------------------------

CONSTANT Thread

VARIABLE victim, owner, wasVictim

Null == CHOOSE v: v \notin Thread

Init ==
/\ victim = Null
/\ owner = [t \in Thread |-> FALSE]
/\ wasVictim = [t \in Thread |-> FALSE]

TypeOK ==
/\ victim \in Thread \cup {Null}
/\ owner \in [Thread -> BOOLEAN]
/\ wasVictim \in [Thread -> BOOLEAN]

BecomeVictim(t) ==
/\ wasVictim[t] = FALSE
/\ owner[t] = FALSE
/\ victim' = t
/\ wasVictim' = [wasVictim EXCEPT ![t] = TRUE]
/\ UNCHANGED owner

AcquireLock(t) ==
/\ wasVictim[t] = TRUE
/\ victim # t
/\ owner' = [owner EXCEPT ![t] = TRUE]
/\ wasVictim' = [wasVictim EXCEPT ![t] = FALSE]
/\ UNCHANGED victim

ReleaseLock(t) ==
/\ owner[t] = TRUE
/\ owner' = [owner EXCEPT ![t] = FALSE]
/\ UNCHANGED <<victim, wasVictim>>

Next ==
\E t \in Thread: BecomeVictim(t) \/ AcquireLock(t) \/ ReleaseLock(t)

MutualExclusion ==
\A t1, t2 \in Thread: (t1 # t2) => ~ (owner[t1] /\ owner[t2])

EventualSuccess ==
\A t \in Thread: (victim = t) ~> owner[t]

Spec == Init /\ [][Next]_<<victim, owner, wasVictim>> /\ EventualSuccess

=============================================================================
```

TLA spec runs fine with Thread = {t1, t2} where t1 and t2 are model values.

How to make TLA to report a deadlock when one thread wants to lock but another one never comes?