Re: [tlaplus] Examples of specs with proofs that use subexpressions?

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?
https://github.com/tlaplus/DrTLAPlus/blob/master/Paxos/Paxos.tla
Don't know if that works in TLC.

Karolis

On 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.