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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Mon, 27 Apr 2020 09:01:49 +0200*References*: <38427413-5d82-4fe4-b54f-9f5535198aa4@googlegroups.com>

You want to use existential quantification for non-deterministic (arbitrary) choice. CHOOSE is deterministic, and randomization is useful for testing, but is not what you want for proofs (unless you consider probabilistic systems, but then TLA+ is not the method of choice). Regards, Stephan
--
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 view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/17EC8615-B388-4CB6-AB3E-E691AF3B709F%40gmail.com. |

**Follow-Ups**:**Re: [tlaplus] About the behavior of RandomElement on refinement proofs***From:*José Eduardo Solsona

**References**:**[tlaplus] About the behavior of RandomElement on refinement proofs***From:*JosEdu Solsona

- Prev by Date:
**[tlaplus] About the behavior of RandomElement on refinement proofs** - Next by Date:
**[tlaplus] on tlaps** - Previous by thread:
**[tlaplus] About the behavior of RandomElement on refinement proofs** - Next by thread:
**Re: [tlaplus] About the behavior of RandomElement on refinement proofs** - Index(es):