// This model is automatically generated from the RoboChart model // by the translator (translate2prism v20201107) plugin in RoboTool // on 2020-11-06 16:43:52 // // All changes made will be lost after regeneration. // PRISM Output dtmc const int Action_11 = 17; const int Action_12 = 18; const int Action_13 = 19; const int Action_14 = 20; const int Action_15 = 21; const int Action_16 = 22; const int Action_17 = 23; const int DieM_CTRL_stm_ref0_INACTIVE = 0; const int DieM_CTRL_stm_ref0_LOCK_FREE = 0; const int DieM_CTRL_stm_ref0_Out = 1; const int DieM_CTRL_stm_ref0_i0 = 4; const int DieM_CTRL_stm_ref0_p0 = 7; const int DieM_CTRL_stm_ref0_p1 = 3; const int DieM_CTRL_stm_ref0_p2 = 12; const int DieM_CTRL_stm_ref0_p3 = 11; const int DieM_CTRL_stm_ref0_p4 = 5; const int DieM_CTRL_stm_ref0_p5 = 8; const int DieM_CTRL_stm_ref0_p6 = 6; const int DieM_CTRL_stm_ref0_s0 = 13; const int DieM_CTRL_stm_ref0_s1 = 14; const int DieM_CTRL_stm_ref0_s2 = 10; const int DieM_CTRL_stm_ref0_s3 = 2; const int DieM_CTRL_stm_ref0_s4 = 9; const int DieM_CTRL_stm_ref0_s5 = 16; const int DieM_CTRL_stm_ref0_s6 = 15; const int DieM_CTRL_stm_ref0_t0 = 3; const int DieM_CTRL_stm_ref0_t1 = 6; const int DieM_CTRL_stm_ref0_t10 = 2; const int DieM_CTRL_stm_ref0_t13 = 1; const int DieM_CTRL_stm_ref0_t14 = 4; const int DieM_CTRL_stm_ref0_t17 = 9; const int DieM_CTRL_stm_ref0_t20 = 8; const int DieM_CTRL_stm_ref0_t4 = 7; const int DieM_CTRL_stm_ref0_t7 = 5; 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; const int Exit_NONE = 0; const int Exit_Sub_ACT_Waiting = 5; module DieM_CTRL_stm_ref0 DieM_CTRL_stm_ref0_scpc_8 : [0..23] init DieM_CTRL_stm_ref0_i0; DieM_CTRL_stm_ref0_exit_9 : [0..6] init Exit_NONE; DieM_CTRL_stm_ref0_lock_7 : [0..9] init DieM_CTRL_stm_ref0_LOCK_FREE; DieM_CTRL_stm_ref0_d : [-2..7]; // Step 4/2: exit command of the state [Out] [] ((DieM_CTRL_stm_ref0_scpc_8=DieM_CTRL_stm_ref0_Out))&((DieM_CTRL_stm_ref0_exit_9=Exit_Sub_ACT)) -> (DieM_CTRL_stm_ref0_exit_9'=Exit_Sub_EXITED); // Step 4/2: exit command of the state [s0] [] ((DieM_CTRL_stm_ref0_scpc_8=DieM_CTRL_stm_ref0_s0))&((DieM_CTRL_stm_ref0_exit_9=Exit_Sub_ACT)) -> (DieM_CTRL_stm_ref0_exit_9'=Exit_Sub_EXITED); // The transition [t17] from a state [s5] to [p5].Step 1: trigger an exit of the state [s5] [flip_10] ((DieM_CTRL_stm_ref0_scpc_8=DieM_CTRL_stm_ref0_s5))&((DieM_CTRL_stm_ref0_lock_7=DieM_CTRL_stm_ref0_LOCK_FREE)) -> (DieM_CTRL_stm_ref0_lock_7'=DieM_CTRL_stm_ref0_t17)&(DieM_CTRL_stm_ref0_scpc_8'=DieM_CTRL_stm_ref0_p5); // The transition [t4] from a state [s1] to [p1].Step 1: trigger an exit of the state [s1] [flip_10] ((DieM_CTRL_stm_ref0_scpc_8=DieM_CTRL_stm_ref0_s1))&((DieM_CTRL_stm_ref0_lock_7=DieM_CTRL_stm_ref0_LOCK_FREE)) -> (DieM_CTRL_stm_ref0_scpc_8'=DieM_CTRL_stm_ref0_p1)&(DieM_CTRL_stm_ref0_lock_7'=DieM_CTRL_stm_ref0_t4); [] (DieM_CTRL_stm_ref0_scpc_8=Action_15) -> (DieM_CTRL_stm_ref0_d'=4)&(DieM_CTRL_stm_ref0_scpc_8'=DieM_CTRL_stm_ref0_Out)&(DieM_CTRL_stm_ref0_lock_7'=DieM_CTRL_stm_ref0_LOCK_FREE); // Step 4/2: exit command of the state [s1] [] ((DieM_CTRL_stm_ref0_scpc_8=DieM_CTRL_stm_ref0_s1))&((DieM_CTRL_stm_ref0_exit_9=Exit_Sub_ACT)) -> (DieM_CTRL_stm_ref0_exit_9'=Exit_Sub_EXITED); // The transition [t0] from [i0] to [s0]. [] (DieM_CTRL_stm_ref0_scpc_8=DieM_CTRL_stm_ref0_i0) -> (DieM_CTRL_stm_ref0_lock_7'=DieM_CTRL_stm_ref0_t0)&(DieM_CTRL_stm_ref0_scpc_8'=Action_11); [] (DieM_CTRL_stm_ref0_scpc_8=Action_17) -> (DieM_CTRL_stm_ref0_d'=1)&(DieM_CTRL_stm_ref0_lock_7'=DieM_CTRL_stm_ref0_LOCK_FREE)&(DieM_CTRL_stm_ref0_scpc_8'=DieM_CTRL_stm_ref0_Out); // Step 4/2: exit command of the state [s4] [] ((DieM_CTRL_stm_ref0_scpc_8=DieM_CTRL_stm_ref0_s4))&((DieM_CTRL_stm_ref0_exit_9=Exit_Sub_ACT)) -> (DieM_CTRL_stm_ref0_exit_9'=Exit_Sub_EXITED); // From the probabilistic junction [p0] [] (DieM_CTRL_stm_ref0_scpc_8=DieM_CTRL_stm_ref0_p0) -> 0.5:(DieM_CTRL_stm_ref0_scpc_8'=DieM_CTRL_stm_ref0_s2)&(DieM_CTRL_stm_ref0_lock_7'=DieM_CTRL_stm_ref0_LOCK_FREE) + 0.5:(DieM_CTRL_stm_ref0_lock_7'=DieM_CTRL_stm_ref0_LOCK_FREE)&(DieM_CTRL_stm_ref0_scpc_8'=DieM_CTRL_stm_ref0_s1); // The transition [t14] from a state [s4] to [p4].Step 1: trigger an exit of the state [s4] [flip_10] ((DieM_CTRL_stm_ref0_scpc_8=DieM_CTRL_stm_ref0_s4))&((DieM_CTRL_stm_ref0_lock_7=DieM_CTRL_stm_ref0_LOCK_FREE)) -> (DieM_CTRL_stm_ref0_lock_7'=DieM_CTRL_stm_ref0_t14)&(DieM_CTRL_stm_ref0_scpc_8'=DieM_CTRL_stm_ref0_p4); // The transition [t13] from a state [Out] to [Out].Step 1: trigger an exit of the state [Out] [flip_10] ((DieM_CTRL_stm_ref0_scpc_8=DieM_CTRL_stm_ref0_Out))&((DieM_CTRL_stm_ref0_lock_7=DieM_CTRL_stm_ref0_LOCK_FREE)) -> (DieM_CTRL_stm_ref0_lock_7'=DieM_CTRL_stm_ref0_LOCK_FREE)&(DieM_CTRL_stm_ref0_scpc_8'=DieM_CTRL_stm_ref0_Out); // From the probabilistic junction [p5] [] (DieM_CTRL_stm_ref0_scpc_8=DieM_CTRL_stm_ref0_p5) -> 0.5:(DieM_CTRL_stm_ref0_scpc_8'=Action_16) + 0.5:(DieM_CTRL_stm_ref0_scpc_8'=Action_15); // Step 4/2: exit command of the state [s6] [] ((DieM_CTRL_stm_ref0_scpc_8=DieM_CTRL_stm_ref0_s6))&((DieM_CTRL_stm_ref0_exit_9=Exit_Sub_ACT)) -> (DieM_CTRL_stm_ref0_exit_9'=Exit_Sub_EXITED); // From the probabilistic junction [p4] [] (DieM_CTRL_stm_ref0_scpc_8=DieM_CTRL_stm_ref0_p4) -> 0.5:(DieM_CTRL_stm_ref0_scpc_8'=Action_13) + 0.5:(DieM_CTRL_stm_ref0_scpc_8'=Action_12); [] (DieM_CTRL_stm_ref0_scpc_8=Action_13) -> (DieM_CTRL_stm_ref0_lock_7'=DieM_CTRL_stm_ref0_LOCK_FREE)&(DieM_CTRL_stm_ref0_scpc_8'=DieM_CTRL_stm_ref0_Out)&(DieM_CTRL_stm_ref0_d'=2); // From the probabilistic junction [p1] [] (DieM_CTRL_stm_ref0_scpc_8=DieM_CTRL_stm_ref0_p1) -> 0.5:(DieM_CTRL_stm_ref0_scpc_8'=DieM_CTRL_stm_ref0_s3)&(DieM_CTRL_stm_ref0_lock_7'=DieM_CTRL_stm_ref0_LOCK_FREE) + 0.5:(DieM_CTRL_stm_ref0_lock_7'=DieM_CTRL_stm_ref0_LOCK_FREE)&(DieM_CTRL_stm_ref0_scpc_8'=DieM_CTRL_stm_ref0_s4); [] (DieM_CTRL_stm_ref0_scpc_8=Action_12) -> (DieM_CTRL_stm_ref0_lock_7'=DieM_CTRL_stm_ref0_LOCK_FREE)&(DieM_CTRL_stm_ref0_scpc_8'=DieM_CTRL_stm_ref0_Out)&(DieM_CTRL_stm_ref0_d'=3); // From the probabilistic junction [p2] [] (DieM_CTRL_stm_ref0_scpc_8=DieM_CTRL_stm_ref0_p2) -> 0.5:(DieM_CTRL_stm_ref0_lock_7'=DieM_CTRL_stm_ref0_LOCK_FREE)&(DieM_CTRL_stm_ref0_scpc_8'=DieM_CTRL_stm_ref0_s6) + 0.5:(DieM_CTRL_stm_ref0_lock_7'=DieM_CTRL_stm_ref0_LOCK_FREE)&(DieM_CTRL_stm_ref0_scpc_8'=DieM_CTRL_stm_ref0_s5); [] (DieM_CTRL_stm_ref0_scpc_8=Action_11) -> (DieM_CTRL_stm_ref0_lock_7'=DieM_CTRL_stm_ref0_LOCK_FREE)&(DieM_CTRL_stm_ref0_d'=0)&(DieM_CTRL_stm_ref0_scpc_8'=DieM_CTRL_stm_ref0_s0); [] (DieM_CTRL_stm_ref0_scpc_8=Action_14) -> (DieM_CTRL_stm_ref0_lock_7'=DieM_CTRL_stm_ref0_LOCK_FREE)&(DieM_CTRL_stm_ref0_d'=6)&(DieM_CTRL_stm_ref0_scpc_8'=DieM_CTRL_stm_ref0_Out); // From the probabilistic junction [p3] [] (DieM_CTRL_stm_ref0_scpc_8=DieM_CTRL_stm_ref0_p3) -> 0.5:(DieM_CTRL_stm_ref0_scpc_8'=DieM_CTRL_stm_ref0_s1)&(DieM_CTRL_stm_ref0_lock_7'=DieM_CTRL_stm_ref0_LOCK_FREE) + 0.5:(DieM_CTRL_stm_ref0_scpc_8'=Action_17); // Step 4/2: exit command of the state [s5] [] ((DieM_CTRL_stm_ref0_scpc_8=DieM_CTRL_stm_ref0_s5))&((DieM_CTRL_stm_ref0_exit_9=Exit_Sub_ACT)) -> (DieM_CTRL_stm_ref0_exit_9'=Exit_Sub_EXITED); // From the probabilistic junction [p6] [] (DieM_CTRL_stm_ref0_scpc_8=DieM_CTRL_stm_ref0_p6) -> 0.5:(DieM_CTRL_stm_ref0_scpc_8'=DieM_CTRL_stm_ref0_s2)&(DieM_CTRL_stm_ref0_lock_7'=DieM_CTRL_stm_ref0_LOCK_FREE) + 0.5:(DieM_CTRL_stm_ref0_scpc_8'=Action_14); // The transition [t1] from a state [s0] to [p0].Step 1: trigger an exit of the state [s0] [flip_10] ((DieM_CTRL_stm_ref0_lock_7=DieM_CTRL_stm_ref0_LOCK_FREE))&((DieM_CTRL_stm_ref0_scpc_8=DieM_CTRL_stm_ref0_s0)) -> (DieM_CTRL_stm_ref0_lock_7'=DieM_CTRL_stm_ref0_t1)&(DieM_CTRL_stm_ref0_scpc_8'=DieM_CTRL_stm_ref0_p0); // Step 4/2: exit command of the state [s2] [] ((DieM_CTRL_stm_ref0_scpc_8=DieM_CTRL_stm_ref0_s2))&((DieM_CTRL_stm_ref0_exit_9=Exit_Sub_ACT)) -> (DieM_CTRL_stm_ref0_exit_9'=Exit_Sub_EXITED); // The transition [t20] from a state [s6] to [p6].Step 1: trigger an exit of the state [s6] [flip_10] ((DieM_CTRL_stm_ref0_lock_7=DieM_CTRL_stm_ref0_LOCK_FREE))&((DieM_CTRL_stm_ref0_scpc_8=DieM_CTRL_stm_ref0_s6)) -> (DieM_CTRL_stm_ref0_lock_7'=DieM_CTRL_stm_ref0_t20)&(DieM_CTRL_stm_ref0_scpc_8'=DieM_CTRL_stm_ref0_p6); [] (DieM_CTRL_stm_ref0_scpc_8=Action_16) -> (DieM_CTRL_stm_ref0_lock_7'=DieM_CTRL_stm_ref0_LOCK_FREE)&(DieM_CTRL_stm_ref0_scpc_8'=DieM_CTRL_stm_ref0_Out)&(DieM_CTRL_stm_ref0_d'=5); // Step 4/2: exit command of the state [s3] [] ((DieM_CTRL_stm_ref0_scpc_8=DieM_CTRL_stm_ref0_s3))&((DieM_CTRL_stm_ref0_exit_9=Exit_Sub_ACT)) -> (DieM_CTRL_stm_ref0_exit_9'=Exit_Sub_EXITED); // The transition [t7] from a state [s2] to [p2].Step 1: trigger an exit of the state [s2] [flip_10] ((DieM_CTRL_stm_ref0_lock_7=DieM_CTRL_stm_ref0_LOCK_FREE))&((DieM_CTRL_stm_ref0_scpc_8=DieM_CTRL_stm_ref0_s2)) -> (DieM_CTRL_stm_ref0_scpc_8'=DieM_CTRL_stm_ref0_p2)&(DieM_CTRL_stm_ref0_lock_7'=DieM_CTRL_stm_ref0_t7); // The transition [t10] from a state [s3] to [p3].Step 1: trigger an exit of the state [s3] [flip_10] ((DieM_CTRL_stm_ref0_lock_7=DieM_CTRL_stm_ref0_LOCK_FREE))&((DieM_CTRL_stm_ref0_scpc_8=DieM_CTRL_stm_ref0_s3)) -> (DieM_CTRL_stm_ref0_scpc_8'=DieM_CTRL_stm_ref0_p3)&(DieM_CTRL_stm_ref0_lock_7'=DieM_CTRL_stm_ref0_t10); endmodule module DieM_RP [flip_10] true -> true; endmodule // Renames of RoboChart elements (automatically generated and used by the assertion language and don't delete) // renames of the STM [DieM::CTRL::stm_ref0] to [DieM_CTRL_stm_ref0] // renames of the event [DieM::CTRL::stm_ref0::flip] to [flip_10] // renames of the variable [DieM::CTRL::stm_ref0::d] to [DieM_CTRL_stm_ref0_d] // renames of the node [DieM::CTRL::stm_ref0::p1] to [DieM_CTRL_stm_ref0_p1] // renames of the node [DieM::CTRL::stm_ref0::p6] to [DieM_CTRL_stm_ref0_p6] // renames of the node [DieM::CTRL::stm_ref0::p2] to [DieM_CTRL_stm_ref0_p2] // renames of the node [DieM::CTRL::stm_ref0::s1] to [DieM_CTRL_stm_ref0_s1] // renames of the node [DieM::CTRL::stm_ref0::s3] to [DieM_CTRL_stm_ref0_s3] // renames of the node [DieM::CTRL::stm_ref0::Out] to [DieM_CTRL_stm_ref0_Out] // renames of the node [DieM::CTRL::stm_ref0::s6] to [DieM_CTRL_stm_ref0_s6] // renames of the node [DieM::CTRL::stm_ref0::s5] to [DieM_CTRL_stm_ref0_s5] // renames of the node [DieM::CTRL::stm_ref0::s4] to [DieM_CTRL_stm_ref0_s4] // renames of the node [DieM::CTRL::stm_ref0::i0] to [DieM_CTRL_stm_ref0_i0] // renames of the node [DieM::CTRL::stm_ref0::p5] to [DieM_CTRL_stm_ref0_p5] // renames of the node [DieM::CTRL::stm_ref0::s0] to [DieM_CTRL_stm_ref0_s0] // renames of the node [DieM::CTRL::stm_ref0::p4] to [DieM_CTRL_stm_ref0_p4] // renames of the node [DieM::CTRL::stm_ref0::s2] to [DieM_CTRL_stm_ref0_s2] // renames of the node [DieM::CTRL::stm_ref0::p0] to [DieM_CTRL_stm_ref0_p0] // renames of the node [DieM::CTRL::stm_ref0::p3] to [DieM_CTRL_stm_ref0_p3] // renames of the transition [DieM::CTRL::stm_ref0::t18] to [DieM_CTRL_stm_ref0_t18] // renames of the transition [DieM::CTRL::stm_ref0::t7] to [DieM_CTRL_stm_ref0_t7] // renames of the transition [DieM::CTRL::stm_ref0::t19] to [DieM_CTRL_stm_ref0_t19] // renames of the transition [DieM::CTRL::stm_ref0::t2] to [DieM_CTRL_stm_ref0_t2] // renames of the transition [DieM::CTRL::stm_ref0::t16] to [DieM_CTRL_stm_ref0_t16] // renames of the transition [DieM::CTRL::stm_ref0::t8] to [DieM_CTRL_stm_ref0_t8] // renames of the transition [DieM::CTRL::stm_ref0::t1] to [DieM_CTRL_stm_ref0_t1] // renames of the transition [DieM::CTRL::stm_ref0::t12] to [DieM_CTRL_stm_ref0_t12] // renames of the transition [DieM::CTRL::stm_ref0::t5] to [DieM_CTRL_stm_ref0_t5] // renames of the transition [DieM::CTRL::stm_ref0::t21] to [DieM_CTRL_stm_ref0_t21] // renames of the transition [DieM::CTRL::stm_ref0::t15] to [DieM_CTRL_stm_ref0_t15] // renames of the transition [DieM::CTRL::stm_ref0::t9] to [DieM_CTRL_stm_ref0_t9] // renames of the transition [DieM::CTRL::stm_ref0::t14] to [DieM_CTRL_stm_ref0_t14] // renames of the transition [DieM::CTRL::stm_ref0::t10] to [DieM_CTRL_stm_ref0_t10] // renames of the transition [DieM::CTRL::stm_ref0::t20] to [DieM_CTRL_stm_ref0_t20] // renames of the transition [DieM::CTRL::stm_ref0::t22] to [DieM_CTRL_stm_ref0_t22] // renames of the transition [DieM::CTRL::stm_ref0::t4] to [DieM_CTRL_stm_ref0_t4] // renames of the transition [DieM::CTRL::stm_ref0::t0] to [DieM_CTRL_stm_ref0_t0] // renames of the transition [DieM::CTRL::stm_ref0::t13] to [DieM_CTRL_stm_ref0_t13] // renames of the transition [DieM::CTRL::stm_ref0::t3] to [DieM_CTRL_stm_ref0_t3] // renames of the transition [DieM::CTRL::stm_ref0::t6] to [DieM_CTRL_stm_ref0_t6] // renames of the transition [DieM::CTRL::stm_ref0::t17] to [DieM_CTRL_stm_ref0_t17] // renames of the transition [DieM::CTRL::stm_ref0::t11] to [DieM_CTRL_stm_ref0_t11] // renames of the variable [DieM::CTRL::stm_ref0::exit_9] to [DieM_CTRL_stm_ref0_exit_9] // renames of the variable [DieM::CTRL::stm_ref0::scpc_8] to [DieM_CTRL_stm_ref0_scpc_8] // renames of the variable [DieM::CTRL::stm_ref0::lock_7] to [DieM_CTRL_stm_ref0_lock_7] // renames of the event [DieM::RP::flip] to [flip_10]