package Communication.FDDI; module station(int ?trt, ?SA, ?TRTT, bool ?TT, !counter_reset, !RT, !transmit_sync, !transmit_async) { int tht; bool sendbreak; loop { counter_reset = true; RT = false; transmit_sync = false; transmit_async = false; station_idle: await(TT); tht = trt; counter_reset = true; 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_async_a: await((tht+trt-SA)==TRTT); sendbreak = true;} ||| {transmit_async = true; station_sending_async_b: pause;} }when(sendbreak); RT = true; fin: pause; } }