state transitions cluster__Invar Invar cluster__Invar_I2 I2 cluster__Invar_I1 I1 __initial __initial->_Invar _Done Done enter ^out.done _Invar_I2_initial _Invar_I2_S4 S4 _Invar_I2_initial->_Invar_I2_S4 _Invar_I2_S6 S6 _Invar_I2_S6->_Done [INSTATE(["/Invar/I1/S3"])]    _Invar_I2_S5 S5 _Invar_I2_S5->_Invar_I2_S6 /a = 3 * a    _Invar_I2_S4->_Invar_I2_S5 /a = a + b    _Invar_I1_initial _Invar_I1_S1 S1 _Invar_I1_initial->_Invar_I1_S1 _Invar_I1_S3 S3 _Invar_I1_S2 S2 _Invar_I1_S2->_Invar_I1_S3 /b = 2 * a + b    _Invar_I1_S1->_Invar_I1_S2 /b = 2 * b