Re: [tlaplus] Unfolding macro definitions

Hmm ... it should not be OS-dependent, but I'll give it a try. I certainly believe having seen this under Linux. Can you use PTL at all in your Linux installation, i.e. for proving a valid temporal formula?

On 1 Apr 2017, at 15:41, Annie Liu <anni...@xxxxxxxxx> wrote:

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

--
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.