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

Re: Practical TLA+ now out



On Thursday, October 18, 2018 at 7:27:43 PM UTC-4, Hillel Wayne wrote:
> The book's done! My announcement is here and the publisher page is here. Super happy to share it out and hope you enjoy reading it!
> 
> Hillel

Hillel, I purchased the book and am trying to start a TLA group at the office. I'll see if I can get  more people to also purchase the book.

One clarification however would be useful for us new persons on Print/PrintT. Consider your example from page 57:

.
 .
  .
Flags == {"f1", "f2"}
.
 .
  .

flags \in {config \in [Flags -> BOOLEAN]: \E f \in Flags: config[f]}

Can you explain how in PlusCal I can print the value of 'flags' after it evaluates the last
line? PlusCal code does not seem to accept Print/PrintT? If I am using TLA+ -- not going from PlusCal to TLA --- but instead using TLA+ directly, how can I do the same thing? In the latter case (direct TLA+) I gather I'll need a dummy invariant that calls Print and returns TRUE? This question amounts to how do I use printf like statements to help me debug expressions ... This is helpful for persons new to the language.

Regards