On Tuesday, 5 February 2019 17:57:19 UTC-6, 7532...@xxxxxxxxx wrote:
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.
In pluscal, you can use the print statement, ie
begin
print flags;
\* ...
You'll probably see multiple outputs, some of which might be duplicates. This is because different behaviors might have the same value for flags in that particular state.
If you're writing your own actions in Pure TLA+, you'll probably want to write something like this:
Increment ==
/\ x < 10
/\ PrintT(x)
/\ x' = x + 1
You can read more about how TLC handles the Print operator on page 249 of Specifying Systems, which is included with the TLA+ Toolbox (under "help").
H
Regards