Add power operator a^b, equivalent to pow(a,b).

For parsing, operator precedence is immediatey below * and /,
and ^ is right associative (a^b^c = a^(b^c)).

This is implemented as another case of ExpressionBinaryOp.

prism-tests/functionality/language/func_power.prism

@@ -0,0 +1,23 @@
+dtmc
+
+module die
+
+	// local state
+	s : [0..7] init 0;
+	// value of the die
+	d : [0..6] init 0;
+
+	[] s=0 -> 0.5 : (s'=1) + 0.5 : (s'=2);
+	[] s=1 -> 0.5 : (s'=3) + 0.5 : (s'=4);
+	[] s=2 -> 0.5 : (s'=5) + 0.5 : (s'=6);
+	[] s=3 -> 0.5 : (s'=1) + 0.5 : (s'=7) & (d'=1);
+	[] s=4 -> 0.5 : (s'=7) & (d'=2) + 0.5 : (s'=7) & (d'=3);
+	[] s=5 -> 0.5 : (s'=7) & (d'=4) + 0.5 : (s'=7) & (d'=5);
+	[] s=6 -> 0.5 : (s'=2) + 0.5 : (s'=7) & (d'=6);
+	[] s=7 -> (s'=7);
+
+endmodule
+
+rewards "coin_flips"
+	[] s<7 : 1;
+endrewards

prism-tests/functionality/language/func_power.prism.props

@@ -0,0 +1,85 @@
+// Some tests of pow(), in each case:
+// * occurring in a constant (so Expression evaluation)
+// * occurring in a constant property (so probably model checking)
+// * occurring in a state-dependent property (so model checking, various engines)
+
+// RESULT: 1
+"one": s+1;
+
+// RESULT: 1
+"one_s": round(1+P=?[F<=1 d=6]);
+
+// RESULT: 1
+"one_m": round(P=?[F true]);
+
+// -------------------------
+
+// RESULT: 8
+cPow1; const int cPow1 = pow(2,3);
+
+// RESULT: 8
+pow(2,3);
+
+// RESULT: 8
+pow(2*"one", d+3);
+
+// RESULT: 8
+pow(2*"one_s", d+3);
+
+// RESULT: 8
+pow(2*"one_m", d+3);
+
+// -------------------------
+
+// RESULT: 1/4
+cPow2; const double cPow2 = pow(0.5, 2);
+
+// RESULT: 1/4
+pow(0.5, 2);
+
+// RESULT: 1/4
+pow(0.5*"one", d+2);
+
+// RESULT: 1/4
+pow(0.5*"one_s", d+2);
+
+// RESULT: 1/4
+pow(0.5*"one_m", d+2);
+
+// -------------------------
+
+// RESULT: 1/2
+cPow3; const double cPow3 = pow(2, -1.0);
+
+// RESULT: 1/2
+pow(2, -1.0);
+
+// RESULT: 1/2
+pow(2*"one", d-1.0);
+
+// RESULT: 1/2
+pow(2*"one_s", d-1.0);
+
+// RESULT: 1/2
+pow(2*"one_m", d-1.0);
+
+// -------------------------
+
+// Don't test errors for now - not done properly for symbolic/param
+
+// RESULT: Error
+//cPow4; const double cPow4 = pow(2,-1);
+
+// RESULT: Error:negative
+//pow(2, -1);
+
+// RESULT: Error:negative
+//pow(2*"one", d-1);
+
+// RESULT: Error:negative
+//pow(2*"one_s", d-1);
+
+// RESULT: Error:negative
+//pow(2*"one_m", d-1);
+
+// -------------------------

prism-tests/functionality/language/func_power.prism.props.args

@@ -0,0 +1,5 @@
+-ex
+-exact
+-h
+-m
+-s

prism-tests/functionality/language/func_power.prism.root.props

@@ -0,0 +1,32 @@
+// Some tests of pow(), in each case:
+// * occurring in a constant (so Expression evaluation)
+// * occurring in a constant property (so probably model checking)
+// * occurring in a state-dependent property (so model checking, various engines)
+
+// RESULT: 1
+"one": s+1;
+
+// RESULT: 1
+"one_s": round(1+P=?[F<=1 d=6]);
+
+// RESULT: 1
+"one_m": round(P=?[F true]);
+
+// -------------------------
+
+// RESULT: 1/2
+cPow4; const double cPow4 = pow(1/4, 1/2);
+
+// RESULT: 1/2
+pow(1/4, 1/2);
+
+// RESULT: 1/2
+pow(1/4*"one", d+1/2);
+
+// RESULT: 1/2
+pow(1/4*"one_s", d+1/2);
+
+// RESULT: 1/2
+pow(1/4*"one_m", d+1/2);
+
+// -------------------------

prism-tests/functionality/language/func_power.prism.root.props.args

@@ -0,0 +1,4 @@
+-ex
+# -exact # no evaluation of roots as rationals
+-h
+-m

prism-tests/functionality/language/power.prism

@@ -0,0 +1,23 @@
+dtmc
+
+module die
+
+	// local state
+	s : [0..7] init 0;
+	// value of the die
+	d : [0..6] init 0;
+
+	[] s=0 -> 0.5 : (s'=1) + 0.5 : (s'=2);
+	[] s=1 -> 0.5 : (s'=3) + 0.5 : (s'=4);
+	[] s=2 -> 0.5 : (s'=5) + 0.5 : (s'=6);
+	[] s=3 -> 0.5 : (s'=1) + 0.5 : (s'=7) & (d'=1);
+	[] s=4 -> 0.5 : (s'=7) & (d'=2) + 0.5 : (s'=7) & (d'=3);
+	[] s=5 -> 0.5 : (s'=7) & (d'=4) + 0.5 : (s'=7) & (d'=5);
+	[] s=6 -> 0.5 : (s'=2) + 0.5 : (s'=7) & (d'=6);
+	[] s=7 -> (s'=7);
+
+endmodule
+
+rewards "coin_flips"
+	[] s<7 : 1;
+endrewards

prism-tests/functionality/language/power.prism.props

@@ -0,0 +1,86 @@
+// Some tests of power operator, in each case:
+// * occurring in a constant (so Expression evaluation)
+// * occurring in a constant property (so probably model checking)
+// * occurring in a state-dependent property (so model checking, various engines)
+
+// RESULT: 1
+"one": s+1;
+
+// RESULT: 1
+"one_s": round(1+P=?[F<=1 d=6]);
+
+// RESULT: 1
+"one_m": round(P=?[F true]);
+
+// -------------------------
+
+// RESULT: 8
+cPow1; const int cPow1 = 2^3;
+
+// RESULT: 8
+2^3;
+
+// RESULT: 8
+(2*"one")^(d+3);
+
+// RESULT: 8
+(2*"one_s")^(d+3);
+
+// RESULT: 8
+(2*"one_m")^(d+3);
+
+// -------------------------
+
+// RESULT: 1/4
+cPow2; const double cPow2 = 0.5^2;
+
+// RESULT: 1/4
+0.5^2;
+
+// RESULT: 1/4
+(0.5*"one")^(d+2);
+
+// RESULT: 1/4
+(0.5*"one_s")^(d+2);
+
+// RESULT: 1/4
+(0.5*"one_m")^(d+2);
+
+// -------------------------
+
+// RESULT: 1/2
+cPow3; const double cPow3 = 2^-1.0;
+
+// RESULT: 1/2
+2^-1.0;
+
+// RESULT: 1/2
+(2*"one")^(d-1.0);
+
+// RESULT: 1/2
+(2*"one_s")^(d-1.0);
+
+// RESULT: 1/2
+(2*"one_m")^(d-1.0);
+
+// -------------------------
+
+// Don't test errors for now - not done properly for symbolic/param
+
+// RESULT: Error
+//cPow4; const double cPow4 = 2^-1;
+//cPow4; const double cPow4 = pow(2,-1);
+
+// RESULT: Error:negative
+//2^-1;
+
+// RESULT: Error:negative
+//(2*"one")^(d-1);
+
+// RESULT: Error:negative
+//(2*"one_s")^(d-1);
+
+// RESULT: Error:negative
+//(2*"one_m")^(d-1);
+
+// -------------------------

prism-tests/functionality/language/power.prism.props.args

@@ -0,0 +1,4 @@
+-ex
+-exact
+-h
+-m

prism-tests/functionality/language/power.prism.root.props

@@ -0,0 +1,32 @@
+// Some tests of power operator, in each case:
+// * occurring in a constant (so Expression evaluation)
+// * occurring in a constant property (so probably model checking)
+// * occurring in a state-dependent property (so model checking, various engines)
+
+// RESULT: 1
+"one": s+1;
+
+// RESULT: 1
+"one_s": round(1+P=?[F<=1 d=6]);
+
+// RESULT: 1
+"one_m": round(P=?[F true]);
+
+// -------------------------
+
+// RESULT: 1/2
+cPow4; const double cPow4 = (1/4)^(1/2);
+
+// RESULT: 1/2
+(1/4)^(1/2);
+
+// RESULT: 1/2
+(1/4*"one")^(d+1/2);
+
+// RESULT: 1/2
+(1/4*"one_s")^(d+1/2);
+
+// RESULT: 1/2
+(1/4*"one_m")^(d+1/2);
+
+// -------------------------

prism-tests/functionality/language/power.prism.root.props.args

@@ -0,0 +1,4 @@
+-ex
+# -exact # no evaluation of roots as rationals
+-h
+-m

prism/src/param/BoxRegion.java

@@ -276,6 +276,9 @@ RegionValues binaryOp(int op, StateValues values1, StateValues values2) {
 				} else if (op == Region.PLUS || op == Region.MINUS || op == Region.TIMES || op == Region.DIVIDE) {
 					Function stateVal = arithOp(op, values1.getStateValueAsFunction(state), values2.getStateValueAsFunction(state));
 					values.setStateValue(state, stateVal);
+				} else if (op == Region.POW) {
+					Function stateVal = powOp(values1.getStateValueAsFunction(state), values2.getStateValueAsFunction(state));
+					values.setStateValue(state, stateVal);
 				} else {
 					throw new UnsupportedOperationException("operator not yet implemented for parametric analyses");
 				}
@@ -386,6 +389,26 @@ private Function arithOp(int op, Function op1, Function op2) {
 		return result;
 	}
 
+	/**
+	 * Performs a power operation on two rational functions.
+	 *
+	 * @param op1 first operand
+	 * @param op2  second operand
+	 * @return value of operation
+	 */
+	private Function powOp(Function op1, Function op2)
+	{
+		if (!op2.isConstant()) {
+			throw new IllegalArgumentException("unsupported pow operation");
+		}
+		BigRational exp = op2.asBigRational();
+		if (!exp.isInteger()) {
+			throw new IllegalArgumentException("unsupported pow operation");
+		}
+		int expInt = exp.getNum().intValue();
+		return op1.pow(expInt);
+	}
+
 	/**
 	 * Performs given operation on two booleans.
 	 * 

prism/src/param/CachedFunction.java

@@ -101,6 +101,11 @@ public Function divide(Function other) {
 		return factory.divide(this, other);
 	}
 
+	@Override
+	public Function pow(int exp) {
+		return factory.pow(this, exp);
+	}
+
 	@Override
 	public Function star() {
 		return factory.star(this);

prism/src/param/CachedFunctionFactory.java

@@ -243,7 +243,13 @@ Function divide(Function cached1, Function cached2)
 		Function function2 = getFunctionFromCache(cached2);
 		return makeUnique(function1.divide(function2));
 	}
-
+
+	Function pow(Function cached1, int exp)
+	{
+		Function function1 = getFunctionFromCache(cached1);
+		return makeUnique(function1.pow(exp));
+	}
+
 	Function star(Function cached) {
 		Function result;
 		if (useOpCache) {

prism/src/param/DagFunction.java

@@ -116,6 +116,11 @@ public Function divide(Function other) {
 		return dagFactory.divide(this, (DagFunction) other);
 	}
 
+	@Override
+	public Function pow(int exp) {
+		throw new RuntimeException("DagFunction does not support powers");
+	}
+
 	@Override
 	public Function star() {
 		return dagFactory.star(this);

prism/src/param/Function.java

@@ -99,6 +99,14 @@ protected Function(FunctionFactory factory)
 	 */
 	public abstract Function divide(Function other);
 
+	/**
+	 * Raises this function to the power {@code exp}.
+	 *
+	 * @param exp integer exponent
+	 * @return {@code this} to the power {@code exp}
+	 */
+	public abstract Function pow(int exp);
+
 	/**
 	 * Performs the {@code star} operation with this function.
 	 * The value of the result is equal to 1/(1-{@code this}).