[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

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.