From 669940ccd3aa619d8f523dae305bb023428f4a17 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 23 Oct 2017 16:21:29 +0200 Subject: [PATCH] only supporting reuse of nothing or of block numbers --- .../settings/modules/BisimulationSettings.cpp | 10 +- .../settings/modules/BisimulationSettings.h | 2 +- .../dd/bisimulation/SignatureRefiner.cpp | 384 +++--------------- 3 files changed, 63 insertions(+), 333 deletions(-) diff --git a/src/storm/settings/modules/BisimulationSettings.cpp b/src/storm/settings/modules/BisimulationSettings.cpp index ee9c6165b..cea523793 100644 --- a/src/storm/settings/modules/BisimulationSettings.cpp +++ b/src/storm/settings/modules/BisimulationSettings.cpp @@ -31,7 +31,7 @@ namespace storm { std::vector signatureModes = { "eager", "lazy" }; this->addOption(storm::settings::OptionBuilder(moduleName, signatureModeOptionName, false, "Sets the signature computation mode.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(signatureModes)).setDefaultValueString("eager").build()).build()); - std::vector reuseModes = {"all", "none", "blocks", "sig"}; + std::vector reuseModes = {"none", "blocks"}; this->addOption(storm::settings::OptionBuilder(moduleName, reuseOptionName, true, "Sets whether to reuse all results.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(reuseModes)) .setDefaultValueString("blocks").build()) @@ -76,16 +76,12 @@ namespace storm { BisimulationSettings::ReuseMode BisimulationSettings::getReuseMode() const { std::string reuseModeAsString = this->getOption(reuseOptionName).getArgumentByName("mode").getValueAsString(); - if (reuseModeAsString == "all") { - return ReuseMode::All; - } else if (reuseModeAsString == "none") { + if (reuseModeAsString == "none") { return ReuseMode::None; } else if (reuseModeAsString == "blocks") { return ReuseMode::BlockNumbers; - } else if (reuseModeAsString == "sig") { - return ReuseMode::SignatureResults; } - return ReuseMode::All; + return ReuseMode::BlockNumbers; } bool BisimulationSettings::check() const { diff --git a/src/storm/settings/modules/BisimulationSettings.h b/src/storm/settings/modules/BisimulationSettings.h index e0678ea71..917c1479a 100644 --- a/src/storm/settings/modules/BisimulationSettings.h +++ b/src/storm/settings/modules/BisimulationSettings.h @@ -19,7 +19,7 @@ namespace storm { enum class QuotientFormat { Sparse, Dd }; - enum class ReuseMode { All, None, BlockNumbers, SignatureResults }; + enum class ReuseMode { None, BlockNumbers }; /*! * Creates a new set of bisimulation settings. diff --git a/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp b/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp index 510cafc45..23c21f01c 100644 --- a/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp +++ b/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp @@ -45,13 +45,11 @@ namespace storm { auto const& bisimulationSettings = storm::settings::getModule(); storm::settings::modules::BisimulationSettings::ReuseMode reuseMode = bisimulationSettings.getReuseMode(); - this->reuseBlockNumbers = reuseMode == storm::settings::modules::BisimulationSettings::ReuseMode::All || reuseMode == storm::settings::modules::BisimulationSettings::ReuseMode::BlockNumbers; - this->reuseSignatureResult = reuseMode == storm::settings::modules::BisimulationSettings::ReuseMode::All || reuseMode == storm::settings::modules::BisimulationSettings::ReuseMode::SignatureResults; + this->reuseBlockNumbers = reuseMode == storm::settings::modules::BisimulationSettings::ReuseMode::BlockNumbers; } bool shiftStateVariables; bool reuseBlockNumbers; - bool reuseSignatureResult; }; class ReuseWrapper { @@ -90,39 +88,24 @@ namespace storm { } Partition refine(Partition const& oldPartition, Signature const& signature) { - storm::dd::Add newPartitionAdd; - if (options.reuseBlockNumbers && !options.reuseSignatureResult) { - newPartitionAdd = refineReuseBlockNumber(oldPartition, signature.getSignatureAdd()); - } else { - newPartitionAdd = refineReuseSignatureResults(oldPartition, signature.getSignatureAdd()); - } + storm::dd::Add newPartitionAdd = refine(oldPartition, signature.getSignatureAdd());; ++numberOfRefinements; - - uint64_t numberOfBlocks = nextFreeBlockIndex; - if (options.reuseSignatureResult) { - std::set blockVariableSet = {blockVariable}; - std::set nonBlockExpressionVariables; - std::set_difference(oldPartition.asAdd().getContainedMetaVariables().begin(), oldPartition.asAdd().getContainedMetaVariables().end(), blockVariableSet.begin(), blockVariableSet.end(), std::inserter(nonBlockExpressionVariables, nonBlockExpressionVariables.begin())); - numberOfBlocks = newPartitionAdd.notZero().existsAbstract(nonBlockExpressionVariables).getNonZeroCount(); - } - - return oldPartition.replacePartition(newPartitionAdd, numberOfBlocks, nextFreeBlockIndex); + return oldPartition.replacePartition(newPartitionAdd, nextFreeBlockIndex, nextFreeBlockIndex); } private: void clearCaches() { signatureCache.clear(); - signatureCache2.clear(); reuseBlocksCache.clear(); } - storm::dd::Add refineReuseBlockNumber(Partition const& oldPartition, storm::dd::Add const& signatureAdd) { + storm::dd::Add refine(Partition const& oldPartition, storm::dd::Add const& signatureAdd) { STORM_LOG_ASSERT(oldPartition.storedAsAdd(), "Expecting partition to be stored as ADD for CUDD."); - nextFreeBlockIndex = oldPartition.getNextFreeBlockIndex(); + nextFreeBlockIndex = options.reuseBlockNumbers ? oldPartition.getNextFreeBlockIndex() : 0; // Perform the actual recursive refinement step. - DdNodePtr result = refineReuseBlockNumber(oldPartition.asAdd().getInternalAdd().getCuddDdNode(), signatureAdd.getInternalAdd().getCuddDdNode(), nondeterminismVariables.getInternalBdd().getCuddDdNode(), nonBlockVariables.getInternalBdd().getCuddDdNode()); + DdNodePtr result = refine(oldPartition.asAdd().getInternalAdd().getCuddDdNode(), signatureAdd.getInternalAdd().getCuddDdNode(), nondeterminismVariables.getInternalBdd().getCuddDdNode(), nonBlockVariables.getInternalBdd().getCuddDdNode()); // Construct resulting ADD from the obtained node and the meta information. storm::dd::InternalAdd internalNewPartitionAdd(&internalDdManager, cudd::ADD(internalDdManager.getCuddManager(), result)); @@ -131,25 +114,6 @@ namespace storm { clearCaches(); return newPartitionAdd; } - - storm::dd::Add refineReuseSignatureResults(Partition const& oldPartition, storm::dd::Add const& signatureAdd) { - STORM_LOG_ASSERT(oldPartition.storedAsAdd(), "Expecting partition to be stored as ADD for CUDD."); - - nextFreeBlockIndex = options.reuseSignatureResult ? oldPartition.getNextFreeBlockIndex() : 0; - - // Perform the actual recursive refinement step. - DdNodePtr result = refineReuseSignatureResults(signatureAdd.getInternalAdd().getCuddDdNode(), nondeterminismVariables.getInternalBdd().getCuddDdNode(), nonBlockVariables.getInternalBdd().getCuddDdNode()); - - // Construct resulting ADD from the obtained node and the meta information. - storm::dd::InternalAdd internalNewPartitionAdd(&internalDdManager, cudd::ADD(internalDdManager.getCuddManager(), result)); - storm::dd::Add newPartitionAdd(oldPartition.asAdd().getDdManager(), internalNewPartitionAdd, oldPartition.asAdd().getContainedMetaVariables()); - - if (options.reuseSignatureResult) { - oldSignatureCache = signatureCache; - } - clearCaches(); - return newPartitionAdd; - } DdNodePtr encodeBlock(uint64_t blockIndex) { for (auto const& blockDdVariableIndex : blockDdVariableIndices) { @@ -165,130 +129,39 @@ namespace storm { return result; } - DdNodePtr refineReuseSignatureResults(DdNode* signatureNode, DdNode* nondeterminismVariablesNode, DdNode* nonBlockVariablesNode) { - // If we arrived at the constant zero node, then this was an illegal state encoding (we require - // all states to be non-deadlock). - if (signatureNode == Cudd_ReadZero(ddman)) { - return signatureNode; - } - - // Check the cache whether we have seen the same node before. - auto it = signatureCache.find(signatureNode); - if (it != signatureCache.end()) { - // If so, we return the corresponding result. - return it->second; - } - - // If we are to reuse signature results, check the old cache. - if (options.reuseSignatureResult) { - it = oldSignatureCache.find(signatureNode); - if (it != oldSignatureCache.end()) { - // If so, we return the corresponding result. - return it->second; - } - } - - // If there are no more non-block variables, we hit the signature. - if (Cudd_IsConstant(nonBlockVariablesNode)) { - DdNode* result = encodeBlock(nextFreeBlockIndex++); - signatureCache[signatureNode] = result; - return result; - } else { - // If there are more variables that belong to the non-block part of the encoding, we need to recursively descend. - - bool skipped = true; - DdNode* signatureThen; - DdNode* signatureElse; - short offset; - bool isNondeterminismVariable = false; - while (skipped && !Cudd_IsConstant(nonBlockVariablesNode)) { - // Remember an offset that indicates whether the top variable is a nondeterminism variable or not. - offset = options.shiftStateVariables ? 1 : 0; - if (!Cudd_IsConstant(nondeterminismVariablesNode) && Cudd_NodeReadIndex(nondeterminismVariablesNode) == Cudd_NodeReadIndex(nonBlockVariablesNode)) { - offset = 0; - isNondeterminismVariable = true; - } - - if (Cudd_NodeReadIndex(signatureNode) == Cudd_NodeReadIndex(nonBlockVariablesNode)) { - signatureThen = Cudd_T(signatureNode); - signatureElse = Cudd_E(signatureNode); - skipped = false; - } else { - signatureThen = signatureElse = signatureNode; - } - - // If we skipped the next variable, we fast-forward. - if (skipped) { - // If the current variable is a nondeterminism variable, we need to advance both variable sets otherwise just the non-block variables. - nonBlockVariablesNode = Cudd_T(nonBlockVariablesNode); - if (isNondeterminismVariable) { - nondeterminismVariablesNode = Cudd_T(nondeterminismVariablesNode); - } - } - } - - // If there are no more non-block variables remaining, make a recursive call to enter the base case. - if (Cudd_IsConstant(nonBlockVariablesNode)) { - return refineReuseSignatureResults(signatureNode, nondeterminismVariablesNode, nonBlockVariablesNode); - } - - DdNode* thenResult = refineReuseSignatureResults(signatureThen, isNondeterminismVariable ? Cudd_T(nondeterminismVariablesNode) : nondeterminismVariablesNode, Cudd_T(nonBlockVariablesNode)); - Cudd_Ref(thenResult); - DdNode* elseResult = refineReuseSignatureResults(signatureElse, isNondeterminismVariable ? Cudd_T(nondeterminismVariablesNode) : nondeterminismVariablesNode, Cudd_T(nonBlockVariablesNode)); - Cudd_Ref(elseResult); - - DdNode* result; - if (thenResult == elseResult) { - Cudd_Deref(thenResult); - Cudd_Deref(elseResult); - result = thenResult; - } else { - // Get the node to connect the subresults. - bool complemented = Cudd_IsComplement(thenResult); - result = cuddUniqueInter(ddman, Cudd_NodeReadIndex(nonBlockVariablesNode) + offset, Cudd_Regular(thenResult), complemented ? Cudd_Not(elseResult) : elseResult); - if (complemented) { - result = Cudd_Not(result); - } - Cudd_Deref(thenResult); - Cudd_Deref(elseResult); - } - - // Store the result in the cache. - signatureCache[signatureNode] = result; - - return result; - } - } - - DdNodePtr refineReuseBlockNumber(DdNode* partitionNode, DdNode* signatureNode, DdNode* nondeterminismVariablesNode, DdNode* nonBlockVariablesNode) { + DdNodePtr refine(DdNode* partitionNode, DdNode* signatureNode, DdNode* nondeterminismVariablesNode, DdNode* nonBlockVariablesNode) { // If we arrived at the constant zero node, then this was an illegal state encoding (we require // all states to be non-deadlock). if (partitionNode == Cudd_ReadZero(ddman)) { return partitionNode; } - + // Check the cache whether we have seen the same node before. auto nodePair = std::make_pair(signatureNode, partitionNode); - auto it = signatureCache2.find(nodePair); - if (it != signatureCache2.end()) { + + auto it = signatureCache.find(nodePair); + if (it != signatureCache.end()) { // If so, we return the corresponding result. return it->second; } // If there are no more non-block variables, we hit the signature. if (Cudd_IsConstant(nonBlockVariablesNode)) { - // If this is the first time (in this traversal) that we encounter this signature, we check - // whether we can assign the old block number to it. - auto& reuseEntry = reuseBlocksCache[partitionNode]; - if (!reuseEntry.isReused()) { - reuseEntry.setReused(); - signatureCache2[nodePair] = partitionNode; - return partitionNode; - } else { - DdNode* result = encodeBlock(nextFreeBlockIndex++); - signatureCache2[nodePair] = result; - return result; + if (options.reuseBlockNumbers) { + + // If this is the first time (in this traversal) that we encounter this signature, we check + // whether we can assign the old block number to it. + auto& reuseEntry = reuseBlocksCache[partitionNode]; + if (!reuseEntry.isReused()) { + reuseEntry.setReused(); + signatureCache[nodePair] = partitionNode; + return partitionNode; + } } + + DdNode* result = encodeBlock(nextFreeBlockIndex++); + signatureCache[nodePair] = result; + return result; } else { // If there are more variables that belong to the non-block part of the encoding, we need to recursively descend. @@ -335,12 +208,12 @@ namespace storm { // If there are no more non-block variables remaining, make a recursive call to enter the base case. if (Cudd_IsConstant(nonBlockVariablesNode)) { - return refineReuseBlockNumber(partitionNode, signatureNode, nondeterminismVariablesNode, nonBlockVariablesNode); + return refine(partitionNode, signatureNode, nondeterminismVariablesNode, nonBlockVariablesNode); } - DdNode* thenResult = refineReuseBlockNumber(partitionThen, signatureThen, isNondeterminismVariable ? Cudd_T(nondeterminismVariablesNode) : nondeterminismVariablesNode, Cudd_T(nonBlockVariablesNode)); + DdNode* thenResult = refine(partitionThen, signatureThen, isNondeterminismVariable ? Cudd_T(nondeterminismVariablesNode) : nondeterminismVariablesNode, Cudd_T(nonBlockVariablesNode)); Cudd_Ref(thenResult); - DdNode* elseResult = refineReuseBlockNumber(partitionElse, signatureElse, isNondeterminismVariable ? Cudd_T(nondeterminismVariablesNode) : nondeterminismVariablesNode, Cudd_T(nonBlockVariablesNode)); + DdNode* elseResult = refine(partitionElse, signatureElse, isNondeterminismVariable ? Cudd_T(nondeterminismVariablesNode) : nondeterminismVariablesNode, Cudd_T(nonBlockVariablesNode)); Cudd_Ref(elseResult); DdNode* result; @@ -360,8 +233,7 @@ namespace storm { } // Store the result in the cache. - signatureCache2[nodePair] = result; - + signatureCache[nodePair] = result; return result; } } @@ -394,9 +266,7 @@ namespace storm { uint64_t lastNumberOfVisitedNodes; // The cache used to identify states with identical signature. - spp::sparse_hash_map oldSignatureCache; - spp::sparse_hash_map signatureCache; - spp::sparse_hash_map, DdNode*, CuddPointerPairHash> signatureCache2; + spp::sparse_hash_map, DdNode*, CuddPointerPairHash> signatureCache; // The cache used to identify which old block numbers have already been reused. spp::sparse_hash_map reuseBlocksCache; @@ -412,44 +282,24 @@ namespace storm { } Partition refine(Partition const& oldPartition, Signature const& signature) { - storm::dd::Bdd newPartitionBdd; - if (options.reuseBlockNumbers && !options.reuseSignatureResult) { - newPartitionBdd = refineReuseBlockNumber(oldPartition, signature.getSignatureAdd()); - } else { - newPartitionBdd = refineReuseSignatureResults(oldPartition, signature.getSignatureAdd()); - } - - auto start = std::chrono::high_resolution_clock::now(); - uint64_t numberOfBlocks = nextFreeBlockIndex; - if (options.reuseSignatureResult) { - std::set blockVariableSet = {blockVariable}; - std::set nonBlockExpressionVariables; - std::set_difference(oldPartition.asBdd().getContainedMetaVariables().begin(), oldPartition.asBdd().getContainedMetaVariables().end(), blockVariableSet.begin(), blockVariableSet.end(), std::inserter(nonBlockExpressionVariables, nonBlockExpressionVariables.begin())); - numberOfBlocks = newPartitionBdd.existsAbstract(nonBlockExpressionVariables).getNonZeroCount(); - } - auto end = std::chrono::high_resolution_clock::now(); - std::cout << "took " << std::chrono::duration_cast(end - start).count() << std::endl; - - return oldPartition.replacePartition(newPartitionBdd, numberOfBlocks, nextFreeBlockIndex); + storm::dd::Bdd newPartitionBdd = refine(oldPartition, signature.getSignatureAdd()); + ++numberOfRefinements; + return oldPartition.replacePartition(newPartitionBdd, nextFreeBlockIndex, nextFreeBlockIndex); } private: void clearCaches() { signatureCache.clear(); - signatureCache2.clear(); reuseBlocksCache.clear(); } - storm::dd::Bdd refineReuseBlockNumber(Partition const& oldPartition, storm::dd::Add const& signatureAdd) { + storm::dd::Bdd refine(Partition const& oldPartition, storm::dd::Add const& signatureAdd) { STORM_LOG_ASSERT(oldPartition.storedAsBdd(), "Expecting partition to be stored as BDD for Sylvan."); - // Set up next refinement. - ++numberOfRefinements; - - nextFreeBlockIndex = oldPartition.getNextFreeBlockIndex(); + nextFreeBlockIndex = options.reuseBlockNumbers ? oldPartition.getNextFreeBlockIndex() : 0; // Perform the actual recursive refinement step. - BDD result = refineReuseBlockNumber(oldPartition.asBdd().getInternalBdd().getSylvanBdd().GetBDD(), signatureAdd.getInternalAdd().getSylvanMtbdd().GetMTBDD(), nondeterminismVariables.getInternalBdd().getSylvanBdd().GetBDD(), nonBlockVariables.getInternalBdd().getSylvanBdd().GetBDD()); + BDD result = refine(oldPartition.asBdd().getInternalBdd().getSylvanBdd().GetBDD(), signatureAdd.getInternalAdd().getSylvanMtbdd().GetMTBDD(), nondeterminismVariables.getInternalBdd().getSylvanBdd().GetBDD(), nonBlockVariables.getInternalBdd().getSylvanBdd().GetBDD()); // Construct resulting BDD from the obtained node and the meta information. storm::dd::InternalBdd internalNewPartitionBdd(&internalDdManager, sylvan::Bdd(result)); @@ -458,29 +308,7 @@ namespace storm { clearCaches(); return newPartitionBdd; } - - storm::dd::Bdd refineReuseSignatureResults(Partition const& oldPartition, storm::dd::Add const& signatureAdd) { - STORM_LOG_ASSERT(oldPartition.storedAsBdd(), "Expecting partition to be stored as BDD for Sylvan."); - - // Set up next refinement. - ++numberOfRefinements; - - nextFreeBlockIndex = options.reuseSignatureResult ? oldPartition.getNextFreeBlockIndex() : 0; - - // Perform the actual recursive refinement step. - BDD result = refineReuseSignatureResults(signatureAdd.getInternalAdd().getSylvanMtbdd().GetMTBDD(), nondeterminismVariables.getInternalBdd().getSylvanBdd().GetBDD(), nonBlockVariables.getInternalBdd().getSylvanBdd().GetBDD()); - - // Construct resulting BDD from the obtained node and the meta information. - storm::dd::InternalBdd internalNewPartitionBdd(&internalDdManager, sylvan::Bdd(result)); - storm::dd::Bdd newPartitionBdd(oldPartition.asBdd().getDdManager(), internalNewPartitionBdd, oldPartition.asBdd().getContainedMetaVariables()); - - if (options.reuseSignatureResult) { - oldSignatureCache = signatureCache; - } - clearCaches(); - return newPartitionBdd; - } - + BDD encodeBlock(uint64_t blockIndex) { std::vector e(numberOfBlockVariables); for (uint64_t i = 0; i < numberOfBlockVariables; ++i) { @@ -490,101 +318,7 @@ namespace storm { return sylvan_cube(blockCube.getInternalBdd().getSylvanBdd().GetBDD(), e.data()); } - BDD refineReuseSignatureResults(MTBDD signatureNode, BDD nondeterminismVariablesNode, BDD nonBlockVariablesNode) { - LACE_ME; - - // If we arrived at the constant zero node, then this was an illegal state encoding (we require - // all states to be non-deadlock). - if (mtbdd_iszero(signatureNode)) { - return sylvan_false; - } - - // Check the cache whether we have seen the same node before. - auto it = signatureCache.find(signatureNode); - if (it != signatureCache.end()) { - // If so, we return the corresponding result. - return it->second; - } - - // If we are to reuse signature results, check the old cache. - if (options.reuseSignatureResult) { - it = oldSignatureCache.find(signatureNode); - if (it != oldSignatureCache.end()) { - // If so, we return the corresponding result. - return it->second; - } - } - - sylvan_gc_test(); - - // If there are no more non-block variables, we hit the signature. - if (sylvan_isconst(nonBlockVariablesNode)) { - BDD result = encodeBlock(nextFreeBlockIndex++); - signatureCache[signatureNode] = result; - return result; - } else { - // If there are more variables that belong to the non-block part of the encoding, we need to recursively descend. - - bool skipped = true; - MTBDD signatureThen; - MTBDD signatureElse; - short offset; - bool isNondeterminismVariable = false; - while (skipped && !sylvan_isconst(nonBlockVariablesNode)) { - // Remember an offset that indicates whether the top variable is a nondeterminism variable or not. - offset = options.shiftStateVariables ? 1 : 0; - if (!sylvan_isconst(nondeterminismVariablesNode) && sylvan_var(nondeterminismVariablesNode) == sylvan_var(nonBlockVariablesNode)) { - offset = 0; - isNondeterminismVariable = true; - } - - if (storm::dd::InternalAdd::matchesVariableIndex(signatureNode, sylvan_var(nonBlockVariablesNode))) { - signatureThen = sylvan_high(signatureNode); - signatureElse = sylvan_low(signatureNode); - skipped = false; - } else { - signatureThen = signatureElse = signatureNode; - } - - // If we skipped the next variable, we fast-forward. - if (skipped) { - // If the current variable is a nondeterminism variable, we need to advance both variable sets otherwise just the non-block variables. - nonBlockVariablesNode = sylvan_high(nonBlockVariablesNode); - if (isNondeterminismVariable) { - nondeterminismVariablesNode = sylvan_high(nondeterminismVariablesNode); - } - } - } - - // If there are no more non-block variables remaining, make a recursive call to enter the base case. - if (sylvan_isconst(nonBlockVariablesNode)) { - return refineReuseSignatureResults(signatureNode, nondeterminismVariablesNode, nonBlockVariablesNode); - } - - BDD thenResult = refineReuseSignatureResults(signatureThen, isNondeterminismVariable ? sylvan_high(nondeterminismVariablesNode) : nondeterminismVariablesNode, sylvan_high(nonBlockVariablesNode)); - bdd_refs_push(thenResult); - BDD elseResult = refineReuseSignatureResults(signatureElse, isNondeterminismVariable ? sylvan_high(nondeterminismVariablesNode) : nondeterminismVariablesNode, sylvan_high(nonBlockVariablesNode)); - bdd_refs_push(elseResult); - - BDD result; - if (thenResult == elseResult) { - result = thenResult; - } else { - // Get the node to connect the subresults. - result = sylvan_makenode(sylvan_var(nonBlockVariablesNode) + offset, elseResult, thenResult); - } - - // Dispose of the intermediate results. - bdd_refs_pop(2); - - // Store the result in the cache. - signatureCache[signatureNode] = result; - - return result; - } - } - - BDD refineReuseBlockNumber(BDD partitionNode, MTBDD signatureNode, BDD nondeterminismVariablesNode, BDD nonBlockVariablesNode) { + BDD refine(BDD partitionNode, MTBDD signatureNode, BDD nondeterminismVariablesNode, BDD nonBlockVariablesNode) { LACE_ME; // If we arrived at the constant zero node, then this was an illegal state encoding (we require @@ -597,8 +331,8 @@ namespace storm { // Check the cache whether we have seen the same node before. auto nodePair = std::make_pair(signatureNode, partitionNode); - auto it = signatureCache2.find(nodePair); - if (it != signatureCache2.end()) { + auto it = signatureCache.find(nodePair); + if (it != signatureCache.end()) { // If so, we return the corresponding result. return it->second; } @@ -607,20 +341,22 @@ namespace storm { // If there are no more non-block variables, we hit the signature. if (sylvan_isconst(nonBlockVariablesNode)) { - // If this is the first time (in this traversal) that we encounter this signature, we check - // whether we can assign the old block number to it. + if (options.reuseBlockNumbers) { + // If this is the first time (in this traversal) that we encounter this signature, we check + // whether we can assign the old block number to it. - auto& reuseBlockEntry = reuseBlocksCache[partitionNode]; - if (!reuseBlockEntry.isReused()) { - reuseBlockEntry.setReused(); - reuseBlocksCache.emplace(partitionNode, true); - signatureCache2[nodePair] = partitionNode; - return partitionNode; - } else { - BDD result = encodeBlock(nextFreeBlockIndex++); - signatureCache2[nodePair] = result; - return result; + auto& reuseBlockEntry = reuseBlocksCache[partitionNode]; + if (!reuseBlockEntry.isReused()) { + reuseBlockEntry.setReused(); + reuseBlocksCache.emplace(partitionNode, true); + signatureCache[nodePair] = partitionNode; + return partitionNode; + } } + + BDD result = encodeBlock(nextFreeBlockIndex++); + signatureCache[nodePair] = result; + return result; } else { // If there are more variables that belong to the non-block part of the encoding, we need to recursively descend. @@ -667,12 +403,12 @@ namespace storm { // If there are no more non-block variables remaining, make a recursive call to enter the base case. if (sylvan_isconst(nonBlockVariablesNode)) { - return refineReuseBlockNumber(partitionNode, signatureNode, nondeterminismVariablesNode, nonBlockVariablesNode); + return refine(partitionNode, signatureNode, nondeterminismVariablesNode, nonBlockVariablesNode); } - BDD thenResult = refineReuseBlockNumber(partitionThen, signatureThen, isNondeterminismVariable ? sylvan_high(nondeterminismVariablesNode) : nondeterminismVariablesNode, sylvan_high(nonBlockVariablesNode)); + BDD thenResult = refine(partitionThen, signatureThen, isNondeterminismVariable ? sylvan_high(nondeterminismVariablesNode) : nondeterminismVariablesNode, sylvan_high(nonBlockVariablesNode)); bdd_refs_push(thenResult); - BDD elseResult = refineReuseBlockNumber(partitionElse, signatureElse, isNondeterminismVariable ? sylvan_high(nondeterminismVariablesNode) : nondeterminismVariablesNode, sylvan_high(nonBlockVariablesNode)); + BDD elseResult = refine(partitionElse, signatureElse, isNondeterminismVariable ? sylvan_high(nondeterminismVariablesNode) : nondeterminismVariablesNode, sylvan_high(nonBlockVariablesNode)); bdd_refs_push(elseResult); BDD result; @@ -687,7 +423,7 @@ namespace storm { bdd_refs_pop(2); // Store the result in the cache. - signatureCache2[nodePair] = result; + signatureCache[nodePair] = result; return result; } @@ -714,9 +450,7 @@ namespace storm { uint64_t numberOfRefinements; // The cache used to identify states with identical signature. - spp::sparse_hash_map oldSignatureCache; - spp::sparse_hash_map signatureCache; - spp::sparse_hash_map, MTBDD, SylvanMTBDDPairHash> signatureCache2; + spp::sparse_hash_map, MTBDD, SylvanMTBDDPairHash> signatureCache; // The cache used to identify which old block numbers have already been reused. spp::sparse_hash_map reuseBlocksCache;