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

RandomElement fails with TLC bug

Every time I try to connect primed variable's state to the outcome of TLC's RandomElement TLC fails with:

Failed to recover the initial state from its fingerprint.
This is probably a TLC bug(2).

What does this mean?

For Example:

LET r == RandomElement(1..100) IN PrintT(r) /\ IF r < 50 THEN d' = "smaller" ELSE d' = "bigger"

if I replace the 50 in "r < 50" with any r such that r is not in 1..100 the error goes away. I don't understand. 

I started studying this stuff 3 days ago and for now I am trying to get a sense of how it can be used to predict common concurrency issues that I have faced before. I basically want to show to myself how it finds the problem of a badly implemented concurrent system. I also think there should be more examples that show this, i.e how it actually can be used to add value.