Individual-task/validate/PartitionsStorageSets_explained.md

# Разбор `PartitionsStorageSets.tla`

Файл `PartitionsStorageSets.tla` описывает упрощенную TLA+ модель для проверки логики партиций, которые хранят множество ключей в виде полуоткрытых интервалов `[lo; hi)`.

Модель намеренно не проверяет AVL и QSBR. Мы считаем, что:

- AVL корректно находит нужную партицию;
- QSBR корректно защищает lifetime нод;
- переменная `tree` абстрактно означает "те partition id, которые сейчас достижимы из дерева".

Главная цель модели: проверить, что операции split/shrink не создают дыр, пересечений и потерянных ключей.

## Заголовок модуля

```tla
---- MODULE PartitionsStorageSets ----
EXTENDS Naturals, FiniteSets
```

`MODULE` объявляет имя TLA+ модуля.

`EXTENDS Naturals, FiniteSets` подключает стандартные модули:

- `Naturals` - натуральные числа, диапазоны `0..N`, арифметика;
- `FiniteSets` - операции над конечными множествами, например `Cardinality`.

## Комментарий про абстракцию

```tla
(*
This model validates only the partition/set logic.
AVL tree lookup and QSBR are abstracted away as the variable `tree`,
which contains ids of currently reachable live partitions.
*)
```

Это важное ограничение модели.

Мы не моделируем:

- форму AVL-дерева;
- балансировку;
- указатели;
- QSBR epochs;
- освобождение памяти;
- lock-free детали дерева.

Вместо этого считаем, что `tree` - это множество id живых партиций, которые доступны через дерево.

## Константы

```tla
CONSTANTS
  PartitionIds,
  Threads,
  NoThread,
  KeyCount,
  MinPartitionSize,
  MaxPartitionSize,
  MaxLoad
```

Константы задаются в `.cfg` файле.

### `PartitionIds`

```tla
PartitionIds
```

Множество всех id партиций, которые модель может использовать.

Пример из `PartitionsStorageSetsSmoke.cfg`:

```tla
PartitionIds = {p0, p1, p2}
```

Важно: `PartitionIds` - это не только живые партиции. Это пул всех возможных id. Часть из них может быть `DEAD`.

### `Threads`

```tla
Threads
```

Множество потоков, которые могут брать locks и выполнять операции.

Пример:

```tla
Threads = {t0}
```

Для более интересных конкурентных сценариев можно поставить:

```tla
Threads = {t0, t1}
```

### `NoThread`

```tla
NoThread
```

Специальное значение, означающее "mutex никем не захвачен".

Пример:

```tla
NoThread = NoThread
```

Это выглядит странно, но в TLA+ справа `NoThread` в `.cfg` задает символическое значение.

### `KeyCount`

```tla
KeyCount
```

Количество ключей в модели.

Если `KeyCount = 3`, то ключи:

```tla
0, 1, 2
```

В модели полный диапазон ключей задается как `[0; KeyCount)`.

### `MinPartitionSize`

```tla
MinPartitionSize
```

Нижний порог размера партиции.

Если `load < MinPartitionSize` и партиций больше одной, партиция считается `NEED_SHRINK`.

### `MaxPartitionSize`

```tla
MaxPartitionSize
```

Верхний нормальный порог размера партиции.

Если `load > MaxPartitionSize`, партиция считается `NEED_SPLIT`.

### `MaxLoad`

```tla
MaxLoad
```

Технический максимум для поля `load`, чтобы пространство состояний было конечным.

TLC должен перебрать конечное число состояний. Поэтому нельзя разрешить `load` быть любым натуральным числом.

## Предположения о константах

```tla
ASSUME NoThread \notin Threads
ASSUME KeyCount > 0
ASSUME MinPartitionSize > 0
ASSUME MaxPartitionSize >= MinPartitionSize
ASSUME MaxLoad > MaxPartitionSize
ASSUME Cardinality(PartitionIds) >= 3
```

`ASSUME` задает требования к конфигурации.

### `NoThread \notin Threads`

```tla
ASSUME NoThread \notin Threads
```

Специальное значение `NoThread` не должно совпадать с реальным потоком.

Иначе было бы невозможно отличить:

- lock свободен;
- lock захвачен потоком с id `NoThread`.

### `KeyCount > 0`

```tla
ASSUME KeyCount > 0
```

В модели должен быть хотя бы один ключ.

### `MinPartitionSize > 0`

```tla
ASSUME MinPartitionSize > 0
```

Минимальный размер должен быть положительным.

### `MaxPartitionSize >= MinPartitionSize`

```tla
ASSUME MaxPartitionSize >= MinPartitionSize
```

Верхний порог не должен быть меньше нижнего.

### `MaxLoad > MaxPartitionSize`

```tla
ASSUME MaxLoad > MaxPartitionSize
```

Нужно, чтобы в модели вообще могли появляться состояния `NEED_SPLIT`.

Если `MaxLoad <= MaxPartitionSize`, то `load > MaxPartitionSize` был бы невозможен.

### `Cardinality(PartitionIds) >= 3`

```tla
ASSUME Cardinality(PartitionIds) >= 3
```

Нужно минимум 3 id:

- один начальный живой partition;
- два новых partition для split.

## Переменные состояния

```tla
VARIABLES
  partitions,
  tree,
  locks
```

Это состояние модели.

В TLA+ каждое состояние - это конкретные значения всех переменных из `VARIABLES`.

### `partitions`

`partitions` хранит данные всех partition id.

Тип:

```tla
partitions \in [PartitionIds -> PartitionRecord]
```

То есть это функция:

```text
partition id -> record партиции
```

### `tree`

`tree` - множество partition id, которые сейчас доступны через дерево.

Важно:

```text
p \in tree
```

означает, что партиция живая и достижима.

```text
p \notin tree
```

означает, что партиция недоступна из дерева. В этой модели такие партиции должны быть `dead = TRUE`.

### `locks`

`locks` хранит владельца mutex для каждой партиции.

Тип:

```tla
locks \in [PartitionIds -> (Threads \cup {NoThread})]
```

То есть:

- `locks[p] = NoThread` - lock свободен;
- `locks[p] = t` - lock захвачен потоком `t`.

## Список всех переменных

```tla
vars == <<partitions, tree, locks>>
```

`vars` нужен для temporal specification:

```tla
Spec == Init /\ [][Next]_vars
```

Запись `[Next]_vars` означает:

```text
либо происходит действие Next,
либо состояние не меняется по переменным vars
```

Это стандартный способ записывать спецификацию в TLA+.

## Множество ключей

```tla
Keys == 0..(KeyCount - 1)
```

Если `KeyCount = 8`, то:

```tla
Keys = 0..7
```

То есть полный диапазон ключей:

```text
[0; KeyCount)
```

## Тип записи партиции

```tla
PartitionRecord ==
  [ lo   : 0..KeyCount,
    hi   : 0..KeyCount,
    dead : BOOLEAN,
    load : 0..MaxLoad ]
```

Каждая партиция - это record с полями:

- `lo` - левая граница интервала;
- `hi` - правая граница интервала;
- `dead` - является ли партиция мертвой;
- `load` - абстрактный размер множества внутри партиции.

Интервал полуоткрытый:

```text
[lo; hi)
```

То есть ключ `k` принадлежит партиции, если:

```text
lo <= k < hi
```

Почему `lo` и `hi` имеют тип `0..KeyCount`, а не `Keys`:

- ключи идут от `0` до `KeyCount - 1`;
- правая граница последнего интервала равна `KeyCount`;
- поэтому `hi = KeyCount` должно быть допустимо.

## Проверка принадлежности ключа партиции

```tla
KeyInPartition(k, p) ==
  /\ partitions[p].lo <= k
  /\ k < partitions[p].hi
```

`KeyInPartition(k, p)` истинно, если ключ `k` лежит внутри интервала партиции `p`.

Пример:

```text
partition = [lo |-> 2, hi |-> 5]
```

Тогда партиция содержит ключи:

```text
2, 3, 4
```

И не содержит `5`.

## Вычисляемый статус партиции

```tla
Status(p) ==
  IF partitions[p].dead THEN "DEAD"
  ELSE IF partitions[p].load > MaxPartitionSize THEN "NEED_SPLIT"
  ELSE IF partitions[p].load < MinPartitionSize /\ Cardinality(tree) > 1 THEN "NEED_SHRINK"
  ELSE "ALIVE"
```

Статус не хранится отдельным полем. Он вычисляется из текущего состояния.

Это полезно, потому что нельзя получить противоречивое состояние вида:

```text
status = "ALIVE", но load > MaxPartitionSize
```

### `DEAD`

```tla
IF partitions[p].dead THEN "DEAD"
```

Если `dead = TRUE`, партиция считается мертвой независимо от `load`.

### `NEED_SPLIT`

```tla
ELSE IF partitions[p].load > MaxPartitionSize THEN "NEED_SPLIT"
```

Если партиция живая и ее нагрузка больше верхнего порога, ее надо split.

### `NEED_SHRINK`

```tla
ELSE IF partitions[p].load < MinPartitionSize /\ Cardinality(tree) > 1 THEN "NEED_SHRINK"
```

Если партиция живая, маленькая, и в дереве больше одной партиции, ее можно shrink.

Условие `Cardinality(tree) > 1` нужно потому, что последнюю оставшуюся партицию нельзя удалить.

### `ALIVE`

```tla
ELSE "ALIVE"
```

Все остальные живые партиции считаются нормальными.

## Начальное состояние `Init`

```tla
Init ==
  \E p \in PartitionIds:
    /\ tree = {p}
    /\ partitions =
      [ q \in PartitionIds |->
          IF q = p THEN
            [ lo |-> 0,
              hi |-> KeyCount,
              dead |-> FALSE,
              load |-> MinPartitionSize ]
          ELSE
            [ lo |-> 0,
              hi |-> 0,
              dead |-> TRUE,
              load |-> 0 ] ]
    /\ locks = [q \in PartitionIds |-> NoThread]
```

`Init` описывает все допустимые начальные состояния.

Здесь используется существование:

```tla
\E p \in PartitionIds:
```

Это значит: TLC может выбрать любой `p` из `PartitionIds` как начальную живую партицию.

### Начальное дерево

```tla
tree = {p}
```

В начале есть ровно одна живая партиция.

Она покрывает весь диапазон ключей.

### Начальное значение `partitions`

```tla
partitions =
  [ q \in PartitionIds |->
      IF q = p THEN
        ...
      ELSE
        ... ]
```

Это функция по всем partition id.

Для выбранного `p` создается живая партиция:

```tla
[ lo |-> 0,
  hi |-> KeyCount,
  dead |-> FALSE,
  load |-> MinPartitionSize ]
```

Она покрывает весь диапазон:

```text
[0; KeyCount)
```

Для всех остальных `q` создаются мертвые пустые партиции:

```tla
[ lo |-> 0,
  hi |-> 0,
  dead |-> TRUE,
  load |-> 0 ]
```

### Начальные locks

```tla
locks = [q \in PartitionIds |-> NoThread]
```

Все mutex свободны.

## TypeInvariant

```tla
TypeInvariant ==
  /\ partitions \in [PartitionIds -> PartitionRecord]
  /\ tree \subseteq PartitionIds
  /\ locks \in [PartitionIds -> (Threads \cup {NoThread})]
  /\ \A p \in tree:
      /\ partitions[p].dead = FALSE
      /\ partitions[p].lo < partitions[p].hi
      /\ partitions[p].hi <= KeyCount
  /\ \A p \in PartitionIds \ tree:
      partitions[p].dead = TRUE
```

`TypeInvariant` проверяет базовую корректность формы состояния.

Это не главный алгоритмический инвариант, но он почти всегда нужен в TLA+ моделях.

### Тип `partitions`

```tla
partitions \in [PartitionIds -> PartitionRecord]
```

Для каждого partition id есть корректная запись с полями:

- `lo`;
- `hi`;
- `dead`;
- `load`.

### Тип `tree`

```tla
tree \subseteq PartitionIds
```

Дерево не может ссылаться на неизвестный partition id.

### Тип `locks`

```tla
locks \in [PartitionIds -> (Threads \cup {NoThread})]
```

Для каждой партиции lock либо свободен, либо принадлежит одному из потоков.

### Все партиции в `tree` живые и непустые

```tla
\A p \in tree:
  /\ partitions[p].dead = FALSE
  /\ partitions[p].lo < partitions[p].hi
  /\ partitions[p].hi <= KeyCount
```

Если партиция достижима из дерева:

- она не `dead`;
- ее интервал непустой;
- правая граница не выходит за общий диапазон.

### Все партиции вне `tree` мертвые

```tla
\A p \in PartitionIds \ tree:
  partitions[p].dead = TRUE
```

Если partition id не достижим из дерева, он должен быть `dead`.

Это сильное упрощение модели. В реальной системе из-за QSBR может существовать старая нода, которую еще кто-то читает. Но для текущей модели мы проверяем только логическую структуру живых интервалов.

## Инвариант уникального владельца ключа

```tla
UniqueOwnerForEveryKey ==
  \A k \in Keys:
    \E p \in tree:
      /\ KeyInPartition(k, p)
      /\ \A q \in tree:
          KeyInPartition(k, q) => q = p
```

Это главный инвариант модели.

Он говорит:

```text
для каждого ключа существует ровно одна живая партиция, которая содержит этот ключ
```

Разберем по частям.

```tla
\A k \in Keys:
```

Для каждого ключа.

```tla
\E p \in tree:
```

Существует живая партиция `p`.

```tla
KeyInPartition(k, p)
```

Эта партиция содержит ключ.

```tla
\A q \in tree:
  KeyInPartition(k, q) => q = p
```

Любая другая живая партиция `q`, которая содержит этот ключ, на самом деле является той же самой партицией `p`.

Иначе говоря:

- нет дыр;
- нет пересечений;
- каждый ключ покрыт ровно одним интервалом.

Если этот инвариант падает, значит split или shrink испортил покрытие диапазона.

## Инвариант `DeadPartitionsAreOutsideTree`

```tla
DeadPartitionsAreOutsideTree ==
  \A p \in PartitionIds:
    partitions[p].dead => p \notin tree
```

Если партиция мертвая, она не должна быть достижима из дерева.

Этот инвариант частично пересекается с `TypeInvariant`, но он более явно выражает важное свойство структуры данных.

## Действие `Lock`

```tla
Lock(t, p) ==
  /\ p \in tree
  /\ locks[p] = NoThread
  /\ locks' = [locks EXCEPT ![p] = t]
  /\ UNCHANGED <<partitions, tree>>
```

`Lock(t, p)` моделирует взятие mutex партиции `p` потоком `t`.

Предусловия:

```tla
p \in tree
```

Можно брать lock только у живой достижимой партиции.

```tla
locks[p] = NoThread
```

Lock должен быть свободен.

Изменение:

```tla
locks' = [locks EXCEPT ![p] = t]
```

В следующем состоянии владелец lock для `p` - поток `t`.

Остальное не меняется:

```tla
UNCHANGED <<partitions, tree>>
```

## Действие `Unlock`

```tla
Unlock(t, p) ==
  /\ locks[p] = t
  /\ locks' = [locks EXCEPT ![p] = NoThread]
  /\ UNCHANGED <<partitions, tree>>
```

`Unlock(t, p)` моделирует освобождение mutex.

Предусловие:

```tla
locks[p] = t
```

Только владелец lock может его освободить.

Изменение:

```tla
locks' = [locks EXCEPT ![p] = NoThread]
```

В следующем состоянии lock свободен.

## Действие `GrowPartition`

```tla
\* Abstract user mutation of the set stored inside a locked partition.
GrowPartition(t, p) ==
  /\ p \in tree
  /\ locks[p] = t
  /\ partitions[p].load < MaxLoad
  /\ partitions' = [partitions EXCEPT ![p].load = @ + 1]
  /\ UNCHANGED <<tree, locks>>
```

Это абстрактное действие, которое увеличивает размер множества внутри партиции.

Оно нужно, чтобы в модели могла появиться партиция со статусом `NEED_SPLIT`.

Предусловия:

```tla
p \in tree
```

Партиция живая.

```tla
locks[p] = t
```

Поток держит mutex этой партиции.

```tla
partitions[p].load < MaxLoad
```

Нельзя выйти за техническую верхнюю границу `MaxLoad`.

Изменение:

```tla
partitions' = [partitions EXCEPT ![p].load = @ + 1]
```

`@` означает старое значение изменяемого поля.

То есть:

```text
new load = old load + 1
```

## Действие `ShrinkPartitionLoad`

```tla
ShrinkPartitionLoad(t, p) ==
  /\ p \in tree
  /\ locks[p] = t
  /\ partitions[p].load > 0
  /\ partitions' = [partitions EXCEPT ![p].load = @ - 1]
  /\ UNCHANGED <<tree, locks>>
```

Это абстрактное действие, которое уменьшает размер множества внутри партиции.

Оно нужно, чтобы в модели могла появиться партиция со статусом `NEED_SHRINK`.

Предусловия:

- партиция живая;
- поток держит ее lock;
- `load > 0`.

Изменение:

```text
new load = old load - 1
```

`tree` и `locks` не меняются.

## Действие `SplitPartition`

```tla
SplitPartition(t, p) ==
  /\ p \in tree
  /\ locks[p] = t
  /\ Status(p) = "NEED_SPLIT"
  /\ partitions[p].lo + 1 < partitions[p].hi
  /\ \E left \in PartitionIds \ tree:
      \E right \in (PartitionIds \ tree) \ {left}:
        \E splitKey \in (partitions[p].lo + 1)..(partitions[p].hi - 1):
          \E leftLoad \in 0..partitions[p].load:
            LET rightLoad == partitions[p].load - leftLoad IN
            /\ rightLoad \in 0..MaxLoad
            /\ leftLoad \in 0..MaxLoad
            /\ partitions' =
              [ partitions EXCEPT
                  ![p].dead = TRUE,
                  ![left] =
                    [ lo |-> partitions[p].lo,
                      hi |-> splitKey,
                      dead |-> FALSE,
                      load |-> leftLoad ],
                  ![right] =
                    [ lo |-> splitKey,
                      hi |-> partitions[p].hi,
                      dead |-> FALSE,
                      load |-> rightLoad ] ]
            /\ tree' = (tree \ {p}) \cup {left, right}
            /\ locks' =
              [ locks EXCEPT
                  ![p] = NoThread,
                  ![left] = NoThread,
                  ![right] = NoThread ]
```

`SplitPartition` моделирует разбиение одной большой партиции на две.

### Предусловия split

```tla
p \in tree
```

Разбиваем только живую партицию.

```tla
locks[p] = t
```

Поток держит lock этой партиции.

```tla
Status(p) = "NEED_SPLIT"
```

Разбиение разрешено только если партиция слишком большая.

```tla
partitions[p].lo + 1 < partitions[p].hi
```

Интервал должен быть достаточно большим, чтобы его можно было разделить на два непустых интервала.

Например, `[0; 2)` можно разделить на `[0; 1)` и `[1; 2)`.

А `[0; 1)` разделить нельзя.

### Выбор новых partition id

```tla
\E left \in PartitionIds \ tree:
  \E right \in (PartitionIds \ tree) \ {left}:
```

TLC недетерминированно выбирает два свободных id:

- `left`;
- `right`.

Они должны быть вне текущего `tree`.

### Выбор точки split

```tla
\E splitKey \in (partitions[p].lo + 1)..(partitions[p].hi - 1):
```

`splitKey` выбирается строго внутри интервала.

Старый интервал:

```text
[lo; hi)
```

Новые интервалы:

```text
[lo; splitKey)
[splitKey; hi)
```

### Распределение load

```tla
\E leftLoad \in 0..partitions[p].load:
  LET rightLoad == partitions[p].load - leftLoad IN
```

Модель не знает, как реальные элементы распределяются между половинами.

Поэтому она разрешает любое распределение:

```text
leftLoad + rightLoad = oldLoad
```

Это полезная абстракция: TLC проверяет больше вариантов, включая неудобные.

### Изменение `partitions`

```tla
partitions' =
  [ partitions EXCEPT
      ![p].dead = TRUE,
      ![left] =
        [ lo |-> partitions[p].lo,
          hi |-> splitKey,
          dead |-> FALSE,
          load |-> leftLoad ],
      ![right] =
        [ lo |-> splitKey,
          hi |-> partitions[p].hi,
          dead |-> FALSE,
          load |-> rightLoad ] ]
```

В следующем состоянии:

- старая партиция `p` становится `dead`;
- `left` становится живой партицией `[old.lo; splitKey)`;
- `right` становится живой партицией `[splitKey; old.hi)`.

### Изменение `tree`

```tla
tree' = (tree \ {p}) \cup {left, right}
```

В дереве:

- удаляем старую партицию `p`;
- добавляем две новые.

### Изменение `locks`

```tla
locks' =
  [ locks EXCEPT
      ![p] = NoThread,
      ![left] = NoThread,
      ![right] = NoThread ]
```

После split locks освобождены.

Это упрощение модели. Если в C++ реализации `get` возвращает пользователю уже locked partition, возможно позднее стоит уточнить это поведение.

## Действие `ShrinkToPrev`

```tla
ShrinkToPrev(t, p) ==
  /\ p \in tree
  /\ locks[p] = t
  /\ Status(p) = "NEED_SHRINK"
  /\ \E prev \in tree \ {p}:
      /\ locks[prev] = t
      /\ partitions[prev].hi = partitions[p].lo
      /\ partitions[prev].load + partitions[p].load <= MaxLoad
      /\ partitions' =
        [ partitions EXCEPT
            ![prev].hi = partitions[p].hi,
            ![prev].load = partitions[prev].load + partitions[p].load,
            ![p].dead = TRUE ]
      /\ tree' = tree \ {p}
      /\ locks' = [locks EXCEPT ![p] = NoThread, ![prev] = NoThread]
```

`ShrinkToPrev` моделирует слияние маленькой партиции `p` с предыдущей соседней партицией.

### Предусловия

```tla
p \in tree
```

Удалять можно только живую партицию.

```tla
locks[p] = t
```

Поток держит lock удаляемой партиции.

```tla
Status(p) = "NEED_SHRINK"
```

Партиция маленькая и есть больше одной живой партиции.

### Выбор предыдущей партиции

```tla
\E prev \in tree \ {p}:
```

TLC выбирает другую живую партицию `prev`.

```tla
locks[prev] = t
```

Тот же поток должен держать lock соседа.

```tla
partitions[prev].hi = partitions[p].lo
```

`prev` должна быть настоящим левым соседом.

Например:

```text
prev = [0; 3)
p    = [3; 5)
```

### Ограничение load

```tla
partitions[prev].load + partitions[p].load <= MaxLoad
```

Нужно, чтобы после слияния `load` не вышел за технический максимум модели.

### Изменение `partitions`

```tla
partitions' =
  [ partitions EXCEPT
      ![prev].hi = partitions[p].hi,
      ![prev].load = partitions[prev].load + partitions[p].load,
      ![p].dead = TRUE ]
```

Сосед `prev` расширяется вправо:

```text
prev: [prev.lo; prev.hi)
p:    [p.lo; p.hi)
```

становится:

```text
prev: [prev.lo; p.hi)
```

Партиция `p` становится мертвой.

### Изменение `tree`

```tla
tree' = tree \ {p}
```

Удаляем `p` из дерева.

### Изменение `locks`

```tla
locks' = [locks EXCEPT ![p] = NoThread, ![prev] = NoThread]
```

После shrink locks освобождаются.

## Действие `ShrinkToNext`

```tla
ShrinkToNext(t, p) ==
  /\ p \in tree
  /\ locks[p] = t
  /\ Status(p) = "NEED_SHRINK"
  /\ \E next \in tree \ {p}:
      /\ locks[next] = t
      /\ partitions[p].hi = partitions[next].lo
      /\ partitions[next].load + partitions[p].load <= MaxLoad
      /\ partitions' =
        [ partitions EXCEPT
            ![next].lo = partitions[p].lo,
            ![next].load = partitions[next].load + partitions[p].load,
            ![p].dead = TRUE ]
      /\ tree' = tree \ {p}
      /\ locks' = [locks EXCEPT ![p] = NoThread, ![next] = NoThread]
```

`ShrinkToNext` моделирует слияние маленькой партиции `p` со следующей соседней партицией.

Это симметрично `ShrinkToPrev`.

### Выбор следующей партиции

```tla
\E next \in tree \ {p}:
```

TLC выбирает другую живую партицию `next`.

```tla
partitions[p].hi = partitions[next].lo
```

`next` должна быть настоящим правым соседом.

Например:

```text
p    = [3; 5)
next = [5; 8)
```

### Изменение интервала

```tla
![next].lo = partitions[p].lo
```

Правая партиция расширяется влево:

```text
p:    [p.lo; p.hi)
next: [next.lo; next.hi)
```

становится:

```text
next: [p.lo; next.hi)
```

Партиция `p` становится мертвой и удаляется из `tree`.

## Действие `Next`

```tla
Next ==
  \/ \E t \in Threads, p \in PartitionIds: Lock(t, p)
  \/ \E t \in Threads, p \in PartitionIds: Unlock(t, p)
  \/ \E t \in Threads, p \in PartitionIds: GrowPartition(t, p)
  \/ \E t \in Threads, p \in PartitionIds: ShrinkPartitionLoad(t, p)
  \/ \E t \in Threads, p \in PartitionIds: SplitPartition(t, p)
  \/ \E t \in Threads, p \in PartitionIds: ShrinkToPrev(t, p)
  \/ \E t \in Threads, p \in PartitionIds: ShrinkToNext(t, p)
```

`Next` описывает один шаг системы.

На каждом шаге TLC выбирает одно из действий:

- взять lock;
- отпустить lock;
- увеличить `load`;
- уменьшить `load`;
- split;
- shrink в предыдущую партицию;
- shrink в следующую партицию.

Запись:

```tla
\/
```

означает логическое "или".

Запись:

```tla
\E t \in Threads, p \in PartitionIds:
```

означает, что TLC перебирает все варианты потока `t` и партиции `p`.

Если предусловия действия не выполняются, этот вариант просто невозможен.

## Спецификация `Spec`

```tla
Spec == Init /\ [][Next]_vars
```

`Spec` - это полное описание поведения системы.

Оно говорит:

1. Первое состояние должно удовлетворять `Init`.
2. Каждый следующий шаг должен удовлетворять `[Next]_vars`.

`[]` означает "всегда".

`[Next]_vars` означает:

- либо произошел один из переходов `Next`;
- либо состояние осталось тем же по переменным `vars`.

## Конец модуля

```tla
====
```

Так заканчивается TLA+ модуль.

## Как читать counterexample

Если TLC найдет ошибку, он покажет последовательность состояний:

```text
State 1
State 2
State 3
...
```

Для этой модели нужно смотреть прежде всего:

- `tree`;
- `partitions`;
- `locks`;
- какое действие было между состояниями.

Если нарушился `UniqueOwnerForEveryKey`, значит произошло одно из двух:

- появился ключ, который не принадлежит ни одной живой партиции;
- появился ключ, который принадлежит двум живым партициям.

Практически это означает ошибку в логике split/shrink или слишком слабое предусловие действия.

## Как запускать

Быстрый smoke-test:

```bash
java -jar /home/hhhh/bin/toolbox/tla2tools.jar \
  -config validate/PartitionsStorageSetsSmoke.cfg \
  validate/PartitionsStorageSets.tla
```

Более тяжелая проверка:

```bash
java -jar /home/hhhh/bin/toolbox/tla2tools.jar \
  -config validate/PartitionsStorageSets.cfg \
  validate/PartitionsStorageSets.tla
```

Smoke-конфиг нужен для быстрой проверки синтаксиса и базовых инвариантов.

Полный конфиг перебирает гораздо больше состояний и может работать долго.

## Что модель пока не проверяет

Текущая модель не проверяет:

- корректность AVL rotations;
- корректность lock-free публикации новых узлов;
- ABA-проблемы;
- QSBR epochs;
- memory reclamation;
- C++ memory ordering;
- порядок взятия нескольких locks;
- deadlock-freedom;
- liveness.

Это осознанно. Сейчас модель проверяет только базовую безопасность интервалов:

```text
каждый ключ всегда принадлежит ровно одной живой партиции
```

Следующий логичный шаг - уточнить `shrink`, добавив состояние операции по шагам:

1. отпустили lock своей партиции;
2. нашли prev;
3. взяли prev lock;
4. снова взяли свой lock;
5. нашли next;
6. взяли next lock;
7. проверили DEAD;
8. удалили текущую партицию.

Тогда модель начнет проверять больше конкурентных interleavings.