Welcome to the TLA+ Wiki
This wiki is community driven, and aims to become a useful resource for TLA+ users.
TLA+ and TLC
TLA+ is a high-level language for modeling programs and systems--especially concurrent and distributed ones. It's based on the idea that the best way to describe things precisely is with simple mathematics. TLA+ and its tools are useful for eliminating fundamental design errors, which are hard to find and expensive to correct in code.
TLC is a model checker for specifications written in TLA+.
----- MODULE HourClock ----- EXTENDS Naturals VARIABLE hr HCini == hr \in (1 .. 12) HCnxt == hr' = IF hr # 12 THEN hr + 1 ELSE 1 HC == HCini /\ [][HCnxt]_hr ------------------------ THEOREM HC => []HCini ======================= ----- CONFIG HourClock ----- (***************************************************************************) (* This is a TLC configuration file for testing that HCini is an invariant *) (* of the specification HC *) (***************************************************************************) SPECIFICATION HC \* This statement tells TLC that HC is the specification that it \* should check. INVARIANT HCini \* This statement tells TLC to check that formula HCini is an \* invariant of the specification--in other words, that the \* specification implies []HCini. ======================
Contributing
These are some of the ways you can contribute.
Wiki
Contributions to the wiki are very welcome!
To contribute you will need to register an account on this website (it only requires a username, email and password). Should you need it, TLA+ was created by Leslie Lamport.
You can learn the syntax from here. Markdown is not supported.
Tools
Currently the main areas are the TLC model checker (java), and the Visual Studio Extension.
If you're looking for some inspiration, be sure to check the monthly development update that usually has good first contribution ideas: https://foundation.tlapl.us/blog/index.html
Browse Topics: