Towards beginner friendly examples

[lemmy]

The current README does not order examples that make it easy to pick beginner-friendly examples.

TLA+ concepts by which to cluster (tag?) specs:

• Constant-level expressions
  • Set of all functions [ S -> T ]
  • recursive function definitions such as sum of all elements in a range of a function
  • recursive operators
  • Second order
  • Standard modules
• "+" in TLA+
  • sets (filter/mapping), functions, records, sequences, ..., TLC!@@, TLC!:>
• CHOOSE vs. \E (existential quantification)
• non-determinism|concurrency|distributed systems
• Safety|Liveness (Fairness)
• Refinement
• PlusCal
• Auxiliary variables (history|prophecy)
• Composition of specs
• Inductive invariants (TLAPS)

Categories

Math:
https://github.com/tlaplus/Examples/tree/master/specifications/SpecifyingSystems/SimpleMath
https://github.com/tlaplus/Examples/tree/master/specifications/SpecifyingSystems/MoreMath
https://github.com/tlaplus/Examples/tree/master/specifications/TransitiveClosure
https://github.com/tlaplus/CommunityModules/blob/master/modules/Graphs.tla
#23

Logic Puzzles:
https://github.com/tlaplus/Examples/blob/master/specifications/Stones/
https://github.com/tlaplus/Examples/tree/master/specifications/DieHard (there are also PlusCal versions somewhere)
https://github.com/tlaplus/Examples/tree/master/specifications/CarTalkPuzzle
https://github.com/tlaplus/Examples/tree/master/specifications/MissionariesAndCannibals
https://github.com/tlaplus/Examples/tree/master/specifications/N-Queens
https://github.com/tlaplus/Examples/tree/master/specifications/Prisoners

Beginner specs based on popular problems in CS:
https://github.com/tlaplus/Examples/tree/master/specifications/tower_of_hanoi
https://github.com/tlaplus/Examples/tree/master/specifications/GameOfLife
https://github.com/tlaplus/Examples/tree/master/specifications/CigaretteSmokers
https://github.com/tlaplus/Examples/tree/master/specifications/SlidingPuzzles

Non-common concepts in TLA+:
https://github.com/tlaplus/Examples/tree/master/specifications/SpecifyingSystems/Syntax (BNF grammar)

Specs of basic concurrent/distributed systems:
https://github.com/tlaplus/Examples/tree/master/specifications/Chameneos
https://github.com/tlaplus/Examples/tree/master/specifications/echo (PlusCal)
https://github.com/tlaplus/Examples/tree/master/specifications/Tla-tortoise-hare (PlusCal)
https://github.com/lemmy/BlockingQueue/ (tutorial)
https://github.com/tlaplus/Examples/tree/master/specifications/dijkstra-mutex
https://github.com/tlaplus/Examples/tree/master/specifications/ewd840
https://github.com/tlaplus/Examples/tree/master/specifications/ewd998

TLAPS:
https://github.com/tlaplus/Examples/tree/master/specifications/sums_even
https://github.com/tlaplus/Examples/tree/master/specifications/LoopInvariance
https://github.com/tlaplus/Examples/tree/master/specifications/TeachingConcurrency

Technical

• git submodules instead of html links where possible
• Standalone examples that rely e.g. on git commits to structuring their content?
• Zero install/browser-based, i.e. open in gitpod or codespaces (would benefit from submodules)
  • What about submodules that bring their own gitpod/codespace config (e.g. BlockingQueue)?
• Classify specifications by TLA+ / PlusCal #8

[ahelwer]

@lemmy do you actually want to add all these feature tags? It's definitely doable in the manifest with tree-sitter queries.

[lemmy]

The intent of this issue is to allow the community to tag and categorize examples. Github Blocks (technical preview) look like a possible solution.

[ahelwer]

PR #105 added beginner flags to the spec table, enforced via CI to correspond to the beginner tag in the manifest.json.

[ahelwer]

Although I guess this doesn't address all the category-related stuff or provide something like a track for people to look at. @lemmy do you think the latest changes suffice or we should do more?

[lemmy]

Thanks for tackling this issue. Tbh, I don't understand the use case for splitting the tables into local and elsewhere? I'd find it more relevant for users if the tables would be categories by complexity levels, such as beginner, intermediate, and real-world? However, I'm not sure there is an audience for intermediate, which is why we could also keep a single lookup table for advanced users and include a beginner-friendly section at the top of the Readme that introduces the specs suitable for beginners.

PS: I believe my BlockingQueue example is very beginner friendly, but it is now at the very bottom.

[ahelwer]

The local/elsewhere split is mostly just very helpful for CI checking; every spec in the local table must correspond to an entry in the manifest, and vice-versa. It also highlights the elsewhere specs as sort of a to-do list for us to bring them into the repo itself.

We can add a beginner flag to your BlockingQueue example and move it near the top! I broadly ordered the specs so that the more "features" they have flagged the higher their position in the table.

[lemmy]

Ideally, the table would be ordered based on community feedback, i.e., the number of stars/votes that specs gets over time. I assume that is not possible with Github flavored markdown?