state transitions __initial _s1 s1 __initial->_s1 _s2 s2 enter ^out.ok _s1->_s2 start(x:int) [x == 42]    _s1->_s1 start(x:int) [inc_x(x)]