Hi Stephan,
I managed to replicate the same behaviour using the file you sent me.
I did however, discover the TLC Console, which led to identifying this as the root cause:
https://github.com/tlaplus/tlaplus/issues/15
Thanks for looking at this.
On Thursday, January 5, 2017 at 7:08:59 PM UTC+11, Stephan Merz wrote:
Hello,
hard to tell what you actually did – the second screenshot shows that TLC is not running but does not indicate any trace of it having run previously.
Attached is the module that you are supposed to write. Create a new model from it, enter "Init1" and "Next1" in the fields "Init" and "Next" of the model overview pane, and hit the green triangle to run TLC. You should see the error described in the hyperbook.
Regards,
Stephan