learntla-v2
learntla-v2 copied to clipboard
hwayne
Learn TLA+ for free! No prior experience necessary!
Hi! Thanks for the awesome project! I encountered a "strange" error with the example in "Writing an Invariant". After setting `is_unique = TRUE`, the code looks like this: ``` ----...
TLA+ Toolbox seems clunky. All the cool kids are using VSCode! (And TLA+ is VSCode is nice and useable thanks to https://github.com/tlaplus/vscode-tlaplus.) The learntla text uses TLA+ Toolbox. But there's...
### Description The [writing specifications page ](https://learntla.com/core/pluscal.html)says this of the duplication checker: > 1. Create an empty set ``seen``, then step through the elements of ``seq``. > 2. Every time...
It's bewildering to me that the [first example _specification_](https://github.com/hwayne/learntla-v2/blob/master/docs/specs/pluscal.tla) in the body text contains only a thing called an `algorithm`, which moreover doesn't seem to do anything meaningful. I understand...
On [Writing an Invariant](https://learntla.com/core/invariants.html) seems to switch silently between examples. It start by using "another spec for finding duplicates that also runs without error", the one where `is_unique` is set...
I think there's a typo in https://github.com/hwayne/learntla-v2/blob/master/docs/core/functions.rst?plain=1#L239 IMO it should be `3^2 = 9` functions when calculating functions mapping 2 tasks with 3 CPUs.
Something that I noticed while reading this is that the often attached images aren't clickable. It would be nice to have them all clickable, ideally opening in a new tab....
I don't know what features exactly this is gonna get us but I've fallen behind on these kinds of upgrades before and *do not* recommend it
After recently witnessing yet another instance of a set being mistakenly declared as symmetric when it is actually not, I would like to propose that users be reminded of their...
Section https://learntla.com/topics/optimization.html#construct-don-t-filter might demonstrate how you can redefine operators. This way, users can keep a simple, more axiomatic definition in the main spec, while using a complex yet more efficient...