Распределённый протокол нельзя покрыть юнит-тестами, но можно проверить модельно
Исправление распределённых багов после деплоя обходится дорого. Модельная проверка позволяет найти их до написания хотя бы одной строчки кода реализации. Вот как это сделать с помощью TLA+.
Распределённый протокол нельзя покрыть юнит-тестами. Юнит-тест запускает один процесс на одной машине в одном порядке. Ваш протокол запускает десять процессов…