diff --git a/prism/src/explicit/AccumulationProductComplexCounting.java b/prism/src/explicit/AccumulationProductComplexCounting.java index 35101c54..90bd48a7 100644 --- a/prism/src/explicit/AccumulationProductComplexCounting.java +++ b/prism/src/explicit/AccumulationProductComplexCounting.java @@ -1,12 +1,8 @@ package explicit; import java.util.BitSet; -import java.util.Vector; -import explicit.rewards.MCRewards; -import explicit.rewards.MDPRewards; import explicit.rewards.Rewards; -import parser.ast.ExpressionAccumulation; import prism.IntegerBound; import prism.PrismException; diff --git a/prism/src/explicit/AccumulationProductComplexRegular.java b/prism/src/explicit/AccumulationProductComplexRegular.java index 9e9149d6..f7aeadcd 100644 --- a/prism/src/explicit/AccumulationProductComplexRegular.java +++ b/prism/src/explicit/AccumulationProductComplexRegular.java @@ -2,16 +2,12 @@ package explicit; import java.util.ArrayList; import java.util.BitSet; -import java.util.Vector; import automata.finite.DeterministicFiniteAutomaton; import automata.finite.EdgeLabel; import automata.finite.NondeterministicFiniteAutomaton; import automata.finite.State; -import explicit.rewards.MCRewards; -import explicit.rewards.MDPRewards; import explicit.rewards.Rewards; -import parser.ast.ExpressionAccumulation; import parser.ast.ExpressionRegular; import prism.PrismException; import prism.PrismSettings; @@ -124,7 +120,6 @@ public class AccumulationProductComplexRegular extends Accumula AccumulationState from_accstate = result.accStates.getById(from_state.getSecondState()); // Get step weights - // THIS IS DIFFERENT FROM ABOVE! double[] weights = ctx.getWeights(from_state.getFirstState(), choice_i); // Update accumulation product state, store it and get its ID. diff --git a/prism/src/explicit/AccumulationProductSimple.java b/prism/src/explicit/AccumulationProductSimple.java index b65c2e3e..3283e1dd 100644 --- a/prism/src/explicit/AccumulationProductSimple.java +++ b/prism/src/explicit/AccumulationProductSimple.java @@ -5,7 +5,6 @@ import java.util.BitSet; import java.util.Iterator; import java.util.Map; -import parser.ast.ExpressionAccumulation; import prism.PrismException; import common.Dottable; diff --git a/prism/src/explicit/AccumulationProductSimpleRegular.java b/prism/src/explicit/AccumulationProductSimpleRegular.java index 05747d98..c0247c24 100644 --- a/prism/src/explicit/AccumulationProductSimpleRegular.java +++ b/prism/src/explicit/AccumulationProductSimpleRegular.java @@ -2,16 +2,12 @@ package explicit; import java.util.ArrayList; import java.util.BitSet; -import java.util.Vector; import automata.finite.DeterministicFiniteAutomaton; import automata.finite.EdgeLabel; import automata.finite.NondeterministicFiniteAutomaton; import automata.finite.State; -import explicit.rewards.MCRewards; -import explicit.rewards.MDPRewards; import explicit.rewards.Rewards; -import parser.ast.ExpressionAccumulation; import parser.ast.ExpressionRegular; import prism.PrismException; import prism.PrismSettings; diff --git a/prism/src/explicit/AccumulationTransformation.java b/prism/src/explicit/AccumulationTransformation.java index 76932c20..7de6c96d 100644 --- a/prism/src/explicit/AccumulationTransformation.java +++ b/prism/src/explicit/AccumulationTransformation.java @@ -21,13 +21,13 @@ public class AccumulationTransformation implements Mode final protected Expression originalExpression; final protected M originalModel; final protected BitSet statesOfInterest; - final protected ProbModelChecker mc; + final protected StateModelChecker mc; protected Expression transformedExpression; protected AccumulationProduct product; public AccumulationTransformation( - ProbModelChecker mc, + StateModelChecker mc, M originalModel, Expression expr, BitSet statesOfInterest) throws PrismException{ super();