[[Категория: Параллельное программирование]]
'''Слабый конъюнктивный предикат (WCP)''' – — [[Глобальные свойства системы|предикат]], имеющий вид конъюнкции локальных предикатов над состоянием каждого процесса.{{Определение|definition=Слабый конъюктивный предикат $P$ '''истинен''', если он истенен на хотя бы одном согласованном срезе}}Сложные предикаты, составленные как логическая комбинация локальных предикатов, можно представить в дизъюнктивной нормальной форме и рассмотреть как дизъюнкцию слабых конъюктивных предикатов.
Его истинность будем определять, как истинность хотя бы на одном согласованном срезе=== Примеры ===Позволяет обнаружить некоторые нежелательные предикаты. '''Локальный предикат''' – предикат по состоянию одного процесса. НапримерОбнаруживает ошибки, если у процесса есть состояние (переменная) x, то локальным предикатом может которые могли бы быть (x < 0). Используется для нежелательных предикатов, например, классическая проблема взаимного исключенияскрыты в определенном запуске из-за race conditions.
Обнаруживает ошибкиНапример, которые могли бы быть скрыты классическую проблема взаимного исключения: локальный предикат "процесс в определенном запуске из-за race conditionsкритической секции".Если есть срез, в котором два процесса в критической секции, то всё плохо.А если такого нет, то любые две критические секции упорядочены.
Пример Ещё пример WCP предиката: “в системе нет координатора”, причем локальное условие – “я не координатор”.
