Re: Unfolding macro definitions

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:

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, Messages

If I change this to:

<3>1. ASSUME NEW b \in Ballots, Phase1a(b) PROVE TypeOK'
BY <3>1, PTL DEF TypeOK, Phase1a, Send\*, Messages

I 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