Re: [tlaplus] Re: Some feedback from a new user

[Alok Menghrajani <al...@xxxxxxxxxxxx>]

Thank you for such a quick response!

> 3.  What PlusCal documentation are you talking about?  It sounds like
> you're not using the HyperBook.  All my documentation effort has been
> going into the HyperBook, not things like the PlusCal manual.

I started with http://research.microsoft.com/en-us/um/people/lamport/tla/c-manual.pdf.
I'm now going over the hyperbook and also
http://research.microsoft.com/en-us/um/people/lamport/tla/book.html.
While I have just started to get comfortable with PlusCal, I'm sure
these two resources will boost my understanding of things.

> Operators like # come from TLA+, which is the expression language of
> PlusCal.  TLA+ is for writing mathematics, and if one designs a
> language for writing mathematical expressions, C is among the worst
> places to look for inspiration.

Makes sense. The mix of PlusCal (C-like constructs) and TLA+ is a
little jarring at first but I'm getting used to it.

> I don't know what you mean by PlusCal sometimes requiring ";" after
> closing braces.  Unlike in C, ";" is a separator, not a closing
> symbol.

I mostly ran into it with the following construct:
while (...) {
  ...
}; <-- the ; is required
...

E.g.
while (FALSE) {
  print "foo";
};
print "bar";


Alok