\input{MethodCallBindingChannels.tex}

\begin{circus}
\circprocess  MethodCallBinder \circdef \circbegin \\
\end{circus}
%
%
\begin{circusaction}
setCabinPressure\_MethodBinder \circdef \\
	\t1 \circblockopen
	binder\_setCabinPressureCall\\ \t1 ~?~loc\prefixcolon(loc \in setCabinPressureLocs)\\ \t1 ~?~caller\prefixcolon(caller \in setCabinPressureCallers)  \cross \mathbb{R}  \then \\
	setCabinPressureCall~.~loc~.~caller  \cross \mathbb{R}  \then \\
	setCabinPressureRet~.~loc~.~caller \then \\
	binder\_setCabinPressureRet~.~loc~.~caller  \then \\
	setCabinPressure\_MethodBinder
	\circblockclose
\end{circusaction}
%
%
\begin{circusaction}
setEmergencyOxygen\_MethodBinder \circdef \\
	\t1 \circblockopen
	binder\_setEmergencyOxygenCall\\ \t1 ~?~loc\prefixcolon(loc \in setEmergencyOxygenLocs)\\ \t1 ~?~caller\prefixcolon(caller \in setEmergencyOxygenCallers)  \cross \mathbb{R}  \then \\
	setEmergencyOxygenCall~.~loc~.~caller  \cross \mathbb{R}  \then \\
	setEmergencyOxygenRet~.~loc~.~caller \then \\
	binder\_setEmergencyOxygenRet~.~loc~.~caller  \then \\
	setEmergencyOxygen\_MethodBinder
	\circblockclose
\end{circusaction}
%
%
\begin{circusaction}
setFuelRemaining\_MethodBinder \circdef \\
	\t1 \circblockopen
	binder\_setFuelRemainingCall\\ \t1 ~?~loc\prefixcolon(loc \in setFuelRemainingLocs)\\ \t1 ~?~caller\prefixcolon(caller \in setFuelRemainingCallers)  \cross \mathbb{R}  \then \\
	setFuelRemainingCall~.~loc~.~caller  \cross \mathbb{R}  \then \\
	setFuelRemainingRet~.~loc~.~caller \then \\
	binder\_setFuelRemainingRet~.~loc~.~caller  \then \\
	setFuelRemaining\_MethodBinder
	\circblockclose
\end{circusaction}
%
%
\begin{circusaction}
setAirSpeed\_MethodBinder \circdef \\
	\t1 \circblockopen
	binder\_setAirSpeedCall\\ \t1 ~?~loc\prefixcolon(loc \in setAirSpeedLocs)\\ \t1 ~?~caller\prefixcolon(caller \in setAirSpeedCallers)  \cross \mathbb{R}  \then \\
	setAirSpeedCall~.~loc~.~caller  \cross \mathbb{R}  \then \\
	setAirSpeedRet~.~loc~.~caller \then \\
	binder\_setAirSpeedRet~.~loc~.~caller  \then \\
	setAirSpeed\_MethodBinder
	\circblockclose
\end{circusaction}
%
%
\begin{circusaction}
setAltitude\_MethodBinder \circdef \\
	\t1 \circblockopen
	binder\_setAltitudeCall\\ \t1 ~?~loc\prefixcolon(loc \in setAltitudeLocs)\\ \t1 ~?~caller\prefixcolon(caller \in setAltitudeCallers)  \cross \mathbb{R}  \then \\
	setAltitudeCall~.~loc~.~caller  \cross \mathbb{R}  \then \\
	setAltitudeRet~.~loc~.~caller \then \\
	binder\_setAltitudeRet~.~loc~.~caller  \then \\
	setAltitude\_MethodBinder
	\circblockclose
\end{circusaction}
%
%
\begin{circusaction}
setHeading\_MethodBinder \circdef \\
	\t1 \circblockopen
	binder\_setHeadingCall\\ \t1 ~?~loc\prefixcolon(loc \in setHeadingLocs)\\ \t1 ~?~caller\prefixcolon(caller \in setHeadingCallers)  \cross \mathbb{R}  \then \\
	setHeadingCall~.~loc~.~caller  \cross \mathbb{R}  \then \\
	setHeadingRet~.~loc~.~caller \then \\
	binder\_setHeadingRet~.~loc~.~caller  \then \\
	setHeading\_MethodBinder
	\circblockclose
\end{circusaction}
%
%
\begin{circusaction}
isLandingGearDeployed\_MethodBinder \circdef \\
	\t1 \circblockopen
	binder\_isLandingGearDeployedCall\\ \t1 ~?~loc\prefixcolon(loc \in isLandingGearDeployedLocs)\\ \t1 ~?~caller\prefixcolon(caller \in isLandingGearDeployedCallers)  \then \\
	isLandingGearDeployedCall~.~loc~.~caller  \then \\
	isLandingGearDeployedRet~.~loc~.~caller~?~ret \then \\
	binder\_isLandingGearDeployedRet~.~loc~.~caller~!~ret  \then \\
	isLandingGearDeployed\_MethodBinder
	\circblockclose
\end{circusaction}
%
%
\begin{circusaction}
stowLandingGear\_MethodBinder \circdef \\
	\t1 \circblockopen
	binder\_stowLandingGearCall\\ \t1 ~?~loc\prefixcolon(loc \in stowLandingGearLocs)\\ \t1 ~?~caller\prefixcolon(caller \in stowLandingGearCallers)  \then \\
	stowLandingGearCall~.~loc~.~caller  \then \\
	stowLandingGearRet~.~loc~.~caller \then \\
	binder\_stowLandingGearRet~.~loc~.~caller  \then \\
	stowLandingGear\_MethodBinder
	\circblockclose
\end{circusaction}
%
%
\begin{circusaction}
deployLandingGear\_MethodBinder \circdef \\
	\t1 \circblockopen
	binder\_deployLandingGearCall\\ \t1 ~?~loc\prefixcolon(loc \in deployLandingGearLocs)\\ \t1 ~?~caller\prefixcolon(caller \in deployLandingGearCallers)  \then \\
	deployLandingGearCall~.~loc~.~caller  \then \\
	deployLandingGearRet~.~loc~.~caller \then \\
	binder\_deployLandingGearRet~.~loc~.~caller  \then \\
	deployLandingGear\_MethodBinder
	\circblockclose
\end{circusaction}
%
%
\begin{circusaction}
getAltitude\_MethodBinder \circdef \\
	\t1 \circblockopen
	binder\_getAltitudeCall\\ \t1 ~?~loc\prefixcolon(loc \in getAltitudeLocs)\\ \t1 ~?~caller\prefixcolon(caller \in getAltitudeCallers)  \then \\
	getAltitudeCall~.~loc~.~caller  \then \\
	getAltitudeRet~.~loc~.~caller~?~ret \then \\
	binder\_getAltitudeRet~.~loc~.~caller~!~ret  \then \\
	getAltitude\_MethodBinder
	\circblockclose
\end{circusaction}
%
%
\begin{circusaction}
getAirSpeed\_MethodBinder \circdef \\
	\t1 \circblockopen
	binder\_getAirSpeedCall\\ \t1 ~?~loc\prefixcolon(loc \in getAirSpeedLocs)\\ \t1 ~?~caller\prefixcolon(caller \in getAirSpeedCallers)  \then \\
	getAirSpeedCall~.~loc~.~caller  \then \\
	getAirSpeedRet~.~loc~.~caller~?~ret \then \\
	binder\_getAirSpeedRet~.~loc~.~caller~!~ret  \then \\
	getAirSpeed\_MethodBinder
	\circblockclose
\end{circusaction}
%
%
\begin{circusaction}
abort\_MethodBinder \circdef \\
	\t1 \circblockopen
	binder\_abortCall\\ \t1 ~?~loc\prefixcolon(loc \in abortLocs)\\ \t1 ~?~caller\prefixcolon(caller \in abortCallers)  \then \\
	abortCall~.~loc~.~caller  \then \\
	abortRet~.~loc~.~caller \then \\
	binder\_abortRet~.~loc~.~caller  \then \\
	abort\_MethodBinder
	\circblockclose
\end{circusaction}
%
%
\begin{circusaction}
getHeading\_MethodBinder \circdef \\
	\t1 \circblockopen
	binder\_getHeadingCall\\ \t1 ~?~loc\prefixcolon(loc \in getHeadingLocs)\\ \t1 ~?~caller\prefixcolon(caller \in getHeadingCallers)  \then \\
	getHeadingCall~.~loc~.~caller  \then \\
	getHeadingRet~.~loc~.~caller~?~ret \then \\
	binder\_getHeadingRet~.~loc~.~caller~!~ret  \then \\
	getHeading\_MethodBinder
	\circblockclose
\end{circusaction}
%
%
\begin{circusaction}
getAirSpeed\_MethodBinder \circdef \\
	\t1 \circblockopen
	binder\_getAirSpeedCall\\ \t1 ~?~loc\prefixcolon(loc \in getAirSpeedLocs)\\ \t1 ~?~caller\prefixcolon(caller \in getAirSpeedCallers)  \then \\
	getAirSpeedCall~.~loc~.~caller  \then \\
	getAirSpeedRet~.~loc~.~caller~?~ret \then \\
	binder\_getAirSpeedRet~.~loc~.~caller~!~ret  \then \\
	getAirSpeed\_MethodBinder
	\circblockclose
\end{circusaction}
%
%
\begin{circusaction}
getAltitude\_MethodBinder \circdef \\
	\t1 \circblockopen
	binder\_getAltitudeCall\\ \t1 ~?~loc\prefixcolon(loc \in getAltitudeLocs)\\ \t1 ~?~caller\prefixcolon(caller \in getAltitudeCallers)  \then \\
	getAltitudeCall~.~loc~.~caller  \then \\
	getAltitudeRet~.~loc~.~caller~?~ret \then \\
	binder\_getAltitudeRet~.~loc~.~caller~!~ret  \then \\
	getAltitude\_MethodBinder
	\circblockclose
\end{circusaction}
%
%
\begin{circusaction}
getAltitude\_MethodBinder \circdef \\
	\t1 \circblockopen
	binder\_getAltitudeCall\\ \t1 ~?~loc\prefixcolon(loc \in getAltitudeLocs)\\ \t1 ~?~caller\prefixcolon(caller \in getAltitudeCallers)  \then \\
	getAltitudeCall~.~loc~.~caller  \then \\
	getAltitudeRet~.~loc~.~caller~?~ret \then \\
	binder\_getAltitudeRet~.~loc~.~caller~!~ret  \then \\
	getAltitude\_MethodBinder
	\circblockclose
\end{circusaction}
%
%
\begin{circusaction}
isLandingGearDeployed\_MethodBinder \circdef \\
	\t1 \circblockopen
	binder\_isLandingGearDeployedCall\\ \t1 ~?~loc\prefixcolon(loc \in isLandingGearDeployedLocs)\\ \t1 ~?~caller\prefixcolon(caller \in isLandingGearDeployedCallers)  \then \\
	isLandingGearDeployedCall~.~loc~.~caller  \then \\
	isLandingGearDeployedRet~.~loc~.~caller~?~ret \then \\
	binder\_isLandingGearDeployedRet~.~loc~.~caller~!~ret  \then \\
	isLandingGearDeployed\_MethodBinder
	\circblockclose
\end{circusaction}
%
%
\begin{circusaction}
stowLandingGear\_MethodBinder \circdef \\
	\t1 \circblockopen
	binder\_stowLandingGearCall\\ \t1 ~?~loc\prefixcolon(loc \in stowLandingGearLocs)\\ \t1 ~?~caller\prefixcolon(caller \in stowLandingGearCallers)  \then \\
	stowLandingGearCall~.~loc~.~caller  \then \\
	stowLandingGearRet~.~loc~.~caller \then \\
	binder\_stowLandingGearRet~.~loc~.~caller  \then \\
	stowLandingGear\_MethodBinder
	\circblockclose
\end{circusaction}
%
%
\begin{circusaction}
deployLandingGear\_MethodBinder \circdef \\
	\t1 \circblockopen
	binder\_deployLandingGearCall\\ \t1 ~?~loc\prefixcolon(loc \in deployLandingGearLocs)\\ \t1 ~?~caller\prefixcolon(caller \in deployLandingGearCallers)  \then \\
	deployLandingGearCall~.~loc~.~caller  \then \\
	deployLandingGearRet~.~loc~.~caller \then \\
	binder\_deployLandingGearRet~.~loc~.~caller  \then \\
	deployLandingGear\_MethodBinder
	\circblockclose
\end{circusaction}
%
%
\begin{circusaction}
getAltitude\_MethodBinder \circdef \\
	\t1 \circblockopen
	binder\_getAltitudeCall\\ \t1 ~?~loc\prefixcolon(loc \in getAltitudeLocs)\\ \t1 ~?~caller\prefixcolon(caller \in getAltitudeCallers)  \then \\
	getAltitudeCall~.~loc~.~caller  \then \\
	getAltitudeRet~.~loc~.~caller~?~ret \then \\
	binder\_getAltitudeRet~.~loc~.~caller~!~ret  \then \\
	getAltitude\_MethodBinder
	\circblockclose
\end{circusaction}
%
%
\begin{circus}
BinderActions \circdef \\
\circblockopen 
	setCabinPressure\_MethodBinder
	\\ \interleave \\

	setEmergencyOxygen\_MethodBinder
	\\ \interleave \\

	setFuelRemaining\_MethodBinder
	\\ \interleave \\

	setAirSpeed\_MethodBinder
	\\ \interleave \\

	setAltitude\_MethodBinder
	\\ \interleave \\

	setHeading\_MethodBinder
	\\ \interleave \\

	isLandingGearDeployed\_MethodBinder
	\\ \interleave \\

	stowLandingGear\_MethodBinder
	\\ \interleave \\

	deployLandingGear\_MethodBinder
	\\ \interleave \\

	getAltitude\_MethodBinder
	\\ \interleave \\

	getAirSpeed\_MethodBinder
	\\ \interleave \\

	abort\_MethodBinder
	\\ \interleave \\

	getHeading\_MethodBinder
	\\ \interleave \\

	getAirSpeed\_MethodBinder
	\\ \interleave \\

	getAltitude\_MethodBinder
	\\ \interleave \\

	getAltitude\_MethodBinder
	\\ \interleave \\

	isLandingGearDeployed\_MethodBinder
	\\ \interleave \\

	stowLandingGear\_MethodBinder
	\\ \interleave \\

	deployLandingGear\_MethodBinder
	\\ \interleave \\

	getAltitude\_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}
