From 29b915ccbf4e8da4f1d04dcc4ce7e8887f76c453 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Sun, 15 Oct 2017 20:37:23 +0200
Subject: [PATCH] fix out-of-index write in bisimulation quotienting

---
 src/storm/storage/dd/bisimulation/QuotientExtractor.cpp | 9 +++++----
 src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp       | 4 +---
 2 files changed, 6 insertions(+), 7 deletions(-)

diff --git a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp
index 273ecb8fc..3e8682b6d 100644
--- a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp
+++ b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp
@@ -427,7 +427,7 @@ namespace storm {
                 
                 void createBlockToOffsetMappingRec(DdNodePtr partitionNode, DdNodePtr representativesNode, DdNodePtr variables, storm::dd::Odd const& odd, uint64_t offset) {
                     STORM_LOG_ASSERT(partitionNode != Cudd_ReadLogicZero(ddman) || representativesNode == Cudd_ReadLogicZero(ddman), "Expected representative to be zero if the partition is zero.");
-                    if (representativesNode == Cudd_ReadLogicZero(ddman)) {
+                    if (representativesNode == Cudd_ReadLogicZero(ddman) || partitionNode == Cudd_ReadLogicZero(ddman)) {
                         return;
                     }
                     
@@ -471,7 +471,7 @@ namespace storm {
                 }
                 
                 void extractVectorRec(DdNodePtr vector, DdNodePtr representativesNode, DdNodePtr variables, storm::dd::Odd const& odd, uint64_t offset, std::vector<ValueType>& result) {
-                    if (representativesNode == Cudd_ReadLogicZero(ddman)) {
+                    if (representativesNode == Cudd_ReadLogicZero(ddman) || vector == Cudd_ReadZero(ddman)) {
                         return;
                     }
                     
@@ -643,7 +643,7 @@ namespace storm {
                 }
                 
                 void extractVectorRec(MTBDD vector, BDD representativesNode, BDD variables, storm::dd::Odd const& odd, uint64_t offset, std::vector<ValueType>& result) {
-                    if (representativesNode == sylvan_false) {
+                    if (representativesNode == sylvan_false || mtbdd_iszero(vector)) {
                         return;
                     }
                     
@@ -680,7 +680,7 @@ namespace storm {
                 
                 void createBlockToOffsetMappingRec(BDD partitionNode, BDD representativesNode, BDD variables, storm::dd::Odd const& odd, uint64_t offset) {
                     STORM_LOG_ASSERT(partitionNode != sylvan_false || representativesNode == sylvan_false, "Expected representative to be zero if the partition is zero.");
-                    if (representativesNode == sylvan_false) {
+                    if (representativesNode == sylvan_false || partitionNode == sylvan_false) {
                         return;
                     }
                     
@@ -892,6 +892,7 @@ namespace storm {
                     
                     boost::optional<std::vector<ValueType>> quotientStateActionRewards;
                     if (rewardModel.hasStateActionRewards()) {
+                        rewardModel.getStateActionRewardVector().exportToDot("vector.dot");
                         quotientStateActionRewards = sparseExtractor.extractStateActionVector(rewardModel.getStateActionRewardVector());
                     }
                     
diff --git a/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp b/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp
index 3eca707ca..ce1576956 100644
--- a/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp
+++ b/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp
@@ -57,9 +57,7 @@ namespace storm {
             bool negated = mtbdd_hascomp(node);
             
             STORM_LOG_ASSERT(mtbdd_gettype(node) == sylvan_storm_rational_number_get_type(), "Expected a storm::RationalNumber value.");
-            uint64_t value = mtbdd_getvalue(node);
-            storm_rational_number_ptr ptr = (storm_rational_number_ptr)value;
-            
+            storm_rational_number_ptr ptr = (storm_rational_number_ptr)mtbdd_getstorm_rational_number_ptr(node);
             storm::RationalNumber* rationalNumber = (storm::RationalNumber*)(ptr);
             
             return negated ? -(*rationalNumber) : (*rationalNumber);