Difficulties using TLA+ Toolbox

[jsma...@gmail.com]

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.

[Stephan Merz]

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

[jsma...@gmail.com]

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.

[Markus Alexander Kuppe]

On 05.01.2017 07:08, jsma...@gmail.com wrote:
> PS I'm using the 32-bit Toolbox because the 64-bit version just gave me a Java error on start.

Hi,

the error likely said that you tried to run the 64bit Toolbox on a 32bit
Java VM. That does not work. If your hardware is 64bits, I suggest you
install a 64bit Java VM from [1]. More available memory usually results
in faster model checking.

Cheers
Markus

[1]
http://www.oracle.com/technetwork/java/javase/downloads/jre8-downloads-2133155.html