TLA+ is a language intended for the high-level specification of
reactive, distributed, and in particular asynchronous systems.
Combining the linear-time temporal logic TLA and classical
set-theory, it provides an expressive specification formalism and
supports assertional verification.
The definition of stuttering invariance given in section 2.4 (p.11) is
erroneous, since it does not identify two sequences that differ in infinitely
many stuttering steps. Please refer to the article
The Specification Language TLA+, which
supersedes this paper.
Reference
@Article{merz:tlaplogic,
author = {Stephan Merz},
title = {On the Logic of TLA{\textsuperscript{+}}},
journal = {Computers and Informatics},
year = 2003,
volume = 22,
pages = {351--379}
}