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

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

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.