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