Ресинхронизация схемы: инкрементный подход: различия между версиями

Для завершения разработки алгоритма осталось реализовать проверку :P3. Из предыдущего обсуждения мы уже знаем, что из :P3 следует, что существует такая вершина u, что r[u] — r0[u] > r[v] — r0[v] после каждого увеличения r[v]. Это означает, что maxv2V r[v] — r0[v] не будет увеличиваться. Иначе говоря, существует по меньшей мере одна вершина v, у которой r[v] не будет меняться. До увеличения r[v] имеет место соотношение wu^v — r[u] + r[v] < 0, где wu^v > 0 – исходное количество регистров на одной пути из u в v, в результате чего неравенство r[v] — r[u] < 1 остается верным даже после увеличения r[v]. Из этого следует, что будет по меньшей мере i + 1 вершин, у которых r не превышает i для 0 < i < jVj. Иными словами, алгоритм может по-прежнему увеличивать r, и когда какое-либо значение r достигнет j Vj, это показывает, что условие P3 удовлетворяется. Таким образом, полный алгоритм имеет следующую форму: r, t,<j) := 0,d,oo; dofP1g