advent-of-tla
ewd998
advent-of-tla | ewd998 | |
---|---|---|
1 | 2 | |
7 | 46 | |
- | - | |
0.0 | 0.0 | |
over 2 years ago | 7 months ago | |
TLA | 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.
advent-of-tla
ewd998
-
How to specify "After P is true, Q is always true"?
You might find https://github.com/tlaplus-workshops/ewd998/blob/main/TemporalLogic.tla useful, where you can explicitly define a set of behaviors (see `seq`), and have TLC check your temporal properties (see `Prop`).
-
Announcement: Public TLA+ workshop at Craft Conf in Budapest
I am excited to announce that I will be conducting a two-day TLA+ workshop at Craft Conf Budapest in May. If you or your colleagues happen to be in the area, I highly recommend considering attending. You can find more information about the workshop on GitHub, and a report on the workshop has been recently published in FMTea2023.
What are some alternatives?
tlaplus - TLC is a model checker for specifications written in TLA+. The TLA+Toolbox is an IDE for TLA+.
TLAplus - TLA+ questions, answers, and experiments
apalache - APALACHE: symbolic model checker for TLA+ and Quint
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
pgo - PGo is a source to source compiler from Modular PlusCal specs into Go programs.
Examples - A collection of TLA⁺ specifications of varying complexities
CommunityModules - TLA+ snippets, operators, and modules contributed and curated by the TLA+ community