From 1187981b5d6d9ba99c364774dee87ee581396b83 Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@gmail.com>
Date: Mon, 10 Aug 2020 20:33:59 -0700
Subject: [PATCH] fixes in creation of dice expressions

---
 .../expressions/ToDiceStringVisitor.cpp       | 33 +++++++++++++++----
 1 file changed, 26 insertions(+), 7 deletions(-)

diff --git a/src/storm/storage/expressions/ToDiceStringVisitor.cpp b/src/storm/storage/expressions/ToDiceStringVisitor.cpp
index d074f1ec0..1904b56c5 100644
--- a/src/storm/storage/expressions/ToDiceStringVisitor.cpp
+++ b/src/storm/storage/expressions/ToDiceStringVisitor.cpp
@@ -91,12 +91,31 @@ namespace storm {
                     expression.getSecondOperand()->accept(*this, data);
                     stream << ")";
                     break;
-                case BinaryNumericalFunctionExpression::OperatorType::Divide:
-                    stream << "(";
-                    expression.getFirstOperand()->accept(*this, data);
-                    stream << "/";
-                    expression.getSecondOperand()->accept(*this, data);
-                    stream << ")";
+                case BinaryNumericalFunctionExpression::OperatorType::Divide: {
+                    STORM_LOG_THROW(expression.getSecondOperand()->isIntegerLiteralExpression(),
+                                    storm::exceptions::NotSupportedException,
+                                    "Dice does not support modulo with nonconst rhs");
+                        uint64_t denominator = expression.getSecondOperand()->evaluateAsInt();
+                        int shifts = 0;
+                        while (denominator % 2 == 0) {
+                            denominator = denominator >> 1;
+                            shifts++;
+                        }
+                        denominator = denominator >> 1;
+                        if (denominator > 0) {
+                            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException,
+                                            "Dice does not support division with non-powers of two");
+                        }
+                        if (shifts > 0) {
+                            stream << "(";
+                            expression.getFirstOperand()->accept(*this, data);
+                            stream << " >> " << shifts;
+                            stream << ")";
+                        } else {
+                            expression.getFirstOperand()->accept(*this, data);
+                        }
+
+                    }
                     break;
                 case BinaryNumericalFunctionExpression::OperatorType::Power:
                     stream << "(";
@@ -109,7 +128,7 @@ namespace storm {
                     STORM_LOG_THROW(expression.getSecondOperand()->isIntegerLiteralExpression(), storm::exceptions::NotSupportedException, "Dice does not support modulo with nonconst rhs");
                     STORM_LOG_THROW(expression.getSecondOperand()->evaluateAsInt() == 2, storm::exceptions::NotSupportedException, "Dice does not support modulo with rhs != 2");
 
-                    stream << "( nth_bit(int(" << nrBits << "," << nrBits << "), ";
+                    stream << "( nth_bit(int(" << nrBits << "," << nrBits-1 << "), ";
                     expression.getFirstOperand()->accept(*this, data);
                     stream << "))";
                     break;