state transitions cluster__Dialing Dialing cluster__Dialing_Redialer Redialer cluster__Dialing_Dialer Dialer __initial __initial->_Dialing _Dialing_Redialer_initial _Dialing_Redialer_WaitForRedial WaitForRedial ✓ _Dialing_Redialer_initial->_Dialing_Redialer_WaitForRedial _Dialing_Redialer_RedialDigits RedialDigits _Dialing_Redialer_RedialDigits->_Dialing_Redialer_RedialDigits [c < numdigits(p)]^dial    _Dialing_Redialer_RedialDigits->_Dialing_Redialer_WaitForRedial [c == numdigits(p)]    _Dialing_Redialer_WaitForRedial->_Dialing_Redialer_RedialDigits redial [c == 0]/p = lp ^dial    _Dialing_Dialer_initial _Dialing_Dialer_WaitForDial WaitForDial ✓ _Dialing_Dialer_initial->_Dialing_Dialer_WaitForDial _Dialing_Dialer_DialDigits DialDigits _Dialing_Dialer_DialDigits->_Dialing_Dialer_DialDigits dial(d:int) [c < 10]/lp = lp * 10 + d⁏ c = c + 1⁏  ^out.out    _Dialing_Dialer_DialDigits->_Dialing_Dialer_WaitForDial [c == 10]    _Dialing_Dialer_WaitForDial->_Dialing_Dialer_DialDigits redial ∧ dial(d:int) [c == 0]/lp = d⁏ c = 1⁏  ^out.out    _Dialing_Dialer_WaitForDial->_Dialing_Dialer_WaitForDial dial(d:int) ∧ ¬redial [c < 10]/c = c + 1⁏ lp = lp * 10 + d⁏  ^out.out