- - - - CENAPAD-MGCO

A seguir: Theorem 1 Acima: O Algoritmo de Naimi-Trehel Anterior: Proof of Mutual Exclusion

Progress: the Graph

Let ${\cal D}$ be a relation defined between nodes of the network by the following rules: Node i j if and only if one of the following conditions is verified:

${\cal D}$1: Next[i] = j

${\cal D}$2: R [i] $\in$ IN[j]

${\cal D}$3: Position(ReqList[j],i) = 1

${\cal D}$4: $\exists$ k, Position(ReqList[k],j) = Position(ReqList[k],i) + 1

${\cal D}$5: $\ensuremath{\mathbf{T}} \in$ IN[j], Position($\ensuremath{\mathbf{T}}$.ReqList,i) = 1

${\cal D}$6: $\exists$ k, $\ensuremath{\mathbf{T}} \in$ IN[k], Position($\ensuremath{\mathbf{T}}$.ReqList, j) = Position($\ensuremath{\mathbf{T}}$.ReqList,i) + 1