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

Re: [tlaplus] error trace on assertion failure?



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?

On Saturday, July 4, 2020 at 6:03:11 PM UTC-4, Markus Alexander Kuppe wrote:
On 04.07.20 13:38, travis...@xxxxxxxxx wrote:
> 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


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

Markus

--
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/476f2159-55d6-4d2d-a633-d304a8c62850o%40googlegroups.com.