diff --git a/prism/src/param/ModelBuilder.java b/prism/src/param/ModelBuilder.java index 1b67a5e4..f13b41f9 100644 --- a/prism/src/param/ModelBuilder.java +++ b/prism/src/param/ModelBuilder.java @@ -28,18 +28,21 @@ package param; import java.util.LinkedList; import java.util.List; +import java.util.Map; import parser.State; +import parser.ast.ConstantList; import parser.ast.Expression; import parser.ast.ExpressionBinaryOp; import parser.ast.ExpressionConstant; import parser.ast.ExpressionLiteral; import parser.ast.ExpressionUnaryOp; import parser.ast.ModulesFile; +import parser.visitor.ASTTraverseModify; import prism.ModelType; import prism.PrismComponent; import prism.PrismException; -import prism.PrismLog; +import prism.PrismLangException; import prism.PrismSettings; import explicit.IndexedSet; import explicit.StateStorage; @@ -69,6 +72,9 @@ public final class ModelBuilder extends PrismComponent /** maximal error probability of DAG function representation */ private double dagMaxError; + /** local storage made static for use in anonymous class */ + private static Map constExprs; + /** * Constructor */ @@ -206,7 +212,21 @@ public final class ModelBuilder extends PrismComponent // build model time = System.currentTimeMillis(); - modulesFile = (ModulesFile) modulesFile.deepCopy().replaceConstants(modulesFile.getConstantValues()).simplify(); + // First, set values for any constants in the model + // (but do this *symbolically* - partly because some constants are parameters and therefore unknown, + // but also to keep values like 1/3 as expressions rather than being converted to doubles, + // resulting in a loss of precision) + ConstantList constantList = modulesFile.getConstantList(); + constExprs = constantList.evaluateConstantsPartially(modulesFile.getUndefinedConstantValues(), null); + modulesFile = (ModulesFile) modulesFile.deepCopy(); + modulesFile = (ModulesFile) modulesFile.accept(new ASTTraverseModify() + { + public Object visit(ExpressionConstant e) throws PrismLangException + { + Expression expr = constExprs.get(e.getName()); + return (expr != null) ? expr.deepCopy() : e; + } + }); ParamModel modelExpl = constructModel(modulesFile); time = System.currentTimeMillis() - time; diff --git a/prism/src/parser/ast/ConstantList.java b/prism/src/parser/ast/ConstantList.java index 533c1d7c..02dc16bf 100644 --- a/prism/src/parser/ast/ConstantList.java +++ b/prism/src/parser/ast/ConstantList.java @@ -26,6 +26,8 @@ package parser.ast; +import java.util.HashMap; +import java.util.Map; import java.util.Vector; import parser.*; @@ -288,6 +290,71 @@ public class ConstantList extends ASTElement return allValues; } + /** + * Set values for some undefined constants, then partially evaluate values for constants where possible + * and return a map from constant names to the Expression representing its value. + * Argument 'someValues' contains values for undefined ones, can be null if all already defined. + * Argument 'otherValues' contains any other values which may be needed, null if none. + */ + public Map evaluateConstantsPartially(Values someValues, Values otherValues) throws PrismLangException + { + ConstantList cl; + Expression e; + int i, j, n, numToEvaluate; + Type t = null; + ExpressionIdent s; + + // Create new copy of this ConstantList + // (copy existing constant definitions, add new ones where undefined) + cl = new ConstantList(); + n = constants.size(); + for (i = 0; i < n; i++) { + s = getConstantNameIdent(i); + e = getConstant(i); + t = getConstantType(i); + if (e != null) { + cl.addConstant((ExpressionIdent)s.deepCopy(), e.deepCopy(), t); + } else { + // Create new literal expression using values passed in (if possible and needed) + if (someValues != null && (j = someValues.getIndexOf(s.getName())) != -1) { + cl.addConstant((ExpressionIdent) s.deepCopy(), new ExpressionLiteral(t, t.castValueTo(someValues.getValue(j))), t); + } + } + } + numToEvaluate = cl.size(); + + // Now add constants corresponding to the 'otherValues' argument to the new constant list + if (otherValues != null) { + n = otherValues.getNumValues(); + for (i = 0; i < n; i++) { + Type iType = otherValues.getType(i); + cl.addConstant(new ExpressionIdent(otherValues.getName(i)), new ExpressionLiteral(iType, iType.castValueTo(otherValues.getValue(i))), iType); + } + } + + // Go trough and expand definition of each constant + // (i.e. replace other constant references with their definitions) + // Note: work with new copy of constant list, don't need to expand 'otherValues' ones. + for (i = 0; i < numToEvaluate; i++) { + try { + e = (Expression)cl.getConstant(i).expandConstants(cl); + cl.setConstant(i, e); + } catch (PrismLangException ex) { + cl.setConstant(i, null); + } + } + + // Store final expressions for each constant in a map and return + Map constExprs = new HashMap<>(); + for (i = 0; i < numToEvaluate; i++) { + if (cl.getConstant(i) != null) { + constExprs.put(cl.getConstantName(i), cl.getConstant(i).deepCopy()); + } + } + + return constExprs; + } + // Methods required for ASTElement: /** diff --git a/prism/src/parser/ast/ModulesFile.java b/prism/src/parser/ast/ModulesFile.java index 00e14cd7..965389b2 100644 --- a/prism/src/parser/ast/ModulesFile.java +++ b/prism/src/parser/ast/ModulesFile.java @@ -66,7 +66,9 @@ public class ModulesFile extends ASTElement private Vector varNames; private Vector varTypes; - // actual values of (some or all) constants + // Values set for undefined constants (null if none) + private Values undefinedConstantValues; + // Actual values of (some or all) constants private Values constantValues; // Constructor @@ -89,6 +91,7 @@ public class ModulesFile extends ASTElement varDecls = new Vector(); varNames = new Vector(); varTypes = new Vector(); + undefinedConstantValues = null; constantValues = null; } @@ -937,6 +940,7 @@ public class ModulesFile extends ASTElement */ public void setUndefinedConstants(Values someValues) throws PrismLangException { + undefinedConstantValues = someValues == null ? null : new Values(someValues); constantValues = constantList.evaluateConstants(someValues, null); semanticCheckAfterConstants(this, null); } @@ -949,6 +953,7 @@ public class ModulesFile extends ASTElement */ public void setSomeUndefinedConstants(Values someValues) throws PrismLangException { + undefinedConstantValues = someValues == null ? null : new Values(someValues); constantValues = constantList.evaluateSomeConstants(someValues, null); semanticCheckAfterConstants(this, null); } @@ -962,6 +967,15 @@ public class ModulesFile extends ASTElement return constantList.isDefinedConstant(name); } + /** + * Get access to the values that have been provided for undefined constants in the model + * (e.g. via the method {@link #setUndefinedConstants(Values)}). + */ + public Values getUndefinedConstantValues() + { + return undefinedConstantValues; + } + /** * Get access to the values for all constants in the model, including the * undefined constants set previously via the method {@link #setUndefinedConstants(Values)}.