Re: [tlaplus] Unfolding macro definitions

[Annie Liu <anni...@xxxxxxxxx>]

Hi Stephan, I wonder why this bug would be tied to the OS used, i.e., showing up in Windows but not Linux.  Thanks.  Annie

On Sat, Apr 1, 2017 at 3:35 AM, Stephan Merz <stepha...@xxxxxxxxx> wrote:

Hi Saksham,

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.

Thanks for reporting this.

Regards,

Stephan