// ************************************************************************** //
//                                                                            //
//    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 is used for managing access to the tunnel, which is a //
// classical problem for mutual exclusion of access to a shared resource. Note//
// that the island is given a higher priority which is necessary to avoid     //
// deadlocks (otherwise the maximum number of cars could be reached on the    //
// island, but the mainland will have control over the tunnel, and thus, no   //
// car could leave the island).                                               //
// ************************************************************************** //

package IslandTrafficControl;

macro MaxCars = 5;

module TunnelAccessControl(
event
   ?il_use, // island has access to the tunnel
   ?il_req, // island requests access to the tunnel
   ?ml_use, // mainland has access to the tunnel
   ?ml_req, // mainland requests access to the tunnel
   !il_grant,   // island is granted access to tunnel
   !il_release, // island is told to release access of tunnel
   !ml_grant,   // mainland is granted access to tunnel
   !ml_release, // mainland is told to release access of tunnel
   nat{MaxCars+1} tc,ic) {
   loop {
      // -------------------------------------------------------
      // wait until there is a request
      // -------------------------------------------------------
      await (il_req | ml_req);
      if(il_req) {
     // ----------------------------------------------------
         // tell mainland to release control over the tunnel
     // ----------------------------------------------------
         while(ml_use) {
            pause;
            emit(ml_release);
         }
     // ----------------------------------------------------
     // wait until all cars left the tunnel
     // ----------------------------------------------------
         immediate await (tc==0);
     // ----------------------------------------------------
     // and give the island control over the tunnel
     // ----------------------------------------------------
         emit(il_grant);
      } else if(ic!=MaxCars) {
     // ----------------------------------------------------
         // tell island to release control over the tunnel
     // ----------------------------------------------------
         while(il_use) {
            pause;
            emit(il_release);
         }
     // ----------------------------------------------------
     // wait until all cars left the tunnel
     // ----------------------------------------------------
         immediate await (tc==0);
     // ----------------------------------------------------
     // and give the island control over the tunnel
     // ----------------------------------------------------
         emit(ml_grant);
      }
   }
}