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