module PARKHAUS: % ####################################################### % ####################################################### % ####################################################### % Inputs / Outputs for TrafficLights on Exit input Exit_go_green; input Exit_go_red; output Exit_signal_red; output Exit_signal_green; % Inputs / Output for TrafficLights on Entry input Entry_go_green; input Entry_go_red; output Entry_signal_red; output Entry_signal_green; % ####################################################### % ####################################################### % ####################################################### % Signals for CAR Potition: output CAR_is_moving_in; output CAR_is_moving_out; % Signals for parking garage output SPACE_LEFT : integer; % Signals for car-tracking % going inside input Entry_car_is_waiting; % S1 input Entry_car_is_going_in; % S2 input Entry_car_is_in_PG; % S3 % going outside input Exit_car_is_waiting; % S4 input Exit_car_is_leaving; % S5 input Exit_car_left_PG; % S6 var SPACE := 20 : integer in % Implementation of car guiding process: loop await case Exit_car_is_leaving do abort sustain CAR_is_moving_out; when Exit_car_left_PG; case Entry_car_is_going_in do abort sustain CAR_is_moving_in; when Entry_car_is_in_PG; end await; end loop || % Implementation for TrafficLights on Exit: loop % implement here end loop || % Implementation for TrafficLights on Entry loop abort sustain Entry_signal_red when Entry_go_green; abort sustain Entry_signal_green when Entry_go_red; end loop || % Implementation of PG-logic loop await case Exit_car_is_waiting do if (SPACE <=20) then emit Exit_go_green; await Exit_car_is_leaving; SPACE := SPACE +1; emit SPACE_LEFT(SPACE); emit Exit_go_red; await Exit_car_left_PG; end if; case Entry_car_is_waiting do if (SPACE > 0) and then emit Entry_go_green; await Entry_car_is_going_in; SPACE := SPACE - 1; emit SPACE_LEFT(SPACE); emit Entry_go_red; await Entry_car_is_in_PG; end if; end await end loop end var; end module