Re: [tlaplus] Confusing line in paxos tlaps proof (USE TRUE /\ TRUE)

[Stephan Merz <stephan.merz@xxxxxxxxx>]

Hello,

the first problem that I have with this module is that it instantiates module Consensus, which is not present in the repository. When I comment out the offending lines at the end of the module, I can reproduce your issue.

Of course, directives such as USE TRUE or USE TRUE /\ TRUE should have no effect.

A superficial inspection indicates that the module is largely a copy of the Paxos specification and proof contained in the collection of examples distributed with TLAPM [1], but which does not contain this strange USE directive and whose proof succeeds. Perhaps Andrew can comment on what is going on here?

Stephan

[1] https://github.com/tlaplus/tlapm/tree/main/examples/paxos

On 17 Jan 2023, at 06:16, Ganesh Rapolu <grapolu@xxxxxxxxxxxx> wrote:

See https://github.com/tlaplus/DrTLAPlus/blob/master/Paxos/Paxos.tla#L238 .

When I ran the proof of lemma SafeAtStable without this line, it fails, but with this line it succeeds.

It also fails if I change this to USE TRUE or USE TRUE \/ TRUE. But what does line actually do?

--
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/2518b08d-b9d2-444e-a0a7-4dc63144838bn%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/0860E81C-FE2B-4041-BD9A-22C9F80EBDB4%40gmail.com.