package Communication.FDDI.Integer; module Station(int ?trt, ?SA, ?TRTT, bool ?TT, event !counter_reset, bool !RT, !transmit_sync, !transmit_async) { int tht; bool sendbreak; loop { emit(counter_reset); RT = false; transmit_sync = false; transmit_async = false; station_idle: await(TT); tht = trt; emit(counter_reset); sendbreak = false; weak abort { {station_sending_sync_wait : await(trt==SA); sendbreak = true;} ||| {transmit_sync=true; station_sending_sync: pause;} }when(sendbreak); sendbreak = false; transmit_sync = false; if (tht+trt-SA<TRTT) { weak abort { {station_sending_async1: await (tht+trt-SA==TRTT); sendbreak = true;} ||| {transmit_async= true; station_sending_async2: pause;} }when(sendbreak); } } RT = true; fin: pause; }