state transitions cluster__Counter Counter cluster__Counter_Bit_2 Bit_2 cluster__Counter_Bit_1 Bit_1 __initial __initial->_Counter _Counter_Bit_2_initial _Counter_Bit_2_Bit_21 Bit_21 _Counter_Bit_2_initial->_Counter_Bit_2_Bit_21 _Counter_Bit_2_Bit_22 Bit_22 _Counter_Bit_2_Bit_22->_Counter_Bit_2_Bit_21 tk1^out.done    _Counter_Bit_2_Bit_21->_Counter_Bit_2_Bit_22 tk1    _Counter_Bit_1_initial _Counter_Bit_1_Bit_11 Bit_11 _Counter_Bit_1_initial->_Counter_Bit_1_Bit_11 _Counter_Bit_1_Bit_12 Bit_12 _Counter_Bit_1_Bit_12->_Counter_Bit_1_Bit_11 tk0^tk1    _Counter_Bit_1_Bit_11->_Counter_Bit_1_Bit_12 tk0