// This model is automatically generated from the RoboChart model // by the translator (translate2prism v20210223) plugin in RoboTool // on 2021-03-29 21:09:00 // // All changes made will be lost after regeneration. // PRISM Output dtmc const int Action_17 = (5); const int Action_18 = (6); const int Action_19 = (7); const int Action_20 = (8); const int Action_21 = (2); const int Action_22 = (13); const int Action_23 = (14); const int ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_INACTIVE_10 = (0); const int ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_LOCK_FREE = (0); const int ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_TERMINATED_11 = ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_f0; const int ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_TestLoop = (4); const int ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_f0 = (2); const int ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_i0 = (1); const int ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_p0 = (3); const int ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_t0 = (1); const int ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_t1 = (3); const int ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_t4 = (2); const int ransacMOD_ransacCTRL_stm_ref0_INACTIVE_10 = (0); const int ransacMOD_ransacCTRL_stm_ref0_LOCK_FREE = (0); const int ransacMOD_ransacCTRL_stm_ref0_TERMINATED_11 = (15); const int ransacMOD_ransacCTRL_stm_ref0_badFit = (11); const int ransacMOD_ransacCTRL_stm_ref0_determineInliners = (3); const int ransacMOD_ransacCTRL_stm_ref0_determineInliners_entering = (1); const int ransacMOD_ransacCTRL_stm_ref0_goodFit = (9); const int ransacMOD_ransacCTRL_stm_ref0_i0 = (6); const int ransacMOD_ransacCTRL_stm_ref0_index0In = (5); const int ransacMOD_ransacCTRL_stm_ref0_loop_1 = (8); const int ransacMOD_ransacCTRL_stm_ref0_loop_self_2 = (5); const int ransacMOD_ransacCTRL_stm_ref0_p1 = (7); const int ransacMOD_ransacCTRL_stm_ref0_p2 = (4); const int ransacMOD_ransacCTRL_stm_ref0_sp1_5 = (8); const int ransacMOD_ransacCTRL_stm_ref0_sp_pj_4 = (10); const int ransacMOD_ransacCTRL_stm_ref0_startChoose = (12); const int ransacMOD_ransacCTRL_stm_ref0_t10 = (1); const int ransacMOD_ransacCTRL_stm_ref0_t11 = (3); const int ransacMOD_ransacCTRL_stm_ref0_t14 = (2); const int ransacMOD_ransacCTRL_stm_ref0_t16 = (7); const int ransacMOD_ransacCTRL_stm_ref0_t4 = (4); const int ransacMOD_ransacCTRL_stm_ref0_to_loop_3 = (6); const int N = (6); const double q = ((1)/(3)); const int Exit_Sub_ACT_Waiting = (5); const int Exit_NONE = (0); const int Exit_EXITED = (3); const int Exit_Sub_EXITED = (6); const int Exit_ACT_Trans = (2); const int Exit_Sub_ACT = (4); const int Exit_ACT_Parent = (1); global ransacMOD_ransacCTRL_c : bool; global ransacMOD_ransacCTRL_i : [0..10]; // For the state machine [simpRansacSTM] in the controller [ransacCTRL] module ransacMOD_ransacCTRL_stm_ref0 ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_exit_9 : [0..6] init Exit_NONE; ransacMOD_ransacCTRL_stm_ref0_exit_9 : [0..6] init Exit_NONE; ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_scpc_8 : [0..9] init ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_INACTIVE_10; ransacMOD_ransacCTRL_stm_ref0_index0 : [0..10]; ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_n : [0..10]; ransacMOD_ransacCTRL_stm_ref0_lock_7 : [0..8] init ransacMOD_ransacCTRL_stm_ref0_LOCK_FREE; ransacMOD_ransacCTRL_stm_ref0_index1 : [0..10]; ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_lock_7 : [0..3] init ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_LOCK_FREE; ransacMOD_ransacCTRL_stm_ref0_scpc_8 : [0..14] init ransacMOD_ransacCTRL_stm_ref0_i0; // Step 4/2: exit command of the state [startChoose] [] ((ransacMOD_ransacCTRL_stm_ref0_scpc_8=ransacMOD_ransacCTRL_stm_ref0_startChoose))&((ransacMOD_ransacCTRL_stm_ref0_exit_9=Exit_Sub_ACT)) -> (ransacMOD_ransacCTRL_stm_ref0_exit_9'=Exit_Sub_EXITED); // The transition [loop_self_2] from a state [loop_1] to [loop_1].Step 1: trigger an exit of the state [loop_1] [] ((ransacMOD_ransacCTRL_stm_ref0_scpc_8=ransacMOD_ransacCTRL_stm_ref0_loop_1))&((ransacMOD_ransacCTRL_stm_ref0_lock_7=ransacMOD_ransacCTRL_stm_ref0_LOCK_FREE)) -> (ransacMOD_ransacCTRL_stm_ref0_scpc_8'=ransacMOD_ransacCTRL_stm_ref0_loop_1)&(ransacMOD_ransacCTRL_stm_ref0_lock_7'=ransacMOD_ransacCTRL_stm_ref0_LOCK_FREE); // From the probabilistic junction [sp_pj_4] [] (ransacMOD_ransacCTRL_stm_ref0_scpc_8=ransacMOD_ransacCTRL_stm_ref0_sp_pj_4) -> (ransacMOD_ransacCTRL_stm_ref0_scpc_8'=Action_23); // The transition [t1] from a state [TestLoop] to [p0].Step 1: trigger an exit of the state [TestLoop] [] ((ransacMOD_ransacCTRL_i (ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_lock_7'=ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_t1)&(ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_scpc_8'=ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_p0); [] (ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_scpc_8=Action_17) -> (ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_scpc_8'=ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_TestLoop)&(ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_lock_7'=ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_LOCK_FREE)&(ransacMOD_ransacCTRL_c'=true); // Step 4/2: exit command of the state [goodFit] [] ((ransacMOD_ransacCTRL_stm_ref0_scpc_8=ransacMOD_ransacCTRL_stm_ref0_goodFit))&((ransacMOD_ransacCTRL_stm_ref0_exit_9=Exit_Sub_ACT)) -> (ransacMOD_ransacCTRL_stm_ref0_exit_9'=Exit_Sub_EXITED); // The transition [t16] from a state [badFit] to [startChoose].Step 1: trigger an exit of the state [badFit] [] ((ransacMOD_ransacCTRL_stm_ref0_scpc_8=ransacMOD_ransacCTRL_stm_ref0_badFit))&((ransacMOD_ransacCTRL_stm_ref0_lock_7=ransacMOD_ransacCTRL_stm_ref0_LOCK_FREE)) -> (ransacMOD_ransacCTRL_stm_ref0_lock_7'=ransacMOD_ransacCTRL_stm_ref0_LOCK_FREE)&(ransacMOD_ransacCTRL_stm_ref0_scpc_8'=ransacMOD_ransacCTRL_stm_ref0_startChoose); // From the probabilistic junction [p1] [] (ransacMOD_ransacCTRL_stm_ref0_scpc_8=ransacMOD_ransacCTRL_stm_ref0_p1) -> ((1)-q):(ransacMOD_ransacCTRL_stm_ref0_lock_7'=ransacMOD_ransacCTRL_stm_ref0_LOCK_FREE)&(ransacMOD_ransacCTRL_stm_ref0_scpc_8'=ransacMOD_ransacCTRL_stm_ref0_index0In) + q:(ransacMOD_ransacCTRL_stm_ref0_scpc_8'=ransacMOD_ransacCTRL_stm_ref0_badFit)&(ransacMOD_ransacCTRL_stm_ref0_lock_7'=ransacMOD_ransacCTRL_stm_ref0_LOCK_FREE); // The transition [to_loop_3] from a state [goodFit] to [loop_1].Step 1: trigger an exit of the state [goodFit] [] ((ransacMOD_ransacCTRL_stm_ref0_lock_7=ransacMOD_ransacCTRL_stm_ref0_LOCK_FREE))&((ransacMOD_ransacCTRL_stm_ref0_scpc_8=ransacMOD_ransacCTRL_stm_ref0_goodFit)) -> (ransacMOD_ransacCTRL_stm_ref0_lock_7'=ransacMOD_ransacCTRL_stm_ref0_LOCK_FREE)&(ransacMOD_ransacCTRL_stm_ref0_scpc_8'=ransacMOD_ransacCTRL_stm_ref0_loop_1); // The transition [t4] from a state [TestLoop] to [f0].Step 1: trigger an exit of the state [TestLoop] [] ((ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_lock_7=ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_LOCK_FREE))&((! ((ransacMOD_ransacCTRL_i (ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_lock_7'=ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_LOCK_FREE)&(ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_scpc_8'=ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_f0); // The transition [t14] from a state [determineInliners] to [badFit].Step 1: trigger an exit of the state [determineInliners] [] ((ransacMOD_ransacCTRL_stm_ref0_index0=ransacMOD_ransacCTRL_stm_ref0_index1))&(((ransacMOD_ransacCTRL_stm_ref0_lock_7=ransacMOD_ransacCTRL_stm_ref0_LOCK_FREE))&((ransacMOD_ransacCTRL_stm_ref0_scpc_8=ransacMOD_ransacCTRL_stm_ref0_determineInliners))) -> (ransacMOD_ransacCTRL_stm_ref0_lock_7'=ransacMOD_ransacCTRL_stm_ref0_LOCK_FREE)&(ransacMOD_ransacCTRL_stm_ref0_scpc_8'=ransacMOD_ransacCTRL_stm_ref0_badFit); // Step 4/2: exit command of the state [f0] [] ((ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_scpc_8=ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_f0))&((ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_exit_9=Exit_Sub_ACT)) -> (ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_exit_9'=Exit_Sub_EXITED); // The transition [t11] from a state [index0In] to [p2].Step 1: trigger an exit of the state [index0In] [] ((ransacMOD_ransacCTRL_stm_ref0_scpc_8=ransacMOD_ransacCTRL_stm_ref0_index0In))&((ransacMOD_ransacCTRL_stm_ref0_lock_7=ransacMOD_ransacCTRL_stm_ref0_LOCK_FREE)) -> (ransacMOD_ransacCTRL_stm_ref0_scpc_8'=ransacMOD_ransacCTRL_stm_ref0_p2)&(ransacMOD_ransacCTRL_stm_ref0_lock_7'=ransacMOD_ransacCTRL_stm_ref0_t11); // The transition [t0] from [i0] to [TestLoop]. [] (ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_scpc_8=ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_i0) -> (ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_lock_7'=ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_t0)&(ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_scpc_8'=Action_18); // From the probabilistic junction [p0] [] (ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_scpc_8=ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_p0) -> (ransacMOD_ransacCTRL_i (ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_scpc_8'=Action_17)&(ransacMOD_ransacCTRL_i'=(1)); // From the probabilistic junction [p2] [] (ransacMOD_ransacCTRL_stm_ref0_scpc_8=ransacMOD_ransacCTRL_stm_ref0_p2) -> ((1)-q):(ransacMOD_ransacCTRL_stm_ref0_lock_7'=ransacMOD_ransacCTRL_stm_ref0_LOCK_FREE)&(ransacMOD_ransacCTRL_stm_ref0_scpc_8'=ransacMOD_ransacCTRL_stm_ref0_goodFit) + q:(ransacMOD_ransacCTRL_stm_ref0_lock_7'=ransacMOD_ransacCTRL_stm_ref0_LOCK_FREE)&(ransacMOD_ransacCTRL_stm_ref0_scpc_8'=ransacMOD_ransacCTRL_stm_ref0_badFit); [] (ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_scpc_8=Action_19) -> (ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_lock_7'=ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_LOCK_FREE)&(ransacMOD_ransacCTRL_c'=false)&(ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_scpc_8'=ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_TestLoop); // Call operation [ChooseUniform] [] ((ransacMOD_ransacCTRL_stm_ref0_scpc_8=ransacMOD_ransacCTRL_stm_ref0_determineInliners_entering))&((ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_scpc_8=ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_INACTIVE_10)) -> (ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_scpc_8'=ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_i0)&(ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_n'=N); // The transition [sp1_5] from a state [startChoose] to [sp_pj_4].Step 1: trigger an exit of the state [startChoose] [RP__choose_16] ((ransacMOD_ransacCTRL_stm_ref0_lock_7=ransacMOD_ransacCTRL_stm_ref0_LOCK_FREE))&((ransacMOD_ransacCTRL_stm_ref0_scpc_8=ransacMOD_ransacCTRL_stm_ref0_startChoose)) -> (ransacMOD_ransacCTRL_stm_ref0_scpc_8'=ransacMOD_ransacCTRL_stm_ref0_sp_pj_4)&(ransacMOD_ransacCTRL_stm_ref0_lock_7'=ransacMOD_ransacCTRL_stm_ref0_sp1_5); // Call operation [ChooseUniform] [] ((ransacMOD_ransacCTRL_stm_ref0_scpc_8=Action_23))&((ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_scpc_8=ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_INACTIVE_10)) -> (ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_n'=N)&(ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_scpc_8'=ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_i0); // Step 4/2: exit command of the state [badFit] [] ((ransacMOD_ransacCTRL_stm_ref0_scpc_8=ransacMOD_ransacCTRL_stm_ref0_badFit))&((ransacMOD_ransacCTRL_stm_ref0_exit_9=Exit_Sub_ACT)) -> (ransacMOD_ransacCTRL_stm_ref0_exit_9'=Exit_Sub_EXITED); // The transition [t10] from a state [determineInliners] to [p1].Step 1: trigger an exit of the state [determineInliners] [] ((ransacMOD_ransacCTRL_stm_ref0_lock_7=ransacMOD_ransacCTRL_stm_ref0_LOCK_FREE))&(((ransacMOD_ransacCTRL_stm_ref0_index0!=ransacMOD_ransacCTRL_stm_ref0_index1))&((ransacMOD_ransacCTRL_stm_ref0_scpc_8=ransacMOD_ransacCTRL_stm_ref0_determineInliners))) -> (ransacMOD_ransacCTRL_stm_ref0_lock_7'=ransacMOD_ransacCTRL_stm_ref0_t10)&(ransacMOD_ransacCTRL_stm_ref0_scpc_8'=ransacMOD_ransacCTRL_stm_ref0_p1); // Step 4/2: exit command of the state [index0In] [] ((ransacMOD_ransacCTRL_stm_ref0_scpc_8=ransacMOD_ransacCTRL_stm_ref0_index0In))&((ransacMOD_ransacCTRL_stm_ref0_exit_9=Exit_Sub_ACT)) -> (ransacMOD_ransacCTRL_stm_ref0_exit_9'=Exit_Sub_EXITED); [] (ransacMOD_ransacCTRL_stm_ref0_scpc_8=Action_21) -> (ransacMOD_ransacCTRL_stm_ref0_lock_7'=ransacMOD_ransacCTRL_stm_ref0_LOCK_FREE)&(ransacMOD_ransacCTRL_stm_ref0_index1'=ransacMOD_ransacCTRL_i)&(ransacMOD_ransacCTRL_stm_ref0_scpc_8'=ransacMOD_ransacCTRL_stm_ref0_determineInliners); [] (ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_scpc_8=Action_20) -> (ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_lock_7'=ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_LOCK_FREE)&(ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_scpc_8'=ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_TestLoop)&(ransacMOD_ransacCTRL_i'=(ransacMOD_ransacCTRL_i (ransacMOD_ransacCTRL_stm_ref0_exit_9'=Exit_Sub_EXITED); // Wait for operation [ChooseUniform] to exit. [] ((ransacMOD_ransacCTRL_stm_ref0_scpc_8=ransacMOD_ransacCTRL_stm_ref0_determineInliners_entering))&((ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_scpc_8=ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_TERMINATED_11)) -> (ransacMOD_ransacCTRL_stm_ref0_scpc_8'=Action_21)&(ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_scpc_8'=ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_INACTIVE_10); // Step 4/2: exit command of the state [TestLoop] [] ((ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_scpc_8=ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_TestLoop))&((ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_exit_9=Exit_Sub_ACT)) -> (ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_exit_9'=Exit_Sub_EXITED); // Step 4/2: exit command of the state [loop_1] [] ((ransacMOD_ransacCTRL_stm_ref0_scpc_8=ransacMOD_ransacCTRL_stm_ref0_loop_1))&((ransacMOD_ransacCTRL_stm_ref0_exit_9=Exit_Sub_ACT)) -> (ransacMOD_ransacCTRL_stm_ref0_exit_9'=Exit_Sub_EXITED); // The transition [t4] from [i0] to [startChoose]. [] (ransacMOD_ransacCTRL_stm_ref0_scpc_8=ransacMOD_ransacCTRL_stm_ref0_i0) -> (ransacMOD_ransacCTRL_stm_ref0_scpc_8'=ransacMOD_ransacCTRL_stm_ref0_startChoose)&(ransacMOD_ransacCTRL_stm_ref0_lock_7'=ransacMOD_ransacCTRL_stm_ref0_LOCK_FREE); // Wait for operation [ChooseUniform] to exit. [] ((ransacMOD_ransacCTRL_stm_ref0_scpc_8=Action_23))&((ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_scpc_8=ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_TERMINATED_11)) -> (ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_scpc_8'=ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_INACTIVE_10)&(ransacMOD_ransacCTRL_stm_ref0_scpc_8'=Action_22); [] (ransacMOD_ransacCTRL_stm_ref0_scpc_8=Action_22) -> (ransacMOD_ransacCTRL_stm_ref0_scpc_8'=ransacMOD_ransacCTRL_stm_ref0_determineInliners_entering)&(ransacMOD_ransacCTRL_stm_ref0_index0'=ransacMOD_ransacCTRL_i); endmodule // For the robotic platform [ransacRP] module ransacMOD_ransacRP [RP__choose_16] true -> true; endmodule // Renames of RoboChart elements (automatically generated and used by the assertion language and don't delete) // renames of the variable [ransacMOD::ransacCTRL::c] to [ransacMOD_ransacCTRL_c] // renames of the variable [ransacMOD::ransacCTRL::i] to [ransacMOD_ransacCTRL_i] // renames of the STM [ransacMOD::ransacCTRL::stm_ref0] to [ransacMOD_ransacCTRL_stm_ref0] // renames of the event [ransacMOD::ransacCTRL::stm_ref0::choose::IN] to [RP__choose_16] // renames of the variable [ransacMOD::ransacCTRL::stm_ref0::index0] to [ransacMOD_ransacCTRL_stm_ref0_index0] // renames of the variable [ransacMOD::ransacCTRL::stm_ref0::index1] to [ransacMOD_ransacCTRL_stm_ref0_index1] // renames of the node [ransacMOD::ransacCTRL::stm_ref0::ChooseUniform::p0] to [ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_p0] // renames of the node [ransacMOD::ransacCTRL::stm_ref0::ChooseUniform::TestLoop] to [ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_TestLoop] // renames of the node [ransacMOD::ransacCTRL::stm_ref0::ChooseUniform::i0] to [ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_i0] // renames of the node [ransacMOD::ransacCTRL::stm_ref0::ChooseUniform::f0] to [ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_f0] // renames of the transition [ransacMOD::ransacCTRL::stm_ref0::ChooseUniform::t2] to [ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_t2] // renames of the transition [ransacMOD::ransacCTRL::stm_ref0::ChooseUniform::t3] to [ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_t3] // renames of the transition [ransacMOD::ransacCTRL::stm_ref0::ChooseUniform::t1] to [ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_t1] // renames of the transition [ransacMOD::ransacCTRL::stm_ref0::ChooseUniform::t4] to [ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_t4] // renames of the transition [ransacMOD::ransacCTRL::stm_ref0::ChooseUniform::t0] to [ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_t0] // renames of the variable [ransacMOD::ransacCTRL::stm_ref0::ChooseUniform::exit_9] to [ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_exit_9] // renames of the variable [ransacMOD::ransacCTRL::stm_ref0::ChooseUniform::scpc_8] to [ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_scpc_8] // renames of the variable [ransacMOD::ransacCTRL::stm_ref0::ChooseUniform::lock_7] to [ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_lock_7] // renames of the operation [ransacMOD::ransacCTRL::stm_ref0::ChooseUniform] to [ransacMOD_ransacCTRL_stm_ref0_ChooseUniform] // renames of the operation parameter [ransacMOD::ransacCTRL::stm_ref0::ChooseUniform::n] to a varaible [ransacMOD_ransacCTRL_stm_ref0_ChooseUniform_n] // renames of the node [ransacMOD::ransacCTRL::stm_ref0::sp_pj_4] to [ransacMOD_ransacCTRL_stm_ref0_sp_pj_4] // renames of the node [ransacMOD::ransacCTRL::stm_ref0::i0] to [ransacMOD_ransacCTRL_stm_ref0_i0] // renames of the node [ransacMOD::ransacCTRL::stm_ref0::p1] to [ransacMOD_ransacCTRL_stm_ref0_p1] // renames of the node [ransacMOD::ransacCTRL::stm_ref0::determineInliners] to [ransacMOD_ransacCTRL_stm_ref0_determineInliners] // renames of the node [ransacMOD::ransacCTRL::stm_ref0::startChoose] to [ransacMOD_ransacCTRL_stm_ref0_startChoose] // renames of the node [ransacMOD::ransacCTRL::stm_ref0::index0In] to [ransacMOD_ransacCTRL_stm_ref0_index0In] // renames of the node [ransacMOD::ransacCTRL::stm_ref0::loop_1] to [ransacMOD_ransacCTRL_stm_ref0_loop_1] // renames of the node [ransacMOD::ransacCTRL::stm_ref0::p2] to [ransacMOD_ransacCTRL_stm_ref0_p2] // renames of the node [ransacMOD::ransacCTRL::stm_ref0::badFit] to [ransacMOD_ransacCTRL_stm_ref0_badFit] // renames of the node [ransacMOD::ransacCTRL::stm_ref0::goodFit] to [ransacMOD_ransacCTRL_stm_ref0_goodFit] // renames of the transition [ransacMOD::ransacCTRL::stm_ref0::t16] to [ransacMOD_ransacCTRL_stm_ref0_t16] // renames of the transition [ransacMOD::ransacCTRL::stm_ref0::to_loop_3] to [ransacMOD_ransacCTRL_stm_ref0_to_loop_3] // renames of the transition [ransacMOD::ransacCTRL::stm_ref0::t9] to [ransacMOD_ransacCTRL_stm_ref0_t9] // renames of the transition [ransacMOD::ransacCTRL::stm_ref0::sp1_5] to [ransacMOD_ransacCTRL_stm_ref0_sp1_5] // renames of the transition [ransacMOD::ransacCTRL::stm_ref0::t8] to [ransacMOD_ransacCTRL_stm_ref0_t8] // renames of the transition [ransacMOD::ransacCTRL::stm_ref0::t12] to [ransacMOD_ransacCTRL_stm_ref0_t12] // renames of the transition [ransacMOD::ransacCTRL::stm_ref0::t14] to [ransacMOD_ransacCTRL_stm_ref0_t14] // renames of the transition [ransacMOD::ransacCTRL::stm_ref0::t4] to [ransacMOD_ransacCTRL_stm_ref0_t4] // renames of the transition [ransacMOD::ransacCTRL::stm_ref0::t11] to [ransacMOD_ransacCTRL_stm_ref0_t11] // renames of the transition [ransacMOD::ransacCTRL::stm_ref0::t10] to [ransacMOD_ransacCTRL_stm_ref0_t10] // renames of the transition [ransacMOD::ransacCTRL::stm_ref0::loop_self_2] to [ransacMOD_ransacCTRL_stm_ref0_loop_self_2] // renames of the transition [ransacMOD::ransacCTRL::stm_ref0::t13] to [ransacMOD_ransacCTRL_stm_ref0_t13] // renames of the transition [ransacMOD::ransacCTRL::stm_ref0::sp2_6] to [ransacMOD_ransacCTRL_stm_ref0_sp2_6] // renames of the variable [ransacMOD::ransacCTRL::stm_ref0::exit_9] to [ransacMOD_ransacCTRL_stm_ref0_exit_9] // renames of the variable [ransacMOD::ransacCTRL::stm_ref0::scpc_8] to [ransacMOD_ransacCTRL_stm_ref0_scpc_8] // renames of the variable [ransacMOD::ransacCTRL::stm_ref0::lock_7] to [ransacMOD_ransacCTRL_stm_ref0_lock_7] // renames of the event [ransacMOD::ransacRP::choose::OUT] to [RP__choose_16] // renames of the variable [ransacMOD::ransacRP::q] to [q] // renames of the constant [q] to [q] // renames of the variable [ransacMOD::ransacRP::N] to [N] // renames of the constant [N] to [N]