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
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.
Browse Topics: