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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Tue, 17 Jan 2023 09:11:00 +0100*References*: <2518b08d-b9d2-444e-a0a7-4dc63144838bn@googlegroups.com>

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

**References**:**[tlaplus] Confusing line in paxos tlaps proof (USE TRUE /\ TRUE)***From:*Ganesh Rapolu

- Prev by Date:
**[tlaplus] Confusing line in paxos tlaps proof (USE TRUE /\ TRUE)** - Next by Date:
**[tlaplus] Re: TLC error with INSTANCE mechanism** - Previous by thread:
**[tlaplus] Confusing line in paxos tlaps proof (USE TRUE /\ TRUE)** - Next by thread:
**[tlaplus] How can I modelcheck an angle-bracket action formula?** - Index(es):