Re: RandomElement fails with TLC bug

[Werner Grift <sky.c...@xxxxxxxxx>]

Correction: 

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

On Thursday, September 15, 2016 at 4:11:26 PM UTC+2, Werner Grift wrote:
> 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.