64
правки
Изменения
Нет описания правки
Токен состоит из двух векторов. Первый назовем $G$. $G[i] = k$ означает, что состояние $k$ $i$-го процесса входит в срез-кандидат. Важно, что этот срез может не быть согласованным, но все состояния в нем удовлетворяют локальным предикатам. $G$ инициализируется нулями.
Второй вектор назовем $color$, где $color[i] $ обозначает цвет состояния среза-кандидата для $i$-го процесса. Цвет состояния может быть красным или зеленым. Если $color[i] $ равен красному, то состояние $(i, G [i])$ и все его предшествующие состояния уже красные и никогда не смогут удовлетворить $WCP$. Если $color [i] $ зеленый, то нет такого состояния в $G$, что $(i, G[i])$ предшествует ему. $color$ инициализируется красными.
Работа $i$-го монитор-процесса описана следующим псевдокодом. Гарантируется: когда переменная $detect = true$, мы получим искомый срез.
=== Псевдокод ===
[[Файл:https://pp.userapi.com/c846120/v846120267/1099b/Y98QwD2teI0Proc_algo.jpgpng]]