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

Re: [tlaplus] TLC model Checker is not working


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 ----------------------------

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,


On 03 Apr 2016, at 09:26, mm1m12 via tlaplus <tla...@xxxxxxxxxxxxxxxx> wrote:

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