package Communication.FDDI.Binary;

module FDDI(event reset1, reset2,
              bool c_1_7, c_1_6, c_1_5, c_1_4,
              c_1_3, c_1_2, c_1_1, c_1_0,
              c_2_7, c_2_6, c_2_5, c_2_4,
              c_2_3, c_2_2, c_2_1, c_2_0,
              TT1, TT2, RT1, RT2, t_s1, t_as1, t_s2, t_as2)
{

   next(TT1) = false;
   next(TT2) = false;
   startp: pause;
   {
      T1 : timer(reset1,c_1_7,c_1_6,c_1_5,c_1_4,c_1_3,c_1_2,c_1_1,c_1_0);
   || T2 : timer(reset2,c_2_7,c_2_6,c_2_5,c_2_4,c_2_3,c_2_2,c_2_1,c_2_0);
   || RING: ring(RT1,RT2,TT1,TT2);
   || S1: station(TT1,c_1_7,c_1_6,c_1_5,c_1_4,c_1_3,c_1_2,c_1_1,c_1_0,
                  reset1,RT1,t_s1, t_as1);
   || S2: station(TT2,c_2_7,c_2_6,c_2_5,c_2_4,c_2_3,c_2_2,c_2_1,c_2_0,
                  reset2,RT2,t_s2, t_as2);
   }
}satisfies {
   exclusive: assert A G !((t_s1 | t_as1) & (t_s2 | t_as2) );
}