Difficulties using TLA+ Toolbox

[jsma...@xxxxxxxxx]

Hi,

I feel somewhat silly posting this as I can see this is a very entry level problem - but I've been stuck on it long enough it's time to reach out.

For background, I've started working through the current Hyperbook. The first issue I hit, in section 2.3, I found if you literally copy + paste the "ASCII version" of the code, you'll just hit a parser error:

Lexical error ... encountered "\u2019" (8217)

Having gotten used to Windows mangling quotes such that ASCII wasn't ASCII at all, I changed b’ into b' and moved on.

Moving on, I created a model, ran the model checker and it ran fine, then inserted the "string" as defined in section 2.5. The attempt to break the model at this point doesn't seem to work for me, as I've saved, parsed, recreated the model, and generally done what I can to make it produce an error and been unsuccessful.

Hopefully with these screenshots someone can point me in the right direction. They include all relevant versions.

https://d86c84grgz45x.cloudfront.net/tla1.PNG
https://d86c84grgz45x.cloudfront.net/tla2.PNG

PS I'm using the 32-bit Toolbox because the 64-bit version just gave me a Java error on start.

Thanks in advance for any advice.