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

*From*: Karolis Petrauskas <k.petrauskas@xxxxxxxxx>*Date*: Tue, 27 Apr 2021 00:32:42 +0300*References*: <21cd1584-64a0-469e-bdb5-ddd8fd8d19dbn@googlegroups.com> <CAFteovJe664o=A=oTy+jjjeDbQ=69Asfg3C5dUSCODzvY_KPQQ@mail.gmail.com> <88d70b38-4c59-4134-9112-fb993521923fn@googlegroups.com>

I tried to use sub-expressions in proofs (in a similar way, as in the Paxos proof), but for me it looks like it should be quite fragile, if paths would become longer than a few levels.

It becomes not obvious how to fix a broken path to a sub-_expression_ after the spec itself is modified. Often it is hard to guess, which _expression_ was referred before the modification of the spec.

And they are actually hard to read, again, if they are longer than a few levels. You need to jump between the proof and the formula itself.

But that's just my impression.

Karolis

On Tue, Apr 27, 2021 at 12:03 AM Andrew Helwer <andrew.helwer@xxxxxxxxx> wrote:

Hi Karolis,By subexpressions I mean stuff like foo(2, 3)!bar!<<!(1)!:!>>, which you can use to refer to specific parts of a larger _expression_. The linked proof does use subexpressions in a limited way, to bind quantifiers, but not in a more involved way.Andrew--On Monday, April 26, 2021 at 2:07:39 PM UTC-4 k.petr...@xxxxxxxxx wrote:Do you mean such an example?Don't know if that works in TLC.KarolisOn Mon, Apr 26, 2021 at 9:03 PM Andrew Helwer <andrew...@xxxxxxxxx> wrote:Been reading the TLA+2 language spec and had no idea that subexpressions existed and were so powerful. You can use the language itself to navigate around the parse tree of the TLA+ file you're working in! Are there any examples of TLAPS proofs which use this? Also, does TLC support it (although I assume it's quite inefficient)?Andrew--

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+u...@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/21cd1584-64a0-469e-bdb5-ddd8fd8d19dbn%40googlegroups.com.

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/88d70b38-4c59-4134-9112-fb993521923fn%40googlegroups.com.

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/CAFteovKrRno8An4WJL_ebvzb7E%2BDvdXpZp5%2BaYU_3KfP_NdOEA%40mail.gmail.com.

**References**:**[tlaplus] Examples of specs with proofs that use subexpressions?***From:*Andrew Helwer

**Re: [tlaplus] Examples of specs with proofs that use subexpressions?***From:*Karolis Petrauskas

**Re: [tlaplus] Examples of specs with proofs that use subexpressions?***From:*Andrew Helwer

- Prev by Date:
**Re: [tlaplus] Examples of specs with proofs that use subexpressions?** - Next by Date:
**Re: [tlaplus] Error with CommunityModules (kSubset)** - Previous by thread:
**Re: [tlaplus] Examples of specs with proofs that use subexpressions?** - Next by thread:
**[tlaplus] Loop not terminating** - Index(es):