Learn TLA+

https://learntla.com
Admin
A free online resource for learning TLA+, a formal specification language for designing and...
Tokens:56,091
Snippets:789
Trust Score:7.5
Update:5 months ago
Show doc for...
Tokens:
Raw
### Basic PlusCal Algorithm Example

Source: https://learntla.com/core/invariants.html

A simple PlusCal algorithm demonstrating variable declaration. This is a starting point for defining algorithms.

```PlusCal
(*--algorithm find_duplicates
variables
  seq \in S \X S \X S \X S;
  is_unique = TRUE;
begin
  is_unique := FALSE;
end algorithm; *)
```

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

### For All Quantifier Example

Source: https://learntla.com/core/invariants.html

Demonstrates the \A (forall) quantifier, testing if a condition is true for every element in a set. This example shows a false condition for the set {1, 2, 3} and elements less than 2.

```tla
\A x \in {1, 2, 3}: x < 2
```

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

### Example Spec with Randomization

Source: https://learntla.com/reference/standard-library.html

This example demonstrates how to use the Randomization module within a TLC specification. Replacing a fixed set with RandomSubset can lead to non-deterministic behavior and reduced state exploration.

```TLA+
EXTENDS Integers, TLC, Randomization
VARIABLE x

Init ==
    /\ x = 0

Next ==
    \/ /\ x = 0
       /\ x' \in {1, 2, 3}
    \/ /\ PrintT(x)
       /\ UNCHANGED x

* Magic magic magic
Spec == Init /\ [][Next]_x

```

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

### Example Usage of Sort Operator

Source: https://learntla.com/core/functions.html

Demonstrates the usage of the `Sort` operator with a sample sequence.

```tla
>>> Sort(<<8, 2, 7, 4, 3, 1, 3>>)
<<1, 2, 3, 3, 4, 7, 8>>
```

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

### TLCGet Example for Current Behavior Level

Source: https://learntla.com/reference/standard-library.html

Shows how to retrieve the current behavior level during model checking using TLCGet.

```TLA+
`TLCGet("level")` can be used to bound an unbound model. 

```

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

### Permutations Function Example

Source: https://learntla.com/reference/standard-library.html

Demonstrates the usage of the Permutations function to generate all possible permutations of a given set.

```TLA+
>>> Permutations({"a", "b"})

{[b |-> "b", a |-> "a"],
 [b |-> "a", a |-> "b"]}

```

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

### Symmetric Set Examples

Source: https://learntla.com/core/constants.html

These examples illustrate sequences that can be treated as symmetric by TLC when using model values. Swapping elements like s1 and s2 can result in equivalent states if they are model values.

```tlaplus
(1) <<s1, s2, s3>>
(2) <<s2, s1, s3>>

(3) <<s1, s2, s2>>
(4) <<s2, s3, s3>>
```

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

### TLA+ Set Operations Examples

Source: https://learntla.com/core/operators.html

Provides examples of common set operations: union, intersection, and set difference. These operations are fundamental for working with collections of unique, unordered elements.

```tla
>>> {1, 3} \union {1, 5}

{1, 3, 5}
```

```tla
>>> {1, 3} \intersect {1, 5}

{1}
```

```tla
>>> {1, 3} \ {1, 5}

{3}
```

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

### Example Output of ToClock2

Source: https://learntla.com/core/operators.html

Shows the result of calling the ToClock2 operator with a specific input value.

```plaintext
>>> ToClock2(90000)

<<25, 0, 0>>
```

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

### Exists Quantifier Example

Source: https://learntla.com/core/invariants.html

Demonstrates the \E (exists) quantifier, testing if a condition is true for at least one element in a set. This example shows a true condition for the set {1, 2, 3} and elements less than 3.

```tla
\E x \in {1, 2, 3}: x < 3
```

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

### Nondeterministic Addition with Prophecy Variables

Source: https://learntla.com/topics/aux-vars.html

This example uses a prophecy variable to represent nondeterministic digit selection. It results in more starting states but a single behavior per state.

```tla
variables
  i = 1;
  sum = 0;
  aux_proph_digits \in [1..NumInputs -> Digits];

begin
  Calculator:
    while i <= NumInputs do
      sum := sum + aux_proph_digits[i];
      i := i + 1;
    end while;


```

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

### TLA+ Product Function Example

Source: https://learntla.com/core/functions.html

Creates a function 'Prod' that maps pairs of numbers from a set S to their product. The domain is S x S.

```tla
Prod ==
  LET S == 1..10 IN
  [p \in S \X S |-> p[1] * p[2]]

\* Prod[<<3, 5>>] = 15

```

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

### TLA+ Action Constraint Example

Source: https://learntla.com/topics/toolbox.html

An action constraint restricts exploration to states where the specified action is true. This example limits exploration to states where 'x' increases.

```TLA+
x' > x
```

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

### Nondeterministic Addition with Standard Variables

Source: https://learntla.com/topics/aux-vars.html

This example demonstrates nondeterministically adding numbers using standard variables within a loop. Each iteration branches 10 ways.

```tla
Digits == 0..9

(* --algorithm calculator
variables
  i = 0;
  sum = 0;

begin
  Calculator:
    while i < NumInputs do
      with x \in Digits do
          * Add
          sum := sum + x;
      end with;
      i := i + 1;
    end while;


```

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

### Basic Scratch File Setup

Source: https://learntla.com/core/setup.html

A scratch file allows testing operator outputs without running the full spec. Set 'no behavior spec' and use the 'Evaluate Constant Expression' box in the model checker to test expressions like 'Eval'.

```tla
---- MODULE scratch ----
EXTENDS Integers, TLC, Sequences

Eval == 0
====

```

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

### ToJson Example for Multi-arity Function Conversion

Source: https://learntla.com/reference/standard-library.html

Demonstrates converting a multi-arity TLA+ function into a JSON object, using TLA+ tuple notation for keys.

```TLA+
>>> ToJson([p, q \in BOOLEAN |-> p => q])

"{"<<FALSE, FALSE>>":true,
  "<<TRUE, FALSE>>":false,
  * ...

```

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

### Use Helper Actions for Complex Updates in TLA+

Source: https://learntla.com/topics/tips.html

Break down complex state transitions into smaller, reusable helper actions. This example shows updating a program counter (pc).

```TLA+
Trans(agent, a, b) ==
  /\ pc[agent] = a
  /\ pc' = [pc EXCEPT ![agent] = b]
```

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

### TLA+ Calculator Error Trace Example

Source: https://learntla.com/core/nondeterminism.html

An example error trace from the TLA+ model checker, showing the sequence of states leading to the target sum of 417 with 5 inputs.

```tla
State 1:
/\ sum = 0
/\ i = 0

State 2:
/\ sum = 1
/\ i = 1

State 3:
/\ sum = 10
/\ i = 2

State 4:
/\ sum = 60
/\ i = 3

State 5:
/\ sum = 420
/\ i = 4

State 6:
/\ sum = 417
/\ i = 5
```

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

### Conditional Initial States with DEBUG Constant

Source: https://learntla.com/core/constants.html

This example demonstrates how a DEBUG constant can be used to define different sets of initial states for model checking, allowing for easier debugging or full exploration.

```tlaplus
Inputs ==
IF DEBUG
THEN {<<1, 2, 3, 4>>}
ELSE S \X S \X S \X S
```

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

### TLCModelValue Example for Constant Definition

Source: https://learntla.com/reference/standard-library.html

Illustrates creating a new model value for use in constant definitions.

```TLA+
CONSTANT Threads <-
  TLCModelValue(ToString(i)): i \in 1..3


```

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

### Queue Read with await

Source: https://learntla.com/core/concurrency.html

This example shows how to use 'await' to ensure a reader only proceeds if the queue is not empty. This prevents the reader from attempting to access elements from an empty queue, which could lead to errors or deadlocks.

```PlusCal
 process reader = 0
 begin
   ReadFromQueue:
     await queue # <<>>;
       total := total + Head(queue);
       queue := Tail(queue);
     goto ReadFromQueue;
 end process;
 end algorithm; (*
```

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

### Add a reader process to the TLA+ concurrency example

Source: https://learntla.com/core/concurrency.html

This snippet extends the previous TLA+ module by adding a reader process that reads from the queue. It shows how to define multiple processes within the same algorithm.

```tlaplus
+ 
+process reader = 0
+begin
+  ReadFromQueue:
+    total := total + Head(queue);
+    queue := Tail(queue);
+end process;
end algorithm; *)
====
```

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

### Python Zip Function Example

Source: https://learntla.com/core/functions.html

Illustrates the behavior of Python's built-in 'zip' function, which pairs elements from two iterables up to the length of the shorter iterable.

```python
list(zip([1, 2], ["a", "b", "c"]))

```

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

### Boolean Operator Examples

Source: https://learntla.com/core/tla.html

Illustrates choices of `<<hr, hr'>>` for which the `Next` action is true, meaning it accurately describes the value of `hr` in the next state.

```TLA+
<<1, 2>>
<<3, 4>>
<<12, 1>>

```

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

### TLC Configuration with Alias

Source: https://learntla.com/topics/cli.html

This example demonstrates using the `ALIAS` directive in a TLC configuration file to customize the error trace output, similar to the Error Trace Explorer.

```tla
---- MODULE aliases ----
EXTENDS Integers

VARIABLE x
Init ==
  x = 0

Next == x' = x + 1
Inv == x < 10
Spec == Init /\ [][Next]_x

Alias ==
  [x |-> x,
   nextx |-> x',
   incx |-> x + 1]
====

```

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

### Example of an Unbound TLA+ Model

Source: https://learntla.com/topics/unbound-models.html

This algorithm demonstrates an unbound model by continuously incrementing a variable 'x'. It will never finish model checking because there are infinite distinct states.

```TLA+
---- MODULE Unbound ----
EXTENDS Integers

(*--algorithm seriously_dont_run_this
variable x = 0
begin
  while TRUE do
    x := x + 1;
  end while;
end algorithm; *)
```

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

### ToJson Example for Sequence Conversion

Source: https://learntla.com/reference/standard-library.html

Converts a TLA+ sequence (range of integers) into a JSON array string.

```TLA+
>>> ToJson(1..3)
"[1,2,3]"

```

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

### ToJson Example for Function Conversion

Source: https://learntla.com/reference/standard-library.html

Converts a TLA+ function into a JSON object string, where keys are string representations of domain elements.

```TLA+
>>> ToJson([x \in 0..2 |-> x^2])

"{\"0\":0,\"1\":1,\"2\":4}"

```

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

### PlusCal Goroutine Initialization

Source: https://learntla.com/examples/golang.html

This PlusCal code snippet demonstrates how to emulate Go's goroutine spawning by using an 'initialized' flag. Each goroutine process awaits this flag before executing its main logic, simulating the asynchronous start of a Go routine.

```PlusCal
variables
  initialized = [w \in Routines |-> FALSE];

\* ...

process goroutine \in Routines
begin
  Work:
    await initialized[self];
\* ...


```

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

### Function Set for Server Status

Source: https://learntla.com/core/functions.html

Example of a function set where the domain is a set of servers and the codomain is a set of possible server states.

```tla
status \in [Server -> {"online", "booting", "offline"}]
```

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

### False Boolean Operator Examples

Source: https://learntla.com/core/tla.html

Illustrates choices of `<<hr, hr'>>` for which the `Next` action is false, meaning it does not accurately describe the value of `hr` in the next state.

```TLA+
<<1, 1>>
<<12, 13>>
<<4, 6>>
<<9, "corn">>

```

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

### PlusCal Interruptible Algorithm Modeling

Source: https://learntla.com/core/tla.html

Illustrates how to model interruptible algorithms in PlusCal using nested 'either' blocks to handle resets to a 'Start' state. This approach can become verbose for many reset points.

```pluscal
A:
  either
    * A step stuff
  or
    goto Start;
  end either;
B:
  either
    * B step stuff
  or
    goto Start;
  end either;
* ...
```

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

### Ignoring Part of the State Space in TLA+

Source: https://learntla.com/topics/optimization.html

This TLA+ example demonstrates how to artificially constrain the model checker to a specific part of the state space by defining 'FastInit' and 'FastNext' operators that include additional constraints on the base 'Init' and 'Next' operators.

```TLA+
Init ==
  x \
in 1..10

FastInit ==
  /\ Init
  /\ x = 3

Next ==
  /\ IncX
  /\ DecX

FastNext ==
  /\ Next
  /\ IncX => x' < 5

FastSpec == FastInit /\ [][FastNext]_vars

```

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

### Basic PlusCal Algorithm Structure

Source: https://learntla.com/core/pluscal.html

This is a fundamental PlusCal algorithm demonstrating variable declaration and basic update statements within labeled sections. It serves as a starting point for understanding PlusCal syntax.

```PlusCal
---- MODULE pluscal ----
EXTENDS Integers, TLC

(* --algorithm pluscal
variables
 x = 2;
 y = TRUE;

begin
  A:
    x := x + 1;
  B:
    x := x + 1;
    y := FALSE;
end algorithm; *)
====
```

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

### TLA+ State Constraint Example

Source: https://learntla.com/topics/toolbox.html

Use a state constraint to limit the states TLC explores. States violating the constraint are discarded, preventing further exploration from them. Invariants are checked before the state constraint is applied.

```TLA+
EXTENDS Integers
VARIABLE x

Init == x = 0
Next == x' = x + 1
Inv == x < 10
Spec == Init /\ [][Next]_x

```

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

### Initialize TLA+ Module with Content

Source: https://learntla.com/core/setup.html

Replace the placeholder content with your actual TLA+ specification. Ensure the module name in the first line matches your filename if it differs from 'wire'.

```tla
---- MODULE wire ----
EXTENDS Integers, TLC, Sequences

(* body of the spec *)

====

```

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

### TLA+ Interruptible Algorithm Modeling

Source: https://learntla.com/core/tla.html

Shows a more concise TLA+ representation for interruptible algorithms, using disjunctions to model parallel steps and a separate disjunct to handle resets to the 'Start' state. This is more scalable than the PlusCal equivalent.

```tla
\/ \/ A
   \/ B
   \/ C
   \/ D
\/ pc' = "Start"
```

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

### Get Struct Keys with DOMAIN

Source: https://learntla.com/core/functions.html

Use the `DOMAIN` keyword to get a set of all keys in a struct. This is analogous to `Len` for sequences.

```TLA+
RangeStruct(struct) == {struct[key]: key \in DOMAIN struct}
```

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

### Define Multiple Initial States for a Sequence

Source: https://learntla.com/core/pluscal.html

Use the \"in\" operator to specify multiple possible starting values for a sequence variable. TLC will test the model for each specified initial state.

```tla
 EXTENDS Integers, Sequences, TLC
 
 (*--algorithm dup
-  variable seq = <<1, 2, 3, 2>>;
+  variable seq \in {<<1, 2, 3, 2>>, <<1, 2, 3, 4>>};
   index = 1;
   seen = {};
   is_unique = TRUE;


```

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

### TLA+ Definition Override Example

Source: https://learntla.com/topics/toolbox.html

Override a definition to limit a variable to a finite set for model checking. This example restricts the 'Int' type to values between 1 and 10.

```TLA+
Int <- 1..10
```

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

### TLA+ LET for Programming-Style Conversion

Source: https://learntla.com/core/operators.html

Demonstrates using LET to break down a complex calculation into smaller, named steps, similar to how one might implement an algorithm in a programming language.

```tla
ToClock2(seconds) ==
  LET
    h == seconds \div 3600
    h_left == seconds % 3600
    m == h_left \div 60
    m_left == h_left % 60
    s == m_left
  IN
    <<h, m, s>>
```

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

### TLA+ View Expression Example

Source: https://learntla.com/topics/toolbox.html

Define a VIEW expression to alter how TLC distinguishes states. Instead of using all variables, the VIEW expression becomes the criteria for state equality. This example uses only the 'x' variable.

```TLA+
VIEW x
```

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

### Basic TLC Configuration File

Source: https://learntla.com/topics/cli.html

A sample configuration file for TLC. It specifies the main specification, invariants, properties, and constants for the model check.

```tla
SPECIFICATION Spec

INVARIANT Inv1, Inv2
PROPERTY Prop1

CONSTANT
  Const1 = {"a", "b", "c"}
  Const2 = Const2
  Const3 = {c1, c2, c3}


```

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

### Get Range of a Function

Source: https://learntla.com/core/functions.html

Defines the `Range` operator which returns the set of all outputs of a function.

```tla
Range(f) == {f[x] : x \in DOMAIN f}
```

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

### Get Domain of a Function

Source: https://learntla.com/core/functions.html

Defines the `DOMAIN` operator which returns the set of all inputs to a function.

```tla
DOMAIN(f) == {x \in</thead><tbody><tr><td>...</td><td>...</td></tr></tbody></table>
```

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

### Get all Sub-Bags

Source: https://learntla.com/reference/standard-library.html

Use `SubBag` to generate a set containing all possible sub-bags of a given bag.

```TLA+
SubBag(EmptyBag) = {<<>>}
SubBag([a |-> 2]) = {<<>>, [a |-> 1], [a |-> 2]}
```

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

### Define LockCantBeStolen using Helper Action

Source: https://learntla.com/core/action-properties.html

Demonstrates using a helper action 'BecomesNull' within an action property. This makes the property definition more readable by abstracting the condition 'x' = NULL'.

```TLA+
BecomesNull(x) == x' = NULL

LockCantBeStolen ==
   [][lock # NULL => BecomesNull(lock)]_lock
```

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

### Sequence Subsequence

Source: https://learntla.com/reference/standard-library.html

Extracts a subsequence from a given sequence using inclusive start and end indices.

```tlaplus
SubSeq(<<7, 8, 9>>, 1, 2) = <<7, 8>>

```

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

### Instantiate a parameterized module with specific values in TLA+

Source: https://learntla.com/core/modules.html

When importing a parameterized module, use the WITH clause to provide values for its constants.

```tla
Origin == INSTANCE Point WITH X <- 0, Y <- 0
```

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

### Get Number of Copies of an Element

Source: https://learntla.com/reference/standard-library.html

 `CopiesIn` returns the count of a specific element `e` in the bag, or 0 if the element is not present.

```TLA+
CopiesIn("a", EmptyBag) = 0
CopiesIn("a", [a |-> 5, b |-> 3]) = 5
```

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

### TLA+ Module for Channels and Goroutines

Source: https://learntla.com/examples/golang.html

Defines constants, routines, and variables for channel communication. Includes macros for goroutine initialization and channel operations (buffered and unbuffered).

```tla
---- MODULE channels ----
EXTENDS Integers, TLC, Sequences

CONSTANTS NumRoutines, NumTokens
Routines == 1..NumRoutines

(* --algorithm channels

variables
  channels = [tokens |-> 0, found |-> {}];
  buffered = [tokens |-> NumTokens];
  initialized = [w \in Routines |-> FALSE];


```

```tla
macro go(routine) begin
  initialized[routine] := TRUE;
end macro


```

```tla
macro write_buffered(chan) begin
  await channels[chan] < buffered[chan];
  channels[chan] := channels[chan] + 1;
end macro;

macro receive_channel(chan) begin
  if chan \in DOMAIN buffered then
    await channels[chan] > 0;
    channels[chan] := channels[chan] - 1;
  else
    await channels[chan] # {};
    with w \in channels[chan] do
      channels[chan] := channels[chan] \ {w}
    end with;
  end if;
end macro;


```

```tla
procedure write_unbuffered(chan) begin
  DeclareSend:
    channels[chan] := channels[chan] \union {self};
  Send:
    await self \notin channels[chan];
    return;
end procedure


```

```tla
process goroutine \in Routines
begin
  A:
    await initialized[self];
    call write_unbuffered("found");
  B:
    receive_channel("tokens");
end process;


```

```tla
process main = 0
variables i = 1;
begin
  Main:
    while i <= NumRoutines do
      write_buffered("tokens");
      go(i);
      i := i + 1;
    end while;
  Get:
    while i > 1 do
      i := i - 1;
      receive_channel("found");
    end while;
end process;

end algorithm; *)


```

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

### Base TLA+ Model for Optimization

Source: https://learntla.com/topics/optimization.html

This is the initial TLA+ module used as a baseline for demonstrating optimization techniques. It includes constants for maximum numbers and workers, and a PlusCal algorithm for processing tasks.

```tlaplus
---- MODULE optimization ----
EXTENDS Integers, Sequences, TLC
CONSTANTS MaxNum, Workers

(*--algorithm alg
variables
  i = 1;
  to_process = [w \in Workers |-> {}];

process writer = "writer"
begin 
  Write:
    while i <= MaxNum do
      with w \in Workers do
        to_process[w] := @ \union {i};
        i := i + 1;
      end with;
    end while;
end process;

process worker \in Workers
variable total = 0;
local = 0;
begin
  Read:
    with x \in to_process[self] do
      local := x;
      to_process[self] := @ \ {local};
    end with;
    Update:
      total := total + local;
      goto Read;
end process;

end algorithm; *)
====
```

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

### TLA+ Helper Action for Transitions

Source: https://learntla.com/core/tla.html

A helper action to simplify state transitions between labels in TLA+.

```tla
Trans(state, from, to) ==
  /\ pc[state] = from
  /\ pc' = [pc EXCEPT ![state] = to]

IncCounter(self) ==
  /\ Trans(self, "IncCounter", "Done")
  /\ counter' = counter + 1


```

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

### Namespace an INSTANCE in TLA+

Source: https://learntla.com/core/modules.html

Namespace operators from an imported module using the INSTANCE keyword followed by a name. Access operators using the '!' operator.

```tla
Foo == INSTANCE Sequences
```

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

### Specify Metadata Directory with TLC

Source: https://learntla.com/topics/cli.html

Use the `-metadir dir` option to store the seen statespace in a specified directory instead of the current one. This is useful for easier cleanup when scripting.

```bash
-metadir dir
```

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

### Map to Get Sequence Range

Source: https://learntla.com/core/operators.html

Use set comprehension with mapping to extract all elements from a sequence. `Range(seq)` defines the set of elements present in `seq`.

```tla
Range(seq) == {seq[i]: i \in 1..Len(seq)}
```

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

### Partially parameterize a module instance in TLA+

Source: https://learntla.com/core/modules.html

Provide some but not all constants when instantiating a module. The remaining constants can be provided at runtime.

```tla
XAxis(X) == INSTANCE Point WITH Y <- 0
```

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

### Colorize and Label Graphviz Edges with TLC

Source: https://learntla.com/topics/cli.html

Enhance Graphviz output with `-dump dot,colorize file` to color edges by action, or `-dump dot,actionlabels` to label edges with corresponding actions. Both options can be used together.

```bash
-dump dot,colorize file
```

```bash
-dump dot,actionlabels
```

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

### Using ModelConstraint to Bound a Model

Source: https://learntla.com/topics/unbound-models.html

Apply a ModelConstraint to limit the state space explored by the model checker. This example constrains 'x' to a maximum value, effectively bounding the model.

```TLA+
ModelConstraint == x \in 0..MaxInt
```

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

### Translate PlusCal to TLA+ CLI

Source: https://learntla.com/topics/cli.html

Use this command to translate a PlusCal algorithm in a TLA+ file to TLA+ syntax. It creates a backup file and a configuration file by default.

```bash
java -cp tla2tools.jar pcal.trans file.tla
```

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

### Basic Nondeterministic Resource Request

Source: https://learntla.com/core/nondeterminism.html

Use this macro to model a resource request that can either succeed or fail, abstracting away the specific reasons for failure.

```tla
macro request_resource(r) begin
  either
    reserved := reserved \union {r};
  or
    * Request failed
    skip;
  end either;
end macro;
```

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

### Defining ModelInvariant to Bound a Model

Source: https://learntla.com/topics/unbound-models.html

Use a ModelInvariant to restrict variables to a finite set, helping to detect unbound models. This example restricts 'x' to the range 0 to MaxX.

```TLA+
CONSTANT MaxX

TypeInvariant == x \in Int
ModelInvariant == x \in 0..MaxX
```

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

### Using a DEBUG Constant for Conditional Logic

Source: https://learntla.com/core/constants.html

A boolean constant like DEBUG can control the flow of a TLA+ specification. This example shows how to use it with an ASSUME clause and within a macro.

```tlaplus
CONSTANT DEBUG
ASSUME DEBUG \in BOOLEAN

macro print_if_debug(str) begin
  if DEBUG then
    print str;
  end if;


```

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

### Parameterize Actions for Reusability in TLA+

Source: https://learntla.com/topics/tips.html

Parameterize actions to allow values to be passed in, enabling reuse across multiple actions and facilitating logging.

```TLA+
Add(w) == s' = s \union {w}
Remove(w) == s' = s \ {w}

Next ==
  \E w \in Worker:
    /\ \/ Add(w)
       /\ Remove(w)
    /\ Log(w)
```

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

### Filter Clock Times

Source: https://learntla.com/core/operators.html

Apply filtering within set comprehension to select specific values from a defined type. This example selects clock times where minutes are 30 or greater and seconds are 0.

```tla
{t \in ClockType: t[2] >= 30 /\ t[3] = 0}
```

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

### Set Comprehension: Filter Operation

Source: https://learntla.com/core/operators.html

Use set comprehension with the format `{var \in set: condition}` for filtering operations. This example selects even numbers from the set `1..4`.

```tla
Evens == {x \in 1..4: x % 2 = 0 }
```

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

### Set Comprehension: Map Operation

Source: https://learntla.com/core/operators.html

Use set comprehension with the format `{expr: var \in set}` for mapping operations. This example calculates the square of each number in the set `1..4`.

```tla
Squares == {x*x: x \in 1..4}
```

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

### Procedure Call

Source: https://learntla.com/core/concurrency.html

Illustrates how to call a defined procedure. A procedure call must be followed by a label, a goto, or another return statement to manage control flow.

```PlusCal
process p = "process"
begin
  A:
    call my_procedure(a, b);
    * Must be followed by a label
  B:
```

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

### Constructing Sets Directly in TLA+

Source: https://learntla.com/topics/optimization.html

This TLA+ code constructs the 'to_process' set directly, which is more efficient than generating a large set and then filtering it. It defines a mapping from items to workers and then constructs the set of items each worker is responsible for.

```TLA+
to_process \
in {
 tp \
in [Workers -> SUBSET 1..MaxNum]:
   \\A x \
in 1..MaxNum:
     \\E w \
in Workers:
       /\ x \
in tp[w]
       /\ \\A w2 \
in Workers \ {w}:
         x \
otin tp[w2]
 }

```

```TLA+
to_process \
in LET
  i_to_worker == [1..MaxNum -> Workers] \* Map of items to workers
IN
  { [w \
in Workers |->  \* Each worker is mapped to
      {x \
in 1..MaxNum: \* the set of items which
      itw[x] = w}]:     \* itw maps to that worker
    itw \
in i_to_worker}

```

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

### TLC Output Showing Property Violation

Source: https://learntla.com/core/action-properties.html

This is an example of TLC output when the `CounterOnlyIncreases` action property is violated. It shows two states where the `counter` value transitions from 1 to 0, demonstrating the failure.

```text
\* some initial states
State 7:
  /\ counter = 1
  /\ lock = 1
  /\ pc = <<"IncCounter", "Done">>
  /\ tmp = <<1, 0>>

State 8:
  /\ counter = 0
  /\ lock = 1
  /\ pc = <<"ReleaseLock", "Done">>
  /\ tmp = <<1, 0>>


```

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

### TLA+ State Machine Implementation

Source: https://learntla.com/topics/state-machines.html

Implement a state machine directly in TLA+ using a `Trans` macro for transitions and defining `Init` and `Next` states. This method is often cleaner for more complex state machine logic compared to PlusCal.

```TLA+
---- MODULE state_machine ----
VARIABLE state

Trans(a, b) ==
  /\ state = a
  /\ state' = b

Init == state = "BothOff"

Next == 
  \/ Trans("BothOff", "WallOff")
  \/ Trans("BothOff", "LampOff")
  \/ Trans("WallOff", "On")
  \/ Trans("WallOff", "BothOff")
  \/ Trans("LampOff", "BothOff")
  \/ Trans("LampOff", "On")
  \/ Trans("On", "WallOff")
  \/ Trans("On", "LampOff")
  \/ Trans("error", "fetching")

Spec == Init /\ [][Next]_state
===

```

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

### TLA+ Sequence Indexing and Operations

Source: https://learntla.com/core/operators.html

Illustrates basic sequence operations like appending, concatenation, head, tail, length, and sub-sequence extraction. Note that TLA+ sequences are 1-indexed.

```tla
EXTENDS Integers, Sequences

ToSeconds(time) == time[1]*3600 + time[2]*60 + time[3]
Earlier(t1, t2) == ToSeconds(t1) < ToSeconds(t2)
```

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

### Define a parameterized module in TLA+

Source: https://learntla.com/core/modules.html

Define a module with constants that can be provided at import time using the WITH clause.

```tla
---- MODULE Point ----
LOCAL INSTANCE Integers
CONSTANTS X, Y
ASSUME X \in Int /\ Y \in Int

Repr == <<X, Y>>
Add(x, y) == <<X + x, Y + y>>
====
```

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

### Auxiliary Variable for Logging Actions

Source: https://learntla.com/topics/aux-vars.html

This example illustrates using an auxiliary variable `aux_log` to maintain a historical log of actions performed by workers. The `Append` function is used to add the worker `w` to the log.

```TLA
\E w \in Workers:
  /\ \/ Action1(w)
     \/ Action2(w)
     \/ Action3(w)
  /\ aux_log' = Append(aux_log, w)
```

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

### Import the same module multiple times with different names in TLA+

Source: https://learntla.com/core/modules.html

A module can be imported multiple times under different names, which is useful for modules with constants.

```tla
Foo == INSTANCE Sequences
Bar == INSTANCE Sequences
```

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

### Bounding Variable for Message Dropping

Source: https://learntla.com/topics/aux-vars.html

This example uses a bounding variable `aux_drops_left` within an `either await` construct to model message dropping. It limits the number of messages that can be dropped, preventing an unbound state space.

```TLA
either
  queue := Append(queue, msg);
or
  await aux_drops_left > 0;
  aux_drops_left := aux_drops_left - 1;
end either
```

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

### Basic Wire Transfer Logic

Source: https://learntla.com/intro/conceptual-overview.html

Illustrates a simple, single-threaded wire transfer function with a guard to prevent overdrafts. This code is illustrative and not production-ready for concurrent environments.

```python
def transfer(from, to, amount)
  if (from.balance >= amount) # guard
    from.balance -= amount;   # withdraw
    to.balance += amount;     # deposit

```

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

### TLA+ Fairness Specification

Source: https://learntla.com/core/tla.html

Demonstrates applying fairness conditions (SF and WF) to subactions in TLA+ for finer control over liveness properties. This is useful when specific actions within a larger step must eventually occur or be taken infinitely often.

```tla
VARIABLES status

Init == status = "start"

Trans(from, to) ==
  /\ status = from
  /\ status' = to

Succeed == Trans("start", "done")
Fail == Trans("start", "fail")
Retry == Trans("fail", "start")

Next == Succeed \/ Fail \/ Retry \/ UNCHANGED status

Fairness ==
  /\ SF_status(Succeed)
  /\ WF_status(Retry)

Spec == Init /\ [][Next]_status /\ Fairness

Liveness == <>(status = "done")

====
```

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

### TLA+ Module with PlusCal Algorithm

Source: https://learntla.com/core/temporal-logic.html

This TLA+ module defines a set of servers and includes a PlusCal algorithm for managing server online status. It serves as a basis for defining and checking temporal properties.

```tlaplus
---- MODULE orchestrator ----
EXTENDS Integers, TLC, FiniteSets

Servers == {"s1", "s2"}

(*--algorithm threads
variables 
  online = Servers;

process orchestrator = "orchestrator" 
begin
  Change:
    while TRUE do
      with s \in Servers do
       either
          await s \notin online;
          online := online \union {s};
        or
          await s \in online;
          await Cardinality(online) > 1;
          online := online \ {s};
        end either;
      end with;
    end while;
end process;

end algorithm; *)
====

```

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

### Module extension for Integers, Sequences, TLC

Source: https://learntla.com/core/invariants.html

This TLA+ module definition shows the extensions required for basic integer operations, sequence manipulation, and TLC model checking. It's a common starting point for many TLA+ specifications.

```TLA+
---- MODULE duplicates ----
EXTENDS Integers, Sequences, TLC

S == 1..10

```

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

### TLA+ Zip Function Implementation (Version 2)

Source: https://learntla.com/core/functions.html

Provides an alternative implementation 'Zip2' for a zip-like function in TLA+ using set intersection of domains to determine the common range for pairing elements.

```tla
Zip2(seq1, seq2) ==
  LET N == (DOMAIN seq1) \intersect (DOMAIN seq2)
  IN
    [i \in N |-> <<seq1[i], seq2[i]>>]

```

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

### TLA+ Zip Function Implementation (Version 1)

Source: https://learntla.com/core/functions.html

Implements a zip-like function 'Zip1' in TLA+ that pairs elements from two sequences up to the minimum length of the two sequences.

```tla
Zip1(seq1, seq2) ==
  LET Min(a, b) == IF a < b THEN a ELSE b
      N == Min(Len(seq1), Len(seq2))
  IN
    [i \in 1..N |-> <<seq1[i], seq2[i]>>]

```

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

### Using Auxiliary Variable for Temporal Property

Source: https://learntla.com/topics/aux-vars.html

This example demonstrates how to use an auxiliary variable `Q_was_true` to model a temporal property where a condition `P` implies `Q` or `Q_was_true`. The `Next` action updates `Q_was_true` based on the current value of `Q`.

```TLA
Prop == P => Q \/ Q_was_true

Next ==
  /\ * regular spec
  /\ IF Q' THEN Q_was_true' ELSE UNCHANGED Q_was_true
```

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

### Bug Example: Incorrect Initial Counter Value

Source: https://learntla.com/core/temporal-logic.html

Demonstrates a bug where an incorrect initial value for 'counter' (set to 1 instead of 0) still passes the '<> (counter = NumThreads)' liveness property because the condition is met in at least one state.

```tla
variables 
  counter = 1;
  lock = NULL;

define
```

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

### Run TLC Model Checker CLI

Source: https://learntla.com/topics/cli.html

Execute the TLC model checker on a TLA+ specification file using a configuration file. If no config file is specified, TLC defaults to looking for a file with the same name as the spec file.

```bash
java -jar tla2tools.jar -config configfile.cfg specfile.tla
```

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

### Create New TLA+ Module

Source: https://learntla.com/core/setup.html

This is the basic structure of a TLA+ module. The module name must match the filename, and it must be enclosed by at least four dashes at the top and four equal signs at the bottom.

```tla
---- MODULE wire ----

====

```

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

### Non-Atomic Counter Increment with Race Condition

Source: https://learntla.com/core/concurrency.html

This TLA+ code modifies the previous example to make the counter increment non-atomic by splitting it into two steps: reading the counter into a temporary variable and then updating the counter. This introduces a race condition, as demonstrated by the failing spec.

```TLA+
 end define;  
 
 process thread \in Threads
+variables tmp = 0;
 begin
+  GetCounter:
+    tmp := counter;
+
   IncCounter:
-    counter := counter + 1;
+    counter := tmp + 1;
 end process;
 end algorithm; *)
 ====
```

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

### Generate Partitions using Intermediate Functions (TLA+)

Source: https://learntla.com/examples/partitions.html

This operator generates partitions by mapping set elements to indices, then converting these mappings back to sets. It requires extending Integers, TLC, Sequences, and FiniteSets modules. The `PartitionsV1` helper function creates mappings, and `Partitions` converts these to the desired set-of-sets format, excluding empty sets.

```TLA+
EXTENDS Integers, TLC, Sequences, FiniteSets

PartitionsV1(set) ==
  LET F == [set -> 1..Cardinality(set)]
    G(f) == [i 	in 1..Cardinality(set) |-> {x 	in set: f[x] = i}]
  IN
    {G(f): f 	in F}

>> PartitionsV1({"a", "b"})
{<<{}, {"a", "b"}>>, <<{"a"}, {"b"}>>, <<{"b"}, {"a"}>>, <<{"a", "b"}, {}>>}

```

```TLA+
Range(f) == {f[x] : x 	in DOMAIN f}

Partitions(set) ==
    {Range(P) \ {{}}: P 	in PartitionsV1(set)}

```
Tokens:
Raw