TLC model Checker is not working

[mm1...@yahoo.com]

Hello,
Hope you are doing well.
I'm trying to learn how to use TLA+ and I'm following the book "hyperbook".
After creating a model for the spec "one bit clock" and run the TLC checker. It runs indicating no error while there is an error " when replacing 0 with a string, and also statistics are not shown. I mean the tables are empty. What am doing wrong?
Note : I'm using windows

Thanks,

[Stephan Merz]

Hello,

and welcome to the mailing list. The description of your problem is unfortunately not very explicit, so it is hard to understand what you actually did.

I am assuming that you followed the instructions in the Hyperbook, and entered something like the following specification.

---------------------------- MODULE OneBitClock ----------------------------
VARIABLE b

Init == b=0 \/ b=1

Next == \/ b=0 /\ b'=1
        \/ b=1 /\ b'=0
=============================================================================

You then probably ran TLC by indicating the initial and next-state predicates in the corresponding fields and clicking on the green triangle, seeing that it generated 4 states, 2 of which are distinct.

If you followed the instructions, you then changed b'=0 into b'="xyz" and saved the module. Did you actually rerun TLC, i.e. click on the green triangle? I am asking because the photo attached to your message shows an empty output pane. If you do, you should see a result similar to the attached screen shot.

Hope this helps,

best regards,

Stephan

[Andrew Helwer]

One possible cause of this error is you're using the 64-bit toolbox but 32-bit Java runtime. If you look in the model checker logs (text file in the directory below your spec) it should say something like "Attempted to allocate [gigantic 64-bit quantity] of memory, only [32-bit quantity of memory] available. The solution is to install the 64-bit Java runtime environment.