3 ms·

This is a great introduction. I liked the pseudocode better than TLA syntax, though, so I think if I needed something like this, I would look into alternatives

This is a great introduction. I liked the pseudocode better than TLA syntax, though, so I think if I needed something like this, I would look into alternatives to TLA itself.

kadoban 2y ago
You can use pluscal, it embeds in tla+ and compiles to it, it's fairly nice.
hwayne 2y ago
In addition to PlusCal, I think the main "pseudocode alternative" to TLA+ is now Quint: https://github.com/informalsystems/quint https://github.com/informalsystems/quint