// This model is automatically generated from the RoboChart model // by the translator (translate2prism) plugin in RoboTool. // // All changes made will be lost after regeneration. // PRISM Output dtmc const int Exit_INVALID = 1; const int Exit_ACTION_Parent = 2; const int Exit_ACTION_Trans = 3; const int Exit_ACTION_Waiting = 4; const int Exit_EXITED = 5; const int Exit_Sub_ACTION = 6; const int Exit_Sub_ACTION_Waiting = 7; const int Exit_Sub_EXITED = 8; const int FD_NoTask = 0; const int FD_FetchMail = 1; const int FD_DeliverMail = 2; const int ctrl_ref0_deliverCTRL_batteryCharge; const int ctrl_ref0_deliverCTRL_chargeSpeed; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_LOCK_FREE = 0; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_INACTIVE = 0; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_i0 = 1; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_INACTIVE = 0; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_i0 = 1; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_s0 = 2; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_s1 = 3; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_s2 = 4; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_s3 = 5; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_s4 = 6; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_s5 = 7; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_s6 = 8; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_s7 = 9; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_s8 = 10; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_p0 = 11; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_p1 = 12; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_p2 = 13; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_p3 = 14; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_p4 = 15; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_p5 = 16; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_p6 = 17; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_p7 = 18; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_p8 = 19; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_p_xxx_1 = 20; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_Alt_xxx_3 = 21; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_t2 = 22; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_t3 = 23; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_t5 = 24; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_t6 = 25; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_t7 = 26; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_t8 = 27; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_t10 = 28; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_t11 = 29; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_t12 = 30; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_t14 = 31; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_t15 = 32; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_t16 = 33; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_t18 = 34; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_t19 = 35; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_t20 = 36; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_t22 = 37; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_t23 = 38; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_t24 = 39; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_t26 = 40; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_t27 = 41; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_t28 = 42; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_t30 = 43; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_t31 = 44; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_t32 = 45; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_t34 = 46; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_t35 = 47; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_t36 = 48; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_T0_XXX_2 = 1; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_T1 = 2; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_T4 = 3; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_T9 = 4; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_T13 = 5; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_T17 = 6; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_T21 = 7; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_T25 = 8; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_T29 = 9; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_T33 = 10; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move = 2; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Stuck = 3; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_p_xxx_6 = 4; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_p_xxx_9 = 5; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_p_xxx_12 = 6; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_p_xxx_15 = 7; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Alt_xxx_8 = 8; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Alt_xxx_11 = 9; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Alt_xxx_14 = 10; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Alt_xxx_17 = 11; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_T0_XXX_7 = 11; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_T2_XXX_10 = 12; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_TR_J_XXX_4_XXX_13 = 13; const int ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_TR_J_XXX_5_XXX_16 = 14; const int ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_LOCK_FREE = 0; const int ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_INACTIVE = 0; const int ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_i0 = 1; const int ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_s0 = 2; const int ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_p_xxx_18 = 3; const int ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_p_xxx_21 = 4; const int ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_p_xxx_24 = 5; const int ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_Alt_xxx_20 = 6; const int ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_Alt_xxx_23 = 7; const int ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_Alt_xxx_26 = 8; const int ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_T0_XXX_19 = 1; const int ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_T1_XXX_22 = 2; const int ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_T3_XXX_25 = 3; const int ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_LOCK_FREE = 0; const double ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_f = 0.5; const int ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_INACTIVE = 0; const int ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_i0 = 1; const int ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_s0 = 2; const int ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_p0 = 3; const int ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_p1 = 4; const int ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_p_xxx_27 = 5; const int ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_p_xxx_30 = 6; const int ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_p_xxx_33 = 7; const int ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_Alt_xxx_29 = 8; const int ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_Alt_xxx_32 = 9; const int ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_t3 = 10; const int ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_t4 = 11; const int ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_t5 = 12; const int ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_t6 = 13; const int ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_t7 = 14; const int ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_t8 = 15; const int ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_t9 = 16; const int ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_t10 = 17; const int ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_t11 = 18; const int ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_t13 = 19; const int ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_t14 = 20; const int ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_t15 = 21; const int ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_t16 = 22; const int ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_t17 = 23; const int ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_t18 = 24; const int ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_t19 = 25; const int ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_t20 = 26; const int ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_Alt_xxx_35 = 27; const int ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_T0_XXX_28 = 1; const int ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_T1_XXX_31 = 2; const int ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_T2 = 3; const int ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_T12 = 4; const int ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_T21_XXX_34 = 5; global ctrl_ref0_deliverCTRL_c : [-40..40] init ctrl_ref0_deliverCTRL_batteryCharge; global ctrl_ref0_deliverCTRL_p : [-40..40] init 0; module ctrl_ref0_deliverCTRL_stm_ref0_movingSTM ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock : [0..15] init ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_LOCK_FREE; ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_scpc : [0..11] init ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_i0; ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_exit : [0..8] init Exit_INVALID; ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc : [0..48] init ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_INACTIVE; ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_exit : [0..8] init Exit_INVALID; // Trigger an exit of the composite state [Move] [] ((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_exit=Exit_Sub_ACTION)) -> (ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_exit'=Exit_ACTION_Parent)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_exit'=Exit_Sub_ACTION_Waiting); // If the composite state [Move] has been exited and its parent state required exit, then its parent state [movingSTM]'s substate has exited too [] (((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_exit=Exit_EXITED)))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_exit=Exit_Sub_ACTION_Waiting)) -> (ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_exit'=Exit_Sub_EXITED); // The state [Move] is going to exit by setting its substates to exit firstly. [] ((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move))&(((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_exit=Exit_ACTION_Parent))|((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_exit=Exit_ACTION_Trans))) -> (ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_exit'=Exit_Sub_ACTION); // Check if all substates of the composite state [Move] are exited [] ((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_exit=Exit_Sub_EXITED)) -> (ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_exit'=Exit_EXITED)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_INACTIVE); // Exit command of the state [s0] [] (((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_s0)))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_exit=Exit_Sub_ACTION)) -> (ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_exit'=Exit_Sub_EXITED); // Exit command of the state [s1] [] (((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_s1)))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_exit=Exit_Sub_ACTION)) -> (ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_exit'=Exit_Sub_EXITED); // Exit command of the state [s2] [] (((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_s2)))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_exit=Exit_Sub_ACTION)) -> (ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_exit'=Exit_Sub_EXITED); // Exit command of the state [s3] [] (((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_s3)))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_exit=Exit_Sub_ACTION)) -> (ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_exit'=Exit_Sub_EXITED); // Exit command of the state [s4] [] (((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_s4)))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_exit=Exit_Sub_ACTION)) -> (ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_exit'=Exit_Sub_EXITED); // Exit command of the state [s5] [] (((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_s5)))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_exit=Exit_Sub_ACTION)) -> (ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_exit'=Exit_Sub_EXITED); // Exit command of the state [s6] [] (((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_s6)))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_exit=Exit_Sub_ACTION)) -> (ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_exit'=Exit_Sub_EXITED); // Exit command of the state [s7] [] (((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_s7)))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_exit=Exit_Sub_ACTION)) -> (ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_exit'=Exit_Sub_EXITED); // Exit command of the state [s8] [] (((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_s8)))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_exit=Exit_Sub_ACTION)) -> (ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_exit'=Exit_Sub_EXITED); // Start of the transition [t0_xxx_2] [] ((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_i0)) -> (ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_p_xxx_1)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_T0_XXX_2); [] (((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_p_xxx_1)))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_T0_XXX_2)) -> (ctrl_ref0_deliverCTRL_p'=0)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_s0)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_LOCK_FREE); // Start of the transition [t1] [move_xxx_9] ((((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_s0)))&(ctrl_ref0_deliverCTRL_c>0))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_LOCK_FREE)) -> (ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_p0)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_T1); [] (((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_p0)))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_T1)) -> 0.5:(ctrl_ref0_deliverCTRL_p'=0)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_s0)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_LOCK_FREE) + 0.5:(ctrl_ref0_deliverCTRL_p'=4)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_s4)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_LOCK_FREE); // Start of the transition [t4] [move_xxx_9] ((((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_s4)))&(ctrl_ref0_deliverCTRL_c>0))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_LOCK_FREE)) -> (ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_p1)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_T4); [] (((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_p1)))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_T4)) -> 0.25:(ctrl_ref0_deliverCTRL_p'=6)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_s6)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_LOCK_FREE) + 0.25:(ctrl_ref0_deliverCTRL_p'=1)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_s1)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_LOCK_FREE) + 0.25:(ctrl_ref0_deliverCTRL_p'=4)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_s4)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_LOCK_FREE) + 0.25:(ctrl_ref0_deliverCTRL_p'=0)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_s0)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_LOCK_FREE); // Start of the transition [t9] [move_xxx_9] ((((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_s1)))&(ctrl_ref0_deliverCTRL_c>0))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_LOCK_FREE)) -> (ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_p2)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_T9); [] (((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_p2)))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_T9)) -> (1/3):(ctrl_ref0_deliverCTRL_p'=4)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_s4)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_LOCK_FREE) + (1/3):(ctrl_ref0_deliverCTRL_p'=2)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_s2)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_LOCK_FREE) + (1/3):(ctrl_ref0_deliverCTRL_p'=1)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_s1)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_LOCK_FREE); // Start of the transition [t13] [move_xxx_9] ((((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_s2)))&(ctrl_ref0_deliverCTRL_c>0))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_LOCK_FREE)) -> (ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_p3)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_T13); [] (((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_p3)))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_T13)) -> (1/3):(ctrl_ref0_deliverCTRL_p'=1)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_s1)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_LOCK_FREE) + (1/3):(ctrl_ref0_deliverCTRL_p'=3)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_s3)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_LOCK_FREE) + (1/3):(ctrl_ref0_deliverCTRL_p'=2)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_s2)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_LOCK_FREE); // Start of the transition [t17] [move_xxx_9] ((((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_s3)))&(ctrl_ref0_deliverCTRL_c>0))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_LOCK_FREE)) -> (ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_p4)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_T17); [] (((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_p4)))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_T17)) -> (1/3):(ctrl_ref0_deliverCTRL_p'=2)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_s2)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_LOCK_FREE) + (1/3):(ctrl_ref0_deliverCTRL_p'=3)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_s3)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_LOCK_FREE) + (1/3):(ctrl_ref0_deliverCTRL_p'=5)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_s5)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_LOCK_FREE); // Start of the transition [t21] [move_xxx_9] ((((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_s5)))&(ctrl_ref0_deliverCTRL_c>0))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_LOCK_FREE)) -> (ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_p5)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_T21); [] (((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_p5)))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_T21)) -> (1/3):(ctrl_ref0_deliverCTRL_p'=3)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_s3)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_LOCK_FREE) + (1/3):(ctrl_ref0_deliverCTRL_p'=8)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_s8)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_LOCK_FREE) + (1/3):(ctrl_ref0_deliverCTRL_p'=5)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_s5)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_LOCK_FREE); // Start of the transition [t25] [move_xxx_9] ((((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_s8)))&(ctrl_ref0_deliverCTRL_c>0))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_LOCK_FREE)) -> (ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_p6)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_T25); [] (((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_p6)))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_T25)) -> (1/3):(ctrl_ref0_deliverCTRL_p'=5)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_s5)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_LOCK_FREE) + (1/3):(ctrl_ref0_deliverCTRL_p'=7)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_s7)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_LOCK_FREE) + (1/3):(ctrl_ref0_deliverCTRL_p'=8)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_s8)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_LOCK_FREE); // Start of the transition [t29] [move_xxx_9] ((((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_s7)))&(ctrl_ref0_deliverCTRL_c>0))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_LOCK_FREE)) -> (ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_p7)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_T29); [] (((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_p7)))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_T29)) -> (1/3):(ctrl_ref0_deliverCTRL_p'=8)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_s8)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_LOCK_FREE) + (1/3):(ctrl_ref0_deliverCTRL_p'=7)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_s7)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_LOCK_FREE) + (1/3):(ctrl_ref0_deliverCTRL_p'=6)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_s6)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_LOCK_FREE); // Start of the transition [t33] [move_xxx_9] ((((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_s6)))&(ctrl_ref0_deliverCTRL_c>0))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_LOCK_FREE)) -> (ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_p8)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_T33); [] (((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_p8)))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_T33)) -> (1/3):(ctrl_ref0_deliverCTRL_p'=4)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_s4)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_LOCK_FREE) + (1/3):(ctrl_ref0_deliverCTRL_p'=6)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_s6)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_LOCK_FREE) + (1/3):(ctrl_ref0_deliverCTRL_p'=7)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_s7)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_LOCK_FREE); // Exit command of the state [Stuck] [] ((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Stuck))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_exit=Exit_Sub_ACTION)) -> (ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_exit'=Exit_Sub_EXITED); // Start of the transition [t0_xxx_7] [] (ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_i0) -> (ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_scpc'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_p_xxx_6)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_T0_XXX_7); [] ((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_p_xxx_6))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_T0_XXX_7)) -> (ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_scpc'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_i0); // Start of the transition [t2_xxx_10] [] ((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Stuck))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_LOCK_FREE)) -> (ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_scpc'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_p_xxx_9)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_T2_XXX_10); [] ((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_p_xxx_9))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_T2_XXX_10)) -> (ctrl_ref0_deliverCTRL_p'=9)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_scpc'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Stuck)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_LOCK_FREE); // Start of the transition [tr_j_xxx_4_xxx_13] [] (((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move))&(((ctrl_ref0_deliverCTRL_c=0))&((ctrl_ref0_deliverCTRL_p=0))))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_LOCK_FREE)) -> (ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_exit'=Exit_ACTION_Trans)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_TR_J_XXX_4_XXX_13); // Make sure the composite source state [Move] has been exited. [] (((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_exit=Exit_EXITED)))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_TR_J_XXX_4_XXX_13)) -> (ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_scpc'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_p_xxx_12); [] ((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_p_xxx_12))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_TR_J_XXX_4_XXX_13)) -> (ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_scpc'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_scpc'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_i0); // Start of the transition [tr_j_xxx_5_xxx_16] [] (((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move))&(((ctrl_ref0_deliverCTRL_c=0))&((ctrl_ref0_deliverCTRL_p!=0))))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_LOCK_FREE)) -> (ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_exit'=Exit_ACTION_Trans)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_TR_J_XXX_5_XXX_16); // Make sure the composite source state [Move] has been exited. [] (((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Move_exit=Exit_EXITED)))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_TR_J_XXX_5_XXX_16)) -> (ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_scpc'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_p_xxx_15); [] ((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_p_xxx_15))&((ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_TR_J_XXX_5_XXX_16)) -> (ctrl_ref0_deliverCTRL_p'=9)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_scpc'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Stuck)&(ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_LOCK_FREE); endmodule module ctrl_ref0_deliverCTRL_stm_ref1_batterySTM ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_lock : [0..4] init ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_LOCK_FREE; ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_scpc : [0..8] init ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_i0; ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_exit : [0..8] init Exit_INVALID; // Exit command of the state [s0] [] ((ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_scpc=ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_s0))&((ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_exit=Exit_Sub_ACTION)) -> (ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_exit'=Exit_Sub_EXITED); // Start of the transition [t0_xxx_19] [] (ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_scpc=ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_i0) -> (ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_scpc'=ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_p_xxx_18)&(ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_lock'=ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_T0_XXX_19); [] ((ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_scpc=ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_p_xxx_18))&((ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_lock=ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_T0_XXX_19)) -> (ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_scpc'=ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_s0)&(ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_lock'=ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_LOCK_FREE); // Start of the transition [t1_xxx_22] [move_xxx_9] (((ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_scpc=ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_s0))&((ctrl_ref0_deliverCTRL_p=0)))&((ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_lock=ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_LOCK_FREE)) -> (ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_scpc'=ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_p_xxx_21)&(ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_lock'=ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_T1_XXX_22); [] ((ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_scpc=ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_p_xxx_21))&((ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_lock=ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_T1_XXX_22)) -> (ctrl_ref0_deliverCTRL_c'=(ctrl_ref0_deliverCTRL_c<=(ctrl_ref0_deliverCTRL_batteryCharge-ctrl_ref0_deliverCTRL_chargeSpeed)?(ctrl_ref0_deliverCTRL_c+ctrl_ref0_deliverCTRL_chargeSpeed):ctrl_ref0_deliverCTRL_batteryCharge))&(ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_scpc'=ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_s0)&(ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_lock'=ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_LOCK_FREE); // Start of the transition [t3_xxx_25] [move_xxx_9] (((ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_scpc=ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_s0))&((ctrl_ref0_deliverCTRL_c>0)&((ctrl_ref0_deliverCTRL_p!=0))))&((ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_lock=ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_LOCK_FREE)) -> (ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_scpc'=ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_p_xxx_24)&(ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_lock'=ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_T3_XXX_25); [] ((ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_scpc=ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_p_xxx_24))&((ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_lock=ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_T3_XXX_25)) -> (ctrl_ref0_deliverCTRL_c'=(ctrl_ref0_deliverCTRL_c>0?(ctrl_ref0_deliverCTRL_c-1):0))&(ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_scpc'=ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_s0)&(ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_lock'=ctrl_ref0_deliverCTRL_stm_ref1_batterySTM_LOCK_FREE); endmodule module ctrl_ref0_deliverCTRL_stm_ref2_taskSTM ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_lock : [0..6] init ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_LOCK_FREE; ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_g : [1..8] init 1; ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_fd : [0..2] init FD_NoTask; ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_scpc : [0..27] init ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_i0; ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_exit : [0..8] init Exit_INVALID; // Exit command of the state [s0] [] ((ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_scpc=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_s0))&((ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_exit=Exit_Sub_ACTION)) -> (ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_exit'=Exit_Sub_EXITED); // Start of the transition [t0_xxx_28] [] (ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_scpc=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_i0) -> (ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_scpc'=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_p_xxx_27)&(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_T0_XXX_28); [] ((ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_scpc=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_p_xxx_27))&((ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_lock=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_T0_XXX_28)) -> (ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_scpc'=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_s0)&(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_LOCK_FREE); // Start of the transition [t1_xxx_31] [move_xxx_9] (((ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_scpc=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_s0))&(((ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_fd!=FD_NoTask))&((ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_g!=ctrl_ref0_deliverCTRL_p))))&((ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_lock=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_LOCK_FREE)) -> (ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_scpc'=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_p_xxx_30)&(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_T1_XXX_31); [] ((ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_scpc=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_p_xxx_30))&((ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_lock=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_T1_XXX_31)) -> (ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_scpc'=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_s0)&(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_LOCK_FREE); // Start of the transition [t2] [move_xxx_9] (((ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_scpc=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_s0))&((ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_fd=FD_NoTask)))&((ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_lock=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_LOCK_FREE)) -> (ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_scpc'=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_p0)&(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_T2); [] ((ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_scpc=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_p0))&((ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_lock=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_T2)) -> (ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_f/8):(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_g'=4)&(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_fd'=FD_FetchMail)&(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_scpc'=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_s0)&(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_LOCK_FREE) + (ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_f/8):(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_g'=3)&(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_fd'=FD_FetchMail)&(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_scpc'=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_s0)&(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_LOCK_FREE) + (ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_f/8):(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_g'=2)&(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_fd'=FD_FetchMail)&(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_scpc'=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_s0)&(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_LOCK_FREE) + (ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_f/8):(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_g'=1)&(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_fd'=FD_FetchMail)&(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_scpc'=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_s0)&(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_LOCK_FREE) + (ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_f/8):(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_g'=5)&(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_fd'=FD_FetchMail)&(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_scpc'=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_s0)&(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_LOCK_FREE) + (ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_f/8):(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_g'=6)&(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_fd'=FD_FetchMail)&(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_scpc'=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_s0)&(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_LOCK_FREE) + (ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_f/8):(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_g'=7)&(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_fd'=FD_FetchMail)&(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_scpc'=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_s0)&(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_LOCK_FREE) + (ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_f/8):(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_g'=8)&(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_fd'=FD_FetchMail)&(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_scpc'=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_s0)&(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_LOCK_FREE) + (1-ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_f):(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_scpc'=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_s0)&(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_LOCK_FREE); // Start of the transition [t12] [] (((ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_scpc=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_s0))&(((ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_g=ctrl_ref0_deliverCTRL_p))&((ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_fd=FD_FetchMail))))&((ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_lock=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_LOCK_FREE)) -> (ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_scpc'=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_p1)&(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_T12); [] ((ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_scpc=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_p1))&((ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_lock=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_T12)) -> ((1/7)*((ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_g=1)?0:1)):(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_g'=1)&(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_fd'=FD_DeliverMail)&(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_scpc'=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_s0)&(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_LOCK_FREE) + ((1/7)*((ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_g=2)?0:1)):(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_g'=2)&(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_fd'=FD_DeliverMail)&(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_scpc'=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_s0)&(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_LOCK_FREE) + ((1/7)*((ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_g=3)?0:1)):(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_g'=3)&(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_fd'=FD_DeliverMail)&(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_scpc'=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_s0)&(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_LOCK_FREE) + ((1/7)*((ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_g=4)?0:1)):(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_g'=4)&(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_fd'=FD_DeliverMail)&(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_scpc'=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_s0)&(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_LOCK_FREE) + ((1/7)*((ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_g=5)?0:1)):(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_g'=5)&(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_fd'=FD_DeliverMail)&(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_scpc'=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_s0)&(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_LOCK_FREE) + ((1/7)*((ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_g=6)?0:1)):(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_g'=6)&(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_fd'=FD_DeliverMail)&(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_scpc'=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_s0)&(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_LOCK_FREE) + ((1/7)*((ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_g=7)?0:1)):(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_g'=7)&(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_fd'=FD_DeliverMail)&(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_scpc'=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_s0)&(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_LOCK_FREE) + ((1/7)*((ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_g=8)?0:1)):(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_g'=8)&(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_fd'=FD_DeliverMail)&(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_scpc'=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_s0)&(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_LOCK_FREE); // Start of the transition [t21_xxx_34] [ctrl_ref0_deliverCTRL_stm_ref2_delivery] (((ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_scpc=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_s0))&(((ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_g=ctrl_ref0_deliverCTRL_p))&((ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_fd=FD_DeliverMail))))&((ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_lock=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_LOCK_FREE)) -> (ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_scpc'=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_p_xxx_33)&(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_T21_XXX_34); [] ((ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_scpc=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_p_xxx_33))&((ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_lock=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_T21_XXX_34)) -> (ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_fd'=FD_NoTask)&(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_scpc'=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_s0)&(ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_lock'=ctrl_ref0_deliverCTRL_stm_ref2_taskSTM_LOCK_FREE); endmodule rewards "nbmove" [move_xxx_9] true : 1; endrewards rewards "nbdelivery" [ctrl_ref0_deliverCTRL_stm_ref2_delivery] true : 1; endrewards