TLA+: Difference between revisions

| publisher = IOS Press,
| location=Amsterdam

| journalseries = NATO Science Series, III: Computer and Systems Sciences

| license = [[MIT License]]<ref name="toolboxlicense">{{cite web

| access-date = 10 May 2015}}

'''TLA⁺''' is a [[formal specification]] language developed by [[Leslie Lamport]]. It is used tofor designdesigning, modelmodelling, documentdocumentation, and verifyverification of programs, especially [[concurrent systems]] and [[distributed systems]]. TLA⁺ hasis beenconsidered describedto asbe exhaustively-testable [[pseudocode]],<ref name="awsorig">

TLA⁺ was introduced in 1999, following several decades of research into a verification method for concurrent systems. AEver since, a toolchain has sincebeen developed, including an [[interactive development environment|IDE]] and a distributed model checker. The pseudocode-like language [[PlusCal]] was created in 2009; it [[Source-to-source compiler|transpiles]] to TLA⁺ and is useful for specifying sequential algorithms. TLA⁺² was announced in 2014, expanding language support for proof constructs. The current TLA⁺ reference is [http://research.microsoft.com/en-us/um/people/lamport/tla/hyperbook.html The TLA⁺ Hyperbook] by Leslie Lamport.

{{quoteblockquote|The usefulness of systems of this sort [on discrete time] does not depend on any serious metaphysical assumption that time is discrete; they are applicable in limited fields of discourse in which we are concerned only with what happens next in a sequence of discrete states, e.g. in the working of a digital computer.}}

{{quoteblockquote|However, I became disillusioned with temporal logic when I saw how Schwartz, Melliar-Smith, and Fritz Vogt were spending days trying to specify a simple [[FIFO (computing and electronics)|FIFO queue]]&nbsp;– arguing over whether the properties they listed were sufficient. I realized that, despite its aesthetic appeal, writing a specification as a conjunction of temporal properties just didn't work in practice.<ref name="lamport-spec"/>}}

</ref> and the TLA⁺ proof system (TLAPS) in 2012.<ref name="tlaps-survey"/> TLA⁺² was announced in 2014, adding some additional language constructs as well as greatly increasing in-language support for the proof system.<ref name="tla2guide" /> Lamport is engaged in creating an updated TLA⁺ reference, "The TLA⁺ Hyperbook". The incomplete work is [http://research.microsoft.com/en-us/um/people/lamport/tla/hyperbook.html available] from his official website. Lamport is also creating [http://lamport.azurewebsites.net/video/videos.html The TLA⁺ Video Course], described therein as "a work in progress that consists of the beginning of a series of video lectures to teach programmers and software engineers how to write their own TLA⁺ specifications".

<nowiki> </nowiki>Temporal existential and universal quantification are included in TLA⁺, although without support from the tools.

The foundational data structure of TLA⁺ is the set. Sets are either explicitly enumerated or constructed from other sets using operators or with <syntaxhighlight lang="tex" inlinecode>{x \in S : p}</syntaxhighlightcode> where ''p'' is some condition on ''x'', or <syntaxhighlight lang="tex" inlinecode>{e : x \in S}</syntaxhighlightcode> where ''e'' is some function of ''x''. The unique [[empty set]] is represented as <code>{}</code>.

| name = TLA⁺ Toolbox

| title = TLA⁺ Toolbox

| latest release version = 1.7.02 Theano

| latest release date = {{Start date and age|20202022|0402|2502}}<!-- {{Start date and age|YYYY|MM|DD|df=yes/no}} -->

| latest preview version = 1.78.10 Clarke

| latest preview date = {{Start date and age|2020|0512|0106}}

</ref> It is distributed separately from the rest of the TLA⁺ tools and is free software, distributed under the [[BSD license]].<ref>[https://tla.msr-inria.inria.fr/tlaps/content/Home.html TLA⁺ Proof System]</ref> TLA⁺² greatly expanded language support for proof constructs.

| title = TLA⁺FM Proofs2012: Formal Methods

| title = WhyAbstract AmazonState ChoseMachines, Alloy, B, TLA⁺, VDM, and Z

| journalseries = Lecture Notes in Computer Science

Altreonic NV used TLA⁺ to [[Model checking|model check]] [[OpenComRTOS#Formal development approach|OpenComRTOS]].

A [[key-value store]] with [[snapshot isolation]]:

<syntaxhighlight lang="Haskelltex">

A rule-based [[firewall (computing)|firewall]]:

<syntaxhighlight lang="Haskelltex">

A multi-car [[elevator]] system:

<syntaxhighlight lang="Haskelltex">