Next: Channel Predicates Up: Figures in the book Previous: Observing Global Predicates

Observing Conjunctive Predicates

**Figure:** WCP 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 .
$\fbox{\begin{minipage}{\textwidth}\sf \begin{tabbing} x\=xxxx\=xxxx\=xxxx\=xxxx\... ...\bf then} $cut[j].color := red$;\\ \>{\bf endfor} \end{tabbing}\end{minipage}}$

**Figure:** The algorithm for the adversary
$\fbox{\begin{minipage}{\textwidth}\sf \begin{tabbing} x\=xxxx\=xxxx\=xxxx\=xxxx\... ...n} $P_j[l] \vert\vert P_i[k];$\\ \> \> {\bf endif} \end{tabbing}\end{minipage}}$

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

**Figure:** Monitor process algorithm
$\fbox{\begin{minipage}{\textwidth}\sf \begin{tabbing} x\=xxxx\=xxxx\=xxxx\=xxxx\... ...ken to $M_j$;\\ \> \> {\bf else} $detect := true$; \end{tabbing}\end{minipage}}$

Vijay K. Garg 2005-02-08