Replaced storm::expressions::Expression::operator^ by storm::expressions::pow. An optional flag indicates if we should allow power expressions of integer type (PRISM semantics) or whether it is always a real (JANI semantics).

src/storm-parsers/parser/ExpressionCreator.cpp

@@ -130,7 +130,7 @@ namespace storm {
             if (this->createExpressions) {
                 try {
                     switch (operatorType) {
-                        case storm::expressions::OperatorType::Power: return e1 ^ e2; break;
+                        case storm::expressions::OperatorType::Power: return storm::expressions::pow(e1, e2, true); break;
                         case storm::expressions::OperatorType::Modulo: return e1 % e2; break;
                         default: STORM_LOG_ASSERT(false, "Invalid operation."); break;
                     }

src/storm-parsers/parser/JaniParser.cpp

@@ -1263,7 +1263,7 @@ namespace storm {
                         assert(arguments.size() == 2);
                         ensureNumericalType(arguments[0], opstring, 0, scope.description);
                         ensureNumericalType(arguments[1], opstring, 1, scope.description);
-                        return arguments[0]^arguments[1];
+                        return storm::expressions::pow(arguments[0], arguments[1]);
                     } else if (opstring == "exp") {
                         arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scope, returnNoneInitializedOnUnknownOperator, auxiliaryVariables);
                         assert(arguments.size() == 2);

src/storm/storage/expressions/Expression.cpp

@@ -283,11 +283,6 @@ namespace storm {
             return Expression(std::shared_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(first.getBaseExpression().getManager(), first.getType().divide(second.getType()), first.getBaseExpressionPointer(), second.getBaseExpressionPointer(), BinaryNumericalFunctionExpression::OperatorType::Divide)));
         }
         
-        Expression operator^(Expression const& first, Expression const& second) {
-            assertSameManager(first.getBaseExpression(), second.getBaseExpression());
-            return Expression(std::shared_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(first.getBaseExpression().getManager(), first.getType().power(second.getType()), first.getBaseExpressionPointer(), second.getBaseExpressionPointer(), BinaryNumericalFunctionExpression::OperatorType::Power)));
-        }
-        
         Expression operator%(Expression const& first, Expression const& second) {
             assertSameManager(first.getBaseExpression(), second.getBaseExpression());
             return Expression(std::shared_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(first.getBaseExpression().getManager(), first.getType().power(second.getType()), first.getBaseExpressionPointer(), second.getBaseExpressionPointer(), BinaryNumericalFunctionExpression::OperatorType::Modulo)));
@@ -408,6 +403,12 @@ namespace storm {
             return Expression(std::shared_ptr<BaseExpression>(new BinaryBooleanFunctionExpression(first.getBaseExpression().getManager(), first.getType().logicalConnective(second.getType()), first.getBaseExpressionPointer(), second.getBaseExpressionPointer(), BinaryBooleanFunctionExpression::OperatorType::Xor)));
         }
         
+        Expression pow(Expression const& base, Expression const& exponent, bool allowIntegerType) {
+            assertSameManager(base.getBaseExpression(), exponent.getBaseExpression());
+            return Expression(std::shared_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(base.getBaseExpression().getManager(), base.getType().power(exponent.getType(), allowIntegerType), base.getBaseExpressionPointer(), exponent.getBaseExpressionPointer(), BinaryNumericalFunctionExpression::OperatorType::Power)));
+        }
+
+        
         Expression floor(Expression const& first) {
             STORM_LOG_THROW(first.hasNumericalType(), storm::exceptions::InvalidTypeException, "Operator 'floor' requires numerical operand.");
             return Expression(std::shared_ptr<BaseExpression>(new UnaryNumericalFunctionExpression(first.getBaseExpression().getManager(), first.getType().floorCeil(), first.getBaseExpressionPointer(), UnaryNumericalFunctionExpression::OperatorType::Floor)));

src/storm/storage/expressions/Expression.h

@@ -32,7 +32,6 @@ namespace storm {
             friend Expression operator-(Expression const& first);
             friend Expression operator*(Expression const& first, Expression const& second);
             friend Expression operator/(Expression const& first, Expression const& second);
-            friend Expression operator^(Expression const& first, Expression const& second);
             friend Expression operator%(Expression const& first, Expression const& second);
             friend Expression operator&&(Expression const& first, Expression const& second);
             friend Expression operator||(Expression const& first, Expression const& second);
@@ -51,6 +50,7 @@ namespace storm {
             friend Expression implies(Expression const& first, Expression const& second);
             friend Expression iff(Expression const& first, Expression const& second);
             friend Expression xclusiveor(Expression const& first, Expression const& second);
+            friend Expression pow(Expression const& base, Expression const& exponent, bool allowIntegerType);
             friend Expression abs(Expression const& first);
             friend Expression truncate(Expression const& first);
             friend Expression sign(Expression const& first);
@@ -412,7 +412,6 @@ namespace storm {
         Expression operator-(Expression const& first);
         Expression operator*(Expression const& first, Expression const& second);
         Expression operator/(Expression const& first, Expression const& second);
-        Expression operator^(Expression const& first, Expression const& second);
         Expression operator&&(Expression const& first, Expression const& second);
         Expression operator||(Expression const& first, Expression const& second);
         Expression operator!(Expression const& first);
@@ -430,6 +429,16 @@ namespace storm {
         Expression implies(Expression const& first, Expression const& second);
         Expression iff(Expression const& first, Expression const& second);
         Expression xclusiveor(Expression const& first, Expression const& second);
+        
+        /*!
+         * The type of the resulting expression is
+         * - integer, if base and exponent are integer expressions and allowIntegerType is true
+         *      (in this case it is assumed that exponent is always positive), and
+         * - rational, otherwise.
+         * The integer case is to reflect the PRISM semantics
+         * @see https://github.com/ahartmanns/qcomp/issues/103
+         */
+        Expression pow(Expression const& base, Expression const& exponent, bool allowIntegerType = false);
         Expression abs(Expression const& first);
         Expression truncate(Expression const& first);
         Expression sign(Expression const& first);

src/storm/storage/expressions/RationalFunctionToExpression.cpp

@@ -49,7 +49,7 @@ namespace storm {
 
                     storm::expressions::Expression nominatorPartExpr = manager->rational(storm::utility::convertNumber<storm::RationalNumber, storm::RationalFunctionCoefficient>(itr->coeff()));
                     for (auto var : varsFunction) {
-                        nominatorPartExpr = nominatorPartExpr * (manager->getVariable(var.name())^manager->rational(storm::utility::convertNumber<storm::RationalNumber, storm::RationalFunctionCoefficient>(itr->monomial()->exponentOfVariable(var))));
+                        nominatorPartExpr = nominatorPartExpr * storm::expressions::pow(manager->getVariable(var.name()), manager->rational(storm::utility::convertNumber<storm::RationalNumber, storm::RationalFunctionCoefficient>(itr->monomial()->exponentOfVariable(var))));
                     }
                     if (varsFunction.size() >= 1) {
                         result = result + nominatorPartExpr;

src/storm/storage/expressions/Type.cpp

@@ -215,10 +215,14 @@ namespace storm {
             return std::max(*this, other);
         }
         
-        Type Type::power(Type const& other) const {
+        Type Type::power(Type const& other, bool allowIntegerType) const {
             STORM_LOG_THROW(this->isNumericalType() && other.isNumericalType(), storm::exceptions::InvalidTypeException, "Operator requires numerical operands.");
             STORM_LOG_THROW(!this->isBitVectorType() && !other.isBitVectorType(), storm::exceptions::InvalidTypeException, "Operator requires non-bitvector operands.");
-            return std::max(*this, other);
+            if (allowIntegerType) {
+                return std::max(*this, other);
+            } else {
+                return this->getManager().getRationalType();
+            }
         }
         
         Type Type::logicalConnective(Type const& other) const {

src/storm/storage/expressions/Type.h

@@ -115,7 +115,7 @@ namespace storm {
             Type plusMinusTimes(Type const& other) const;
             Type minus() const;
             Type divide(Type const& other) const;
-            Type power(Type const& other) const;
+            Type power(Type const& other, bool allowIntegerType = false) const;
             Type logicalConnective(Type const& other) const;
             Type logicalConnective() const;
             Type numericalComparison(Type const& other) const;

src/test/storm/storage/ExpressionTest.cpp

@@ -252,10 +252,12 @@ TEST(Expression, OperatorTest) {
     ASSERT_NO_THROW(tempExpression = storm::expressions::ceil(rationalVarExpression));
     EXPECT_TRUE(tempExpression.hasIntegerType());
 
-    STORM_SILENT_ASSERT_THROW(tempExpression = trueExpression ^ piExpression, storm::exceptions::InvalidTypeException);
-    ASSERT_NO_THROW(tempExpression = threeExpression ^ threeExpression);
+    STORM_SILENT_ASSERT_THROW(tempExpression = storm::expressions::pow(trueExpression, piExpression), storm::exceptions::InvalidTypeException);
+    ASSERT_NO_THROW(tempExpression = storm::expressions::pow(threeExpression, threeExpression, true));
     EXPECT_TRUE(tempExpression.hasIntegerType());
-    ASSERT_NO_THROW(tempExpression = intVarExpression ^ rationalVarExpression);
+    ASSERT_NO_THROW(tempExpression = storm::expressions::pow(threeExpression, threeExpression, false));
+    EXPECT_TRUE(tempExpression.hasRationalType());
+    ASSERT_NO_THROW(tempExpression = storm::expressions::pow(intVarExpression, rationalVarExpression));
     EXPECT_TRUE(tempExpression.hasRationalType());
 
     STORM_SILENT_ASSERT_THROW(tempExpression = storm::expressions::modulo(trueExpression, piExpression), storm::exceptions::InvalidTypeException);