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 | 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 | 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 | Const | Const | States | Transitions | Time | Result |
---|---|---|---|---|---|---|
A_stuck | deliverMOD::rp_ref0::chargeStep=4 | deliverMOD::rp_ref0::batteryCapacity=20 | 25935984 | 53649520 | 413.017 seconds | false |