CommunityModules
DrTLAPlus
| CommunityModules | DrTLAPlus | |
|---|---|---|
| 3 | 1 | |
| 256 | 777 | |
| 2.7% | 1.2% | |
| 6.9 | 1.8 | |
| 5 days ago | about 2 years ago | |
| TLA | TLA | |
| MIT License | - |
Stars - the number of stars that a project has on GitHub. Growth - month over month growth in stars.
Activity is a relative number indicating how actively a project is being developed. Recent commits have higher weight than older ones.
For example, an activity of 9.0 indicates that a project is amongst the top 10% of the most actively developed projects that we are tracking.
CommunityModules
-
Generate (message) sequence diagrams from TLA+ state traces
Adding a vector clock is relatively straightforward (see e.g. https://github.com/tlaplus/Examples/commit/ee10c6ed1c65f1002c8ad402edceeffcf1a833e). For PlusCal, the vector clock can be computed from the PC variable: https://github.com/tlaplus/CommunityModules/blob/master/modules/ShiViz.tla
- JSON to TLA+
-
Converting tuples to record
You can find such definitions in the community modules. Here's one for sets, and here's one you can use for sequences.
DrTLAPlus
-
Ask HN: Do You Use TLA+
## TLA+
Wikipedia: https://en.wikipedia.org/wiki/TLA%2B
Src: https://github.com/tlaplus/tlaplus
Awesome: https://github.com/tlaplus/awesome-tlaplus
### Dr TLA+
Web: https://github.com/tlaplus/DrTLAPlus
Src: https://github.com/tlaplus/DrTLAPlus :
> Dr. TLA+ series - learn an algorithm and protocol, study a specification; [Byzantine] Paxos, Raft, Cosmos,
##
"Concurrency: The Works of Leslie Lamport" ( https://g.co/kgs/nx1BaB
##
https://westurner.github.io/hnlog/#comment-27442819 :
> Can there still be side channel attacks in formally verified systems? Can e.g. TLA+ help with that at all?
What are some alternatives?
practical-fm - A gently curated list of companies using verification formal methods in industry
BlockingQueue - Tutorial "Weeks of debugging can save you hours of TLA+". Each git commit introduces a new concept => check the git history!
Examples - A collection of TLA⁺ specifications of varying complexities
tlaplus - TLC is a model checker for specifications written in TLA+. The TLA+Toolbox is an IDE for TLA+.
pgo - PGo is a source to source compiler from Modular PlusCal specs into Go programs.
tlsd - Generate (message) sequence diagrams from TLA+ state traces
people
ewd998 - Distributed termination detection on a ring, due to Shmuel Safra: