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

From: Andrew Helwer <andrew.helwer@xxxxxxxxx>

Date: Mon, 26 Apr 2021 14:03:30 -0700 (PDT)

References: <21cd1584-64a0-469e-bdb5-ddd8fd8d19dbn@googlegroups.com> <CAFteovJe664o=A=oTy+jjjeDbQ=69Asfg3C5dUSCODzvY_KPQQ@mail.gmail.com>

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.

tlaplus+unsubscribe@xxxxxxxxxxxxxxxx

https://groups.google.com/d/msgid/tlaplus/88d70b38-4c59-4134-9112-fb993521923fn%40googlegroups.com