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 const& manager, storm::expressions::Variable const& blockVariable, std::set const& stateVariables, storm::dd::Bdd const& nondeterminismVariables, storm::dd::Bdd 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 @@ -30,13 +32,14 @@ namespace storm { Partition InternalSignatureRefiner::refine(Partition const& oldPartition, Signature const& signature) { std::pair, boost::optional>> newPartitionDds = refine(oldPartition, signature.getSignatureAdd()); ++numberOfRefinements; + return oldPartition.replacePartition(newPartitionDds.first, nextFreeBlockIndex, nextFreeBlockIndex, newPartitionDds.second); } template void InternalSignatureRefiner::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(3 * refiner->currentCapacity); + refiner->table = std::vector(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); }