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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Tue, 8 Jun 2021 08:28:14 +0200*References*: <f71490a1-015b-c6f0-a24f-efe11a7757e4@gmail.com> <7046ccfb-a964-408f-bc0b-9a65ae0f5f1an@googlegroups.com> <52638458-9159-98a3-c757-2efaaae015bc@lemmster.de> <333f8258-b3a9-478f-a50c-143c9368dfd1n@googlegroups.com> <0633552b-769b-425a-84da-09a8c44a2b45n@googlegroups.com>

Hi Andrew,
that definition indeed uniquely defines the value of me'. TLAPS has no problem with it (assuming that me \in Person). TLC can handle it provided you override the definition of Person by a finite set that TLC can enumerate, but is slow due to the explicit enumeration that TLC implements. I believe that Apalache and ProB would handle it just fine because they rely on constraint solving. 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/1A6AB48A-2856-48BC-85AD-BFCB44E0453A%40gmail.com. |

**Follow-Ups**:**Re: [tlaplus] How do you do functions of structures?***From:*Igor Konnov

**References**:**[tlaplus] How do you do functions of structures?***From:*Hillel Wayne

**[tlaplus] Re: How do you do functions of structures?***From:*Andrew Helwer

**Re: [tlaplus] Re: How do you do functions of structures?***From:*Markus Kuppe

**Re: [tlaplus] Re: How do you do functions of structures?***From:*Aaron Elligsen

**Re: [tlaplus] Re: How do you do functions of structures?***From:*Andrew Helwer

- Prev by Date:
**Re: [tlaplus] Re: About "implies" between WF and SF** - Next by Date:
**Re: [tlaplus] How do you do functions of structures?** - Previous by thread:
**Re: [tlaplus] Re: How do you do functions of structures?** - Next by thread:
**Re: [tlaplus] How do you do functions of structures?** - Index(es):