|
|
@ -2,16 +2,12 @@ package explicit; |
|
|
|
|
|
|
|
|
import java.util.ArrayList; |
|
|
import java.util.ArrayList; |
|
|
import java.util.BitSet; |
|
|
import java.util.BitSet; |
|
|
import java.util.Vector; |
|
|
|
|
|
|
|
|
|
|
|
import automata.finite.DeterministicFiniteAutomaton; |
|
|
import automata.finite.DeterministicFiniteAutomaton; |
|
|
import automata.finite.EdgeLabel; |
|
|
import automata.finite.EdgeLabel; |
|
|
import automata.finite.NondeterministicFiniteAutomaton; |
|
|
import automata.finite.NondeterministicFiniteAutomaton; |
|
|
import automata.finite.State; |
|
|
import automata.finite.State; |
|
|
import explicit.rewards.MCRewards; |
|
|
|
|
|
import explicit.rewards.MDPRewards; |
|
|
|
|
|
import explicit.rewards.Rewards; |
|
|
import explicit.rewards.Rewards; |
|
|
import parser.ast.ExpressionAccumulation; |
|
|
|
|
|
import parser.ast.ExpressionRegular; |
|
|
import parser.ast.ExpressionRegular; |
|
|
import prism.PrismException; |
|
|
import prism.PrismException; |
|
|
import prism.PrismSettings; |
|
|
import prism.PrismSettings; |
|
|
@ -124,7 +120,6 @@ public class AccumulationProductComplexRegular<M extends Model> extends Accumula |
|
|
AccumulationState<State> from_accstate = result.accStates.getById(from_state.getSecondState()); |
|
|
AccumulationState<State> from_accstate = result.accStates.getById(from_state.getSecondState()); |
|
|
|
|
|
|
|
|
// Get step weights |
|
|
// Get step weights |
|
|
// THIS IS DIFFERENT FROM ABOVE! |
|
|
|
|
|
double[] weights = ctx.getWeights(from_state.getFirstState(), choice_i); |
|
|
double[] weights = ctx.getWeights(from_state.getFirstState(), choice_i); |
|
|
|
|
|
|
|
|
// Update accumulation product state, store it and get its ID. |
|
|
// Update accumulation product state, store it and get its ID. |
|
|
|