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 , but which does not contain this strange USE directive and whose proof succeeds. Perhaps Andrew can comment on what is going on here?
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.