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

*From*: Werner Grift <sky.c...@xxxxxxxxx>*Date*: Thu, 15 Sep 2016 07:18:23 -0700 (PDT)*References*: <accfba26-73e3-468a-80be-e2064806bbd6@googlegroups.com>

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.

**References**:**RandomElement fails with TLC bug***From:*Werner Grift

- Prev by Date:
**RandomElement fails with TLC bug** - Next by Date:
**PrintT behaviour** - Previous by thread:
**RandomElement fails with TLC bug** - Next by thread:
**Re: RandomElement fails with TLC bug** - Index(es):