Re: RandomElement fails with TLC bug

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

Ok I see. I need more education. 

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?

On Thursday, September 15, 2016 at 5:17:37 PM UTC+2, Leslie Lamport wrote:
> 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.
> PrintT is a mathematical expression defined so PrintT(e) = TRUE for
> 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.
> 
> 
> It would be possible to explain why TLC is doing what it is if you
> 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.