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 |
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 |
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 |
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 |