// This model is automatically generated from the RoboChart model // by the translator (translate2prism v20201107) plugin in RoboTool // on 2020-11-06 16:57:40 // // All changes made will be lost after regeneration. // PRISM Output mdp const int Action_13 = 5; const int Action_14 = 6; const int Action_15 = 7; const int Action_16 = 8; const int foraging_foraging_stm_ref0_FORAGE = 3; const int foraging_foraging_stm_ref0_INACTIVE = 0; const int foraging_foraging_stm_ref0_LOCK_FREE = 0; const int foraging_foraging_stm_ref0_N; const int foraging_foraging_stm_ref0_STOP = 4; const int foraging_foraging_stm_ref0_i0 = 1; const int foraging_foraging_stm_ref0_p0 = 2; const int foraging_foraging_stm_ref0_t0 = 1; const int foraging_foraging_stm_ref0_t1 = 2; const int foraging_foraging_stm_ref0_t4 = 3; const int foraging_foraging_stm_ref0_t5 = 4; const int Exit_EXITED = 3; const int Exit_NONE = 0; const int Exit_Sub_ACT = 4; const int Exit_Sub_EXITED = 6; const int Exit_Sub_ACT_Waiting = 5; const int Exit_ACT_Parent = 1; const int Exit_ACT_Trans = 2; module foraging_foraging_stm_ref0 foraging_foraging_stm_ref0_lock_7 : [0..4] init foraging_foraging_stm_ref0_LOCK_FREE; foraging_foraging_stm_ref0_exit_9 : [0..6] init Exit_NONE; foraging_foraging_stm_ref0_flips : [0..100] init 0; foraging_foraging_stm_ref0_scpc_8 : [0..8] init foraging_foraging_stm_ref0_i0; // Step 4/2: exit command of the state [FORAGE] [] ((foraging_foraging_stm_ref0_scpc_8=foraging_foraging_stm_ref0_FORAGE))&((foraging_foraging_stm_ref0_exit_9=Exit_Sub_ACT)) -> (foraging_foraging_stm_ref0_exit_9'=Exit_Sub_EXITED); [stop_12] (foraging_foraging_stm_ref0_scpc_8=Action_13) -> (foraging_foraging_stm_ref0_scpc_8'=foraging_foraging_stm_ref0_STOP)&(foraging_foraging_stm_ref0_lock_7'=foraging_foraging_stm_ref0_LOCK_FREE); [] (foraging_foraging_stm_ref0_scpc_8=Action_16) -> (foraging_foraging_stm_ref0_scpc_8'=Action_15)&(foraging_foraging_stm_ref0_flips'=(foraging_foraging_stm_ref0_flips (foraging_foraging_stm_ref0_scpc_8'=Action_13)&(foraging_foraging_stm_ref0_flips'=(foraging_foraging_stm_ref0_flips (foraging_foraging_stm_ref0_lock_7'=foraging_foraging_stm_ref0_LOCK_FREE)&(foraging_foraging_stm_ref0_scpc_8'=foraging_foraging_stm_ref0_STOP); // From the probabilistic junction [p0] [] (foraging_foraging_stm_ref0_scpc_8=foraging_foraging_stm_ref0_p0) -> 0.5:(foraging_foraging_stm_ref0_scpc_8'=Action_16) + 0.5:(foraging_foraging_stm_ref0_scpc_8'=Action_14); // The transition [t4] from a state [FORAGE] to [FORAGE].Step 1: trigger an exit of the state [FORAGE] [flip_11] ((foraging_foraging_stm_ref0_lock_7=foraging_foraging_stm_ref0_LOCK_FREE))&((foraging_foraging_stm_ref0_scpc_8=foraging_foraging_stm_ref0_FORAGE)) -> (foraging_foraging_stm_ref0_lock_7'=foraging_foraging_stm_ref0_LOCK_FREE)&(foraging_foraging_stm_ref0_scpc_8'=foraging_foraging_stm_ref0_FORAGE); // Step 4/2: exit command of the state [STOP] [] ((foraging_foraging_stm_ref0_scpc_8=foraging_foraging_stm_ref0_STOP))&((foraging_foraging_stm_ref0_exit_9=Exit_Sub_ACT)) -> (foraging_foraging_stm_ref0_exit_9'=Exit_Sub_EXITED); // The transition [t0] from [i0] to [FORAGE]. [] (foraging_foraging_stm_ref0_scpc_8=foraging_foraging_stm_ref0_i0) -> (foraging_foraging_stm_ref0_scpc_8'=foraging_foraging_stm_ref0_FORAGE)&(foraging_foraging_stm_ref0_lock_7'=foraging_foraging_stm_ref0_LOCK_FREE); [forage_10] (foraging_foraging_stm_ref0_scpc_8=Action_15) -> (foraging_foraging_stm_ref0_scpc_8'=foraging_foraging_stm_ref0_FORAGE)&(foraging_foraging_stm_ref0_lock_7'=foraging_foraging_stm_ref0_LOCK_FREE); // The transition [t1] from a state [FORAGE] to [p0].Step 1: trigger an exit of the state [FORAGE] [flip_11] ((foraging_foraging_stm_ref0_lock_7=foraging_foraging_stm_ref0_LOCK_FREE))&((foraging_foraging_stm_ref0_flips (foraging_foraging_stm_ref0_lock_7'=foraging_foraging_stm_ref0_t1)&(foraging_foraging_stm_ref0_scpc_8'=foraging_foraging_stm_ref0_p0); endmodule module foraging_rp0 [flip_11] true -> true; [stop_12] true -> true; [forage_10] true -> true; endmodule // Renames of RoboChart elements (automatically generated and used by the assertion language and don't delete) // renames of the STM [foraging::foraging::stm_ref0] to [foraging_foraging_stm_ref0] // renames of the event [foraging::foraging::stm_ref0::flip] to [flip_11] // renames of the event [foraging::foraging::stm_ref0::stop] to [stop_12] // renames of the event [foraging::foraging::stm_ref0::forage] to [forage_10] // renames of the constant [foraging::foraging::stm_ref0::N] to [foraging_foraging_stm_ref0_N] // renames of the variable [foraging::foraging::stm_ref0::flips] to [foraging_foraging_stm_ref0_flips] // renames of the node [foraging::foraging::stm_ref0::STOP] to [foraging_foraging_stm_ref0_STOP] // renames of the node [foraging::foraging::stm_ref0::i0] to [foraging_foraging_stm_ref0_i0] // renames of the node [foraging::foraging::stm_ref0::p0] to [foraging_foraging_stm_ref0_p0] // renames of the node [foraging::foraging::stm_ref0::FORAGE] to [foraging_foraging_stm_ref0_FORAGE] // renames of the transition [foraging::foraging::stm_ref0::t3] to [foraging_foraging_stm_ref0_t3] // renames of the transition [foraging::foraging::stm_ref0::t0] to [foraging_foraging_stm_ref0_t0] // renames of the transition [foraging::foraging::stm_ref0::t5] to [foraging_foraging_stm_ref0_t5] // renames of the transition [foraging::foraging::stm_ref0::t1] to [foraging_foraging_stm_ref0_t1] // renames of the transition [foraging::foraging::stm_ref0::t2] to [foraging_foraging_stm_ref0_t2] // renames of the transition [foraging::foraging::stm_ref0::t4] to [foraging_foraging_stm_ref0_t4] // renames of the variable [foraging::foraging::stm_ref0::exit_9] to [foraging_foraging_stm_ref0_exit_9] // renames of the variable [foraging::foraging::stm_ref0::scpc_8] to [foraging_foraging_stm_ref0_scpc_8] // renames of the variable [foraging::foraging::stm_ref0::lock_7] to [foraging_foraging_stm_ref0_lock_7] // renames of the event [foraging::rp0::flip] to [flip_11] // renames of the event [foraging::rp0::stop] to [stop_12] // renames of the event [foraging::rp0::forage] to [forage_10]