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