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

*From*: saksha...@xxxxxxxxxxxxxx*Date*: Fri, 31 Mar 2017 10:33:22 -0700 (PDT)*References*: <0e42f363-76c3-4828-bd78-e95e56b68b1a@googlegroups.com>

I think this is a bug. If I change the definition of Messages to something incorrect, the proof (with PTL) still goes through(marked green).

On Friday, March 31, 2017 at 1:14:27 PM UTC-4, saks...@xxxxxxxxxxxxxx wrote:

On Friday, March 31, 2017 at 1:14:27 PM UTC-4, saks...@xxxxxxxxxxxxxx wrote:

Hi,I was intrigued by a statement proved by TLAPS 1.5.2 on my Windows 10 machine. If we look at Paxos.tla in the examples directory, the proof of THEOREM Invariant -> <2>1 TypeOK' -> <3>1. PROVE for Phase1a(b), we have, (line 295)<3>1. ASSUME NEW b \in Ballots, Phase1a(b) PROVE TypeOK'BY <3>1 DEF TypeOK, Phase1a, Send, MessagesIf I change this to:<3>1. ASSUME NEW b \in Ballots, Phase1a(b) PROVE TypeOK'BY <3>1, PTL DEF TypeOK, Phase1a, Send\*, MessagesI comment out Messages definition and add PTL, the proof goes through. In fact you can comment out the whole DEF. Is this expected behaviour or a bug?Note that it doesn't prove on my Linux machine.Thanks,Saksham Chand

**Follow-Ups**:**Re: [tlaplus] Unfolding macro definitions***From:*Stephan Merz

**References**:**Unfolding macro definitions***From:*saksha . . .

- Prev by Date:
**Unfolding macro definitions** - Next by Date:
**Re: [tlaplus] Unfolding macro definitions** - Previous by thread:
**Unfolding macro definitions** - Next by thread:
**Re: [tlaplus] Unfolding macro definitions** - Index(es):