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

Assertion: P_deadlock_free

Assertion Const Const States Transitions Time Result
P_deadlock_free deliverMOD::rp_ref0::chargeStep=4 deliverMOD::rp_ref0::batteryCapacity=20 25935984 53649520 0.029 seconds true

Assertion: R_outofpower_moves

Assertion Const Const States Transitions Time Result
R_outofpower_moves deliverMOD::rp_ref0::chargeStep=4 deliverMOD::rp_ref0::batteryCapacity=8 8983152 18618736 82.822 seconds 14.075227429698785
R_outofpower_moves deliverMOD::rp_ref0::chargeStep=4 deliverMOD::rp_ref0::batteryCapacity=12 14634096 30295664 183.529 seconds 19.952926881030333
R_outofpower_moves deliverMOD::rp_ref0::chargeStep=4 deliverMOD::rp_ref0::batteryCapacity=16 20285040 41972592 309.496 seconds 25.793420816525206
R_outofpower_moves deliverMOD::rp_ref0::chargeStep=4 deliverMOD::rp_ref0::batteryCapacity=20 25935984 53649520 460.928 seconds 31.68848420483299

Assertion: R_outofpower_deliveries

Assertion Const Const States Transitions Time Result
R_outofpower_deliveries deliverMOD::rp_ref0::chargeStep=4 deliverMOD::rp_ref0::batteryCapacity=8 8983152 18618736 95.828 seconds 0.6895273801121579
R_outofpower_deliveries deliverMOD::rp_ref0::chargeStep=4 deliverMOD::rp_ref0::batteryCapacity=12 14634096 30295664 210.1 seconds 0.8517713406202103
R_outofpower_deliveries deliverMOD::rp_ref0::chargeStep=4 deliverMOD::rp_ref0::batteryCapacity=16 20285040 41972592 337.386 seconds 1.0087499744621522
R_outofpower_deliveries deliverMOD::rp_ref0::chargeStep=4 deliverMOD::rp_ref0::batteryCapacity=20 25935984 53649520 498.381 seconds 1.1689687863444185

Assertion: A_stuck

Assertion Const Const States Transitions Time Result
A_stuck deliverMOD::rp_ref0::chargeStep=4 deliverMOD::rp_ref0::batteryCapacity=20 25935984 53649520 413.017 seconds false