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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Wed, 13 Sep 2023 15:25:41 +0200*References*: <3caab352-1bd8-4335-bbc1-5568ce7782b6n@googlegroups.com> <93E9F1D1-3676-4B14-8355-355DBE1FA168@gmail.com> <2372af21-7cd8-45c2-94b7-84e5b39ad16cn@googlegroups.com>

In fact, TLC checks neither of the two implications that you indicate but verifies LET f == CHOOSE f \in F : TRUE IN Spec => Inv Assuming that F is non-empty, this is implied by \A f \in F : Spec => Inv and it implies \E f \in F : Spec => Inv The actual choice of f is fixed by the interpretation in which the formula is evaluated (and which includes a choice operator mapping every non-empty set to some element of that set). TLC does not enumerate the possible choice operators but conceptually implements a fixed one. [1] Stephan [1] In full detail, it's more complicated than that because it is only possible to implement an approximation of a choice operator, which does not ensure that two non-empty sets that are equal but represented differently are mapped to the same element, see section 14.6 of Specifying Systems.
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/CF771482-DB2D-4771-A65A-B7FD4FB29D05%40gmail.com. |

**Follow-Ups**:**Re: [tlaplus] A CHOOSE+TLC conundrum***From:*Ognjen Maric

**References**:**[tlaplus] A CHOOSE+TLC conundrum***From:*Ognjen Maric

**Re: [tlaplus] A CHOOSE+TLC conundrum***From:*Stephan Merz

**Re: [tlaplus] A CHOOSE+TLC conundrum***From:*Ognjen Maric

- Prev by Date:
**Re: [tlaplus] A CHOOSE+TLC conundrum** - Next by Date:
**Re: [tlaplus] A CHOOSE+TLC conundrum** - Previous by thread:
**Re: [tlaplus] A CHOOSE+TLC conundrum** - Next by thread:
**Re: [tlaplus] A CHOOSE+TLC conundrum** - Index(es):