exact/parametric: support if-the-else expressions in properties

+ test case

prism-tests/functionality/verify/param/param-ite.prism

@@ -0,0 +1,10 @@
+dtmc
+
+const double p;
+formula outcome = (s>0 ? s-1 : -1);
+
+module M1
+  s: [0..4] init 0;
+
+  [] s=0 -> 1/2:(s'=0) + 1/8:(s'=1) + 1/8:(s'=2) + 1/8:(s'=3) + 1/8:(s'=4);
+endmodule

prism-tests/functionality/verify/param/param-ite.prism.args

@@ -0,0 +1,2 @@
+-exact -const p=0
+-param p=0:1

prism-tests/functionality/verify/param/param-ite.prism.props

@@ -0,0 +1,7 @@
+// test case: support for if-then-else and formulas in expressions (exact / parametric)
+
+// RESULT: 1/4
+P=?[F outcome=2]
+
+// RESULT: 0
+P=?[G outcome=-1]

prism/src/param/BoxRegion.java

@@ -416,6 +416,24 @@ final class BoxRegion extends Region {
 		return result;
 	}
 	
+	@Override
+	RegionValues ITE(StateValues valuesI, StateValues valuesT, StateValues valuesE)
+	{
+		RegionValues result = new RegionValues(factory);
+		int numStates = valuesI.getNumStates();
+		StateValues values = new StateValues(numStates, factory.getInitialState());
+		for (int state = 0; state < numStates; state++) {
+			if (valuesI.getStateValueAsBoolean(state)) {
+				values.setStateValue(state, valuesT.getStateValue(state));
+			} else {
+				values.setStateValue(state, valuesE.getStateValue(state));
+			}
+		}
+		result.add(this, values);
+
+		return result;
+	}
+
 	/**
 	 * Split region in longest dimension.
 	 * 

prism/src/param/ParamModelChecker.java

@@ -70,6 +70,7 @@ import parser.ast.ExpressionFilter.FilterOperator;
 import parser.ast.ExpressionForAll;
 import parser.ast.ExpressionFormula;
 import parser.ast.ExpressionFunc;
+import parser.ast.ExpressionITE;
 import parser.ast.ExpressionLabel;
 import parser.ast.ExpressionLiteral;
 import parser.ast.ExpressionProb;
@@ -371,6 +372,8 @@ final public class ParamModelChecker extends PrismComponent
 			res = checkExpressionUnaryOp(model, (ExpressionUnaryOp) expr, needStates);
 		} else if (expr instanceof ExpressionBinaryOp) {
 			res = checkExpressionBinaryOp(model, (ExpressionBinaryOp) expr, needStates);
+		} else if (expr instanceof ExpressionITE) {
+			res = checkExpressionITE(model, (ExpressionITE) expr, needStates);
 		} else if (expr instanceof ExpressionLabel) {
 			res = checkExpressionLabel(model, (ExpressionLabel) expr, needStates);
 		} else if (expr instanceof ExpressionFormula) {
@@ -466,6 +469,21 @@ final public class ParamModelChecker extends PrismComponent
 		return res1.binaryOp(parserBinaryOpToRegionOp(expr.getOperator()), res2);
 	}
 
+	/**
+	 * Model check an If-Then-Else operator.
+	 */
+	protected RegionValues checkExpressionITE(ParamModel model, ExpressionITE expr, BitSet needStates) throws PrismException
+	{
+		RegionValues resI = checkExpression(model, expr.getOperand1(), needStates);
+		RegionValues resT = checkExpression(model, expr.getOperand2(), needStates);
+		RegionValues resE = checkExpression(model, expr.getOperand3(), needStates);
+		resI.clearNotNeeded(needStates);
+		resT.clearNotNeeded(needStates);
+		resE.clearNotNeeded(needStates);
+
+		return resI.ITE(resT, resE);
+	}
+
 	/**
 	 * Model check a label.
 	 */

prism/src/param/Region.java

@@ -94,6 +94,8 @@ abstract class Region {
 	
 	abstract RegionValues binaryOp(int op, StateValues values1, StateValues values2);
 
+	abstract RegionValues ITE(StateValues valueI, StateValues valueT, StateValues valueE);
+
 	/**
 	 * Splits this region into several parts.
 	 * How this is done exactly depends on the implementation in derived

prism/src/param/RegionIntersection.java

@@ -30,7 +30,7 @@ package param;
  * Maintains the intersection of two regions.
  * This class is to be used in combination with
  * {@code RegionValuesIntersections} to iterate over the intersection
- * of two {@RegionValues}.
+ * of two (or three) {@RegionValues}.
  * 
  * @author Ernst Moritz Hahn <emhahn@cs.ox.ac.uk> (University of Oxford)
  * @see RegionValuesIntersections
@@ -39,14 +39,21 @@ final class RegionIntersection {
 	private Region region;
 	private StateValues values1;
 	private StateValues values2;
+	private StateValues values3;
 
 	public RegionIntersection(Region region, StateValues values1, StateValues values2)
+	{
+		this(region, values1, values2, null);
+	}
+
+	public RegionIntersection(Region region, StateValues values1, StateValues values2, StateValues values3)
 	{
 		this.region = region;
 		this.values1 = values1;
 		this.values2 = values2;
+		this.values3 = values3;
 	}
-	
+
 	public Region getRegion()
 	{
 		return region;
@@ -61,4 +68,10 @@ final class RegionIntersection {
 	{
 		return values2;
 	}
+
+	public StateValues getStateValues3()
+	{
+		return values3;
+	}
+
 }

prism/src/param/RegionValues.java

@@ -176,6 +176,40 @@ public final class RegionValues implements Iterable<Entry<Region, StateValues>>
 		other.values = otherNewStateValues;
 	}
 
+	public void cosplit(RegionValues other, RegionValues other2)
+	{
+		this.simplify();
+		other.simplify();
+		other2.simplify();
+
+		ArrayList<Region> newRegions = new ArrayList<Region>();
+		HashMap<Region, StateValues> thisNewStateValues = new HashMap<Region, StateValues>();
+		HashMap<Region, StateValues> otherNewStateValues = new HashMap<Region, StateValues>();
+		HashMap<Region, StateValues> other2NewStateValues = new HashMap<Region, StateValues>();
+		for (Region thisRegion : this.regions) {
+			for (Region otherRegion : other.regions) {
+				for (Region other2Region : other2.regions) {
+					Region newRegion = thisRegion.conjunct(otherRegion);
+					if (newRegion != null)
+						newRegion = newRegion.conjunct(other2Region);
+					if (newRegion != null) {
+						newRegions.add(newRegion);
+						thisNewStateValues.put(newRegion, this.values.get(thisRegion));
+						otherNewStateValues.put(newRegion, other.values.get(otherRegion));
+						other2NewStateValues.put(newRegion, other2.values.get(other2Region));
+					}
+				}
+			}
+		}
+
+		this.regions = new ArrayList<Region>(newRegions);
+		this.values = thisNewStateValues;
+		other.regions = new ArrayList<Region>(newRegions);
+		other.values = otherNewStateValues;
+		other2.regions = new ArrayList<Region>(newRegions);
+		other2.values = other2NewStateValues;
+	}
+
 	@Override
 	public String toString()
 	{
@@ -478,4 +512,19 @@ public final class RegionValues implements Iterable<Entry<Region, StateValues>>
 		}
 		return result;
 	}
+
+	public RegionValues ITE(RegionValues resT, RegionValues resE)
+	{
+		RegionValues result = new RegionValues(factory);
+		RegionValuesIntersections co = new RegionValuesIntersections(this, resT, resE);
+		for (RegionIntersection inter : co) {
+			Region region = inter.getRegion();
+			StateValues valueI = inter.getStateValues1();
+			StateValues valueT = inter.getStateValues2();
+			StateValues valueE = inter.getStateValues3();
+			RegionValues values = region.ITE(valueI, valueT, valueE);
+			result.addAll(values);
+		}
+		return result;
+	}
 }

prism/src/param/RegionValuesIntersections.java

@@ -30,28 +30,33 @@ import java.util.Iterator;
 import java.util.NoSuchElementException;
 
 /**
+ * Computes the intersections of two (or three) regions.
  * @author Ernst Moritz Hahn <emhahn@cs.ox.ac.uk> (University of Oxford)
  */
 final class RegionValuesIntersections implements Iterable<RegionIntersection> {
 	final private class RegionIntersectionOperator implements Iterator<RegionIntersection> {
 		private RegionValues regions1;
 		private RegionValues regions2;
+		private RegionValues regions3;
 		private int numRegions1;
 		private int regions1Index;
 		private boolean hasNext;
 		private Region region;
 		private StateValues stateValues1;
 		private StateValues stateValues2;
+		private StateValues stateValues3;
 
-		RegionIntersectionOperator(RegionValues regions1, RegionValues regions2)
+		RegionIntersectionOperator(RegionValues regions1, RegionValues regions2, RegionValues regions3)
 		{
 			this.regions1 = regions1;
 			this.regions2 = regions2;
+			this.regions3 = regions3;
 			regions1Index = 0;
 			numRegions1 = regions1.getNumRegions();
 			region = null;
 			stateValues1 = null;
 			stateValues2 = null;
+			stateValues3 = null;
 			findNext();
 		}
 		
@@ -61,7 +66,9 @@ final class RegionValuesIntersections implements Iterable<RegionIntersection> {
 				region = regions1.getRegion(regions1Index);
 				stateValues1 = regions1.getResult(region);
 				stateValues2 = regions2.getResult(region);
-				found = stateValues2 != null;
+				stateValues3 = regions3 != null ? regions3.getResult(region) : null;
+				found = (stateValues2 != null
+						&& (regions3 == null || stateValues3 != null));
 				regions1Index++;
 			}
 			hasNext = found;
@@ -75,7 +82,7 @@ final class RegionValuesIntersections implements Iterable<RegionIntersection> {
 		@Override
 		public RegionIntersection next() {
 			if (hasNext) {
-				RegionIntersection result = new RegionIntersection(region, stateValues1, stateValues2);
+				RegionIntersection result = new RegionIntersection(region, stateValues1, stateValues2, stateValues3);
 				findNext();
 				return result;
 			} else {
@@ -91,16 +98,25 @@ final class RegionValuesIntersections implements Iterable<RegionIntersection> {
 
 	private RegionValues regions1;
 	private RegionValues regions2;
+	private RegionValues regions3;
 
 	public RegionValuesIntersections(RegionValues regions1, RegionValues regions2) {
 		regions1.cosplit(regions2);
 		this.regions1 = regions1;
 		this.regions2 = regions2;
+		this.regions3 = null;
+	}
+
+	public RegionValuesIntersections(RegionValues regions1, RegionValues regions2, RegionValues regions3) {
+		regions1.cosplit(regions2, regions3);
+		this.regions1 = regions1;
+		this.regions2 = regions2;
+		this.regions3 = regions3;
 	}
 
 	@Override
 	public Iterator<RegionIntersection> iterator() {
-		return new RegionIntersectionOperator(regions1, regions2);
+		return new RegionIntersectionOperator(regions1, regions2, regions3);
 	}
 
 }