tlsd
CommunityModules
| tlsd | CommunityModules | |
|---|---|---|
| 2 | 3 | |
| 12 | 256 | |
| - | 2.7% | |
| 0.0 | 6.9 | |
| about 1 year ago | 3 days ago | |
| Python | TLA | |
| MIT License | 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.
tlsd
-
If you deal in state machines, you might enjoy StateSmith. It compiles diagrams to C or C++ with zero dependencies. Free & opensource.
I've previously written this tool to generate sequence diagrams from TLA+ models (by having tlc first generate state transition graphs). It visualizes clearly how it actually takes time for a message to end up from the sender to the client.
- Generate (message) sequence diagrams from TLA+ state traces
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.
What are some alternatives?
StateSmith - A state machine code generation tool suitable for bare metal, embedded and more.
practical-fm - A gently curated list of companies using verification formal methods in industry
pytm - A Pythonic framework for threat modeling
Examples - A collection of TLA⁺ specifications of varying complexities
BlockingQueue - Tutorial "Weeks of debugging can save you hours of TLA+". Each git commit introduces a new concept => check the git history!
timewinder - Temporal Logic of Actions in Rust via Starlark
DrTLAPlus - Dr. TLA+ series - learn an algorithm and protocol, study a specification
modelator-py - Utilities for the TLA+ ecoystem and model-based testing using TLA+.
pgo - PGo is a source to source compiler from Modular PlusCal specs into Go programs.
ewd998 - Distributed termination detection on a ring, due to Shmuel Safra: