[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