Re: [tlaplus] Unfolding macro definitions

indeed – this is a known bug but apparently it had never been entered in the bug tracker. I just did that as https://github.com/tlaplus/tlaplus/issues/40. For the moment, please make sure that you use PTL only for proving temporal logic formulas, preferably in a context where all assumptions are constant formulas.

On 31 Mar 2017, at 19:33, saksha...@xxxxxxxxxxxxxx wrote:

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, saksha...@stonybrook.edu 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

--
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+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.