// This model is automatically generated from the RoboChart model // by the translator (translate2prism v20210223) plugin in RoboTool // on 2021-03-30 10:12:20 // // All changes made will be lost after regeneration. // PRISM Output dtmc const int LRH_lt = (0); const int LRH_rt = (1); const int LRH_vt = (2); const int UPH_ut = (0); const int UPH_dt = (1); const int UPH_ht = (2); const int Action_58 = (2); const int Action_59 = (11); const int Action_60 = (12); const int random_walker_recorderC_stm_ref0_INACTIVE_10 = (0); const int random_walker_recorderC_stm_ref0_LOCK_FREE = (0); const int random_walker_recorderC_stm_ref0_REC = (6); const int random_walker_recorderC_stm_ref0_RECx = (9); const int random_walker_recorderC_stm_ref0_RECx2 = (4); const int random_walker_recorderC_stm_ref0_RECy = (7); const int random_walker_recorderC_stm_ref0_RECy_entering = (1); const int random_walker_recorderC_stm_ref0_RECy2 = (8); const int random_walker_recorderC_stm_ref0_STOP = (3); const int random_walker_recorderC_stm_ref0_TERMINATED_11 = (13); const int random_walker_recorderC_stm_ref0_i0 = (5); const int random_walker_recorderC_stm_ref0_loop_9 = (10); const int random_walker_recorderC_stm_ref0_loop_self_10 = (9); const int random_walker_recorderC_stm_ref0_t0 = (3); const int random_walker_recorderC_stm_ref0_t1 = (6); const int random_walker_recorderC_stm_ref0_t2 = (7); const int random_walker_recorderC_stm_ref0_t4 = (4); const int random_walker_recorderC_stm_ref0_t5 = (8); const int random_walker_recorderC_stm_ref0_t6 = (5); const int random_walker_recorderC_stm_ref0_t7 = (2); const int random_walker_recorderC_stm_ref0_to_loop_11 = (1); const int Action_21 = (2); const int Action_22 = (11); const int Action_23 = (12); const int Action_24 = (13); const int Action_25 = (14); const int Action_26 = (15); const int Action_27 = (16); const int Action_28 = (17); const int Action_29 = (18); const int Action_30 = (19); const int Action_31 = (20); const int Action_32 = (21); const int Action_33 = (22); const int Action_34 = (23); const int Action_35 = (24); const int Action_36 = (25); const int Action_37 = (26); const int Action_38 = (27); const int Action_39 = (28); const int Action_40 = (29); const int Action_41 = (30); const int Action_42 = (31); const int random_walker_up_downC_stm_ref0_INACTIVE_10 = (0); const int random_walker_up_downC_stm_ref0_LOCK_FREE = (0); const int random_walker_up_downC_stm_ref0_LR = (10); const int random_walker_up_downC_stm_ref0_LR_entering = (1); const int random_walker_up_downC_stm_ref0_TERMINATED_11 = (32); const int random_walker_up_downC_stm_ref0_i0 = (5); const int random_walker_up_downC_stm_ref0_j0 = (3); const int random_walker_up_downC_stm_ref0_j1 = (9); const int random_walker_up_downC_stm_ref0_p0 = (7); const int random_walker_up_downC_stm_ref0_p1 = (4); const int random_walker_up_downC_stm_ref0_p2 = (6); const int random_walker_up_downC_stm_ref0_p3 = (8); const int random_walker_up_downC_stm_ref0_t0 = (1); const int random_walker_up_downC_stm_ref0_t1 = (4); const int random_walker_up_downC_stm_ref0_t11 = (8); const int random_walker_up_downC_stm_ref0_t14 = (2); const int random_walker_up_downC_stm_ref0_t17 = (5); const int random_walker_up_downC_stm_ref0_t3 = (3); const int random_walker_up_downC_stm_ref0_t6 = (7); const int random_walker_up_downC_stm_ref0_t8 = (6); const int Action_43 = (2); const int Action_44 = (11); const int Action_45 = (12); const int Action_46 = (13); const int Action_47 = (14); const int Action_48 = (15); const int Action_49 = (16); const int Action_50 = (17); const int Action_51 = (18); const int Action_52 = (19); const int Action_53 = (20); const int Action_54 = (21); const int Action_55 = (22); const int Action_56 = (23); const int Action_57 = (24); const int random_walker_left_rightC_stm_ref0_INACTIVE_10 = (0); const int random_walker_left_rightC_stm_ref0_LOCK_FREE = (0); const int random_walker_left_rightC_stm_ref0_LR = (4); const int random_walker_left_rightC_stm_ref0_LR_entering = (1); const int random_walker_left_rightC_stm_ref0_TERMINATED_11 = (25); const int random_walker_left_rightC_stm_ref0_i0 = (6); const int random_walker_left_rightC_stm_ref0_p0 = (7); const int random_walker_left_rightC_stm_ref0_p1 = (3); const int random_walker_left_rightC_stm_ref0_p2 = (5); const int random_walker_left_rightC_stm_ref0_p3 = (9); const int random_walker_left_rightC_stm_ref0_sp1_4 = (5); const int random_walker_left_rightC_stm_ref0_sp1_7 = (4); const int random_walker_left_rightC_stm_ref0_sp_pj_3 = (10); const int random_walker_left_rightC_stm_ref0_sp_pj_6 = (8); const int random_walker_left_rightC_stm_ref0_t0 = (8); const int random_walker_left_rightC_stm_ref0_t11 = (6); const int random_walker_left_rightC_stm_ref0_t14 = (7); const int random_walker_left_rightC_stm_ref0_t17 = (3); const int random_walker_left_rightC_stm_ref0_t3 = (1); const int random_walker_left_rightC_stm_ref0_t8 = (2); const int M; const int MAX; const int N; const int Exit_ACT_Trans = (2); const int Exit_Sub_EXITED = (6); const int Exit_Sub_ACT = (4); const int Exit_NONE = (0); const int Exit_ACT_Parent = (1); const int Exit_EXITED = (3); const int Exit_Sub_ACT_Waiting = (5); global y : [0..4]; global steps : [-1..100]; global x : [0..4]; // For the robotic platform [RW_RP] module random_walker_RW_RP endmodule // For the state machine [up_down] in the controller [up_downC] module random_walker_up_downC_stm_ref0 random_walker_up_downC_stm_ref0_lock_7 : [0..8] init random_walker_up_downC_stm_ref0_LOCK_FREE; random_walker_up_downC_stm_ref0_uph : [0..2]; random_walker_up_downC_stm_ref0_scpc_8 : [0..31] init random_walker_up_downC_stm_ref0_i0; random_walker_up_downC_stm_ref0_exit_9 : [0..6] init Exit_NONE; [rcrd_end_20] (random_walker_up_downC_stm_ref0_scpc_8=Action_21) -> (random_walker_up_downC_stm_ref0_scpc_8'=random_walker_up_downC_stm_ref0_LR)&(random_walker_up_downC_stm_ref0_lock_7'=random_walker_up_downC_stm_ref0_LOCK_FREE); // The transition [t7] from a junction [j1] to [LR]. [] (random_walker_up_downC_stm_ref0_scpc_8=random_walker_up_downC_stm_ref0_j1) -> (random_walker_up_downC_stm_ref0_scpc_8'=Action_35); [] (random_walker_up_downC_stm_ref0_scpc_8=Action_27) -> (random_walker_up_downC_stm_ref0_scpc_8'=Action_26)&(y'=(1)); // The transition [t1] from a state [LR] to [j0].Step 1: trigger an exit of the state [LR] [] ((random_walker_up_downC_stm_ref0_lock_7=random_walker_up_downC_stm_ref0_LOCK_FREE))&(((random_walker_up_downC_stm_ref0_scpc_8=random_walker_up_downC_stm_ref0_LR))&((((random_walker_up_downC_stm_ref0_uph=UPH_dt))&(y (random_walker_up_downC_stm_ref0_scpc_8'=Action_38)&(random_walker_up_downC_stm_ref0_lock_7'=random_walker_up_downC_stm_ref0_t1); [] (random_walker_up_downC_stm_ref0_scpc_8=Action_25) -> (random_walker_up_downC_stm_ref0_scpc_8'=Action_24)&(y'=(y (random_walker_up_downC_stm_ref0_uph'=UPH_ht)&(random_walker_up_downC_stm_ref0_scpc_8'=random_walker_up_downC_stm_ref0_LR_entering); [move_19] (random_walker_up_downC_stm_ref0_scpc_8=Action_39) -> (random_walker_up_downC_stm_ref0_scpc_8'=random_walker_up_downC_stm_ref0_LR_entering); [] (random_walker_up_downC_stm_ref0_scpc_8=Action_23) -> (random_walker_up_downC_stm_ref0_uph'=UPH_ht)&(random_walker_up_downC_stm_ref0_scpc_8'=random_walker_up_downC_stm_ref0_LR_entering); [move_19] (random_walker_up_downC_stm_ref0_scpc_8=Action_40) -> (random_walker_up_downC_stm_ref0_scpc_8'=random_walker_up_downC_stm_ref0_p1); [] (random_walker_up_downC_stm_ref0_scpc_8=Action_22) -> (random_walker_up_downC_stm_ref0_scpc_8'=random_walker_up_downC_stm_ref0_LR_entering)&(y'=(y (random_walker_up_downC_stm_ref0_scpc_8'=random_walker_up_downC_stm_ref0_p3); // The transition [t8] from a state [LR] to [p1].Step 1: trigger an exit of the state [LR] [] ((random_walker_up_downC_stm_ref0_lock_7=random_walker_up_downC_stm_ref0_LOCK_FREE))&(((random_walker_up_downC_stm_ref0_scpc_8=random_walker_up_downC_stm_ref0_LR))&((((random_walker_up_downC_stm_ref0_uph=UPH_ut))&((y=(1))))&(steps (random_walker_up_downC_stm_ref0_scpc_8'=Action_40)&(random_walker_up_downC_stm_ref0_lock_7'=random_walker_up_downC_stm_ref0_t8); [] (random_walker_up_downC_stm_ref0_scpc_8=Action_34) -> (random_walker_up_downC_stm_ref0_scpc_8'=Action_33)&(y'=(y (0.5):(random_walker_up_downC_stm_ref0_scpc_8'=Action_32) + (0.5):(random_walker_up_downC_stm_ref0_scpc_8'=Action_31); [move_19] (random_walker_up_downC_stm_ref0_scpc_8=Action_41) -> (random_walker_up_downC_stm_ref0_scpc_8'=random_walker_up_downC_stm_ref0_j1); [] (random_walker_up_downC_stm_ref0_scpc_8=Action_24) -> (random_walker_up_downC_stm_ref0_uph'=UPH_dt)&(random_walker_up_downC_stm_ref0_scpc_8'=random_walker_up_downC_stm_ref0_LR_entering); // The transition [t0] from [i0] to [LR]. [] (random_walker_up_downC_stm_ref0_scpc_8=random_walker_up_downC_stm_ref0_i0) -> (random_walker_up_downC_stm_ref0_scpc_8'=Action_27)&(random_walker_up_downC_stm_ref0_lock_7'=random_walker_up_downC_stm_ref0_t0); [] (random_walker_up_downC_stm_ref0_scpc_8=Action_30) -> (random_walker_up_downC_stm_ref0_uph'=UPH_ut)&(random_walker_up_downC_stm_ref0_scpc_8'=random_walker_up_downC_stm_ref0_LR_entering); // From the probabilistic junction [p3] [] (random_walker_up_downC_stm_ref0_scpc_8=random_walker_up_downC_stm_ref0_p3) -> (0.5):(random_walker_up_downC_stm_ref0_scpc_8'=random_walker_up_downC_stm_ref0_LR_entering) + (0.5):(random_walker_up_downC_stm_ref0_scpc_8'=Action_34); [] (random_walker_up_downC_stm_ref0_scpc_8=Action_28) -> (random_walker_up_downC_stm_ref0_scpc_8'=random_walker_up_downC_stm_ref0_LR_entering)&(random_walker_up_downC_stm_ref0_uph'=UPH_ut); [move_19] (random_walker_up_downC_stm_ref0_scpc_8=Action_37) -> (random_walker_up_downC_stm_ref0_scpc_8'=random_walker_up_downC_stm_ref0_p0); [] (random_walker_up_downC_stm_ref0_scpc_8=Action_31) -> (random_walker_up_downC_stm_ref0_scpc_8'=Action_30)&(y'=(y>(1)?(y-(1)):y)); [rcrd_start_17] (random_walker_up_downC_stm_ref0_scpc_8=random_walker_up_downC_stm_ref0_LR_entering) -> (random_walker_up_downC_stm_ref0_scpc_8'=Action_21); [] (random_walker_up_downC_stm_ref0_scpc_8=Action_33) -> (random_walker_up_downC_stm_ref0_scpc_8'=random_walker_up_downC_stm_ref0_LR_entering)&(random_walker_up_downC_stm_ref0_uph'=UPH_dt); // Step 4/2: exit command of the state [LR] [] ((random_walker_up_downC_stm_ref0_scpc_8=random_walker_up_downC_stm_ref0_LR))&((random_walker_up_downC_stm_ref0_exit_9=Exit_Sub_ACT)) -> (random_walker_up_downC_stm_ref0_exit_9'=Exit_Sub_EXITED); // The transition [t14] from a state [LR] to [p3].Step 1: trigger an exit of the state [LR] [] ((random_walker_up_downC_stm_ref0_scpc_8=random_walker_up_downC_stm_ref0_LR))&(((((random_walker_up_downC_stm_ref0_uph=UPH_ht))&((y=(1))))&(steps (random_walker_up_downC_stm_ref0_lock_7'=random_walker_up_downC_stm_ref0_t14)&(random_walker_up_downC_stm_ref0_scpc_8'=Action_36); [] (random_walker_up_downC_stm_ref0_scpc_8=Action_32) -> (random_walker_up_downC_stm_ref0_scpc_8'=random_walker_up_downC_stm_ref0_LR_entering)&(random_walker_up_downC_stm_ref0_uph'=UPH_ht); // The transition [t17] from a state [LR] to [LR].Step 1: trigger an exit of the state [LR] [] ((random_walker_up_downC_stm_ref0_scpc_8=random_walker_up_downC_stm_ref0_LR))&(((random_walker_up_downC_stm_ref0_lock_7=random_walker_up_downC_stm_ref0_LOCK_FREE))&((steps=MAX))) -> (random_walker_up_downC_stm_ref0_scpc_8'=Action_39)&(random_walker_up_downC_stm_ref0_lock_7'=random_walker_up_downC_stm_ref0_t17); // From the probabilistic junction [p2] [] (random_walker_up_downC_stm_ref0_scpc_8=random_walker_up_downC_stm_ref0_p2) -> (0.5):(random_walker_up_downC_stm_ref0_scpc_8'=Action_29) + (0.5):(random_walker_up_downC_stm_ref0_scpc_8'=random_walker_up_downC_stm_ref0_LR_entering); [] (random_walker_up_downC_stm_ref0_scpc_8=Action_35) -> (y'=(y>(1)?(y-(1)):y))&(random_walker_up_downC_stm_ref0_scpc_8'=random_walker_up_downC_stm_ref0_LR_entering); // The transition [t6] from a state [LR] to [j1].Step 1: trigger an exit of the state [LR] [] ((((random_walker_up_downC_stm_ref0_uph=UPH_ut))&(y>(1)))&(steps (random_walker_up_downC_stm_ref0_scpc_8'=Action_41)&(random_walker_up_downC_stm_ref0_lock_7'=random_walker_up_downC_stm_ref0_t6); [] (random_walker_up_downC_stm_ref0_scpc_8=Action_29) -> (random_walker_up_downC_stm_ref0_scpc_8'=Action_28)&(y'=(y>(1)?(y-(1)):y)); [move_19] (random_walker_up_downC_stm_ref0_scpc_8=Action_42) -> (random_walker_up_downC_stm_ref0_scpc_8'=random_walker_up_downC_stm_ref0_p2); // The transition [t11] from a state [LR] to [p2].Step 1: trigger an exit of the state [LR] [] ((random_walker_up_downC_stm_ref0_scpc_8=random_walker_up_downC_stm_ref0_LR))&(((random_walker_up_downC_stm_ref0_lock_7=random_walker_up_downC_stm_ref0_LOCK_FREE))&((((random_walker_up_downC_stm_ref0_uph=UPH_ht))&((y=N)))&(steps (random_walker_up_downC_stm_ref0_lock_7'=random_walker_up_downC_stm_ref0_t11)&(random_walker_up_downC_stm_ref0_scpc_8'=Action_42); [move_19] (random_walker_up_downC_stm_ref0_scpc_8=Action_38) -> (random_walker_up_downC_stm_ref0_scpc_8'=random_walker_up_downC_stm_ref0_j0); // The transition [t3] from a state [LR] to [p0].Step 1: trigger an exit of the state [LR] [] ((random_walker_up_downC_stm_ref0_lock_7=random_walker_up_downC_stm_ref0_LOCK_FREE))&(((((random_walker_up_downC_stm_ref0_uph=UPH_dt))&((y=N)))&(steps (random_walker_up_downC_stm_ref0_lock_7'=random_walker_up_downC_stm_ref0_t3)&(random_walker_up_downC_stm_ref0_scpc_8'=Action_37); // The transition [t2] from a junction [j0] to [LR]. [] (random_walker_up_downC_stm_ref0_scpc_8=random_walker_up_downC_stm_ref0_j0) -> (random_walker_up_downC_stm_ref0_scpc_8'=Action_22); // From the probabilistic junction [p1] [] (random_walker_up_downC_stm_ref0_scpc_8=random_walker_up_downC_stm_ref0_p1) -> (0.5):(random_walker_up_downC_stm_ref0_scpc_8'=Action_23) + (0.5):(random_walker_up_downC_stm_ref0_scpc_8'=Action_25); endmodule // For the state machine [recorder] in the controller [recorderC] module random_walker_recorderC_stm_ref0 random_walker_recorderC_stm_ref0_v_3_1 : bool; random_walker_recorderC_stm_ref0_v_1_1 : bool; random_walker_recorderC_stm_ref0_v_1_2 : bool; random_walker_recorderC_stm_ref0_v_2_1 : bool; random_walker_recorderC_stm_ref0_v_3_2 : bool; random_walker_recorderC_stm_ref0_v_3_3 : bool; random_walker_recorderC_stm_ref0_v_2_2 : bool; random_walker_recorderC_stm_ref0_scpc_8 : [0..12] init random_walker_recorderC_stm_ref0_i0; random_walker_recorderC_stm_ref0_v_1_3 : bool; random_walker_recorderC_stm_ref0_lock_7 : [0..9] init random_walker_recorderC_stm_ref0_LOCK_FREE; random_walker_recorderC_stm_ref0_v_2_3 : bool; random_walker_recorderC_stm_ref0_exit_9 : [0..6] init Exit_NONE; [] ((random_walker_recorderC_stm_ref0_scpc_8=Action_58))&((((y-(1))=(2)))&(((x-(1))=(2)))) -> (random_walker_recorderC_stm_ref0_scpc_8'=random_walker_recorderC_stm_ref0_RECy)&(random_walker_recorderC_stm_ref0_lock_7'=random_walker_recorderC_stm_ref0_LOCK_FREE)&(random_walker_recorderC_stm_ref0_v_3_3'=true); // Step 4/2: exit command of the state [RECy2] [] ((random_walker_recorderC_stm_ref0_scpc_8=random_walker_recorderC_stm_ref0_RECy2))&((random_walker_recorderC_stm_ref0_exit_9=Exit_Sub_ACT)) -> (random_walker_recorderC_stm_ref0_exit_9'=Exit_Sub_EXITED); // Step 4/2: exit command of the state [RECx] [] ((random_walker_recorderC_stm_ref0_scpc_8=random_walker_recorderC_stm_ref0_RECx))&((random_walker_recorderC_stm_ref0_exit_9=Exit_Sub_ACT)) -> (random_walker_recorderC_stm_ref0_exit_9'=Exit_Sub_EXITED); // The transition [to_loop_11] from a state [STOP] to [loop_9].Step 1: trigger an exit of the state [STOP] [] ((random_walker_recorderC_stm_ref0_lock_7=random_walker_recorderC_stm_ref0_LOCK_FREE))&((random_walker_recorderC_stm_ref0_scpc_8=random_walker_recorderC_stm_ref0_STOP)) -> (random_walker_recorderC_stm_ref0_scpc_8'=random_walker_recorderC_stm_ref0_loop_9)&(random_walker_recorderC_stm_ref0_lock_7'=random_walker_recorderC_stm_ref0_LOCK_FREE); [] ((random_walker_recorderC_stm_ref0_scpc_8=Action_58))&((((y-(1))=(2)))&(((x-(1))=(0)))) -> (random_walker_recorderC_stm_ref0_scpc_8'=random_walker_recorderC_stm_ref0_RECy)&(random_walker_recorderC_stm_ref0_v_3_1'=true)&(random_walker_recorderC_stm_ref0_lock_7'=random_walker_recorderC_stm_ref0_LOCK_FREE); [] (random_walker_recorderC_stm_ref0_scpc_8=random_walker_recorderC_stm_ref0_RECy_entering) -> (steps'=(steps (random_walker_recorderC_stm_ref0_lock_7'=random_walker_recorderC_stm_ref0_LOCK_FREE)&(random_walker_recorderC_stm_ref0_scpc_8'=random_walker_recorderC_stm_ref0_RECy)&(random_walker_recorderC_stm_ref0_v_3_2'=true); // Step 4/2: exit command of the state [loop_9] [] ((random_walker_recorderC_stm_ref0_scpc_8=random_walker_recorderC_stm_ref0_loop_9))&((random_walker_recorderC_stm_ref0_exit_9=Exit_Sub_ACT)) -> (random_walker_recorderC_stm_ref0_exit_9'=Exit_Sub_EXITED); // The transition [t0] from [i0] to [REC]. [] (random_walker_recorderC_stm_ref0_scpc_8=random_walker_recorderC_stm_ref0_i0) -> (random_walker_recorderC_stm_ref0_scpc_8'=Action_60)&(random_walker_recorderC_stm_ref0_lock_7'=random_walker_recorderC_stm_ref0_t0); [] ((random_walker_recorderC_stm_ref0_scpc_8=Action_58))&((((y-(1))=(1)))&(((x-(1))=(0)))) -> (random_walker_recorderC_stm_ref0_v_2_1'=true)&(random_walker_recorderC_stm_ref0_scpc_8'=random_walker_recorderC_stm_ref0_RECy)&(random_walker_recorderC_stm_ref0_lock_7'=random_walker_recorderC_stm_ref0_LOCK_FREE); // The transition [t6] from a state [RECy] to [RECx2].Step 1: trigger an exit of the state [RECy] [rcrd_end_16] ((random_walker_recorderC_stm_ref0_lock_7=random_walker_recorderC_stm_ref0_LOCK_FREE))&((random_walker_recorderC_stm_ref0_scpc_8=random_walker_recorderC_stm_ref0_RECy)) -> (random_walker_recorderC_stm_ref0_lock_7'=random_walker_recorderC_stm_ref0_LOCK_FREE)&(random_walker_recorderC_stm_ref0_scpc_8'=random_walker_recorderC_stm_ref0_RECx2); [] ((random_walker_recorderC_stm_ref0_scpc_8=Action_58))&((((y-(1))=(0)))&(((x-(1))=(2)))) -> (random_walker_recorderC_stm_ref0_v_1_3'=true)&(random_walker_recorderC_stm_ref0_scpc_8'=random_walker_recorderC_stm_ref0_RECy)&(random_walker_recorderC_stm_ref0_lock_7'=random_walker_recorderC_stm_ref0_LOCK_FREE); // The transition [t4] from a state [REC] to [RECx].Step 1: trigger an exit of the state [REC] [rcrd_start_18] ((random_walker_recorderC_stm_ref0_lock_7=random_walker_recorderC_stm_ref0_LOCK_FREE))&((random_walker_recorderC_stm_ref0_scpc_8=random_walker_recorderC_stm_ref0_REC)) -> (random_walker_recorderC_stm_ref0_scpc_8'=random_walker_recorderC_stm_ref0_RECx)&(random_walker_recorderC_stm_ref0_lock_7'=random_walker_recorderC_stm_ref0_LOCK_FREE); [] ((random_walker_recorderC_stm_ref0_scpc_8=Action_58))&((((y-(1))=(0)))&(((x-(1))=(0)))) -> (random_walker_recorderC_stm_ref0_v_1_1'=true)&(random_walker_recorderC_stm_ref0_scpc_8'=random_walker_recorderC_stm_ref0_RECy)&(random_walker_recorderC_stm_ref0_lock_7'=random_walker_recorderC_stm_ref0_LOCK_FREE); // The transition [t7] from a state [RECx2] to [RECy2].Step 1: trigger an exit of the state [RECx2] [rcrd_end_20] ((random_walker_recorderC_stm_ref0_scpc_8=random_walker_recorderC_stm_ref0_RECx2))&((random_walker_recorderC_stm_ref0_lock_7=random_walker_recorderC_stm_ref0_LOCK_FREE)) -> (random_walker_recorderC_stm_ref0_lock_7'=random_walker_recorderC_stm_ref0_LOCK_FREE)&(random_walker_recorderC_stm_ref0_scpc_8'=random_walker_recorderC_stm_ref0_RECy2); // Step 4/2: exit command of the state [STOP] [] ((random_walker_recorderC_stm_ref0_scpc_8=random_walker_recorderC_stm_ref0_STOP))&((random_walker_recorderC_stm_ref0_exit_9=Exit_Sub_ACT)) -> (random_walker_recorderC_stm_ref0_exit_9'=Exit_Sub_EXITED); // The transition [loop_self_10] from a state [loop_9] to [loop_9].Step 1: trigger an exit of the state [loop_9] [] ((random_walker_recorderC_stm_ref0_lock_7=random_walker_recorderC_stm_ref0_LOCK_FREE))&((random_walker_recorderC_stm_ref0_scpc_8=random_walker_recorderC_stm_ref0_loop_9)) -> (random_walker_recorderC_stm_ref0_lock_7'=random_walker_recorderC_stm_ref0_LOCK_FREE)&(random_walker_recorderC_stm_ref0_scpc_8'=random_walker_recorderC_stm_ref0_loop_9); // The transition [t5] from a state [RECx] to [RECy].Step 1: trigger an exit of the state [RECx] [rcrd_start_17] ((random_walker_recorderC_stm_ref0_scpc_8=random_walker_recorderC_stm_ref0_RECx))&((random_walker_recorderC_stm_ref0_lock_7=random_walker_recorderC_stm_ref0_LOCK_FREE)) -> (random_walker_recorderC_stm_ref0_lock_7'=random_walker_recorderC_stm_ref0_t5)&(random_walker_recorderC_stm_ref0_scpc_8'=random_walker_recorderC_stm_ref0_RECy_entering); // The transition [t1] from a state [RECy2] to [REC].Step 1: trigger an exit of the state [RECy2] [] (steps (random_walker_recorderC_stm_ref0_lock_7'=random_walker_recorderC_stm_ref0_LOCK_FREE)&(random_walker_recorderC_stm_ref0_scpc_8'=random_walker_recorderC_stm_ref0_REC); [] ((random_walker_recorderC_stm_ref0_scpc_8=Action_58))&((((y-(1))=(1)))&(((x-(1))=(2)))) -> (random_walker_recorderC_stm_ref0_lock_7'=random_walker_recorderC_stm_ref0_LOCK_FREE)&(random_walker_recorderC_stm_ref0_v_2_3'=true)&(random_walker_recorderC_stm_ref0_scpc_8'=random_walker_recorderC_stm_ref0_RECy); // The transition [t2] from a state [RECy2] to [STOP].Step 1: trigger an exit of the state [RECy2] [] ((random_walker_recorderC_stm_ref0_scpc_8=random_walker_recorderC_stm_ref0_RECy2))&(((random_walker_recorderC_stm_ref0_lock_7=random_walker_recorderC_stm_ref0_LOCK_FREE))&(steps>=MAX)) -> (random_walker_recorderC_stm_ref0_scpc_8'=random_walker_recorderC_stm_ref0_STOP)&(random_walker_recorderC_stm_ref0_lock_7'=random_walker_recorderC_stm_ref0_LOCK_FREE); // Step 4/2: exit command of the state [RECy] [] ((random_walker_recorderC_stm_ref0_scpc_8=random_walker_recorderC_stm_ref0_RECy))&((random_walker_recorderC_stm_ref0_exit_9=Exit_Sub_ACT)) -> (random_walker_recorderC_stm_ref0_exit_9'=Exit_Sub_EXITED); [] (random_walker_recorderC_stm_ref0_scpc_8=Action_59) -> (random_walker_recorderC_stm_ref0_scpc_8'=random_walker_recorderC_stm_ref0_REC)&(random_walker_recorderC_stm_ref0_v_1_2'=false)&(random_walker_recorderC_stm_ref0_lock_7'=random_walker_recorderC_stm_ref0_LOCK_FREE)&(random_walker_recorderC_stm_ref0_v_1_3'=false)&(random_walker_recorderC_stm_ref0_v_3_3'=false)&(random_walker_recorderC_stm_ref0_v_1_1'=false)&(random_walker_recorderC_stm_ref0_v_2_1'=false)&(random_walker_recorderC_stm_ref0_v_2_3'=false)&(random_walker_recorderC_stm_ref0_v_3_1'=false)&(random_walker_recorderC_stm_ref0_v_3_2'=false)&(random_walker_recorderC_stm_ref0_v_2_2'=false); // Step 4/2: exit command of the state [RECx2] [] ((random_walker_recorderC_stm_ref0_scpc_8=random_walker_recorderC_stm_ref0_RECx2))&((random_walker_recorderC_stm_ref0_exit_9=Exit_Sub_ACT)) -> (random_walker_recorderC_stm_ref0_exit_9'=Exit_Sub_EXITED); [] (random_walker_recorderC_stm_ref0_scpc_8=Action_60) -> (random_walker_recorderC_stm_ref0_scpc_8'=Action_59)&(steps'=(0)); // Step 4/2: exit command of the state [REC] [] ((random_walker_recorderC_stm_ref0_scpc_8=random_walker_recorderC_stm_ref0_REC))&((random_walker_recorderC_stm_ref0_exit_9=Exit_Sub_ACT)) -> (random_walker_recorderC_stm_ref0_exit_9'=Exit_Sub_EXITED); [] ((random_walker_recorderC_stm_ref0_scpc_8=Action_58))&((((y-(1))=(0)))&(((x-(1))=(1)))) -> (random_walker_recorderC_stm_ref0_lock_7'=random_walker_recorderC_stm_ref0_LOCK_FREE)&(random_walker_recorderC_stm_ref0_scpc_8'=random_walker_recorderC_stm_ref0_RECy)&(random_walker_recorderC_stm_ref0_v_1_2'=true); [] ((random_walker_recorderC_stm_ref0_scpc_8=Action_58))&((((y-(1))=(1)))&(((x-(1))=(1)))) -> (random_walker_recorderC_stm_ref0_scpc_8'=random_walker_recorderC_stm_ref0_RECy)&(random_walker_recorderC_stm_ref0_v_2_2'=true)&(random_walker_recorderC_stm_ref0_lock_7'=random_walker_recorderC_stm_ref0_LOCK_FREE); endmodule // For the state machine [left_right] in the controller [left_rightC] module random_walker_left_rightC_stm_ref0 random_walker_left_rightC_stm_ref0_exit_9 : [0..6] init Exit_NONE; random_walker_left_rightC_stm_ref0_scpc_8 : [0..24] init random_walker_left_rightC_stm_ref0_i0; random_walker_left_rightC_stm_ref0_lock_7 : [0..8] init random_walker_left_rightC_stm_ref0_LOCK_FREE; random_walker_left_rightC_stm_ref0_lrh : [0..2]; // From the probabilistic junction [p3] [] (random_walker_left_rightC_stm_ref0_scpc_8=random_walker_left_rightC_stm_ref0_p3) -> (0.5):(random_walker_left_rightC_stm_ref0_scpc_8'=random_walker_left_rightC_stm_ref0_LR_entering) + (0.5):(random_walker_left_rightC_stm_ref0_scpc_8'=Action_56); [rcrd_start_18] (random_walker_left_rightC_stm_ref0_scpc_8=random_walker_left_rightC_stm_ref0_LR_entering) -> (random_walker_left_rightC_stm_ref0_scpc_8'=Action_43); [] (random_walker_left_rightC_stm_ref0_scpc_8=Action_45) -> (random_walker_left_rightC_stm_ref0_scpc_8'=Action_44)&(x'=(x (x'=(x>(1)?(x-(1)):x))&(random_walker_left_rightC_stm_ref0_scpc_8'=Action_47); // From the probabilistic junction [sp_pj_6] [] (random_walker_left_rightC_stm_ref0_scpc_8=random_walker_left_rightC_stm_ref0_sp_pj_6) -> (random_walker_left_rightC_stm_ref0_scpc_8'=Action_54); // From the probabilistic junction [p1] [] (random_walker_left_rightC_stm_ref0_scpc_8=random_walker_left_rightC_stm_ref0_p1) -> (0.5):(random_walker_left_rightC_stm_ref0_scpc_8'=Action_45) + (0.5):(random_walker_left_rightC_stm_ref0_scpc_8'=Action_46); // The transition [sp1_4] from a state [LR] to [sp_pj_3].Step 1: trigger an exit of the state [LR] [move_19] ((random_walker_left_rightC_stm_ref0_lock_7=random_walker_left_rightC_stm_ref0_LOCK_FREE))&(((((random_walker_left_rightC_stm_ref0_lrh=LRH_rt))&(x (random_walker_left_rightC_stm_ref0_scpc_8'=random_walker_left_rightC_stm_ref0_sp_pj_3)&(random_walker_left_rightC_stm_ref0_lock_7'=random_walker_left_rightC_stm_ref0_sp1_4); [rcrd_end_16] (random_walker_left_rightC_stm_ref0_scpc_8=Action_43) -> (random_walker_left_rightC_stm_ref0_scpc_8'=random_walker_left_rightC_stm_ref0_LR)&(random_walker_left_rightC_stm_ref0_lock_7'=random_walker_left_rightC_stm_ref0_LOCK_FREE); // The transition [t14] from a state [LR] to [p3].Step 1: trigger an exit of the state [LR] [move_19] ((random_walker_left_rightC_stm_ref0_scpc_8=random_walker_left_rightC_stm_ref0_LR))&(((random_walker_left_rightC_stm_ref0_lock_7=random_walker_left_rightC_stm_ref0_LOCK_FREE))&((((random_walker_left_rightC_stm_ref0_lrh=LRH_vt))&((x=(1))))&(steps (random_walker_left_rightC_stm_ref0_lock_7'=random_walker_left_rightC_stm_ref0_t14)&(random_walker_left_rightC_stm_ref0_scpc_8'=random_walker_left_rightC_stm_ref0_p3); [] (random_walker_left_rightC_stm_ref0_scpc_8=Action_52) -> (random_walker_left_rightC_stm_ref0_scpc_8'=random_walker_left_rightC_stm_ref0_LR_entering)&(random_walker_left_rightC_stm_ref0_lrh'=LRH_lt); [] (random_walker_left_rightC_stm_ref0_scpc_8=Action_54) -> (x'=(x>(1)?(x-(1)):x))&(random_walker_left_rightC_stm_ref0_scpc_8'=random_walker_left_rightC_stm_ref0_LR_entering); // The transition [t0] from [i0] to [LR]. [] (random_walker_left_rightC_stm_ref0_scpc_8=random_walker_left_rightC_stm_ref0_i0) -> (random_walker_left_rightC_stm_ref0_lock_7'=random_walker_left_rightC_stm_ref0_t0)&(random_walker_left_rightC_stm_ref0_scpc_8'=Action_50); [] (random_walker_left_rightC_stm_ref0_scpc_8=Action_56) -> (random_walker_left_rightC_stm_ref0_scpc_8'=Action_55)&(x'=(x (random_walker_left_rightC_stm_ref0_lrh'=LRH_lt)&(random_walker_left_rightC_stm_ref0_scpc_8'=random_walker_left_rightC_stm_ref0_LR_entering); // The transition [t11] from a state [LR] to [p2].Step 1: trigger an exit of the state [LR] [move_19] ((((random_walker_left_rightC_stm_ref0_lrh=LRH_vt))&((x=M)))&(steps (random_walker_left_rightC_stm_ref0_lock_7'=random_walker_left_rightC_stm_ref0_t11)&(random_walker_left_rightC_stm_ref0_scpc_8'=random_walker_left_rightC_stm_ref0_p2); [] (random_walker_left_rightC_stm_ref0_scpc_8=Action_53) -> (random_walker_left_rightC_stm_ref0_scpc_8'=Action_52)&(x'=(x>(1)?(x-(1)):x)); [] (random_walker_left_rightC_stm_ref0_scpc_8=Action_57) -> (x'=(x (random_walker_left_rightC_stm_ref0_scpc_8'=random_walker_left_rightC_stm_ref0_LR_entering)&(random_walker_left_rightC_stm_ref0_lrh'=LRH_vt); [] (random_walker_left_rightC_stm_ref0_scpc_8=Action_49) -> (random_walker_left_rightC_stm_ref0_lrh'=LRH_vt)&(random_walker_left_rightC_stm_ref0_scpc_8'=random_walker_left_rightC_stm_ref0_LR_entering); // Step 4/2: exit command of the state [LR] [] ((random_walker_left_rightC_stm_ref0_scpc_8=random_walker_left_rightC_stm_ref0_LR))&((random_walker_left_rightC_stm_ref0_exit_9=Exit_Sub_ACT)) -> (random_walker_left_rightC_stm_ref0_exit_9'=Exit_Sub_EXITED); [] (random_walker_left_rightC_stm_ref0_scpc_8=Action_44) -> (random_walker_left_rightC_stm_ref0_lrh'=LRH_rt)&(random_walker_left_rightC_stm_ref0_scpc_8'=random_walker_left_rightC_stm_ref0_LR_entering); // The transition [sp1_7] from a state [LR] to [sp_pj_6].Step 1: trigger an exit of the state [LR] [move_19] ((random_walker_left_rightC_stm_ref0_lock_7=random_walker_left_rightC_stm_ref0_LOCK_FREE))&(((random_walker_left_rightC_stm_ref0_scpc_8=random_walker_left_rightC_stm_ref0_LR))&((((random_walker_left_rightC_stm_ref0_lrh=LRH_lt))&(x>(1)))&(steps (random_walker_left_rightC_stm_ref0_lock_7'=random_walker_left_rightC_stm_ref0_sp1_7)&(random_walker_left_rightC_stm_ref0_scpc_8'=random_walker_left_rightC_stm_ref0_sp_pj_6); // From the probabilistic junction [p2] [] (random_walker_left_rightC_stm_ref0_scpc_8=random_walker_left_rightC_stm_ref0_p2) -> (0.5):(random_walker_left_rightC_stm_ref0_scpc_8'=random_walker_left_rightC_stm_ref0_LR_entering) + (0.5):(random_walker_left_rightC_stm_ref0_scpc_8'=Action_48); // The transition [t17] from a state [LR] to [LR].Step 1: trigger an exit of the state [LR] [move_19] ((random_walker_left_rightC_stm_ref0_scpc_8=random_walker_left_rightC_stm_ref0_LR))&(((steps=MAX))&((random_walker_left_rightC_stm_ref0_lock_7=random_walker_left_rightC_stm_ref0_LOCK_FREE))) -> (random_walker_left_rightC_stm_ref0_scpc_8'=random_walker_left_rightC_stm_ref0_LR_entering)&(random_walker_left_rightC_stm_ref0_lock_7'=random_walker_left_rightC_stm_ref0_t17); // The transition [t3] from a state [LR] to [p0].Step 1: trigger an exit of the state [LR] [move_19] ((random_walker_left_rightC_stm_ref0_lock_7=random_walker_left_rightC_stm_ref0_LOCK_FREE))&(((((random_walker_left_rightC_stm_ref0_lrh=LRH_rt))&((x=M)))&(steps (random_walker_left_rightC_stm_ref0_lock_7'=random_walker_left_rightC_stm_ref0_t3)&(random_walker_left_rightC_stm_ref0_scpc_8'=random_walker_left_rightC_stm_ref0_p0); // From the probabilistic junction [sp_pj_3] [] (random_walker_left_rightC_stm_ref0_scpc_8=random_walker_left_rightC_stm_ref0_sp_pj_3) -> (random_walker_left_rightC_stm_ref0_scpc_8'=Action_57); [] (random_walker_left_rightC_stm_ref0_scpc_8=Action_55) -> (random_walker_left_rightC_stm_ref0_scpc_8'=random_walker_left_rightC_stm_ref0_LR_entering)&(random_walker_left_rightC_stm_ref0_lrh'=LRH_rt); [] (random_walker_left_rightC_stm_ref0_scpc_8=Action_50) -> (x'=(1))&(random_walker_left_rightC_stm_ref0_scpc_8'=Action_49); // From the probabilistic junction [p0] [] (random_walker_left_rightC_stm_ref0_scpc_8=random_walker_left_rightC_stm_ref0_p0) -> (0.5):(random_walker_left_rightC_stm_ref0_scpc_8'=Action_53) + (0.5):(random_walker_left_rightC_stm_ref0_scpc_8'=Action_51); // The transition [t8] from a state [LR] to [p1].Step 1: trigger an exit of the state [LR] [move_19] ((random_walker_left_rightC_stm_ref0_scpc_8=random_walker_left_rightC_stm_ref0_LR))&(((((random_walker_left_rightC_stm_ref0_lrh=LRH_lt))&((x=(1))))&(steps (random_walker_left_rightC_stm_ref0_scpc_8'=random_walker_left_rightC_stm_ref0_p1)&(random_walker_left_rightC_stm_ref0_lock_7'=random_walker_left_rightC_stm_ref0_t8); [] (random_walker_left_rightC_stm_ref0_scpc_8=Action_51) -> (random_walker_left_rightC_stm_ref0_lrh'=LRH_vt)&(random_walker_left_rightC_stm_ref0_scpc_8'=random_walker_left_rightC_stm_ref0_LR_entering); endmodule // Renames of RoboChart elements (automatically generated and used by the assertion language and don't delete) // renames of the STM [random_walker::up_downC::stm_ref0] to [random_walker_up_downC_stm_ref0] // renames of the event [random_walker::up_downC::stm_ref0::move::OUT] to [move_19] // renames of the event [random_walker::up_downC::stm_ref0::rcrd_start::OUT] to [rcrd_start_17] // renames of the event [random_walker::up_downC::stm_ref0::rcrd_end::OUT] to [rcrd_end_20] // renames of the variable [random_walker::up_downC::stm_ref0::uph] to [random_walker_up_downC_stm_ref0_uph] // renames of the node [random_walker::up_downC::stm_ref0::j1] to [random_walker_up_downC_stm_ref0_j1] // renames of the node [random_walker::up_downC::stm_ref0::i0] to [random_walker_up_downC_stm_ref0_i0] // renames of the node [random_walker::up_downC::stm_ref0::p1] to [random_walker_up_downC_stm_ref0_p1] // renames of the node [random_walker::up_downC::stm_ref0::p0] to [random_walker_up_downC_stm_ref0_p0] // renames of the node [random_walker::up_downC::stm_ref0::LR] to [random_walker_up_downC_stm_ref0_LR] // renames of the node [random_walker::up_downC::stm_ref0::p2] to [random_walker_up_downC_stm_ref0_p2] // renames of the node [random_walker::up_downC::stm_ref0::p3] to [random_walker_up_downC_stm_ref0_p3] // renames of the node [random_walker::up_downC::stm_ref0::j0] to [random_walker_up_downC_stm_ref0_j0] // renames of the transition [random_walker::up_downC::stm_ref0::t12] to [random_walker_up_downC_stm_ref0_t12] // renames of the transition [random_walker::up_downC::stm_ref0::t10] to [random_walker_up_downC_stm_ref0_t10] // renames of the transition [random_walker::up_downC::stm_ref0::t3] to [random_walker_up_downC_stm_ref0_t3] // renames of the transition [random_walker::up_downC::stm_ref0::t7] to [random_walker_up_downC_stm_ref0_t7] // renames of the transition [random_walker::up_downC::stm_ref0::t14] to [random_walker_up_downC_stm_ref0_t14] // renames of the transition [random_walker::up_downC::stm_ref0::t2] to [random_walker_up_downC_stm_ref0_t2] // renames of the transition [random_walker::up_downC::stm_ref0::t6] to [random_walker_up_downC_stm_ref0_t6] // renames of the transition [random_walker::up_downC::stm_ref0::t5] to [random_walker_up_downC_stm_ref0_t5] // renames of the transition [random_walker::up_downC::stm_ref0::t13] to [random_walker_up_downC_stm_ref0_t13] // renames of the transition [random_walker::up_downC::stm_ref0::t4] to [random_walker_up_downC_stm_ref0_t4] // renames of the transition [random_walker::up_downC::stm_ref0::t11] to [random_walker_up_downC_stm_ref0_t11] // renames of the transition [random_walker::up_downC::stm_ref0::t1] to [random_walker_up_downC_stm_ref0_t1] // renames of the transition [random_walker::up_downC::stm_ref0::t8] to [random_walker_up_downC_stm_ref0_t8] // renames of the transition [random_walker::up_downC::stm_ref0::t0] to [random_walker_up_downC_stm_ref0_t0] // renames of the transition [random_walker::up_downC::stm_ref0::t17] to [random_walker_up_downC_stm_ref0_t17] // renames of the transition [random_walker::up_downC::stm_ref0::t15] to [random_walker_up_downC_stm_ref0_t15] // renames of the transition [random_walker::up_downC::stm_ref0::t9] to [random_walker_up_downC_stm_ref0_t9] // renames of the transition [random_walker::up_downC::stm_ref0::t16] to [random_walker_up_downC_stm_ref0_t16] // renames of the variable [random_walker::up_downC::stm_ref0::exit_9] to [random_walker_up_downC_stm_ref0_exit_9] // renames of the variable [random_walker::up_downC::stm_ref0::scpc_8] to [random_walker_up_downC_stm_ref0_scpc_8] // renames of the variable [random_walker::up_downC::stm_ref0::lock_7] to [random_walker_up_downC_stm_ref0_lock_7] // renames of the STM [random_walker::left_rightC::stm_ref0] to [random_walker_left_rightC_stm_ref0] // renames of the event [random_walker::left_rightC::stm_ref0::move::IN] to [move_19] // renames of the event [random_walker::left_rightC::stm_ref0::rcrd_start::OUT] to [rcrd_start_18] // renames of the event [random_walker::left_rightC::stm_ref0::rcrd_end::OUT] to [rcrd_end_16] // renames of the variable [random_walker::left_rightC::stm_ref0::lrh] to [random_walker_left_rightC_stm_ref0_lrh] // renames of the node [random_walker::left_rightC::stm_ref0::sp_pj_6] to [random_walker_left_rightC_stm_ref0_sp_pj_6] // renames of the node [random_walker::left_rightC::stm_ref0::LR] to [random_walker_left_rightC_stm_ref0_LR] // renames of the node [random_walker::left_rightC::stm_ref0::p0] to [random_walker_left_rightC_stm_ref0_p0] // renames of the node [random_walker::left_rightC::stm_ref0::p3] to [random_walker_left_rightC_stm_ref0_p3] // renames of the node [random_walker::left_rightC::stm_ref0::sp_pj_3] to [random_walker_left_rightC_stm_ref0_sp_pj_3] // renames of the node [random_walker::left_rightC::stm_ref0::i0] to [random_walker_left_rightC_stm_ref0_i0] // renames of the node [random_walker::left_rightC::stm_ref0::p2] to [random_walker_left_rightC_stm_ref0_p2] // renames of the node [random_walker::left_rightC::stm_ref0::p1] to [random_walker_left_rightC_stm_ref0_p1] // renames of the transition [random_walker::left_rightC::stm_ref0::t0] to [random_walker_left_rightC_stm_ref0_t0] // renames of the transition [random_walker::left_rightC::stm_ref0::sp1_7] to [random_walker_left_rightC_stm_ref0_sp1_7] // renames of the transition [random_walker::left_rightC::stm_ref0::t16] to [random_walker_left_rightC_stm_ref0_t16] // renames of the transition [random_walker::left_rightC::stm_ref0::t15] to [random_walker_left_rightC_stm_ref0_t15] // renames of the transition [random_walker::left_rightC::stm_ref0::sp2_5] to [random_walker_left_rightC_stm_ref0_sp2_5] // renames of the transition [random_walker::left_rightC::stm_ref0::t12] to [random_walker_left_rightC_stm_ref0_t12] // renames of the transition [random_walker::left_rightC::stm_ref0::sp2_8] to [random_walker_left_rightC_stm_ref0_sp2_8] // renames of the transition [random_walker::left_rightC::stm_ref0::t13] to [random_walker_left_rightC_stm_ref0_t13] // renames of the transition [random_walker::left_rightC::stm_ref0::t17] to [random_walker_left_rightC_stm_ref0_t17] // renames of the transition [random_walker::left_rightC::stm_ref0::t3] to [random_walker_left_rightC_stm_ref0_t3] // renames of the transition [random_walker::left_rightC::stm_ref0::t5] to [random_walker_left_rightC_stm_ref0_t5] // renames of the transition [random_walker::left_rightC::stm_ref0::t11] to [random_walker_left_rightC_stm_ref0_t11] // renames of the transition [random_walker::left_rightC::stm_ref0::t9] to [random_walker_left_rightC_stm_ref0_t9] // renames of the transition [random_walker::left_rightC::stm_ref0::t4] to [random_walker_left_rightC_stm_ref0_t4] // renames of the transition [random_walker::left_rightC::stm_ref0::t14] to [random_walker_left_rightC_stm_ref0_t14] // renames of the transition [random_walker::left_rightC::stm_ref0::t8] to [random_walker_left_rightC_stm_ref0_t8] // renames of the transition [random_walker::left_rightC::stm_ref0::sp1_4] to [random_walker_left_rightC_stm_ref0_sp1_4] // renames of the transition [random_walker::left_rightC::stm_ref0::t10] to [random_walker_left_rightC_stm_ref0_t10] // renames of the variable [random_walker::left_rightC::stm_ref0::exit_9] to [random_walker_left_rightC_stm_ref0_exit_9] // renames of the variable [random_walker::left_rightC::stm_ref0::scpc_8] to [random_walker_left_rightC_stm_ref0_scpc_8] // renames of the variable [random_walker::left_rightC::stm_ref0::lock_7] to [random_walker_left_rightC_stm_ref0_lock_7] // renames of the STM [random_walker::recorderC::stm_ref0] to [random_walker_recorderC_stm_ref0] // renames of the event [random_walker::recorderC::stm_ref0::rcrd_x_end::IN] to [rcrd_end_16] // renames of the event [random_walker::recorderC::stm_ref0::rcrd_y_start::IN] to [rcrd_start_17] // renames of the event [random_walker::recorderC::stm_ref0::rcrd_x_start::IN] to [rcrd_start_18] // renames of the event [random_walker::recorderC::stm_ref0::rcrd_y_end::IN] to [rcrd_end_20] // renames of the variable [random_walker::recorderC::stm_ref0::v] to [random_walker_recorderC_stm_ref0_v] // renames of the node [random_walker::recorderC::stm_ref0::loop_9] to [random_walker_recorderC_stm_ref0_loop_9] // renames of the node [random_walker::recorderC::stm_ref0::RECy2] to [random_walker_recorderC_stm_ref0_RECy2] // renames of the node [random_walker::recorderC::stm_ref0::REC] to [random_walker_recorderC_stm_ref0_REC] // renames of the node [random_walker::recorderC::stm_ref0::i0] to [random_walker_recorderC_stm_ref0_i0] // renames of the node [random_walker::recorderC::stm_ref0::RECx] to [random_walker_recorderC_stm_ref0_RECx] // renames of the node [random_walker::recorderC::stm_ref0::STOP] to [random_walker_recorderC_stm_ref0_STOP] // renames of the node [random_walker::recorderC::stm_ref0::RECy] to [random_walker_recorderC_stm_ref0_RECy] // renames of the node [random_walker::recorderC::stm_ref0::RECx2] to [random_walker_recorderC_stm_ref0_RECx2] // renames of the transition [random_walker::recorderC::stm_ref0::t1] to [random_walker_recorderC_stm_ref0_t1] // renames of the transition [random_walker::recorderC::stm_ref0::t6] to [random_walker_recorderC_stm_ref0_t6] // renames of the transition [random_walker::recorderC::stm_ref0::t0] to [random_walker_recorderC_stm_ref0_t0] // renames of the transition [random_walker::recorderC::stm_ref0::t7] to [random_walker_recorderC_stm_ref0_t7] // renames of the transition [random_walker::recorderC::stm_ref0::loop_self_10] to [random_walker_recorderC_stm_ref0_loop_self_10] // renames of the transition [random_walker::recorderC::stm_ref0::to_loop_11] to [random_walker_recorderC_stm_ref0_to_loop_11] // renames of the transition [random_walker::recorderC::stm_ref0::t4] to [random_walker_recorderC_stm_ref0_t4] // renames of the transition [random_walker::recorderC::stm_ref0::t5] to [random_walker_recorderC_stm_ref0_t5] // renames of the transition [random_walker::recorderC::stm_ref0::t2] to [random_walker_recorderC_stm_ref0_t2] // renames of the variable [random_walker::recorderC::stm_ref0::exit_9] to [random_walker_recorderC_stm_ref0_exit_9] // renames of the variable [random_walker::recorderC::stm_ref0::scpc_8] to [random_walker_recorderC_stm_ref0_scpc_8] // renames of the variable [random_walker::recorderC::stm_ref0::lock_7] to [random_walker_recorderC_stm_ref0_lock_7] // renames of the variable [random_walker::RW_RP::N] to [N] // renames of the constant [N] to [N] // renames of the variable [random_walker::RW_RP::MAX] to [MAX] // renames of the constant [MAX] to [MAX] // renames of the variable [random_walker::RW_RP::y] to [y] // renames of the variable [y] to [y] // renames of the variable [random_walker::RW_RP::steps] to [steps] // renames of the variable [steps] to [steps] // renames of the variable [random_walker::RW_RP::M] to [M] // renames of the constant [M] to [M] // renames of the variable [random_walker::RW_RP::x] to [x] // renames of the variable [x] to [x]