Confusing line in paxos tlaps proof (USE TRUE /\ TRUE)

[Ganesh Rapolu]

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?

[Stephan Merz]

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

--
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...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/2518b08d-b9d2-444e-a0a7-4dc63144838bn%40googlegroups.com.