4551
правка
Ресинхронизация схемы: инкрементный подход: различия между версиями
Материал из WEGA
Ресинхронизация схемы: инкрементный подход (посмотреть исходный код)
Версия от 19:37, 27 мая 2017
, 27 мая 2017→Ограничения и цель
Irina (обсуждение | вклад) м (→Нотация) |
Irina (обсуждение | вклад) |
||
| Строка 19: | Строка 19: | ||
== Ограничения и цель == | == Ограничения и цель == | ||
В силу данной нотации допустимая ресинхронизация r не должна иметь отрицательного количества регистров по какому-либо ребру. Подобное условие допустимости задается формулой P0(r) , | В силу данной нотации допустимая ресинхронизация r не должна иметь отрицательного количества регистров по какому-либо ребру. Подобное условие допустимости задается формулой | ||
<math>P0(r) \triangleq \forall (u, v) \in E: w[u, v] + r[v] - r[u] \ge 0 \;</math>. | |||
Как уже было установлено, условия, согласно которым t является допустимым временем прибытия, задаются следующими двумя предикатами. | Как уже было установлено, условия, согласно которым t является допустимым временем прибытия, задаются следующими двумя предикатами. | ||
P1(t) | |||
<math>P1(t) \triangleq \forall v \in V: t[v] \ge d[v] \;</math>, | |||
<math>P2(r, t) \triangleq \forall u, v \in E: r[u] - r[v] = w[u, v] \implies t[v] - t[u] \ge d[v] \;</math>. | |||
Предикат P обозначает конъюнкцию двух вышеупомянутых условий: | Предикат P обозначает конъюнкцию двух вышеупомянутых условий: | ||
P(r | |||
<math>P(r, t) \triangleq P0(r) \and P1(t) \and P2(r, t) \;</math>. | |||
