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.
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.
TLA+ is mathematics. The TLC module introduces some operators that
aren't mathematics. They are there because they can be useful when
running TLC, but you have to understand how TLC works to make good use
of them. The formula e = e is true for any mathematical expression e.
It isn't true if e is Random(...). Hence Random isn't mathematics, so
you shouldn't use it unless you understand how TLC works.
We all wish there were more examples of TLA+ specs, but we all have
lots of things to do. Industrial users generally don't publish their
specifications. One exception is a book that describes the use of
TLA+ to design a real-time operating system for the European Space
Agency spacecraft that's now sitting in the shade on a comet that I
believe is now heading away from the sun. The principal author is
Eric Verhulst. However, did you really want to read a few hundred
pages of an example? You can read about how TLA+ helped at Amazon,
without any actual specifications, in an article published in
Communications of the ACM in spring 2015 with Chris Newcombe as
lead author.
--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.