I've been working on a TLA+ guide

[Hillel Wayne]

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.

[Jaak Ristioja]

Hello!

On 08.02.2017 01:28, Hillel Wayne wrote:
> 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 really like the approach you've taken in the guide, starting with
PlusCal. As a TLA+ user, it would have saved me many days if something
like this were available when I first started learning TLA+. I think
this will be a very valuable guide for newcomers because it covers the
essentials to get started quickly, and it does so well. Good work! :-)

Jaak

[Hillel Wayne]

Github repo is now public: https://github.com/hwayne/learntla

[Markus Kuppe]

On 01.03.2017 04:54, Hillel Wayne wrote:
> Github repo is now public: https://github.com/hwayne/learntla

Hi,

when I locally run hugo, I just get an empty page with a single open and
closing <pre>. I suppose the missing lexer errors are related to the
missing Pygments formatter? Does this also explain the empty page?

Cheers

Markus

---

markus@avocado:~/src/TLA/learntla(master) $ hugo server
Started building sites ...
ERROR 2017/03/01 08:53:46 Unable to locate template for shortcode
'notice' in page index
ERROR 2017/03/01 08:53:46 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:46 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:46 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:46 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:46 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:46 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:46 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:46 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:46 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:46 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:46 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:46 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:46 Unable to locate template for shortcode
'notice' in page a-simple-spec
ERROR 2017/03/01 08:53:46 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:46 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:46 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:46 Unable to locate template for shortcode
'notice' in page procedures-and-macros
ERROR 2017/03/01 08:53:46 Unable to locate template for shortcode
'notice' in page index
ERROR 2017/03/01 08:53:46 Unable to locate template for shortcode
'notice' in page index
ERROR 2017/03/01 08:53:46 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:46 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:46 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:46 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:46 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:46 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:46 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:46 Unable to locate template for shortcode
'notice' in page index
ERROR 2017/03/01 08:53:46 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:46 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:47 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:47 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:47 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:47 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:47 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:47 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:47 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:47 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:47 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:47 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:47 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:47 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:47 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:47 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:47 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:47 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:47 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:47 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:47 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:47 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:47 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:47 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:47 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:47 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:47 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:47 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:47 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:47 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:47 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:47 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:47 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:48 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:48 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:48 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:48 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:48 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:48 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:48 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:48 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:48 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:48 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:48 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:48 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:48 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:48 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:48 Error: no lexer for alias 'tla' found
ERROR 2017/03/01 08:53:48 Error: no lexer for alias 'tla' found
Built site for language en:
0 of 1 draft rendered
0 future content
0 expired content
41 regular pages created
11 other pages created
55 non-page files copied
0 paginator pages created
0 tags created
0 categories created
total in 2537 ms
Watching for changes in
/home/markus/src/TLA/learntla/{content,layouts,static}
Serving pages from memory
Web Server is available at http://localhost:1313/ (bind address 127.0.0.1)
Press Ctrl+C to stop

[Hillel Wayne]

On Wednesday, 1 March 2017 02:09:03 UTC-6, Markus Kuppe wrote:

On 01.03.2017 04:54, Hillel Wayne wrote:
> Github repo is now public: https://github.com/hwayne/learntla

Hi,

when I locally run hugo, I just get an empty page with a single open and
closing <pre>. I suppose the missing lexer errors are related to the
missing Pygments formatter? Does this also explain the empty page?

Turns out the theme I was using wasn't part of the repo. I added it and confirmed that on a fresh install the instructions work as expected. I also uploaded the Pygments plugin I'm using as well as instructions to disable syntax highlighting if you don't want to setup Pygments.

Hillel

[Gary Price]

I have been finding this guide very useful. Thanks for the effort.

[ston...@gmail.com]

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