This chapter attempts to formally define the core concepts of TLA and TLA+ and to motivate some choices, in particular with respect to competing formalisms. Before doing so, an introductory overview of system specification in TLA+ is given using the example of a resource allocator. Lamport's book remains the definitive reference for the language itself and on the methodology for using TLA+. In particular, the module language of TLA+ is only introduced by example, and the rich standard mathematical library is only sketched.
@InCollection{merz:tlabook, author = {Stephan Merz}, title = {The Specification Language TLA\textsuperscript{+}}, booktitle = {Logics of Specification Languages}, pages = {401--451}, publisher = {Springer}, year = 2008, editor = {Dines Bjørner and Martin C. Henson}, series = {Monographs in Theoretical Computer Science}, address = {Berlin-Heidelberg} }