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
On Friday, 19 October 2018 12:27:43 UTC+13, 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