Re: I've been working on a TLA+ guide

[ston...@xxxxxxxxx]

On Tuesday, February 7, 2017 at 6:28:59 PM UTC-5, Hillel Wayne wrote:
> Hi everyone,
> 
> 
> For the past few months I've been working on a TLA+ Guide (www.learntla.com). It's aimed at a less rigorous audience than Specifying Systems or the Hyperbook are: it's a lot less comprehensive and in-depth and focuses more on patterns and troubleshooting. The hope is that it'll be useful for software developers who may not necessarily need the full power of TLA+ but would benefit from having something more sophisticated than unit tests.
> 
> 
> It's still in early drafts but I would love to get some feedback. Feel free to check it out! And please let me know if something is confusing, explained poorly, or flat-out wrong. Writing v1 is the easy part, after all. ;)
> 
> 
> Hillel
> 
> 
> PS: While I think it's ready to share with you folks, it's definitely not ready to fully publicize, and I plan on doing five or six more rounds of editing to get it there. Doesn't even have exercises yet.

I found the guide very useful. I had read a few other things but for whatever reason couldn't quite figure out how to, in practice, do my own simple spec, hit 'go', and get a result. Your guide is very clear on how to do that.

One minor nit: you should mention to put the Init & Next steps in the model, if they don't appear automatically.

Thanks!

---rdf