%+++ Channel Sets +++

% MAKE THIS PARSE

\begin{zsection}
	\SECTION ~ NetworkChannels ~ \parents ~ scj\_prelude, MissionId, MissionIds, \\
		\t1 SchedulableId, SchedulableIds, MissionChan, SchedulableChan, TopLevelMissionSequencerFWChan,\\
		\t1 FrameworkChan, SafeletChan
\end{zsection}
%
\begin{circus}
\circchannelset ~ TerminateSync == \\ \t1 \lchanset schedulables\_terminated, schedulables\_stopped, get\_activeSchedulables \rchanset
\end{circus}
%
\begin{circus}
\circchannelset ~ ControlTierSync ==\\ \t1 \lchanset start\_toplevel\_sequencer, done\_toplevel\_sequencer, done\_safeletFW \rchanset
\end{circus}
% IDs wont type check again   Start Mission and Done Mission wont parse?
\begin{circus}
\circchannelset ~ TierSync == \\ \t1 \lchanset start\_mission~.~MainMission, done\_mission~.~MainMission,\\
	\t1 done\_safeletFW, done\_toplevel\_sequencer \rchanset
\end{circus}
%
\begin{circus}
\circchannelset ~ MissionSync == \\ \t1 \lchanset done\_safeletFW, done\_toplevel\_sequencer, register, \\
                 signalTerminationCall, signalTerminationRet, activate\_schedulables, done\_schedulable, \\
                 cleanupSchedulableCall, cleanupSchedulableRet  \rchanset
\end{circus}
%
\begin{circus}
\circchannelset ~ SchedulablesSync == \\ \t1 \lchanset activate\_schedulables, done\_safeletFW, done\_toplevel\_sequencer \rchanset
\end{circus}
%
\begin{circus}
\circchannelset ~ ClusterSync == \\ \t1 \lchanset done\_toplevel\_sequencer, done\_safeletFW \rchanset
\end{circus}
%
\begin{circus}
\circchannelset ~ AppSync == \\ \t1  \bigcup \{SafeltAppSync, MissionSequencerAppSync, MissionAppSync, \\ \t1 MTAppSync, OSEHSync , APEHSync,  \\ \t1
	\lchanset getSequencer, end\_mission\_app, end\_managedThread\_app, \\ \t1 setCeilingPriority, requestTerminationCall,requestTerminationRet, terminationPendingCall, \\ \t1 terminationPendingRet, handleAsyncEventCall, handleAsyncEventRet \rchanset  \}
\end{circus}
%
%\begin{circus}
%\circchannelset ~ ObjectSync   == \\ \t1    \lchanset	 \rchanset
%\end{circus}

\begin{circus}
\circchannelset ~ ThreadSync == \\ \t1  \lchanset raise\_thread\_priority, lower\_thread\_priority, isInterruptedCall, isInterruptedRet, get\_priorityLevel \rchanset
\end{circus}

\begin{circus}
\circchannelset ~ LockingSync == \\ \t1  \lchanset lockAcquired, startSyncMeth, endSyncMeth, waitCall, waitRet, notify, isInterruptedCall, isInterruptedRet, \\
\t1 interruptedCall, interruptedRet, done\_toplevel\_sequencer, get\_priorityLevel  \rchanset
\end{circus}

%IDs wont type check
\begin{circus}
\circchannelset ~ Tier0Sync == \\
\t1 \lchanset
done\_toplevel\_sequencer, done\_safeletFW, \\
\t1 start\_mission~.~TakeOffMission, done\_mission~.~TakeOffMission,\\
\t1 initializeRet~.~TakeOffMission,
requestTermination~.~TakeOffMission~.~MainMissionSequencer

, \\
\t1 start\_mission~.~CruiseMission, done\_mission~.~CruiseMission,\\
\t1 initializeRet~.~CruiseMission,
requestTermination~.~CruiseMission~.~MainMissionSequencer

, \\
\t1 start\_mission~.~LandMission, done\_mission~.~LandMission,\\
\t1 initializeRet~.~LandMission,
requestTermination~.~LandMission~.~MainMissionSequencer


\rchanset
\end{circus}
%
%
