if the translation made the branch occur between different steps
The translation doesn't make anything happen. The translation maps a
PlusCal algorithm to a TLA+ formula. If you can explain what TLA+ formula
you would like the either...or statement to be mapped to, we can discuss
whether that would be a good translation.
But all of this is only relevant if other peoples intuition is that a
fair execution of the small program would indeed terminate.
People's intuition about concepts they don't understand is irrelevant.
I have no trouble accepting that the earth is moving me at over 1000 km
per hour as I type this, even though it contradicts people's intuition.