As has been pointed out in response to recent posts, PlusCal has only
a limited ability to express the fairness properties that can be
expressed in TLA+. The TLA+ spec you want is obtained by conjoining
the following fairness formula to the specification Spec produced by
the PlusCal to TLA+ translation:
SF_vars(RETRY_BEGIN /\ (pc'["retry_example"] = "RETRY_SUCCEED"))
And no, I do not intend to try to enhance PlusCal to allow it to
express such conditions. TLA+ is so expressive because it is based on
mathematics, not on programming-language notation. PlusCal is an
attempt to capture much of the power of TLA+ in such a notation.
Expecting it to capture all of that power would be like expecting C++
to express Maxwell's equations.