while (not v_Done) {

   []Port_X.receive(cr_X) -> value v_X {
    ...
   }
   []Port_Y.receive(cr_Y) -> value v_Y {
    ...
   }
   ...
   [] any component.killed {
     v_Done := true;
   }
  } // while
  f_MTC_Stop(pass)

  function f_MTC_Stop(verdicttype p_Verdict)
  {
    setverdict(p_Verdict);
    all component.stop; 
    mtc.stop;
  }

 /* @desc: Main MTC loop and clean shutdown.
  *
  * Wait until all (critical) components complete or timeout 
  */
  function f_MTC_MainLoop_Shutdown(timer p_GuardTimer) runs on MTC
  {
    var boolean b_MTC_Done := false
    var boolean b_PTC_Main_Done := false;
    var boolean b_PTC_1_Done := false;
    var boolean b_PTC_2_Done := false;

    while (not b_MTC_Done) {
      alt {
        [not b_PTC_Main_Done] vc_Components.ptc_main.done { 
          b_PTC_Main_Done := true;
        }
        [not b_PTC_1_Done] vc_Components.ptc_1.done { 
          b_PTC_1_Done := true;
        }
        [not b_PTC_2_Done] vc_Components.ptc_2.done { 
          b_PTC_2_Done := true;
        }
        [] p_GuardTimer.timeout {
	  f_MTC_Stop(fail);
	  b_MTC_Done := true;
	}
	
        [] any component.killed {
          f_MTC_Stop(inconc);
	  b_MTC_Done := true;
        }
      } // alt
      // check whether all components are done
      if (b_PTC_Main_Done and b_PTC_1_Done and b_PTC_2_Done) {
        b_MTC_Done := true;
      }
    } // while
    f_MTC_Stop(pass);
  }