Thanks for the pointer, I'll try a nightly build for now.
On Saturday, July 4, 2020 at 3:03:11 PM UTC-7, 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