if you look at the TLA+ that is generated without weak fairness, the main formula is
Spec == Init /\ [Next]_vars
This specification allows for executions that stutter indefinitely from any point onwards, therefore termination is not guaranteed. Invariance to stuttering is a fundamental concept of TLA+, and for verifying liveness properties you always need some fairness conditions in order to rule out indefinite stuttering. When you add the weak fairness option, the specification becomes
Spec == /\ Init /\ [Next]_vars
ensuring that executions cannot halt as long as some action is executable.
NB: I was not even aware of the possibility of passing options to PlusCal via a comment, and the feature appears to be somewhat brittle (for example, it breaks when you have a space between "\*" and "PlusCal"). You may alternatively write "--fair algorithm", and similarly "fair process" when you have multi-process algorithms.
The effect is independent of depth-first or breadth-first search.