PRISM
=====

Version: 4.7
Date: Fri Jun 10 11:40:03 PKT 2022
Hostname: savelab-PowerEdge-T320
Memory limits: cudd=1g, java(heap)=8g
Command line: prism -javastack 1g -javamaxmem 8g BMS_06_mod.pm -pf 'E[F((st=5 & left_charging_prem=1))]'

Parsing model file "BMS_06_mod.pm"...

Type:        DTMC
Modules:     Initial idle Error Charge_Nom Charge_Knee Charge_Term Discharge_Nom Discharge_Knee Discharge_Term 
Variables:   st vi vx ip bms_err lower_knee_crossed upper_knee_crossed left_charging_prem left_discharging_prem relay_open fully_char fully_dischar knee_cross_det finish_delta_ah_table_pop cal_energy_at_top cal_energy_at_bottom reset_delta_ah_table err_LED a1 a2 a3 a4 a5 a6 a7 a8 

1 property:
(1) E [ F ((st=5&left_charging_prem=1)) ]

---------------------------------------------------------------------

Model checking: E [ F ((st=5&left_charging_prem=1)) ]

Building model...

Computing reachable states...

Reachability (BFS): 41 iterations in 0.10 seconds (average 0.002561, setup 0.00)

Time for model construction: 0.27 seconds.

Warning: Deadlocks detected and fixed in 13656 states

Type:        DTMC
States:      199022 (1 initial)
Transitions: 528277

Transition matrix: 10328 nodes (5 terminal), 528277 minterms, vars: 51r/51c

CTL EU fixpoint: 22 iterations in 0.052 seconds
Processing counterexample trace (17 states long)...

Property satisfied in 1 of 1 initial states.

Time for model checking: 0.079 seconds.

Result: true

Counterexample/witness:
(0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0)
(1,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0)
(1,1,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0)
(1,1,1,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,2,0,0,0,0,0,0,0)
(1,1,1,5,0,0,0,0,0,1,0,0,0,0,0,0,0,0,3,0,0,0,0,0,0,0)
(1,1,1,5,0,0,0,0,0,1,0,0,0,0,0,0,0,0,4,0,0,0,0,0,0,0)
(3,1,1,5,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0)
(3,3,1,5,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,1,0,0,0,0,0)
(3,3,1,5,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,2,0,0,0,0,0)
(3,3,1,1,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,3,0,0,0,0,0)
(3,3,1,1,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,4,0,0,0,0,0)
(8,3,1,1,0,1,0,1,0,1,0,1,0,0,0,1,0,0,0,0,0,0,0,0,0,0)
(8,1,1,1,0,1,0,1,0,1,0,1,0,0,0,1,0,0,0,0,0,0,0,0,0,1)
(8,1,10,1,0,1,0,1,0,1,0,1,0,0,0,1,0,0,0,0,0,0,0,0,0,2)
(8,1,10,5,0,1,0,1,0,1,0,1,0,0,0,1,0,0,0,0,0,0,0,0,0,3)
(8,1,10,5,0,1,0,1,0,1,0,1,0,0,0,1,0,0,0,0,0,0,0,0,0,4)
(5,1,10,5,0,0,1,1,0,1,1,0,1,1,1,0,0,0,0,0,0,0,0,0,0,0)

---------------------------------------------------------------------

Note: There was 1 warning during computation.