[SOLVED] How can I get a diagnostic for unreached code?

(TLA+ newbie here) I am trying to PlusCal model the double-switch lamp state machine that you can see here: https://learntla.com/topics/state-machines.html. The model works but then I knocked off one of the state transitions on purpose, to simulate a faulty model. It still passes :) How can I elicit a diagnostic about that dysfunction? Thanks!
The line is marked <== dead in the code below:
Model for the double switch: https://learntla.com/topics/state-machines.html

---- MODULE switch ----------------------------------------------------

EXTENDS TLC, Integers, Sequences

(**********************************************************************

--algorithm lamp {

fair+ process (Switch \in {1})
variables
    state \in {"BothOff", "WallOff", "LampOff", "On"};
    initialState = "BothOff";
    v1 = 2;
{
  ProcBody:
    state := "BothOff";

  EntryBothOff:
    skip;
  BodyBothOff:
    either {
        await (/\ state = initialState /\ v1 = 3); \* <== dead as v1 = 2!!
        state := "WallOff";
        goto BodyWallOff;
    } or {
        await (/\ state = initialState);
        state := "LampOff";
        goto BodyLampOff;
    };

  BodyLampOff:
    either {
        await state = "LampOff";
        state := "BothOff";
        goto BodyBothOff;
    } or {
        await state = "LampOff";
        state := "On";
        goto BodyOn;
    };

  BodyWallOff:
    either {
        await state = "WallOff";
        state := "BothOff";
        goto BodyBothOff;
    } or {
        await state = "WallOff";
        state := "On";
        goto BodyOn;
    };

  BodyOn:
    either {
        await state = "On";
        state := "LampOff";
        goto BodyLampOff;
    } or {
        await state = "On";
        state := "WallOff";
        goto BodyWallOff;
    };

} \* Switch

} \* algorithm lamp

**********************************************************************)

\* BEGIN TRANSLATION (chksum(pcal) = "e4214bef" /\ chksum(tla) = "67c8ad81")
VARIABLES pc, state, initialState, v1

vars == << pc, state, initialState, v1 >>

ProcSet == ({1})

Init == (* Process Switch *)
        /\ state \in [{1} -> {"BothOff", "WallOff", "LampOff", "On"}]
        /\ initialState = [self \in {1} |-> "BothOff"]
        /\ v1 = [self \in {1} |-> 2]
        /\ pc = [self \in ProcSet |-> "ProcBody"]

ProcBody(self) == /\ pc[self] = "ProcBody"
                  /\ state' = [state EXCEPT ![self] = "BothOff"]
                  /\ pc' = [pc EXCEPT ![self] = "EntryBothOff"]
                  /\ UNCHANGED << initialState, v1 >>

EntryBothOff(self) == /\ pc[self] = "EntryBothOff"
                      /\ TRUE
                      /\ pc' = [pc EXCEPT ![self] = "BodyBothOff"]
                      /\ UNCHANGED << state, initialState, v1 >>

BodyBothOff(self) == /\ pc[self] = "BodyBothOff"
                     /\ \/ /\ (/\ state[self] = initialState[self] /\ v1[self] = 3)
                           /\ state' = [state EXCEPT ![self] = "WallOff"]
                           /\ pc' = [pc EXCEPT ![self] = "BodyWallOff"]
                        \/ /\ (/\ state[self] = initialState[self])
                           /\ state' = [state EXCEPT ![self] = "LampOff"]
                           /\ pc' = [pc EXCEPT ![self] = "BodyLampOff"]
                     /\ UNCHANGED << initialState, v1 >>

BodyLampOff(self) == /\ pc[self] = "BodyLampOff"
                     /\ \/ /\ state[self] = "LampOff"
                           /\ state' = [state EXCEPT ![self] = "BothOff"]
                           /\ pc' = [pc EXCEPT ![self] = "BodyBothOff"]
                        \/ /\ state[self] = "LampOff"
                           /\ state' = [state EXCEPT ![self] = "On"]
                           /\ pc' = [pc EXCEPT ![self] = "BodyOn"]
                     /\ UNCHANGED << initialState, v1 >>

BodyWallOff(self) == /\ pc[self] = "BodyWallOff"
                     /\ \/ /\ state[self] = "WallOff"
                           /\ state' = [state EXCEPT ![self] = "BothOff"]
                           /\ pc' = [pc EXCEPT ![self] = "BodyBothOff"]
                        \/ /\ state[self] = "WallOff"
                           /\ state' = [state EXCEPT ![self] = "On"]
                           /\ pc' = [pc EXCEPT ![self] = "BodyOn"]
                     /\ UNCHANGED << initialState, v1 >>

BodyOn(self) == /\ pc[self] = "BodyOn"
                /\ \/ /\ state[self] = "On"
                      /\ state' = [state EXCEPT ![self] = "LampOff"]
                      /\ pc' = [pc EXCEPT ![self] = "BodyLampOff"]
                   \/ /\ state[self] = "On"
                      /\ state' = [state EXCEPT ![self] = "WallOff"]
                      /\ pc' = [pc EXCEPT ![self] = "BodyWallOff"]
                /\ UNCHANGED << initialState, v1 >>

Switch(self) == ProcBody(self) \/ EntryBothOff(self) \/ BodyBothOff(self)
                   \/ BodyLampOff(self) \/ BodyWallOff(self)
                   \/ BodyOn(self)

(* Allow infinite stuttering to prevent deadlock on termination. *)
Terminating == /\ \A self \in ProcSet: pc[self] = "Done"
               /\ UNCHANGED vars

Next == (\E self \in {1}: Switch(self))
           \/ Terminating

Spec == /\ Init /\ [][Next]_vars
        /\ \A self \in {1} : SF_vars(Switch(self))

Termination == <>(\A self \in ProcSet: pc[self] = "Done")

\* END TRANSLATION

====