TLC

Формальная верификация · первая программа проверки TLA+

создано 25 октября 2026 г. · обновлено 25 октября 2026 г.

Первая программа, которая проверяет модели на TLA+. Она перебирает все состояния модели по одному и для каждого проверяет правила, помня, где уже была. Поэтому её работа предсказуема, но мир модели должен быть небольшим: иначе состояний слишком много. Модели на Quint тоже можно проверять в TLC, но сначала их нужно перевести в запись для этой программы.

Источник: TLA+ Tools и TLC на GitHub

Весь глоссарий