Practical TLA+ now out

[Hillel Wayne]

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

[Morgan Weetman]

Thanks Wayne..great work...my copy arrived recently and I've just got to chapter 3

On Fri, 19 Oct. 2018, 10:27 Hillel Wayne <hwa...@gmail.com 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

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

[neil.o...@koodoo.io]

Ha! This post came in just as I took my seat on a train to London and opened up my shiny new copy of Practical TLA+. Super excited about getting into the guts of it!

[7532...@gmail.com]

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

[Philip White]

Hi, Hillel,

How much overlap is there between the book and your site "Learn TLA”? Is the book a physical form of the site, or is there a significant amount that’s JUST in the book?

Thanks.

—
Philip

[A. Jesse Jiryu Davis]

I see an answer from Hillel here:

https://learntla.com/book/

I haven't read the book yet though, I've only read the site, so I don't personally know the degree of overlap.

[Philip White]

Thanks, that’s exactly what I was looking for. Just bought a copy. :)

[Leslie Lamport]

Before reading the book, people might want to check out this page from the TLA+ site

 

https://lamport.azurewebsites.net/tla/practical-tla.html?back-link=learning.html#hillel?unhideBut@EQhide-hillel@AMPunhideDiv@EQhillel

[lor...@gmail.com]

"Most engineers and programmers will prefer the C syntax, which will look more familiar to them, so I've used it for all my published algorithms."

I'm not sure that's true. While I learned Pascal before C, I have many more years of experience writing programs in C-like languages (e.g., C, C++, Java, C#), and I still prefer the P syntax to the C syntax. I've always found the placement of braces of PlusCal examples in the C syntax to be very strange-looking to my eyes.

In addition, many programmers today have experience with languages such as Python and Ruby which are (arguably) more like the P syntax than the C syntax.

On Wed, Feb 6, 2019 at 6:11 PM Leslie Lamport <tlapl...@gmail.com> wrote:

Before reading the book, people might want to check out this page from the TLA+ site

 

https://lamport.azurewebsites.net/tla/practical-tla.html?back-link=learning.html#hillel?unhideBut@EQhide-hillel@AMPunhideDiv@EQhillel

--

[Hillel Wayne]

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

[fwefew 4t4tg]

Perfect. thanks . S

--
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/wzzaJrtvpTY/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@googlegroups.com.

[david streader]

As someone although relatively new to TLA+/PlusCal. I must thank Hillel for an excellent book and extraordinarily clear web page. Because the TLC is not a sequential execution but a search of the state space the order print statements  appear on the screen cn appear to be jumbled so I have found  it very useful to concatenate print statements 

 print ("Safety only Rec END " \o ToString(messOut));

also as a beginner I found it very helpful to view the state graph of my specification (you need to integrate GraphViz with the tool to produce them). But that may be more of a reflection of how I think.

regards david