Results of probabilistic analysis of assertions in mail.assertions using PRISM

Assertion: P_deadlock_free

Assertion Const Const Const States Transitions Time Result
P_deadlock_free l=0 deliverMOD::rp_ref0::chargeStep=2 deliverMOD::rp_ref0::batteryCapacity=8 20571606 50776850 0.036 seconds true
P_deadlock_free l=1 deliverMOD::rp_ref0::chargeStep=2 deliverMOD::rp_ref0::batteryCapacity=8 20571606 50776850 0.062 seconds true
P_deadlock_free l=2 deliverMOD::rp_ref0::chargeStep=2 deliverMOD::rp_ref0::batteryCapacity=8 20571606 50776850 0.025 seconds true
P_deadlock_free l=3 deliverMOD::rp_ref0::chargeStep=2 deliverMOD::rp_ref0::batteryCapacity=8 20571606 50776850 0.027 seconds true
P_deadlock_free l=4 deliverMOD::rp_ref0::chargeStep=2 deliverMOD::rp_ref0::batteryCapacity=8 20571606 50776850 0.021 seconds true
P_deadlock_free l=5 deliverMOD::rp_ref0::chargeStep=2 deliverMOD::rp_ref0::batteryCapacity=8 20571606 50776850 0.022 seconds true
P_deadlock_free l=6 deliverMOD::rp_ref0::chargeStep=2 deliverMOD::rp_ref0::batteryCapacity=8 20571606 50776850 0.064 seconds true
P_deadlock_free l=7 deliverMOD::rp_ref0::chargeStep=2 deliverMOD::rp_ref0::batteryCapacity=8 20571606 50776850 0.022 seconds true
P_deadlock_free l=8 deliverMOD::rp_ref0::chargeStep=2 deliverMOD::rp_ref0::batteryCapacity=8 20571606 50776850 0.028 seconds true
P_deadlock_free l=9 deliverMOD::rp_ref0::chargeStep=2 deliverMOD::rp_ref0::batteryCapacity=8 20571606 50776850 0.034 seconds true
P_deadlock_free l=10 deliverMOD::rp_ref0::chargeStep=2 deliverMOD::rp_ref0::batteryCapacity=8 20571606 50776850 0.041 seconds true

Assertion: P_stuck_loc

Assertion Const Const Const States Transitions Time Result
P_stuck_loc l=0 deliverMOD::rp_ref0::chargeStep=2 deliverMOD::rp_ref0::batteryCapacity=8 20571606 50776850 410.645 seconds 1.0
P_stuck_loc l=1 deliverMOD::rp_ref0::chargeStep=2 deliverMOD::rp_ref0::batteryCapacity=8 20571606 50776850 552.779 seconds 0.24222207470110763
P_stuck_loc l=2 deliverMOD::rp_ref0::chargeStep=2 deliverMOD::rp_ref0::batteryCapacity=8 20571606 50776850 581.32 seconds 0.22301973060711916
P_stuck_loc l=3 deliverMOD::rp_ref0::chargeStep=2 deliverMOD::rp_ref0::batteryCapacity=8 20571606 50776850 585.709 seconds 0.17685200158130263
P_stuck_loc l=4 deliverMOD::rp_ref0::chargeStep=2 deliverMOD::rp_ref0::batteryCapacity=8 20571606 50776850 446.958 seconds 0.2581919916153952
P_stuck_loc l=5 deliverMOD::rp_ref0::chargeStep=2 deliverMOD::rp_ref0::batteryCapacity=8 20571606 50776850 584.385 seconds 0.15437812752347763
P_stuck_loc l=6 deliverMOD::rp_ref0::chargeStep=2 deliverMOD::rp_ref0::batteryCapacity=8 20571606 50776850 487.59 seconds 0.24222207470110763
P_stuck_loc l=7 deliverMOD::rp_ref0::chargeStep=2 deliverMOD::rp_ref0::batteryCapacity=8 20571606 50776850 561.763 seconds 0.2230197306071192
P_stuck_loc l=8 deliverMOD::rp_ref0::chargeStep=2 deliverMOD::rp_ref0::batteryCapacity=8 20571606 50776850 573.368 seconds 0.17685200158130265
P_stuck_loc l=9 deliverMOD::rp_ref0::chargeStep=2 deliverMOD::rp_ref0::batteryCapacity=8 20571606 50776850 6.106 seconds 1.0
P_stuck_loc l=10 deliverMOD::rp_ref0::chargeStep=2 deliverMOD::rp_ref0::batteryCapacity=8 20571606 50776850 0.11 seconds 0.0

Assertion: P_stuck_BC

Assertion Const Const Const States Transitions Time Result
P_stuck_BC l=1 deliverMOD::rp_ref0::chargeStep=2 deliverMOD::rp_ref0::batteryCapacity=4 7692850 19016286 125.344 seconds 0.3352852441654426
P_stuck_BC l=2 deliverMOD::rp_ref0::chargeStep=2 deliverMOD::rp_ref0::batteryCapacity=4 7692850 19016286 129.186 seconds 0.21977214543456025
P_stuck_BC l=3 deliverMOD::rp_ref0::chargeStep=2 deliverMOD::rp_ref0::batteryCapacity=4 7692850 19016286 128.157 seconds 0.08859412988115117
P_stuck_BC l=4 deliverMOD::rp_ref0::chargeStep=2 deliverMOD::rp_ref0::batteryCapacity=4 7692850 19016286 99.441 seconds 0.3893441388639083
P_stuck_BC l=5 deliverMOD::rp_ref0::chargeStep=2 deliverMOD::rp_ref0::batteryCapacity=4 7692850 19016286 129.108 seconds 0.03034715353521035
P_stuck_BC l=6 deliverMOD::rp_ref0::chargeStep=2 deliverMOD::rp_ref0::batteryCapacity=4 7692850 19016286 122.265 seconds 0.3352852441654426
P_stuck_BC l=7 deliverMOD::rp_ref0::chargeStep=2 deliverMOD::rp_ref0::batteryCapacity=4 7692850 19016286 131.965 seconds 0.2197721454345602
P_stuck_BC l=8 deliverMOD::rp_ref0::chargeStep=2 deliverMOD::rp_ref0::batteryCapacity=4 7692850 19016286 145.699 seconds 0.08859412988115117
P_stuck_BC l=1 deliverMOD::rp_ref0::chargeStep=2 deliverMOD::rp_ref0::batteryCapacity=6 14134648 34914476 294.774 seconds 0.2771285200559171
P_stuck_BC l=2 deliverMOD::rp_ref0::chargeStep=2 deliverMOD::rp_ref0::batteryCapacity=6 14134648 34914476 341.23 seconds 0.22536102865730856
P_stuck_BC l=3 deliverMOD::rp_ref0::chargeStep=2 deliverMOD::rp_ref0::batteryCapacity=6 14134648 34914476 329.426 seconds 0.142761979614284
P_stuck_BC l=4 deliverMOD::rp_ref0::chargeStep=2 deliverMOD::rp_ref0::batteryCapacity=6 14134648 34914476 264.08 seconds 0.30642442734238917
P_stuck_BC l=5 deliverMOD::rp_ref0::chargeStep=2 deliverMOD::rp_ref0::batteryCapacity=6 14134648 34914476 328.72 seconds 0.10436472344095786
P_stuck_BC l=6 deliverMOD::rp_ref0::chargeStep=2 deliverMOD::rp_ref0::batteryCapacity=6 14134648 34914476 302.19 seconds 0.2771285200559171
P_stuck_BC l=7 deliverMOD::rp_ref0::chargeStep=2 deliverMOD::rp_ref0::batteryCapacity=6 14134648 34914476 314.314 seconds 0.22536102865730856
P_stuck_BC l=8 deliverMOD::rp_ref0::chargeStep=2 deliverMOD::rp_ref0::batteryCapacity=6 14134648 34914476 317.895 seconds 0.142761979614284
P_stuck_BC l=1 deliverMOD::rp_ref0::chargeStep=2 deliverMOD::rp_ref0::batteryCapacity=8 20571606 50776850 546.662 seconds 0.24222207470110763
P_stuck_BC l=2 deliverMOD::rp_ref0::chargeStep=2 deliverMOD::rp_ref0::batteryCapacity=8 20571606 50776850 560.271 seconds 0.22301973060711916
P_stuck_BC l=3 deliverMOD::rp_ref0::chargeStep=2 deliverMOD::rp_ref0::batteryCapacity=8 20571606 50776850 577.967 seconds 0.17685200158130263
P_stuck_BC l=4 deliverMOD::rp_ref0::chargeStep=2 deliverMOD::rp_ref0::batteryCapacity=8 20571606 50776850 480.911 seconds 0.2581919916153952
P_stuck_BC l=5 deliverMOD::rp_ref0::chargeStep=2 deliverMOD::rp_ref0::batteryCapacity=8 20571606 50776850 555.943 seconds 0.15437812752347763
P_stuck_BC l=6 deliverMOD::rp_ref0::chargeStep=2 deliverMOD::rp_ref0::batteryCapacity=8 20571606 50776850 557.419 seconds 0.24222207470110763
P_stuck_BC l=7 deliverMOD::rp_ref0::chargeStep=2 deliverMOD::rp_ref0::batteryCapacity=8 20571606 50776850 565.95 seconds 0.2230197306071192
P_stuck_BC l=8 deliverMOD::rp_ref0::chargeStep=2 deliverMOD::rp_ref0::batteryCapacity=8 20571606 50776850 588.331 seconds 0.17685200158130265

Assertion: P_stuck_CP

Assertion Const Const Const States Transitions Time Result
P_stuck_CP l=1 deliverMOD::rp_ref0::chargeStep=1 deliverMOD::rp_ref0::batteryCapacity=8 21043022 51956842 512.264 seconds 0.2547194301284873
P_stuck_CP l=2 deliverMOD::rp_ref0::chargeStep=1 deliverMOD::rp_ref0::batteryCapacity=8 21043022 51956842 536.02 seconds 0.22035952828045685
P_stuck_CP l=3 deliverMOD::rp_ref0::chargeStep=1 deliverMOD::rp_ref0::batteryCapacity=8 21043022 51956842 562.269 seconds 0.16516602375439654
P_stuck_CP l=4 deliverMOD::rp_ref0::chargeStep=1 deliverMOD::rp_ref0::batteryCapacity=8 21043022 51956842 474.191 seconds 0.27390926920173914
P_stuck_CP l=5 deliverMOD::rp_ref0::chargeStep=1 deliverMOD::rp_ref0::batteryCapacity=8 21043022 51956842 530.108 seconds 0.1408441998518652
P_stuck_CP l=6 deliverMOD::rp_ref0::chargeStep=1 deliverMOD::rp_ref0::batteryCapacity=8 21043022 51956842 514.676 seconds 0.2547194301284873
P_stuck_CP l=7 deliverMOD::rp_ref0::chargeStep=1 deliverMOD::rp_ref0::batteryCapacity=8 21043022 51956842 532.151 seconds 0.22035952828045685
P_stuck_CP l=8 deliverMOD::rp_ref0::chargeStep=1 deliverMOD::rp_ref0::batteryCapacity=8 21043022 51956842 562.367 seconds 0.16516602375439654
P_stuck_CP l=1 deliverMOD::rp_ref0::chargeStep=2 deliverMOD::rp_ref0::batteryCapacity=8 20571606 50776850 538.708 seconds 0.24222207470110763
P_stuck_CP l=2 deliverMOD::rp_ref0::chargeStep=2 deliverMOD::rp_ref0::batteryCapacity=8 20571606 50776850 527.818 seconds 0.22301973060711916
P_stuck_CP l=3 deliverMOD::rp_ref0::chargeStep=2 deliverMOD::rp_ref0::batteryCapacity=8 20571606 50776850 581.591 seconds 0.17685200158130263
P_stuck_CP l=4 deliverMOD::rp_ref0::chargeStep=2 deliverMOD::rp_ref0::batteryCapacity=8 20571606 50776850 492.444 seconds 0.2581919916153952
P_stuck_CP l=5 deliverMOD::rp_ref0::chargeStep=2 deliverMOD::rp_ref0::batteryCapacity=8 20571606 50776850 583.469 seconds 0.15437812752347763
P_stuck_CP l=6 deliverMOD::rp_ref0::chargeStep=2 deliverMOD::rp_ref0::batteryCapacity=8 20571606 50776850 533.766 seconds 0.24222207470110763
P_stuck_CP l=7 deliverMOD::rp_ref0::chargeStep=2 deliverMOD::rp_ref0::batteryCapacity=8 20571606 50776850 571.42 seconds 0.2230197306071192
P_stuck_CP l=8 deliverMOD::rp_ref0::chargeStep=2 deliverMOD::rp_ref0::batteryCapacity=8 20571606 50776850 562.876 seconds 0.17685200158130265
P_stuck_CP l=1 deliverMOD::rp_ref0::chargeStep=3 deliverMOD::rp_ref0::batteryCapacity=8 20430520 50447004 553.883 seconds 0.23786248841631005
P_stuck_CP l=2 deliverMOD::rp_ref0::chargeStep=3 deliverMOD::rp_ref0::batteryCapacity=8 20430520 50447004 578.208 seconds 0.2231369031857097
P_stuck_CP l=3 deliverMOD::rp_ref0::chargeStep=3 deliverMOD::rp_ref0::batteryCapacity=8 20430520 50447004 586.052 seconds 0.1812946902911461
P_stuck_CP l=4 deliverMOD::rp_ref0::chargeStep=3 deliverMOD::rp_ref0::batteryCapacity=8 20430520 50447004 519.107 seconds 0.2517781804617701
P_stuck_CP l=5 deliverMOD::rp_ref0::chargeStep=3 deliverMOD::rp_ref0::batteryCapacity=8 20430520 50447004 600.032 seconds 0.16017795025018228
P_stuck_CP l=6 deliverMOD::rp_ref0::chargeStep=3 deliverMOD::rp_ref0::batteryCapacity=8 20430520 50447004 556.851 seconds 0.23786248841631005
P_stuck_CP l=7 deliverMOD::rp_ref0::chargeStep=3 deliverMOD::rp_ref0::batteryCapacity=8 20430520 50447004 585.641 seconds 0.2231369031857097
P_stuck_CP l=8 deliverMOD::rp_ref0::chargeStep=3 deliverMOD::rp_ref0::batteryCapacity=8 20430520 50447004 588.893 seconds 0.1812946902911461
P_stuck_CP l=1 deliverMOD::rp_ref0::chargeStep=4 deliverMOD::rp_ref0::batteryCapacity=8 20289434 50117158 565.276 seconds 0.2358433665321688
P_stuck_CP l=2 deliverMOD::rp_ref0::chargeStep=4 deliverMOD::rp_ref0::batteryCapacity=8 20289434 50117158 578.694 seconds 0.22312843262884013
P_stuck_CP l=3 deliverMOD::rp_ref0::chargeStep=4 deliverMOD::rp_ref0::batteryCapacity=8 20289434 50117158 568.653 seconds 0.18323461979202682
P_stuck_CP l=4 deliverMOD::rp_ref0::chargeStep=4 deliverMOD::rp_ref0::batteryCapacity=8 20289434 50117158 510.067 seconds 0.24905539028936324
P_stuck_CP l=5 deliverMOD::rp_ref0::chargeStep=4 deliverMOD::rp_ref0::batteryCapacity=8 20289434 50117158 602.251 seconds 0.1629424420721745
P_stuck_CP l=6 deliverMOD::rp_ref0::chargeStep=4 deliverMOD::rp_ref0::batteryCapacity=8 20289434 50117158 531.31 seconds 0.2358433665321688
P_stuck_CP l=7 deliverMOD::rp_ref0::chargeStep=4 deliverMOD::rp_ref0::batteryCapacity=8 20289434 50117158 598.528 seconds 0.2231284326288402
P_stuck_CP l=8 deliverMOD::rp_ref0::chargeStep=4 deliverMOD::rp_ref0::batteryCapacity=8 20289434 50117158 611.9 seconds 0.18323461979202682

Assertion: R_stuck_move

Assertion Const Const States Transitions Time Result
R_stuck_move deliverMOD::rp_ref0::chargeStep=2 deliverMOD::rp_ref0::batteryCapacity=8 20571606 50776850 567.232 seconds 0.0

Assertion: R_stuck_deliveries

Assertion Const Const States Transitions Time Result
R_stuck_deliveries deliverMOD::rp_ref0::chargeStep=2 deliverMOD::rp_ref0::batteryCapacity=8 20571606 50776850 668.45 seconds 0.0

Assertion: A_stuck

Assertion Const Const States Transitions Time Result
A_stuck deliverMOD::rp_ref0::chargeStep=2 deliverMOD::rp_ref0::batteryCapacity=8

Assertion: P_not_stuck

Assertion Const Const States Transitions Time Result
P_not_stuck deliverMOD::rp_ref0::chargeStep=2 deliverMOD::rp_ref0::batteryCapacity=8 20571606 50776850 4.134 seconds 0.0