Слабый конъюнктивный предикат — различия между версиями

Материал из Викиконспекты
Перейти к: навигация, поиск
м (rollbackEdits.php mass rollback)
 
(не показаны 2 промежуточные версии 2 участников)
Строка 6: Строка 6:
 
'''Локальный предикат''' – предикат по состоянию одного процесса. Например, если у процесса есть состояние (переменная) x, то локальным предикатом может быть (x < 0).
 
'''Локальный предикат''' – предикат по состоянию одного процесса. Например, если у процесса есть состояние (переменная) x, то локальным предикатом может быть (x < 0).
  
Пример предиката: “в системе нет координатора”, причем локальное условие – “я не координатор”.
+
Пример WCP предиката: “в системе нет координатора”, причем локальное условие – “я не координатор”.

Текущая версия на 19:36, 4 сентября 2022

Слабый конъюнктивный предикат (WCP) – предикат, удовлетворяющий двум условиям:

  • имеет вид конъюнкции локальных предикатов над состоянием каждого процесса;
  • его истинность есть истинность хотя бы на одном согласованном срезе.

Локальный предикат – предикат по состоянию одного процесса. Например, если у процесса есть состояние (переменная) x, то локальным предикатом может быть (x < 0).

Пример WCP предиката: “в системе нет координатора”, причем локальное условие – “я не координатор”.