Что на самом деле говорит зелёный прогон
Тест — это утверждение о существовании: «есть прогон, на котором система ведёт себя правильно». Набор тестов — много таких утверждений. Ни одно из них и все вместе они не говорят «поведения, которое ломает систему, не существует», — они говорят «мы его не встретили».
Для линейного кода разница почти не важна: пути наперечёт, и покрытие их закрывает. Она становится решающей там, где порядок шагов выбирает не программист: два запроса к одному счёту, повтор платежа после таймаута, очередь и обработчик, блокировка и её ожидание. Там пространство поведений комбинаторно, а тесты берут из него горсть.
Сделать редкое расписание воспроизводимым — отдельная задача, и она решается детерминированной симуляцией: сид вместо случайности, повтор побайтово. Но и это выборка. Двести расписаний из астрономического пространства — очень хороший фаззинг, а не теорема.
Где эта разница стоит денег
Все четыре — не про объём кода, а про число сочетаний. Это и есть область, где перебор состояний реально применим: протоколы, конечные автоматы, блокировки, согласование между сервисами. Обычный CRUD в эту область не входит, и тащить туда проверку моделей незачем.
Что такое проверка моделей
Вы описываете систему как машину состояний: начальные состояния, действия (у каждого условие срабатывания и результат) и утверждения, которые должны быть верны всегда. Дальше инструмент обходит все достижимые состояния и либо находит путь в состояние, где утверждение ложно, либо доказывает, что такого пути нет.
const spec = {
name: 'counter',
processes: 2,
init: [{ n: 0 }],
actions: [
{
name: 'p0: увеличить',
process: 0,
reads: ['n'],
writes: ['n'],
step: (s) => (s.n < 3 ? [{ n: s.n + 1 }] : []),
},
],
invariants: [{ name: 'n не растёт сверх меры', reads: ['n'], holds: (s) => s.n <= 3 }],
terminal: (s) => s.n === 3,
};Важна одна деталь формы: условие и результат живут в одной функции. Действие само возвращает следующие состояния, а пустой список означает «сейчас невозможно». Так guard и эффект не могут разъехаться — классический источник ошибок в ручных моделях.
Второе: reads, writes и множества симметричных процессов объявляются, а не угадываются. Ровно так же поступает TLA+. Плата за это честная: неверное объявление становится ошибкой в спецификации, а не тихой неполнотой инструмента, который молча выбросил нужные состояния.
Контрпример важнее вердикта
Ответ «нарушение возможно» бесполезен без пути к нему. Обход в ширину даёт кратчайший путь по построению, поэтому контрпример читается как протокол происшествия, а не как дамп.
✗ нарушен инвариант «в критической секции не больше одного процесса»
трасса
(начало) pc=00 flag=00
p0: проверил чужой флаг pc=10 flag=00
p1: проверил чужой флаг pc=11 flag=00
p0: поднял флаг и вошёл pc=31 flag=10
p1: поднял флаг и вошёл pc=33 flag=11Оба посмотрели, оба увидели опущенный флаг, оба вошли. Четыре шага — и понятно, почему флаг обязан подниматься до проверки. Такие вещи разбираются за минуту, если у вас есть трасса, и неделями, если у вас есть только «иногда двое оказываются внутри».
Почему перебор нельзя делать в лоб
Число состояний растёт как произведение: шесть процессов по пять фаз — это 15 625 сочетаний, и это игрушечный пример. Поэтому содержательная часть инструмента — не поиск, а то, что позволяет не искать.
Последняя строка важнее первых двух. Там, где процессы постоянно читают и пишут чужие переменные, сокращать нечего — и инструмент обязан честно не дать ничего. Эта строка вынесена в тест как утверждение: инструмент, который отрапортовал бы там выигрыш, врал бы.
Два способа не искать
Симметрия. Если процессы взаимозаменяемы, состояния, отличающиеся только их перестановкой, — это одно состояние. Шесть работников в пяти фазах дают 15 625 назначений, но всего 210 мультимножеств: важно, сколько кого, а не кто именно где.
Коммутирующие действия. Если два действия не трогают ничего общего, порядок между ними не наблюдаем: изучив один порядок, вы ничего не узнаете из второго. Формально это ample-множества, и у них четыре условия, каждое из которых заслужено — выбросьте одно, и проверка начнёт уверенно пропускать нарушения.
Как проверить сам сокращатель
Здесь начинается самое неприятное место всей затеи. Сокращение, которое выбрасывает лишнее, выдаёт ровно тот же ответ, что и правильное: «нарушений не найдено». Изнутри сокращённого поиска отличить одно от другого невозможно.
Единственный работающий ответ — не доверять сокращению на слово. Полный перебор остаётся рядом: медленный, исчерпывающий и неспособный ошибиться. Каждая спецификация гоняется через оба поиска, и сокращённый вердикт обязан совпасть с полным. Сокращению верят не потому, что его автор уверен, а потому, что оно согласуется с тем, что ошибиться не может.
У этой гарантии есть граница, и её честно назвать: сверка возможна там, где полный перебор ещё запускается, — то есть на маленьких моделях. Ровно там, где сокращение не нужно. Это врождённое свойство подхода, и оно не отменяет проверку, но задаёт её потолок.
Тот же приём в других местах: музей багов, где каждый экспонат выключает одно правило алгоритма и обязан быть пойманным, — и лестница уровней изоляции, где каждая ступень обязана произвести то, что запрещает следующая.
Живость: система не падает, а просто не доходит
Безопасность — это вопрос «достижимо ли плохое состояние», и обход в ширину на него отвечает. Живость — вопрос «случится ли когда-нибудь хорошее», и нарушает её бесконечный прогон, в котором хорошее не случается. В конечном пространстве состояний такой прогон — это лассо: путь до цикла и цикл навсегда.
Беда в том, что большинство таких циклов абсурдны: они требуют, чтобы процесс, который мог бы выполниться, просто никогда не запускался. Их отсекает слабая справедливость: непрерывно готовый процесс обязан когда-нибудь сделать шаг. Без этого условия любая конкурентная программа «проваливает» живость, и проверка бесполезна.
✗ спинлок — возможен бесконечный прогон, где процесс 0 не входит в критическую секцию
цикл справедлив: процесс 1 продолжает двигаться, процесс 0 заблокирован
дальше навсегда
p1: захватил pc=03 lock=1
p1: освободил pc=00 lock=-1Спинлок безопасен — двое внутри не окажутся — и при этом голодает. Алгоритм Петерсона ту же проверку проходит, и переменная turn существует ровно для этого. Разницу между «безопасно» и «безопасно и доходит» стоит уметь называть: в очередях, локах и распределённых блокировках она и есть источник зависаний, которые не видны в мониторинге как ошибки.
Чего этот метод не умеет
- Проверяется модель, а не код. Это главное ограничение и главный риск: доказанная модель и расходящаяся с ней реализация — обычное дело. Модель ловит ошибки замысла, тесты — ошибки исполнения; одно не заменяет другое.
- Сокращения верны относительно того, что вы объявили. Действие, которое пишет незаявленную переменную, может стоить пропущенных состояний. Это контракт, а не анализ.
- Только инварианты и одна форма живости. Утверждения вида «всегда верно» и «когда-нибудь случится» под слабой справедливостью. Ни вложенных временных операторов, ни сильной справедливости, ни полного LTL.
- Всё в памяти. Тысячи и десятки тысяч состояний, а не миллиарды: нет ни хранилища на диске, ни символьного представления.
- Для серьёзной работы есть TLC и SPIN. За ними десятилетия, дисковые хранилища состояний, распределённая проверка и языки, придуманные под задачу.
Когда это оправдано на коммерческом проекте
- 01
Считаем участников общего состояния
Если над одними данными работают два и более независимых процесса — платёж и вебхук, воркер и планировщик, пользователь и фоновая сверка, — сочетаний больше, чем вы напишете тестов.
- 02
Формулируем инвариант одной фразой
«Из состояния оплачен заказ не возвращается в ожидает оплаты», «два перевода не спишут больше остатка». Если инвариант не формулируется, проверять пока нечего — сначала договоритесь, что должно быть верно.
- 03
Пишем модель на 30–60 строк, а не всю систему
Моделируется протокол, а не приложение: состояния заказа, шаги провайдера, отказы и повторы. Всё остальное в модель не входит — и это не упрощение, а условие того, что перебор вообще закончится.
- 04
Полученный контрпример превращаем в тест
Трасса — готовый сценарий регрессии. Модель осталась в репозитории, тест сторожит реализацию, и обе стороны делают то, что умеют.
В деньгах это оправдано там, где цена ошибки в данных выше цены простоя: финансовые системы, учёт остатков, интеграции с внешними провайдерами. Смежные разборы — про идемпотентность платежей и про то, что происходит с данными при отказе мастера.
Частые вопросы
Это то же самое, что TLA+?
Та же идея и те же алгоритмы: описать систему как машину состояний и обойти достижимые. TLA+ с TLC — промышленный инструмент со своим языком, хранением состояний на диске и распределённой проверкой; для реальной верификации протокола берите его. Разница в пороге входа: модель на TypeScript пишется в том же репозитории, что и код, и её читает вся команда, а не один энтузиаст.
Нам придётся описывать систему дважды — моделью и кодом?
Моделью описывается не система, а протокол: состояния, переходы, отказы. Это десятки строк, а не тысячи. Дублирования нет ровно потому, что модель намеренно беднее реализации — в ней нет базы, сети и интерфейса, зато есть все сочетания шагов.
Что делать, если состояний слишком много?
Уменьшать модель, а не мощность машины: три процесса вместо десяти, две валюты вместо тридцати. Ошибки протоколов почти всегда проявляются на маленьких экземплярах — это известное практическое наблюдение, на нём построена вся работа с моделями. Если и это не помогает, задача уходит к TLC и SPIN.
Зачем вы написали свой model checker, если есть готовые?
Чтобы понимать, чему я доверяю. Сокращения перебора — это код, который может тихо выбрасывать нужные состояния и выдавать тот же зелёный ответ; написав их, вы понимаете, чем именно рискуете, пользуясь чужим инструментом. Код открыт: pnueli, MIT, ссылка в источниках.
Источники
Утверждения из статьи можно проверить: ниже первоисточники, а не пересказ.
- 01Clarke, Grumberg, Peled. Model Checking — Частично-упорядоченное сокращение и условия ample-множеств
- 02TLA+ и TLC — Промышленный инструмент для той же задачи
- 03SPIN — Проверка моделей протоколов, десятилетия практики
- 04Amir Pnueli — Turing Award — Временная логика в верификации программ: «всегда» и «когда-нибудь»
- 05pnueli — Инструмент из этой статьи: MIT, полный перебор рядом с сокращениями
Этот материал подписан именем, в отличие от остальных: за ним не стоит клиент. Код, о котором идёт речь, открыт целиком и лежит под тем же именем — его можно прочитать, запустить и проверить утверждения статьи, не поверив ни одному из них на слово.