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

*From*: Leslie Lamport <tlaplus.ll@xxxxxxxxx>*Date*: Sat, 23 Feb 2019 08:34:51 -0800 (PST)*References*: <15ade3f5-b044-4796-95dd-4d22c10963dc@googlegroups.com>

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:

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.

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.

**Follow-Ups**:**Re: [tlaplus] Re: How to test a process eventually succeeds after indefinite number of retries?***From:*A. Jesse Jiryu Davis

**References**:**[tlaplus] How to test a process eventually succeeds after indefinite number of retries?***From:*A. Jesse Jiryu Davis

- Prev by Date:
**[tlaplus] How to test a process eventually succeeds after indefinite number of retries?** - Next by Date:
**Re: [tlaplus] Re: How to test a process eventually succeeds after indefinite number of retries?** - Previous by thread:
**[tlaplus] How to test a process eventually succeeds after indefinite number of retries?** - Next by thread:
**Re: [tlaplus] Re: How to test a process eventually succeeds after indefinite number of retries?** - Index(es):