// ************************************************************************** //
//                                                                            //
//    eses                   eses                                             //
//   eses                     eses                                            //
//  eses    eseses  esesese    eses   Embedded Systems Group                  //
//  ese    ese  ese ese         ese                                           //
//  ese    eseseses eseseses    ese   Department of Computer Science          //
//  eses   eses          ese   eses                                           //
//   eses   eseses  eseseses  eses    University of Kaiserslautern            //
//    eses                   eses                                             //
//                                                                            //
// ************************************************************************** //
// The following module implements the traffic light controllers that are used//
// at both ends of the tunnel. These modules are also responsible for counting//
// the cars on the island and in the tunnel.                                  //
// ************************************************************************** //

package IslandTrafficControl;

module TrafficLightController(
event
   ?grantTunnel,    // by TunnelAccessControl when tunnel access is granted
   ?releaseTunnel,  // by TunnelAccessControl when tunnel must be released
   ?want_enter,     // sent from sensor when car wants to enter the tunnel
   ?leave,          // sent from sensor when car is leaving the tunnel
   ?max_level,      // maximal number of cars on island is reached
   !green_light,    // set traffic light green
   !red_light,      // set traffic light red
   !use,            // tell that the tunnel is currently in use
   !req,            // request access of the tunnel
   !tc_inc,!tc_dec, // increment/decrement counter for cars in tunnel
   !ic_change       // increment/decrement counter for cars on island
) {
   emit(red_light);
   loop {
      // --------------------------------------------------------
      // Red light phase: cars can only leave the tunnel. If a
      // car leaves the tunnel, the tc counter is decremented.
      // During the red light phase, a request is sent if a car
      // wants to enter the tunnel. The red light phase ends if
      // the access to the tunnel is grantTunneled.
      // --------------------------------------------------------
      weak abort
         loop {
            while(!leave) {
               pause;
               emit(red_light);
               if(want_enter) emit(req);
            }
            emit(tc_dec);
            while(leave) {
               pause;
               emit(red_light);
            }
         }
      when(!leave & grantTunnel);
      // --------------------------------------------------------
      // Green light phase: cars can only enter the tunnel. This
      // either increments or decrements the number of cars on
      // the island, depending on the side where this controller
      // is used. The number of cars in the tunnel is incremented.
      // The green light phase ends if the maximal number of cars
      // is reached (if it is the mainland controller) or if the
      // TunnelAccessController instructs the controller to releaseTunnel
      // the tunnel (since the other side send higher priortiy
      // requests).
      // --------------------------------------------------------
      weak abort
         loop {
            while(!want_enter) {
               pause;
               emit(green_light);
               emit(use);
        }
        emit(ic_change);
            emit(tc_inc);
            while(want_enter) {
               pause;
               emit(green_light);
               emit(use);
        }
         }
      when(max_level | releaseTunnel);
   }
}