error trace on assertion failure?

33 views
Skip to first unread message

travis...@gmail.com

unread,
Jul 4, 2020, 5:39:01 PM7/4/20
to tlaplus
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

unread,
Jul 4, 2020, 6:03:11 PM7/4/20
to tla...@googlegroups.com

travis...@gmail.com

unread,
Jul 4, 2020, 6:36:56 PM7/4/20
to tlaplus
Thanks for the pointer, I'll try a nightly build for now.

Huaixi Lu

unread,
Aug 4, 2020, 10:39:24 AM8/4/20
to tlaplus
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

unread,
Aug 4, 2020, 2:00:54 PM8/4/20
to tla...@googlegroups.com
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
Reply all
Reply to author
Forward
0 new messages