Add ? operator to explicit engine.

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

prism/src/explicit/StateModelChecker.java

@@ -45,6 +45,7 @@ import parser.ast.ExpressionFilter;
 import parser.ast.ExpressionFilter.FilterOperator;
 import parser.ast.ExpressionFormula;
 import parser.ast.ExpressionFunc;
+import parser.ast.ExpressionITE;
 import parser.ast.ExpressionIdent;
 import parser.ast.ExpressionLabel;
 import parser.ast.ExpressionLiteral;
@@ -270,8 +271,12 @@ public class StateModelChecker
 	{
 		StateValues res = null;
 
+		// If-then-else
+		if (expr instanceof ExpressionITE) {
+			res = checkExpressionITE(model, (ExpressionITE) expr);
+		}
 		// Binary ops
-		if (expr instanceof ExpressionBinaryOp) {
+		else if (expr instanceof ExpressionBinaryOp) {
 			res = checkExpressionBinaryOp(model, (ExpressionBinaryOp) expr);
 		}
 		// Unary ops
@@ -327,6 +332,34 @@ public class StateModelChecker
 		return res;
 	}
 
+	/**
+	 * Model check a binary operator.
+	 */
+	protected StateValues checkExpressionITE(Model model, ExpressionITE expr) throws PrismException
+	{
+		StateValues res1 = null, res2 = null, res3 = null;
+		
+		// Check operands recursively
+		try {
+			res1 = checkExpression(model, expr.getOperand1());
+			res2 = checkExpression(model, expr.getOperand2());
+			res3 = checkExpression(model, expr.getOperand3());
+		} catch (PrismException e) {
+			if (res1 != null)
+				res1.clear();
+			if (res2 != null)
+				res2.clear();
+			throw e;
+		}
+		
+		// Apply operation
+		res3.applyITE(res1, res2);
+		res1.clear();
+		res2.clear();
+		
+		return res3;
+	}
+
 	/**
 	 * Model check a binary operator.
 	 */

prism/src/explicit/StateValues.java

@@ -291,6 +291,54 @@ public class StateValues
 		valuesB.set(i, val);
 	}
 
+	/**
+	 * Modify the vector by applying If-Then-Else, i.e. {@code svIf} ? {@code svThen} : {@code this}.
+	 */
+	public void applyITE(StateValues svIf, StateValues svThen) throws PrismException
+	{
+		if (!(svIf.type instanceof TypeBool)) {
+			throw new PrismException("Type error in ? operator");
+		}
+		if (type instanceof TypeInt) {
+			if (svThen.type instanceof TypeInt) {
+				for (int i = 0; i < size; i++) {
+					valuesI[i] = svIf.valuesB.get(i) ? svThen.valuesI[i] : valuesI[i];
+				}
+			} else if (svThen.type instanceof TypeDouble) {
+				valuesD = new double[size];
+				type = TypeDouble.getInstance();
+				for (int i = 0; i < size; i++) {
+					valuesD[i] = svIf.valuesB.get(i) ? svThen.valuesD[i] : valuesD[i];
+				}
+				valuesI = null;
+			} else {
+				throw new PrismException("Type error in ? operator");
+			}
+		} else if (type instanceof TypeDouble) {
+			if (svThen.type instanceof TypeInt) {
+				for (int i = 0; i < size; i++) {
+					valuesD[i] = svIf.valuesB.get(i) ? svThen.valuesI[i] : valuesD[i];
+				}
+			} else if (svThen.type instanceof TypeDouble) {
+				for (int i = 0; i < size; i++) {
+					valuesD[i] = svIf.valuesB.get(i) ? svThen.valuesD[i] : valuesD[i];
+				}
+			} else {
+				throw new PrismException("Type error in ? operator");
+			}
+		} else if (type instanceof TypeBool) {
+			if (svThen.type instanceof TypeBool) {
+				for (int i = svIf.valuesB.nextSetBit(0); i >= 0; i = svIf.valuesB.nextSetBit(i + 1)) {
+					valuesB.set(i, svThen.valuesB.get(i));
+				}
+			} else {
+				throw new PrismException("Type error in ? operator");
+			}
+		} else {
+			throw new PrismException("Type error in ? operator");
+		}
+	}
+
 	/**
 	 * Modify the vector by applying binary operator {@code op} with second operand {@code sv},
 	 * where {@code op} refers to the codes in {@link ExpressionBinaryOp}.