Изменения

* Есть один процесс-координатор, ответственный за поиск согласованного среза;.* Остальные процессы обычные, их задача — проверять свои локальные предикаты;.* Всякий раз, когда впервые с момента последнего отправленного сообщения локальный предикат становится true, оповещаем об этом координатора, указывая свое векторное время (впервые — чтобы не спамить, состояния процесса между посылками сообщений для системы неотличимы);. Векторное время при этом увеличивается.** Из этого следует, что если есть наименьший согласованный срез, в котором слабый конъюнктивный предикат верен, то в нём векторные часы всех потоков попарно несравнимы.** Более того: если у нас есть срез (необязательно согласованный), в котором все векторные часы всех потоков попарно несравнимы, то он согласован (см. [[Срез, согласованный срез|согласованный срез]]).** Таким образом нам достаточно искать наименьший срез из событий, в которых выполняется локальный предикат, а все векторные часы попарно несравнимы.* Координатор поддерживает в памяти срез-кандидат и очередь необработанных сообщений от каждого процесса;* Срез. Инвариант: все срезы, у которых хотя бы одна компонента меньше нашего среза-кандидат согласован тогда и только тогдакандидата, когда все соответствующие вектора попарно несравнимы;гарантированно не подходят.* Координатор хранит вектора среза-кандидата и флажок для каждой его компоненты: красный – этот элемент это событие не может быть частью последним для данного процесса в срезе-кандидате (т.е. нет согласованного срезасреда с верным предикатом, в котором в данном процессе в срез взяты события до данного или раньше), зеленый – может;.

* Обрабатываем приходящие сообщения только от красных процессов, сообщения от зеленых ставим в очередь:.** Пришедший от красного процесса вектор гарантированно попадает в срез-кандидат.** Сравниваем пришедший вектор попарно с другими процессами, если . Если новый вектор больше, то делаем меньший процесс красным;, потому что новый вектор гарантированно попадает, а тогда после меньшего вектора должно идти что-то ещё (иначе не получим попарно несравнимые события).** После обработки сообщения делаем бывший красный процесс зеленым.