Изменения
Нет описания правки
'''Локальный предикат''' – предикат по состоянию одного процесса. Например, если у процесса есть состояние (переменная) x, то локальным предикатом может быть (x < 0).
Используется для нежелательных предикатов, например, классическая проблема взаимного исключения.
Обнаруживает ошибки, которые могли бы быть скрыты в определенном запуске из-за race conditions.
Пример WCP предиката: “в системе нет координатора”, причем локальное условие – “я не координатор”.
