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

*From*: Leslie Lamport <tlapl...@xxxxxxxxx>*Date*: Thu, 15 Sep 2016 08:17:37 -0700 (PDT)*References*: <accfba26-73e3-468a-80be-e2064806bbd6@googlegroups.com>

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.

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.

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.

**Follow-Ups**:**Re: [tlaplus] Re: RandomElement fails with TLC bug***From:*Chris Newcombe

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

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

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