Слабый конъюнктивный предикат — различия между версиями
| Строка 6: | Строка 6: | ||
'''Локальный предикат''' – предикат по состоянию одного процесса. Например, если у процесса есть состояние (переменная) x, то локальным предикатом может быть (x < 0). | '''Локальный предикат''' – предикат по состоянию одного процесса. Например, если у процесса есть состояние (переменная) x, то локальным предикатом может быть (x < 0). | ||
| − | Пример предиката: “в системе нет координатора”, причем локальное условие – “я не координатор”. | + | Пример WCP предиката: “в системе нет координатора”, причем локальное условие – “я не координатор”. |
Версия 14:28, 14 марта 2018
Слабый конъюнктивный предикат (WCP) – предикат, удовлетворяющий двум условиям:
- имеет вид конъюнкции локальных предикатов над состоянием каждого процесса;
- его истинность есть истинность хотя бы на одном согласованном срезе.
Локальный предикат – предикат по состоянию одного процесса. Например, если у процесса есть состояние (переменная) x, то локальным предикатом может быть (x < 0).
Пример WCP предиката: “в системе нет координатора”, причем локальное условие – “я не координатор”.
