state transitions __initial _s1 s1 enter /x = increment() __initial->_s1 _s3 s3 enter ^out.done _s2 s2 enter /x = increment() _s2->_s3 [x == 2]    _s1->_s2 [x == 1]