package Communication.FDDI.Binary;

module counterTest(event !ok, bool t7, c0)
{
   bool t6, t5, t4, t3, t2, t1, t0,
        r7, r6, r5, r4, r3, r2, r1, r0;

   next(t7) = false;
   next(t6) = false;
   next(t5) = false;
   next(t4) = false;
   next(t3) = false;
   next(t2) = false;
   next(t1) = false;
   next(t0) = false;

   loop {
       w1: pause;

       A1: Adder8(t7,t6,t5,t4,t3,t2,t1,t0, false,false,false,false,false,false,false,true, false,
                  c0, r7,r6,r5,r4,r3,r2,r1,r0);

       next(t7) = r7;
       next(t6) = r6;
       next(t5) = r5;
       next(t4) = r4;
       next(t3) = r3;
       next(t2) = r2;
       next(t1) = r1;
       next(t0) = r0;
       w3: pause;
   }

}satisfies {
   s1: assert !A F (t7 == true);
   s2: assert !A F (c0 == true);
}