counter: THEORY
BEGIN
   basics : LIBRARY ="../../hw/basics";
   IMPORTING
     basics@incrementer

   reg_type:TYPE=bvec[32];

   counter(clr,ce,up:bit,a:bvec[32]):
     [# next_counter: bvec[32], output: bvec[32] #]=
     LET out = IF clr THEN
                 fill[32](FALSE)
               ELSE
                 IF ce THEN
                   LET incr_input = IF up THEN 
                                      a 
                                    ELSE
                                      LAMBDA (i:below(32)):NOT a(i)
                                    ENDIF,
                       incr_output= incr_impl(32,incr_input,TRUE)^(31,0) IN
                     IF up THEN
                       incr_output
                     ELSE
                       LAMBDA (i:below(32)):NOT incr_output(i)
                     ENDIF
                 ELSE
                   a
                 ENDIF
               ENDIF IN
     (# next_counter := out,
        output       := a #);

End counter