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

[tlaplus] error trace on assertion failure?

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!

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/453df25b-8f74-4a5d-b8be-5f2a31d56b0fo%40googlegroups.com.