// ************************************************************************** // // // // 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); } }