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

Re: Unclear TLC evaluation behavior

I don't quite follow what you're saying, but I think you understand.

There are lots of ways to write sensible specs in TLA+, and TLC can handle
only a tiny fraction of them.  Fortunately, our experience writing programs
almost always leads us to write sensible specs that TLC handles.  For
example we naturally write  x' = x+1  rather than  x+1 = x', and

   (y # << >>) /\ (y' = Tail(y)) 

rather than

   (y' = Tail(y))  /\ (y # << >>)

However, there are things that programming languages allow that lead to
non-sensible specs if naively translated into TLA+.  These include
an assignment statement such as y[1] := ... and putting an assignment
statement in an `if' test.  That's why you need to understand what
a TLA+ spec means.

On rare occasions, we (including me) write a sensible spec in a way
that seems reasonable but that TLC can't handle.  That's why there's a
description of how TLC works.  But they are rare--I think it's
happened to me only a couple of times.  A much more difficult problem
is teaching people to go outside the limits of what programming
languages allow them to do and take advantage of the power of math
that TLA+ provides and that TLC can handle.