[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

TLC model Checker is not working

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 


JPEG image