error trace on assertion failure?

[travis...@gmail.com]

Hello, I'm rather new to TLA+ and formal methods in general and have been going through LearnTLA+. I'm encountering some friction though from a behavior difference between the advertised behavior of the TLA+ toolbox in LearnTLA+ and the 1.7.0 version I'm using: namely that when an assertion is violated, I'm not seeing any error trace, just a notice that the assertion failed and the TLA+ and PlusCal line numbers of the failure.

I've been able to mostly work around it by changing assertions to invariants, but I'd like to learn either what I'm doing wrong or what has changed since the toolbox version that LearnTLA+ was written with. I've searched around in the toolbox help system and online and haven't been able to find anything.

Appreciate any guidance you can give me!

Travis

[Markus Kuppe]

https://github.com/tlaplus/tlaplus/issues/461

Markus

[travis...@gmail.com]

Thanks for the pointer, I'll try a nightly build for now.

[Huaixi Lu]

I tried the nightly build in mac os, but when I opened the app, an error called the app has been damaged poped up, do you know what's wring with that?

[Markus Kuppe]

On 04.08.20 07:39, Huaixi Lu wrote:
> I tried the nightly build in mac os, but when I opened the app, an error
> called the app has been damaged poped up, do you know what's wring with
> that?

Hi,

to track this, can you please add your version of macOS to the related
issue on Github [1]?

Thanks,
Markus

[1] https://github.com/tlaplus/tlaplus/issues/320