diff --git a/prism/src/prism/StateModelChecker.java b/prism/src/prism/StateModelChecker.java index f89fdac0..816b3f54 100644 --- a/prism/src/prism/StateModelChecker.java +++ b/prism/src/prism/StateModelChecker.java @@ -122,7 +122,11 @@ public class StateModelChecker implements ModelChecker /** * Additional constructor for creating stripped down StateModelChecker for - * expression to MTBDD conversions. + * expression to MTBDD conversions (no colum variables, no transition function, ...). + *
+ * The dummy model constructed for these purposes has to be cleared by calling + * {@code clearDummyModel()} later. + *
[ REFS: none, DEREFS: none ] */ public StateModelChecker(Prism prism, VarList varList, JDDVars allDDRowVars, JDDVars[] varDDRowVars, Values constantValues) throws PrismException { @@ -135,9 +139,24 @@ public class StateModelChecker implements ModelChecker this.constantValues = constantValues; // Create dummy model reach = null; - allDDRowVars.refAll(); - model = new ProbModel(JDD.Constant(0), JDD.Constant(0), new JDDNode[] {}, new JDDNode[] {}, null, allDDRowVars, new JDDVars(), null, 0, null, null, - null, 0, varList, varDDRowVars, null, constantValues); + model = new ProbModel(JDD.Constant(0), // trans + JDD.Constant(0), // start + new JDDNode[] {}, // state-rew + new JDDNode[] {}, // trans-rew + null, // rewardStructNames + allDDRowVars.copy(), // allDDRowVars + new JDDVars(), // allDDColVars + null, // ddVarNames + 0, // numModules + null, // moduleNames + null, // moduleRowVars + null, // moduleColVars + 0, // numVars + varList, // varList + varDDRowVars, // varDDRowVars + null, // varDDColVars + constantValues // constantValues + ); } /**