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;
}