[tlaplus] Re: How to test a process eventually succeeds after indefinite number of retries?

[Leslie Lamport <tlaplus.ll@xxxxxxxxx>]

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.

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.