param: convert expressions to functions earlier in model building

Already convert the expression to a function for ChoiceListFlexi,
as this will allow filtering zero probability updates (next commit)


git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11653 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/param/ChoiceListFlexi.java

@@ -48,7 +48,7 @@ public class ChoiceListFlexi //implements Choice
 	// Probabilities/rates are already evaluated, target states are not
 	// but are just stored as lists of updates (for efficiency)
 	protected List<List<Update>> updates;
-	protected List<Expression> probability;
+	protected List<Function> probability;
 
 	/**
 	 * Create empty choice.
@@ -56,7 +56,7 @@ public class ChoiceListFlexi //implements Choice
 	public ChoiceListFlexi()
 	{
 		updates = new ArrayList<List<Update>>();
-		probability = new ArrayList<Expression>();
+		probability = new ArrayList<Function>();
 	}
 
 	/**
@@ -74,8 +74,8 @@ public class ChoiceListFlexi //implements Choice
 				listNew.add(up);
 			}
 		}
-		probability = new ArrayList<Expression>(ch.size());
-		for (Expression p : ch.probability) {
+		probability = new ArrayList<Function>(ch.size());
+		for (Function p : ch.probability) {
 			probability.add(p);
 		}
 	}
@@ -97,7 +97,7 @@ public class ChoiceListFlexi //implements Choice
 	 * @param probability Probability (or rate) of the transition
 	 * @param ups List of Update objects defining transition
 	 */
-	public void add(Expression probability, List<Update> ups)
+	public void add(Function probability, List<Update> ups)
 	{
 		this.updates.add(ups);
 		this.probability.add(probability);
@@ -122,7 +122,7 @@ public class ChoiceListFlexi //implements Choice
 	{
 		List<Update> list;
 		int i, j, n, n2;
-		Expression pi;
+		Function pi;
 
 		n = ch.size();
 		n2 = size();
@@ -139,7 +139,7 @@ public class ChoiceListFlexi //implements Choice
 				for (Update u : ch.updates.get(i)) {
 					list.add(u);
 				}
-				add((Expression)Expression.Times(pi, getProbability(j)).simplify(), list);
+				add(pi.multiply(getProbability(j)), list);
 			}
 		}
 		// Modify elements of current choice to get (0,j) elements of product
@@ -148,7 +148,7 @@ public class ChoiceListFlexi //implements Choice
 			for (Update u : ch.updates.get(0)) {
 				updates.get(j).add(u);
 			}
-			probability.set(j, (Expression)Expression.Times(pi, getProbability(j)).simplify());
+			probability.set(j, pi.multiply(getProbability(j)));
 		}
 	}
 
@@ -223,7 +223,7 @@ public class ChoiceListFlexi //implements Choice
 			up.update(currentState, newState);
 	}
 
-	public Expression getProbability(int i)
+	public Function getProbability(int i)
 	{
 		return probability.get(i);
 	}

prism/src/param/ModelBuilder.java

@@ -378,7 +378,7 @@ public final class ModelBuilder extends PrismComponent
 		if (modelType != ModelType.DTMC && modelType != ModelType.CTMC && modelType != ModelType.MDP) {
 			throw new PrismNotSupportedException("Unsupported model type: " + modelType);
 		}
-		SymbolicEngine engine = new SymbolicEngine(modulesFile);
+		SymbolicEngine engine = new SymbolicEngine(modulesFile, this, functionFactory);
 
 		if (modulesFile.getInitialStates() != null) {
 			throw new PrismNotSupportedException("Explicit model construction does not support multiple initial states");
@@ -410,8 +410,7 @@ public final class ModelBuilder extends PrismComponent
 				Function sumOutForChoice = functionFactory.getZero();
 				for (int succNr = 0; succNr < numSuccessors; succNr++) {
 					ChoiceListFlexi succ = tranlist.getChoice(choiceNr);
-					Expression probExpr = succ.getProbability(succNr);
-					Function probFunc = expr2function(functionFactory, probExpr);
+					Function probFunc = succ.getProbability(succNr);
 					if (computeSumOut)
 						sumOut = sumOut.add(probFunc);
 					if (checkChoiceSumEqualsOne)
@@ -443,12 +442,12 @@ public final class ModelBuilder extends PrismComponent
 				for (int succNr = 0; succNr < numSuccessors; succNr++) {
 					ChoiceListFlexi succ = tranlist.getChoice(choiceNr);
 					State stateNew = succ.computeTarget(succNr, state);
-					Expression probExpr = succ.getProbability(succNr);
+					Function probFn = succ.getProbability(succNr);
 					// divide by sumOut
 					// for DTMC, this normalises over the choices
 					// for CTMC this builds the embedded DTMC
 					// for MDP this does nothing (sumOut is set to 1)
-					Function probFn = expr2function(functionFactory, probExpr).divide(sumOut);
+					probFn = probFn.divide(sumOut);
 					model.addTransition(permut[states.get(stateNew)], probFn, action);
 				}
 				if (isNonDet) {

prism/src/param/SymbolicEngine.java

@@ -67,9 +67,14 @@ public class SymbolicEngine
 	// Element j of enabledModules is a BitSet showing modules which enable action j
 	// (where j=0 denotes independent, otherwise 1-indexed action label)
 	protected BitSet enabledModules[];
+	protected ModelBuilder modelBuilder;
+	protected FunctionFactory functionFactory;
 
-	public SymbolicEngine(ModulesFile modulesFile)
+	public SymbolicEngine(ModulesFile modulesFile, ModelBuilder modelBuilder, FunctionFactory functionFactory)
 	{
+		this.modelBuilder = modelBuilder;
+		this.functionFactory = functionFactory;
+
 		// Get info from model
 		this.modulesFile = modulesFile;
 		modelType = modulesFile.getModelType();
@@ -285,7 +290,13 @@ public class SymbolicEngine
 			p = (Expression) p.deepCopy().evaluatePartially(state, varMap);
 			list = new ArrayList<Update>();
 			list.add(ups.getUpdate(i));
-			ch.add(p, list);
+
+			try {
+				Function pFn = modelBuilder.expr2function(functionFactory, p);
+				ch.add(pFn, list);
+			} catch (PrismException e) {
+				throw new PrismLangException(e.getMessage());
+			}
 		}
 
 		return ch;

prism/src/param/TransitionList.java

@@ -202,7 +202,7 @@ public class TransitionList
 	/**
 	 * Get the probability/rate of a transition, specified by its index.
 	 */
-	public Expression getTransitionProbability(int index)
+	public Function getTransitionProbability(int index)
 	{
 		return getChoiceOfTransition(index).getProbability(transitionOffsets.get(index));
 	}
@@ -256,10 +256,8 @@ public class TransitionList
 	public boolean isDeterministic()
 	{
 		if(numTransitions == 1) {
-			Expression e = getChoice(0).getProbability(0);
-			if(Expression.isDouble(e)) {
-				return (Double)((ExpressionLiteral)e).getValue() == 1.0;
-			}
+			Function e = getChoice(0).getProbability(0);
+			return e.isOne();
 		}
 		return false;
 	}