\input{MethodCallBindingChannels.tex}

\begin{circus}
\circprocess  MethodCallBinder \circdef \circbegin \\
\end{circus}
%
%
\begin{circusaction}
read\_MethodBinder \circdef \\
	\t1 \circblockopen
	binder\_readCall\\ \t1 ~?~loc\prefixcolon(loc \in readLocs)\\ \t1 ~?~caller\prefixcolon(caller \in readCallers)  \then \\
	readCall~.~loc~.~caller  \then \\
	readRet~.~loc~.~caller~?~ret \then \\
	binder\_readRet~.~loc~.~caller~!~ret  \then \\
	read\_MethodBinder
	\circblockclose
\end{circusaction}
%
%
\begin{circusaction}
write\_MethodBinder \circdef \\
	\t1 \circblockopen
	binder\_writeCall\\ \t1 ~?~loc\prefixcolon(loc \in writeLocs)\\ \t1 ~?~caller\prefixcolon(caller \in writeCallers)  \cross \num  \then \\
	writeCall~.~loc~.~caller  \cross \num  \then \\
	writeRet~.~loc~.~caller \then \\
	binder\_writeRet~.~loc~.~caller  \then \\
	write\_MethodBinder
	\circblockclose
\end{circusaction}
%
%
\begin{circus}
BinderActions \circdef \\
\circblockopen 
	read\_MethodBinder
	\\ \interleave \\

	write\_MethodBinder
	
\circblockclose
\end{circus}
%
\begin{circus}
\circspot BinderActions \circinterrupt (done\_toplevel\_sequencer \then \Skip)
\end{circus}
%
\begin{circus}
\circend
\end{circus}
%
\begin{circus}
\circprocess ApplicationB \circdef Application \lpar MethodCallBinderSync \rpar MethodCallBinder
\end{circus}
