Re: [tlaplus] error trace on assertion failure?

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

On 04.07.20 13:38, travis.parker@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/c44b4c42-12e0-e55a-deb0-3974c9d2ee39%40lemmster.de.