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

*From*: saksha...@xxxxxxxxxxxxxx*Date*: Fri, 31 Mar 2017 10:14:27 -0700 (PDT)

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

**Follow-Ups**:**Re: Unfolding macro definitions***From:*saksha . . .

- Prev by Date:
**I've been working on a TLA+ guide** - Next by Date:
**Re: Unfolding macro definitions** - Previous by thread:
**Re: [tlaplus] About Finite Set of records** - Next by thread:
**Re: Unfolding macro definitions** - Index(es):