package Communication.FDDI;

module FDDI(bool reset1, int counter1, bool reset2, int counter2,
            bool TT1, RT1, !ts1, !tas1,
                 TT2, RT2, !ts2, !tas2,
            int  SA, TRTT, !TD)
{
   TRTT = 50*2;
   SA = 20;
   TD = 0;
   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;
}