package Communication.FDDI.Binary;

module timer(event ?reset, bool c0, c1, c2, c3, c4, c5, c6, c7) {

  bool s7, s6, s5, s4, s3, s2, s1, s0, cry8;

  loop {
      next(c7) = false;
      next(c6) = false;
      next(c5) = false;
      next(c4) = false;
      next(c3) = false;
      next(c2) = false;
      next(c1) = false;
      next(c0) = false;
      w1: pause;
      abort {
        loop {
          Add: Adder8(c7,c6,c5,c4,c3,c2,c1,c0,
                            false,false,false,false,false,false,false,false,
                            true, cry8,s7,s6,s5,s4,s3,s2,s1,s0);
          next(c7) = s7;
          next(c6) = s6;
          next(c5) = s5;
          next(c4) = s4;
          next(c3) = s3;
          next(c2) = s2;
          next(c1) = s1;
          next(c0) = s0;
          consume_time: pause;
        }
      }when(reset);
  }
}satisfies {
   cf1 : assert A X w1;
   cf2 : assert A G (w1 -> A X consume_time);
   cf3 : assert A G (consume_time & !reset -> A X consume_time);
   cf4 : assert A G (consume_time &  reset -> A X w1);
   df1 : assert !(c7 | c6 | c5 | c4 | c3 | c2 | c1 | c0);
   df20 : assert A X !(c7 | c6 | c5 | c4 | c3 | c2 | c1 | c0);
   df21 : assert A X A X (!(c7 | c6 | c5 | c4 | c3 | c2 | c1 ) & c0);
   reset0 : assert A G (c0 -> A X !c0);
   reset1 : assert A X A G (reset -> A X (!c7 & !c6 & !c5 & !c4 & !c3 & !c2 & !c1));
}