package Communication.FDDI.Integer; module FDDI (event reset1, int counter1, bool TT1, RT1, ts1, tas1, event reset2, int counter2, bool TT2, RT2, ts2, tas2, int SA, TRTT) { TRTT = 50*2; SA = 20; TT1 = false; TT2 = false; RT1 = false; RT2 = false; { T1 : Timer(reset1,counter1); || T2 : Timer(reset2,counter2); || S1 : Station(counter1,SA,TRTT,TT1,reset1,RT1,ts1,tas1); || S2 : Station(counter2,SA,TRTT,TT2,reset2,RT2,ts2,tas2); || R : Ring(RT1,RT2,TT1,TT2); } }satisfies { reactive : assert ! E F A X false; }