RandomElement fails with TLC bug
Werner Grift
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.
Werner Grift
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.
Leslie Lamport
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.
any expression e. It has the non-mathematical effect of sometimes
causing TLC to print something. You need to understand how TLC works
to understand what it prints when.
described the specification you're running TLC on. I don't have time
to try to reconstruct your specification by looking at a few snippets
of TLA+ expressions and an incomplete description of what TLC did.
However, instead of trying random features and asking why they don't
do what you expect them to, it would be more productive if you explained
what you're trying to do and asked for advice on how to do it.
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.
Werner Grift
I just found your book "Specifying Systems" which is exactly what I need. I did go through "The Temporal Logic of Actions", but it's to condense and not enough to make me understand what I am doing. I thought PrintT might help.
After I read your book I will give it another go. My goal is to have a good understanding of how I can use this stuff to help design our new software which is distributed. I do agree that winging development in a distributed system is a bad idea.
In any case, this stuff is really really cool. I want TLA become part of how I think about the behaviors of algorithms. It makes so much more sense than the conventional way, which is... every one just winging it I guess?
Chris Newcombe
Slides and notes: http://hpts.ws/papers/2011/sessions_2011/Debugging.pdf
Example specs: http://hpts.ws/papers/2011/sessions_2011/amazonbundle.tar.gz
The specs are for algorithms for concurrency control (isolation) in transaction processing systems. There's one spec for textbook snapshot isolation, and another for serializable snapshot isolation. I was able to publish the specs because Amazon did not invent those algorithms (see links to papers in the comments of the algorithms). I wrote the specs to learn about the algorithms, and as a basis for experimentation with new algorithms and optimizations. Subsequently I wrote other specs that will not be published.
The specs above are the first I ever wrote in TLA+, so I'm sure that they can be improved in lots of ways. But they might be interesting examples of 'real world specs' that are useful to industry.
I've been asked to give a talk about serializable snapshot isolation algorithm (using the above spec) in the "Dr TLA+" talk series on youtube:
https://github.com/tlaplus/DrTLAPlus
My talk is still months away at the earliest, as I haven't yet had time to prepare anything due to other commitments.
However, the other algorithms covered so far in the Dr TLA+ series are certainly relevant to industry, so I suggest that you look at those talks and specs.
Finally, if you want examples of how TLA+ and TLC can add value in other ways, e.g. find real bugs, when working on concurrent algorithms, then I'd recommend reading the following story and paper by Leslie:
https://www.microsoft.com/en-us/research/publication/checking-a-multithreaded-algorithm-with-cal/
cheers,
Chris
--
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.
Markus Alexander Kuppe
> I just found your book "Specifying Systems" which is exactly what I
> need. I did go through "The Temporal Logic of Actions", but it's to
> condense and not enough to make me understand what I am doing. I
> thought PrintT might help.
you might also want to read the Hyperbook found at
http://research.microsoft.com/en-us/um/people/lamport/tla/hyperbook.html
Markus