Next: Termination Detection Up: Figures in the book Previous: Observing Conjunctive Predicates

Channel Predicates

**Figure:** The set of cuts satisfying the predicate is not a sublattice.
$\begin{figure}\centerline{\epsfbox{figs/non-friendly.eps}}\end{figure}$

**Figure:** Application process algorithm for
$\fbox{\begin{minipage}{\textwidth}\sf \begin{tabbing} x\=xxxx\=xxxx\=xxxx\=xxxx\... ...\ \>\> $incsend:= \emptyset; increcv:=\emptyset$; \end{tabbing}\end{minipage}}$

**Figure:** GCP detection algorithm--checker process
$\fbox{\begin{minipage}{\textwidth}\sf \begin{tabbing} x\=xxxx\=xxxx\=xxxx\=xxxx\... ...\>{\bf endwhile};\\ \>\\ \>$detect$ := $true$; \end{tabbing}\end{minipage}}$

**Figure:** Procedure $update\_channels$
$\fbox{\begin{minipage}{\textwidth}\sf \begin{tabbing} x\=xxxx\=xxxx\=xxxx\=xxxx\... ... then} $cut[j].color := red$;\\ \>{\bf endfor}\\ \end{tabbing}\end{minipage}}$

Vijay K. Garg 2005-02-08