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

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



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.