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.
On Sunday, April 3, 2016 at 12:36:38 AM UTC-7, mm1...@xxxxxxxxx wrote:
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,