state transitions __initial _counting counting __initial->_counting _done done onentry/ ^out.done _counting->_done [x == 3]    _counting->_counting e    _counting->_counting [x < 3]/x = x + 1 ^out.inc