@@ -259,13 +259,13 @@ function _bellman_helper!(
259
259
workspace:: ProductWorkspace ,
260
260
strategy_cache:: AbstractStrategyCache ,
261
261
Vres,
262
- V,
262
+ V:: AbstractArray{R} ,
263
263
dfa:: DFA ,
264
264
mp:: IntervalMarkovProcess ,
265
265
lf:: ProbabilisticLabelling ,
266
266
upper_bound = false ,
267
267
maximize = true ,
268
- )
268
+ ) where {R}
269
269
W = workspace. intermediate_values
270
270
271
271
@inbounds for state in dfa
@@ -274,12 +274,20 @@ function _bellman_helper!(
274
274
# Select the value function for the current DFA state
275
275
# according to the appropriate DFA transition function
276
276
map! (W, CartesianIndices (state_values (mp))) do idx
277
+ v = zero (R)
278
+
279
+ for (label, prob) in enumerate (lf[idx])
280
+ new_dfa_state = dfa[state, label]
281
+ v += prob * V[idx, new_dfa_state]
282
+ end
283
+
284
+ return v
277
285
278
- A = lf[idx] # (Lx1) for IMDP state s', get all the p(f | s') for each label
279
- B = V[idx, :] # (Mx1) fir IMDP state s', get all V(s', z') for each DFA state
280
- C = onehot (transition (dfa))[state, :, :] # (LxM)
286
+ # A = lf[idx] #(Lx1) for IMDP state s', get all the p(f | s') for each label
287
+ # B = V[idx, :] #(Mx1) fir IMDP state s', get all V(s', z') for each DFA state
288
+ # C = onehot(transition(dfa))[state, :, :] #(LxM)
281
289
282
- return B' * C' * A
290
+ # return B' * C' * A
283
291
end
284
292
285
293
# For each state in the product process, compute the Bellman operator
0 commit comments