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

Re: [tlaplus] error trace on assertion failure?

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



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.