From ea21aca117f6fef689e7f38f5aab269fe7ae2d8a Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Fri, 2 Mar 2018 13:34:19 +0100
Subject: [PATCH] second attempt at fixing issue when not reusing blocks

---
 .../InternalSylvanSignatureRefiner.cpp        | 23 ++++++++++---------
 1 file changed, 12 insertions(+), 11 deletions(-)

diff --git a/src/storm/storage/dd/bisimulation/InternalSylvanSignatureRefiner.cpp b/src/storm/storage/dd/bisimulation/InternalSylvanSignatureRefiner.cpp
index 9d47e648e..ce14cd837 100644
--- a/src/storm/storage/dd/bisimulation/InternalSylvanSignatureRefiner.cpp
+++ b/src/storm/storage/dd/bisimulation/InternalSylvanSignatureRefiner.cpp
@@ -11,13 +11,15 @@ namespace storm {
     namespace dd {
         namespace bisimulation {
             
+            static const uint64_t NO_ELEMENT_MARKER = -1ull;
+            
             InternalSylvanSignatureRefinerBase::InternalSylvanSignatureRefinerBase(storm::dd::DdManager<storm::dd::DdType::Sylvan> const& manager, storm::expressions::Variable const& blockVariable, std::set<storm::expressions::Variable> const& stateVariables, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& nondeterminismVariables, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& nonBlockVariables, InternalSignatureRefinerOptions const& options) : manager(manager), blockVariable(blockVariable), stateVariables(stateVariables), nondeterminismVariables(nondeterminismVariables), nonBlockVariables(nonBlockVariables), options(options), numberOfBlockVariables(manager.getMetaVariable(blockVariable).getNumberOfDdVariables()), blockCube(manager.getMetaVariable(blockVariable).getCube()), nextFreeBlockIndex(0), numberOfRefinements(0), currentCapacity(1ull << 20), resizeFlag(0) {
                 
                 // Perform garbage collection to clean up stuff not needed anymore.
                 LACE_ME;
                 sylvan_gc();
                 
-                table.resize(3 * currentCapacity);
+                table.resize(3 * currentCapacity, NO_ELEMENT_MARKER);
             }
                         
             template<typename ValueType>
@@ -30,13 +32,14 @@ namespace storm {
             Partition<storm::dd::DdType::Sylvan, ValueType> InternalSignatureRefiner<storm::dd::DdType::Sylvan, ValueType>::refine(Partition<storm::dd::DdType::Sylvan, ValueType> const& oldPartition, Signature<storm::dd::DdType::Sylvan, ValueType> const& signature) {
                 std::pair<storm::dd::Bdd<storm::dd::DdType::Sylvan>, boost::optional<storm::dd::Bdd<storm::dd::DdType::Sylvan>>> newPartitionDds = refine(oldPartition, signature.getSignatureAdd());
                 ++numberOfRefinements;
+                
                 return oldPartition.replacePartition(newPartitionDds.first, nextFreeBlockIndex, nextFreeBlockIndex, newPartitionDds.second);
             }
             
             template<typename ValueType>
             void InternalSignatureRefiner<storm::dd::DdType::Sylvan, ValueType>::clearCaches() {
                 for (auto& e : this->table) {
-                    e = 0ull;
+                    e = NO_ELEMENT_MARKER;
                 }
                 for (auto& e : this->signatures) {
                     e = 0ull;
@@ -49,7 +52,7 @@ namespace storm {
                 
                 LACE_ME;
 
-                nextFreeBlockIndex = options.reuseBlockNumbers ? oldPartition.getNextFreeBlockIndex() : 1;
+                nextFreeBlockIndex = options.reuseBlockNumbers ? oldPartition.getNextFreeBlockIndex() : 0;
                 signatures.resize(nextFreeBlockIndex);
                 
                 // Perform the actual recursive refinement step.
@@ -142,7 +145,7 @@ namespace storm {
                 
                 uint64_t oldCapacity = refiner->currentCapacity;
                 refiner->currentCapacity <<= 1;
-                refiner->table = std::vector<uint64_t>(3 * refiner->currentCapacity);
+                refiner->table = std::vector<uint64_t>(3 * refiner->currentCapacity, NO_ELEMENT_MARKER);
                 
                 CALL(sylvan_rehash, 0, oldCapacity, refiner);
                 
@@ -161,8 +164,6 @@ namespace storm {
                 }
             }
             
-            static const uint64_t NO_ELEMENT_MARKER = -1ull;
-            
             static uint64_t sylvan_search_or_insert(uint64_t sig, uint64_t previous_block, InternalSylvanSignatureRefinerBase* refiner)
             {
                 uint64_t hash = sylvan_hash(sig, previous_block);
@@ -175,13 +176,13 @@ namespace storm {
                     ptr = refiner->table.data() + pos*3;
                     a = *ptr;
                     if (a == sig) {
-                        while ((b=ptr[1]) == 0) continue;
+                        while ((b=ptr[1]) == NO_ELEMENT_MARKER) continue;
                         if (b == previous_block) {
-                            while ((c=ptr[2]) == 0) continue;
+                            while ((c=ptr[2]) == NO_ELEMENT_MARKER) continue;
                             return c;
                         }
-                    } else if (a == 0) {
-                        if (cas(ptr, 0, sig)) {
+                    } else if (a == NO_ELEMENT_MARKER) {
+                        if (cas(ptr, NO_ELEMENT_MARKER, sig)) {
                             c = ptr[2] = __sync_fetch_and_add(&refiner->nextFreeBlockIndex, 1);
                             ptr[1] = previous_block;
                             return c;
@@ -250,7 +251,7 @@ namespace storm {
                 
                 // no previous block number, search or insert
                 uint64_t c;
-                while ((c = sylvan_search_or_insert(sig, refiner->options.reuseBlockNumbers ? previous_block : sig, refiner)) == NO_ELEMENT_MARKER) {
+                while ((c = sylvan_search_or_insert(sig, previous_block, refiner)) == NO_ELEMENT_MARKER) {
                     CALL(sylvan_grow, refiner);
                 }