TLA+

https://lamport.azurewebsites.net/tla/
Admin
TLA+ is a high-level language created by Leslie Lamport for modeling programs and systems,...
Tokens:196,177
Snippets:1,652
Trust Score:7.7
Update:9 months ago
Show doc for...
Tokens:
Raw
### TLA+ Tuple Example and Access

Source: https://lamport.azurewebsites.net/tla/tutorial/session4

Shows the syntax for creating a TLA+ tuple and accessing its elements by index. It also demonstrates how to get the length of a tuple.

```text
Tuple: `<<"a",-3,"bc">>`
Accessing first element: `<<"a",-3,"bc">>[1]`
Tuple length: `Len(<<"a",-3,"bc">>)`
```

--------------------------------

### TLA+ Initialization Function Example

Source: https://lamport.azurewebsites.net/tla/tutorial/session9

An example of a TLA+ initialization function 'Init' for a multi-process algorithm. It uses a function-valued expression with the 'CASE' construct to define initial values for variables like 'pc'.

```tla
[i in D |-> exp]
```

--------------------------------

### TLA+ Operator Application Example

Source: https://lamport.azurewebsites.net/tla/practical-tla_back-link=learning.html

Demonstrates applying an operator with arguments. The example shows that defining custom operators like 'Add' is not always necessary, as built-in operators like '+' can be used directly.

```TLA+
Apply(Add, 1, 2)
(* Equivalent to: *)
Apply(+, 1, 2)
```

--------------------------------

### TLA+ Formula Simplification Examples

Source: https://lamport.azurewebsites.net/tla/tutorial/session4

Demonstrates the simplification of a TLA+ logical formula for primality checking using quantifier negation rules and abbreviation for multiple quantifiers.

```TLA+
(* Original formula *) 
(n > 1)   /       A m in 2..(n-1) :      ~ E p in 2..(n-1) : n = m * p 

(* Simplified using ~ E p : ... <=> A p : ~ ... *) 
(n > 1)   /       A m in 2..(n-1) :      A p in 2..(n-1) : ~ (n = m * p) 

(* Further simplified using n /= m * p and abbreviation A m : A p : ... <=> A m, p : ... *) 
(n > 1)   /       A m, p in 2..(n-1) : n /= m * p 

```

--------------------------------

### TLA+ Set Membership and Range Example

Source: https://lamport.azurewebsites.net/tla/tutorial/session1

This example shows TLA+ syntax for checking element membership in a set and defining a range of integers. It illustrates the use of the `\in` operator for membership and the `..` operator for creating a set of integers within a specified range.

```TLA+
3 \in (Nat \setminus -5..5)
```

--------------------------------

### TLA+ String Example and Equality Check

Source: https://lamport.azurewebsites.net/tla/tutorial/session4

Demonstrates the basic syntax for TLA+ strings and illustrates how TLC handles equality checks between strings and numbers, typically resulting in an error due to type perbedaan.

```text
Strings are like `"ab_3X"` and `""` (the empty string).
1 = "a"
```

--------------------------------

### PlusCal 1BitNoDeadlock Algorithm Example

Source: https://lamport.azurewebsites.net/tla/tutorial/session8

This PlusCal algorithm, 1BitNoDeadlock, demonstrates a scenario where the 'goto' statement is used. It aims to satisfy mutual exclusion but can suffer from livelock. The 'goto' statement here helps in minimizing labels.

```PlusCal
--algorithm 1BitNoDeadlock {
    variables flag = [i \in Procs |-> FALSE] ;
    process (P \in Procs) {
      ncs: while (TRUE) {
             skip ; 
      enter: flag[self] := TRUE ; 
         e2: if (flag[1 - self]) {              
         e3:   flag[self] := FALSE ;
               goto enter 
             } ;
         cs: skip ;
       exit: flag[self] := FALSE ;            
      }
    }
}
```

--------------------------------

### TLA+ Set Operations Examples

Source: https://lamport.azurewebsites.net/tla/tutorial/session1

This snippet provides direct TLA+ syntax for common set operations: union, intersection, set difference, and subset. These examples are useful for understanding the TLA+ notation for manipulating sets.

```TLA+
{1,1,2,2,3,3} \setminus {2, 3, 4}
```

```TLA+
{1,1,1} \subseteq {1,1,2,2}
```

```TLA+
{{"a","b"}, {"a"}, {"b"}} \cap {{"a","b","c"}, {"a","b"}, {"a"}}
```

```TLA+
{<<1>>, <<2,2>>, <<3,3,3>>} \cup {<<1>>, <<1,2>>, <<1,2,3>>}
```

--------------------------------

### TLA+ Set Difference with Infinite Sets

Source: https://lamport.azurewebsites.net/tla/tutorial/session4

Shows an example of set difference involving an infinite set ('Nat') and a finite range, demonstrating how to check membership in the resulting set.

```TLA+
Nat  -5..5
3 in (Nat  -5..5)
```

--------------------------------

### TLA+ Tuple Representation and Access

Source: https://lamport.azurewebsites.net/tla/tutorial/session1

Demonstrates the creation of a TLA+ tuple with mixed data types and how to access its elements using 1-based indexing. It also shows how to get the length of a tuple.

```TLA+
t == <<"a", -3, "bc">>
t[1] == "a"
Len(t) == 3
```

--------------------------------

### TLA+ Operator Application Example

Source: https://lamport.azurewebsites.net/tla/practical-tla

Shows two ways to apply an operator in TLA+: using a defined operator 'Add' and using the '+' operator directly. The latter is preferred when a named operator is not necessary.

```TLA+
Apply(Add, 1, 2)
```

```TLA+
Apply(+, 1, 2)
```

--------------------------------

### TLA+ Set Membership and Range Examples

Source: https://lamport.azurewebsites.net/tla/tutorial/session6

Demonstrates membership testing using 'in' and 'notin' and range generation using '..'. It shows how to create sets of integers and handle empty sets.

```TLA+
2 in {2,4,6}
2 in {1,3,5}
2 notin {1,3,5}
(-2)..1
4..2
```

--------------------------------

### PlusCal Range Operator Example

Source: https://lamport.azurewebsites.net/tla/practical-tla_back-link=learning.html

Illustrates the behavior of the range operator '..' in PlusCal, specifically showing that a range with a start value less than the end value (e.g., 3..1) results in an empty set.

```PlusCal
3..1

```

--------------------------------

### TLA+ Specification Example with Stuttering

Source: https://lamport.azurewebsites.net/tla/stuttering_back-link=advanced.html

This TLA+ specification defines a variable 'v' and asserts that it starts at 0 and increments by 1 in every step. The square brackets indicate that 'v' is the only variable whose state changes across steps, allowing other variables to take on any value, thus enabling stuttering.

```tla
Spec == (v=0)  /\  [][v' = v+1]_v  
```

--------------------------------

### TLA+ Tuple Definition and Element Access

Source: https://lamport.azurewebsites.net/tla/tutorial/session2

Demonstrates the definition and element access of a tuple in TLA+. A tuple is defined using the `<<...>>` syntax, containing elements of different data types. Element access is performed using square brackets, where the index starts at 1. The example shows a tuple with a string, a number, and another string, and retrieves the first element.

```TLA+
t == <<"a", -3, "bc">>
t[1] == "a"
```

--------------------------------

### Fine-grained Atomicity Example: Add2XFG Algorithm

Source: https://lamport.azurewebsites.net/tla/tutorial/session8

This snippet demonstrates a fine-grained atomic step (ab1a, ab1b, ab2) within a process, showing a more detailed model of execution compared to coarser-grained algorithms. It highlights how splitting increments into separate steps allows for finer interleaving of other process steps.

```pseudocode
process (AB in {3,-7}) 
variable t = -1 ;
{
  ab1a: t := x ;
  ab1b: t := t + 1 ;
  ab2: x := t 
}
```

--------------------------------

### Check pdflatex Installation (Shell)

Source: https://lamport.azurewebsites.net/tla/toolbox

Verifies if the pdflatex program is installed on your system by running a help command. This is necessary for using the TLA+ pretty-printer. If pdflatex is not found, LaTeX needs to be installed.

```shell
pdflatex -help
```

--------------------------------

### TLA+ Infinite Set Operations

Source: https://lamport.azurewebsites.net/tla/tutorial/session3

Demonstrates the usage of infinite sets like `Int` and `Nat` in TLA+ along with set difference. It shows how to check element membership even when dealing with infinite sets, and how TLC can evaluate expressions involving intersections of infinite and finite sets.

```TLA+
Nat  -5..5
3 in (Nat  -5..5)
(-5..5) cap Nat
```

--------------------------------

### TLA+ Tuple Quantifier Example (Discouraged)

Source: https://lamport.azurewebsites.net/tla/practical-tla

Shows an example of using quantifiers over tuples in TLA+. This construct is discouraged due to complexity and lack of support in tools like the TLA+ prover.

```TLA+
\A <<x, y>> \in S \X S:             Op(x, y) = Op(y, x)
```

--------------------------------

### TLA+ UNION Operator Definition and Examples

Source: https://lamport.azurewebsites.net/tla/tutorial/session4

Explains the TLA+ UNION operator, which computes the union of all sets within a given set. Provides examples of its definition and usage, including its relationship with SUBSET.

```TLA+
UNION {S1, S2, ... , S99}   _and_   S1 \cup S2 \cup  ... \cup S99
Any set S equals UNION (SUBSET S).
```

--------------------------------

### TLA+ Example: Set Containing 0-Tuple

Source: https://lamport.azurewebsites.net/tla/tutorial/session3

Demonstrates how to represent a set containing the 0-tuple in TLA+. It illustrates different syntaxes for the empty set and how they apply to tuple representation.

```TLA+
\A i \in {} : f[i] \in S
```

```TLA+
[{} -> S]
```

```TLA+
[{} -> {}]
```

```TLA+
[1..0 -> -0..-1]
```

--------------------------------

### TLA+ Example: Prime Number Definition using Quantifiers

Source: https://lamport.azurewebsites.net/tla/tutorial/session1

Demonstrates how TLA+ quantifiers '\A' and '\E' can be used to define complex mathematical properties, such as the primality of an integer 'n'. This example shows nested quantifiers and logical operators.

```plaintext
Formula defining a prime number 'n' in TLA+:
(n > 1) /\ \A m \in 2..(n-1) : ~ (\E p \in 2..(n-1) : n = m * p)
```

--------------------------------

### Initial TLA+ Translation with Single Process Set

Source: https://lamport.azurewebsites.net/tla/tutorial/session7

Shows the initial part of a TLA+ translation for an algorithm using a single process set 'AB'. It defines variables, the process set, initialization conditions, and the initial states for actions within the process set, demonstrating the adaptation from separate process declarations.

```tla
VARIABLES x, pc, ta, tb
vars == << x, pc, ta, tb >>
ProcSet == {3} \cup {-7}
Init == /\ x = 0
        /\ ta = -1
        /\ tb = -1
        /\ pc = [self \in ProcSet |-> CASE self = 3 -> "a1"
                                        [] self = -7 -> "b1"]
a1 == /\ pc[3] = "a1"
      /\ ta' = x
      /\ pc' = [pc EXCEPT ![3] = "a2"]
      /\ UNCHANGED << x, tb >>
a2 == ...
b1 == /\ pc[-7] = "b1"
      /\ tb' = x
      /\ pc' = [pc EXCEPT ![-7] = "b2"]
      /\ UNCHANGED << x, ta >>
b2 == ...
```

--------------------------------

### TLA+ Set Building Syntax

Source: https://lamport.azurewebsites.net/tla/tutorial/session4

Demonstrates the TLA+ 'building' method for set construction, where new elements are generated from existing sets. This is compared to 'subsetting' and is noted to be less efficiently evaluated by TLC for membership tests if the resulting set is infinite.

```TLA+
{exp : x \in S}
```

```TLA+
{2 * n  : n \in Int}
```

```TLA+
{ { {<<i, j, k>> : i \in Int} : j \in Int } : k \in Nat }
```

--------------------------------

### PlusCal `SillyTupleMax` Algorithm Example

Source: https://lamport.azurewebsites.net/tla/tutorial/session4

An example PlusCal algorithm named `SillyTupleMax` that repeatedly examines an arbitrary element of the input tuple `inp` and terminates with `max` set to that value if it's the maximum. It uses a boolean flag `b` to control loop termination and includes assertions for correctness.

```PlusCal
--algorithm SillyTupleMax {
   variables inp \in Tuples, max = minValue, I = 1..Len(inp), b = (I /= {}) ;    
   { while (b) {
       with (i \in I) {
         if (\A j \in I : inp[i] >= inp[j]) {
            max := inp[i] ;
            b := FALSE
          }
       }
     } ; 
     assert IF inp = << >> THEN max = minValue
                           ELSE /\ \E n \in 1..Len(inp) : max = inp[n]
                                /\ \A n \in 1..Len(inp) : max >= inp[n]
   }
}
```

--------------------------------

### LaTeX Document Style Setup - IEEEtran.sty

Source: https://lamport.azurewebsites.net/tla/IEEEtran

This snippet shows the basic setup and configuration of the IEEEtran.sty LaTeX document style file. It defines boolean variables for draft and technote modes, sets font sizes, and adjusts margins and spacing according to the selected options. It also includes definitions for different font sizes to avoid external file loading.

```latex
\documentclass[..,Xpt,twoside]{IEEEtran}
\author{..}
\title{..}
\maketitle
\begin{abstract}...\end{abstract}
\begin{keywords}...\end{keywords}
...\begin{biography}{Author's name}...\end{biography}
\end{document}
```

```latex
%% define new needed boolean variables
\newif\if@tmptwocolumn  \@tmptwocolumnfalse
\newif\if@draftversion  \@draftversionfalse
\newif\if@technote      \@technotefalse

\def\@ptsize{10}
\@namedef{ds@9pt}{\def\@ptsize{9}}
\@namedef{ds@10pt}{\def\@ptsize{10}}
\@namedef{ds@11pt}{\def\@ptsize{11}}
\@namedef{ds@12pt}{\def\@ptsize{12}}
\@namedef{ds@twoside}{\@twosidetrue \@mparswitchtrue}
\@namedef{ds@draft}{\global\@draftversiontrue} % sets variable for draft
\@namedef{ds@technote}{\global\@technotetrue}  % sets variable for techn. note
\@namedef{ds@twocolumn}{\global\@tmptwocolumntrue } 
\@options
```

```latex
%% change sizes and margins
\topmargin      -16.0mm
\oddsidemargin  -11.0mm
\evensidemargin -11.0mm
\textheight     243.5mm
\textwidth      183.0mm
\columnsep        4.1mm
\parindent        1.0em
\headsep          6.3mm
\headheight        12pt
\lineskip           1pt
\normallineskip     1pt
\def\baselinestretch{1}

\if@draftversion 
\topmargin       -6.0mm
\oddsidemargin      0mm
\evensidemargin     0mm
\textheight     223.5mm
\textwidth      161.0mm
\fi

\marginparsep      10pt
\marginparwidth    20pt
\marginparpush     25pt

\partopsep          \z@
\topsep           1.3ex
\parsep             \z@
\itemsep            \z@
%% see further below for lists
```

```latex
%% FONT DEFINITION: avoids having to read in font files.
%% Check if we have selected 9 points
\def\@tempa{9}\ifx\@ptsize\@tempa
\typeout{-- This is a 9 point document}
\def\@normalsize{\@setsize\normalsize{10.7pt}\ixpt\@ixpt
\abovedisplayskip 1em plus2pt minus5pt\belowdisplayskip \abovedisplayskip
\abovedisplayshortskip \z@ plus3pt\belowdisplayshortskip .6em plus3pt minus3pt}
\def\small{\@setsize\small{9.12pt}\viiipt\@viipt}
\def\footnotesize{\@setsize\footnotesize{8.15pt}\viipt\@vipt}
\def\scriptsize{\@setsize\scriptsize{8pt}\vipt\@vpt}
\def\tiny{\@setsize\tiny{5pt}\vpt\@vpt}
\def\large{\@setsize\large{12pt}\xpt\@xpt}
\def\Large{\@setsize\Large{14pt}\xiipt\@xiipt}
\def\LARGE{\@setsize\LARGE{18pt}\xivpt\@xivpt}
\def\huge{\@setsize\huge{22pt}\xviipt\@xviipt}
\def\Huge{\@setsize\Huge{25pt}\xxpt\@xxpt}
\fi
%% Check if we have selected 10 points
\def\@tempa{10}\ifx\@ptsize\@tempa
\typeout{-- This is a 10 point document}
\def\@normalsize{\@setsize\normalsize{11.9pt}\xpt\@xpt
\abovedisplayskip 1em plus2pt minus5pt\belowdisplayskip \abovedisplayskip

```

--------------------------------

### TLA+ Tuple Creation and Access

Source: https://lamport.azurewebsites.net/tla/tutorial/session6

Demonstrates the creation of a TLA+ tuple with mixed data types and accessing its elements using 1-based indexing. It also shows how to calculate the length of a tuple.

```TLA+
Len(<<"a",-3,"bc">>) 
<<"a",-3,"bc">>[1]
```

--------------------------------

### Efficient Leftpad Algorithm Logic

Source: https://lamport.azurewebsites.net/tla/practical-tla_back-link=learning.html

Illustrates the logic for an efficient Leftpad algorithm using a helper variable 'v' and string concatenation '\o'. The goal is to achieve O(log k) complexity instead of O(k).

```pseudocode
I(output, v, in_c, in_n, in_str) // Assertion invariant
// ... algorithm logic ...
assert I(output, v, in_c, in_n, in_str)
```

--------------------------------

### TLA+ Theorem Assertion Example

Source: https://lamport.azurewebsites.net/tla/practical-tla_back-link=learning.html

Demonstrates how to assert a mathematical formula as a theorem in TLA+. The truth of the theorem depends on the context defined by CONSTANT and ASSUME clauses.

```TLA+
CONSTANT x
ASSUME x \in 3..10
THEOREM x+2 > 4
```

```TLA+
x == 2
THEOREM x+2 > 4
```

--------------------------------

### Import TLA+ Module Definitions using INSTANCE

Source: https://lamport.azurewebsites.net/tla/tutorial/session11-1

This snippet shows how to import all definitions from a TLA+ module into the current module using the INSTANCE keyword. It allows aliasing the imported module's definitions by prepending a chosen identifier, facilitating name-space management and avoiding naming conflicts. This is useful for incorporating specifications or other modules without direct copying.

```tla
Foo == INSTANCE Session11a
```

--------------------------------

### PlusCal: Algorithm Initialization and Process Variables

Source: https://lamport.azurewebsites.net/tla/tutorial/session10

Initializes the global message queues and sets up the 'depth' and 'parent' variables for each process. 'depth' is initialized to 0 for the root and 'MaxNodes' for others, while 'parent' is initialized to the process's own identifier.

```PlusCal
--algorithm FindRoutes {
   variable msgs = [q in Queues |-> IF q[1] = root THEN <<0>> 
                                                    ELSE << >>] ;
   fair process (node in Nodes) 
     variables depth = IF self = root THEN 0 ELSE MaxNodes ,
               parent = self ;              
     { _the process's code_ 
     }
}

```

--------------------------------

### Handle TLA+ Syntax Errors

Source: https://lamport.azurewebsites.net/tla/tutorial/session2

Shows the error message typically displayed by the TLA+ Toolbox when a syntactically incorrect expression is entered. It guides users on how to identify and fix errors.

```tla
**No error information.
**
```

--------------------------------

### PlusCal Algorithm Initialization and Process Structure

Source: https://lamport.azurewebsites.net/tla/tutorial/session10

Illustrates the basic structure of the 'FindRoutes' PlusCal algorithm. It defines global message queues and initializes process-local variables like 'depth' and 'parent'. The code sets initial depths to 0 for the root and 'MaxNodes' for others, and initializes 'parent' to self for all nodes.

```PlusCal
--algorithm FindRoutes {
      variable msgs = [q in Queues |-> IF q[1] = root THEN <<0>> 
                                                       ELSE << >>] ; 
      fair process (node in Nodes) 
        variables depth = IF self = root THEN 0 ELSE MaxNodes ,
                  parent = self ;              
        { _the process's code_ 
        }
   }

```

--------------------------------

### TLA+ Tuple Creation and Access

Source: https://lamport.azurewebsites.net/tla/tutorial/session4

Demonstrates the creation of a TLA+ tuple and accessing its elements by index. TLA+ tuples are 1-indexed.

```TLA+
Len(<<"a",-3,"bc">>) \
// Returns: 3

<<"a",-3,"bc">>[1] \
// Returns: "a"
```
Tokens:
Raw