From d2d129a8360fbb98b5d693c7423ccd1f782f5008 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 9 Nov 2017 16:39:40 +0100 Subject: [PATCH] toward multi-threaded dd bisimulation --- .../settings/modules/BisimulationSettings.cpp | 17 ++ .../settings/modules/BisimulationSettings.h | 8 + .../dd/bisimulation/QuotientExtractor.cpp | 22 +- .../dd/bisimulation/SignatureRefiner.cpp | 270 ++++++++++++++---- .../storage/dd/sylvan/InternalSylvanAdd.cpp | 7 +- .../storage/dd/sylvan/InternalSylvanAdd.h | 10 - .../storage/dd/sylvan/InternalSylvanBdd.cpp | 4 - .../storage/dd/sylvan/InternalSylvanBdd.h | 10 - src/storm/utility/sylvan.h | 30 ++ 9 files changed, 276 insertions(+), 102 deletions(-) diff --git a/src/storm/settings/modules/BisimulationSettings.cpp b/src/storm/settings/modules/BisimulationSettings.cpp index 8ed66dbdf..8c03c27c3 100644 --- a/src/storm/settings/modules/BisimulationSettings.cpp +++ b/src/storm/settings/modules/BisimulationSettings.cpp @@ -20,6 +20,7 @@ namespace storm { const std::string BisimulationSettings::reuseOptionName = "reuse"; const std::string BisimulationSettings::initialPartitionOptionName = "init"; const std::string BisimulationSettings::refinementModeOptionName = "refine"; + const std::string BisimulationSettings::parallelismModeOptionName = "parallel"; BisimulationSettings::BisimulationSettings() : ModuleSettings(moduleName) { std::vector types = { "strong", "weak" }; @@ -50,6 +51,12 @@ namespace storm { .addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(refinementModes)) .setDefaultValueString("full").build()) .build()); + + std::vector parallelismModes = {"on", "off"}; + this->addOption(storm::settings::OptionBuilder(moduleName, parallelismModeOptionName, true, "Sets whether to use parallelism mode or not.") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(parallelismModes)) + .setDefaultValueString("on").build()) + .build()); } bool BisimulationSettings::isStrongBisimulationSet() const { @@ -118,6 +125,16 @@ namespace storm { return RefinementMode::Full; } + BisimulationSettings::ParallelismMode BisimulationSettings::getParallelismMode() const { + std::string parallelismModeAsString = this->getOption(parallelismModeOptionName).getArgumentByName("mode").getValueAsString(); + if (parallelismModeAsString == "on") { + return ParallelismMode::Parallel; + } else if (parallelismModeAsString == "off") { + return ParallelismMode::Sequential; + } + return ParallelismMode::Parallel; + } + bool BisimulationSettings::check() const { bool optionsSet = this->getOption(typeOptionName).getHasOptionBeenSet(); STORM_LOG_WARN_COND(storm::settings::getModule().isBisimulationSet() || !optionsSet, "Bisimulation minimization is not selected, so setting options for bisimulation has no effect."); diff --git a/src/storm/settings/modules/BisimulationSettings.h b/src/storm/settings/modules/BisimulationSettings.h index 46deac738..4a12a4f28 100644 --- a/src/storm/settings/modules/BisimulationSettings.h +++ b/src/storm/settings/modules/BisimulationSettings.h @@ -25,6 +25,8 @@ namespace storm { enum class RefinementMode { Full, ChangedStates }; + enum class ParallelismMode { Parallel, Sequential }; + /*! * Creates a new set of bisimulation settings. */ @@ -76,6 +78,11 @@ namespace storm { */ RefinementMode getRefinementMode() const; + /*! + * Retrieves whether parallel is set. + */ + ParallelismMode getParallelismMode() const; + virtual bool check() const override; // The name of the module. @@ -90,6 +97,7 @@ namespace storm { static const std::string reuseOptionName; static const std::string initialPartitionOptionName; static const std::string refinementModeOptionName; + static const std::string parallelismModeOptionName; }; } // namespace modules } // namespace settings diff --git a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp index 895cea154..218b11ad7 100644 --- a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp +++ b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp @@ -175,7 +175,7 @@ namespace storm { bool skipped = false; BDD elsePartitionNode; BDD thenPartitionNode; - if (storm::dd::InternalBdd::matchesVariableIndex(partitionNode, sylvan_var(stateVariablesCube))) { + if (sylvan_bdd_matches_variable_index(partitionNode, sylvan_var(stateVariablesCube))) { elsePartitionNode = sylvan_low(partitionNode); thenPartitionNode = sylvan_high(partitionNode); } else { @@ -647,7 +647,7 @@ namespace storm { } else { MTBDD vectorT; MTBDD vectorE; - if (storm::dd::InternalAdd::matchesVariableIndex(vector, sylvan_var(variables))) { + if (sylvan_mtbdd_matches_variable_index(vector, sylvan_var(variables))) { vectorT = sylvan_high(vector); vectorE = sylvan_low(vector); } else { @@ -656,7 +656,7 @@ namespace storm { BDD representativesT; BDD representativesE; - if (storm::dd::InternalBdd::matchesVariableIndex(representativesNode, sylvan_var(variables))) { + if (sylvan_bdd_matches_variable_index(representativesNode, sylvan_var(variables))) { representativesT = sylvan_high(representativesNode); representativesE = sylvan_low(representativesNode); } else { @@ -687,7 +687,7 @@ namespace storm { STORM_LOG_ASSERT(!odd.isTerminalNode(), "Expected non-terminal node."); BDD partitionT; BDD partitionE; - if (storm::dd::InternalBdd::matchesVariableIndex(partitionNode, sylvan_var(variables))) { + if (sylvan_bdd_matches_variable_index(partitionNode, sylvan_var(variables))) { partitionT = sylvan_high(partitionNode); partitionE = sylvan_low(partitionNode); } else { @@ -696,7 +696,7 @@ namespace storm { BDD representativesT; BDD representativesE; - if (storm::dd::InternalBdd::matchesVariableIndex(representativesNode, sylvan_var(variables))) { + if (sylvan_bdd_matches_variable_index(representativesNode, sylvan_var(variables))) { representativesT = sylvan_high(representativesNode); representativesE = sylvan_low(representativesNode); } else { @@ -732,7 +732,7 @@ namespace storm { MTBDD e; // Determine whether the variable was skipped in the matrix. - if (storm::dd::InternalAdd::matchesVariableIndex(transitionMatrixNode, sylvan_var(variables))) { + if (sylvan_mtbdd_matches_variable_index(transitionMatrixNode, sylvan_var(variables))) { t = sylvan_high(transitionMatrixNode); e = sylvan_low(transitionMatrixNode); } else { @@ -749,7 +749,7 @@ namespace storm { MTBDD e; MTBDD et; MTBDD ee; - if (storm::dd::InternalAdd::matchesVariableIndex(transitionMatrixNode, sylvan_var(variables))) { + if (sylvan_mtbdd_matches_variable_index(transitionMatrixNode, sylvan_var(variables))) { // Source node was not skipped in transition matrix. t = sylvan_high(transitionMatrixNode); e = sylvan_low(transitionMatrixNode); @@ -757,7 +757,7 @@ namespace storm { t = e = transitionMatrixNode; } - if (storm::dd::InternalAdd::matchesVariableIndex(t, sylvan_var(variables) + 1)) { + if (sylvan_mtbdd_matches_variable_index(t, sylvan_var(variables) + 1)) { // Target node was not skipped in transition matrix. tt = sylvan_high(t); te = sylvan_low(t); @@ -766,7 +766,7 @@ namespace storm { tt = te = t; } if (t != e) { - if (storm::dd::InternalAdd::matchesVariableIndex(e, sylvan_var(variables) + 1)) { + if (sylvan_mtbdd_matches_variable_index(e, sylvan_var(variables) + 1)) { // Target node was not skipped in transition matrix. et = sylvan_high(e); ee = sylvan_low(e); @@ -781,7 +781,7 @@ namespace storm { BDD targetT; BDD targetE; - if (storm::dd::InternalBdd::matchesVariableIndex(targetPartitionNode, sylvan_var(variables))) { + if (sylvan_bdd_matches_variable_index(targetPartitionNode, sylvan_var(variables))) { // Node was not skipped in target partition. targetT = sylvan_high(targetPartitionNode); targetE = sylvan_low(targetPartitionNode); @@ -792,7 +792,7 @@ namespace storm { BDD representativesT; BDD representativesE; - if (storm::dd::InternalBdd::matchesVariableIndex(representativesNode, sylvan_var(variables))) { + if (sylvan_bdd_matches_variable_index(representativesNode, sylvan_var(variables))) { // Node was not skipped in representatives. representativesT = sylvan_high(representativesNode); representativesE = sylvan_low(representativesNode); diff --git a/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp b/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp index d6d674c4a..dfc24ec0f 100644 --- a/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp +++ b/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp @@ -1,6 +1,7 @@ #include "storm/storage/dd/bisimulation/SignatureRefiner.h" #include +#include #include #include @@ -41,7 +42,7 @@ namespace storm { // Intentionally left empty. } - InternalSignatureRefinerOptions(bool shiftStateVariables) : shiftStateVariables(shiftStateVariables), createChangedStates(true) { + InternalSignatureRefinerOptions(bool shiftStateVariables) : shiftStateVariables(shiftStateVariables), createChangedStates(true), parallel(false) { auto const& bisimulationSettings = storm::settings::getModule(); storm::settings::modules::BisimulationSettings::ReuseMode reuseMode = bisimulationSettings.getReuseMode(); @@ -49,11 +50,15 @@ namespace storm { storm::settings::modules::BisimulationSettings::RefinementMode refinementMode = bisimulationSettings.getRefinementMode(); this->createChangedStates = refinementMode == storm::settings::modules::BisimulationSettings::RefinementMode::ChangedStates; + + storm::settings::modules::BisimulationSettings::ParallelismMode parallelismMode = bisimulationSettings.getParallelismMode(); + this->parallel = parallelismMode == storm::settings::modules::BisimulationSettings::ParallelismMode::Parallel; } bool shiftStateVariables; bool reuseBlockNumbers; bool createChangedStates; + bool parallel; }; class ReuseWrapper { @@ -461,24 +466,79 @@ namespace storm { spp::sparse_hash_map reuseBlocksCache; }; - template - class InternalSignatureRefiner { + TASK_DECL_5(BDD, refine_double, BDD, MTBDD, BDD, BDD, void*); + + template + class InternalSignatureRefinerBase; + + template<> + class InternalSignatureRefinerBase { public: - InternalSignatureRefiner(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), internalDdManager(manager.getInternalDdManager()), blockVariable(blockVariable), stateVariables(stateVariables), nondeterminismVariables(nondeterminismVariables), nonBlockVariables(nonBlockVariables), options(options), numberOfBlockVariables(manager.getMetaVariable(blockVariable).getNumberOfDdVariables()), blockCube(manager.getMetaVariable(blockVariable).getCube()), nextFreeBlockIndex(0), numberOfRefinements(0), signatureCache() { + InternalSignatureRefinerBase(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), internalDdManager(manager.getInternalDdManager()), blockVariable(blockVariable), stateVariables(stateVariables), nondeterminismVariables(nondeterminismVariables), nonBlockVariables(nonBlockVariables), options(options), numberOfBlockVariables(manager.getMetaVariable(blockVariable).getNumberOfDdVariables()), blockCube(manager.getMetaVariable(blockVariable).getCube()), nextFreeBlockIndex(0), numberOfRefinements(0), signatureCache() { + // Perform garbage collection to clean up stuff not needed anymore. LACE_ME; sylvan_gc(); } + BDD encodeBlock(uint64_t blockIndex) { + std::vector e(numberOfBlockVariables); + for (uint64_t i = 0; i < numberOfBlockVariables; ++i) { + e[i] = blockIndex & 1 ? 1 : 0; + blockIndex >>= 1; + } + return sylvan_cube(blockCube.getInternalBdd().getSylvanBdd().GetBDD(), e.data()); + } + + storm::dd::DdManager const& manager; + storm::dd::InternalDdManager const& internalDdManager; + storm::expressions::Variable blockVariable; + std::set stateVariables; + + storm::dd::Bdd nondeterminismVariables; + storm::dd::Bdd nonBlockVariables; + + // The provided options. + InternalSignatureRefinerOptions options; + + uint64_t numberOfBlockVariables; + + storm::dd::Bdd blockCube; + + // The current number of blocks of the new partition. + uint64_t nextFreeBlockIndex; + + // The number of completed refinements. + uint64_t numberOfRefinements; + + // The cache used to identify states with identical signature. + spp::sparse_hash_map, std::pair, SylvanMTBDDPairHash> signatureCache; + spp::sparse_hash_map, BDD, SylvanMTBDDPairHash> signatureCacheSingle; + + // The cache used to identify which old block numbers have already been reused. + spp::sparse_hash_map reuseBlocksCache; + + // A mutex that can be used to synchronize concurrent accesses to the members. + std::mutex mutex; + }; + + template + class InternalSignatureRefiner : public InternalSignatureRefinerBase { + public: + InternalSignatureRefiner(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) : InternalSignatureRefinerBase(manager, blockVariable, stateVariables, nondeterminismVariables, nonBlockVariables, options) { + + // Intentionally left empty. + } + Partition 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); } - private: void clearCaches() { signatureCache.clear(); + signatureCacheSingle.clear(); reuseBlocksCache.clear(); } @@ -488,14 +548,21 @@ namespace storm { nextFreeBlockIndex = options.reuseBlockNumbers ? oldPartition.getNextFreeBlockIndex() : 0; // Perform the actual recursive refinement step. - std::pair result = refine(oldPartition.asBdd().getInternalBdd().getSylvanBdd().GetBDD(), signatureAdd.getInternalAdd().getSylvanMtbdd().GetMTBDD(), nondeterminismVariables.getInternalBdd().getSylvanBdd().GetBDD(), nonBlockVariables.getInternalBdd().getSylvanBdd().GetBDD()); - + std::pair result; + if (options.parallel) { + STORM_LOG_TRACE("Using parallel refine."); + result = refineParallel(oldPartition.asBdd().getInternalBdd().getSylvanBdd().GetBDD(), signatureAdd.getInternalAdd().getSylvanMtbdd().GetMTBDD(), nondeterminismVariables.getInternalBdd().getSylvanBdd().GetBDD(), nonBlockVariables.getInternalBdd().getSylvanBdd().GetBDD()); + } else { + STORM_LOG_TRACE("Using sequential refine."); + result = refineSequential(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.first)); storm::dd::Bdd newPartitionBdd(oldPartition.asBdd().getDdManager(), internalNewPartitionBdd, oldPartition.asBdd().getContainedMetaVariables()); boost::optional> optionalChangedBdd; - if (options.createChangedStates) { + if (options.createChangedStates && result.second != 0) { storm::dd::InternalBdd internalChangedBdd(&internalDdManager, sylvan::Bdd(result.second)); storm::dd::Bdd changedBdd(oldPartition.asBdd().getDdManager(), internalChangedBdd, stateVariables); optionalChangedBdd = changedBdd; @@ -504,15 +571,6 @@ namespace storm { clearCaches(); return std::make_pair(newPartitionBdd, optionalChangedBdd); } - - BDD encodeBlock(uint64_t blockIndex) { - std::vector e(numberOfBlockVariables); - for (uint64_t i = 0; i < numberOfBlockVariables; ++i) { - e[i] = blockIndex & 1 ? 1 : 0; - blockIndex >>= 1; - } - return sylvan_cube(blockCube.getInternalBdd().getSylvanBdd().GetBDD(), e.data()); - } std::pair reuseOrRelabel(BDD partitionNode, BDD nondeterminismVariablesNode, BDD nonBlockVariablesNode) { LACE_ME; @@ -580,7 +638,7 @@ namespace storm { isNondeterminismVariable = true; } - if (storm::dd::InternalAdd::matchesVariableIndex(partitionNode, sylvan_var(nonBlockVariablesNode), -offset)) { + if (sylvan_mtbdd_matches_variable_index(partitionNode, sylvan_var(nonBlockVariablesNode), -offset)) { partitionThen = sylvan_high(partitionNode); partitionElse = sylvan_low(partitionNode); skipped = false; @@ -649,7 +707,12 @@ namespace storm { } } - std::pair refine(BDD partitionNode, MTBDD signatureNode, BDD nondeterminismVariablesNode, BDD nonBlockVariablesNode) { + std::pair refineParallel(BDD partitionNode, MTBDD signatureNode, BDD nondeterminismVariablesNode, BDD nonBlockVariablesNode) { + LACE_ME; + return std::make_pair(CALL(refine_double, partitionNode, signatureNode, nondeterminismVariablesNode, nonBlockVariablesNode, this), 0); + } + + std::pair refineSequential(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 @@ -675,9 +738,9 @@ namespace storm { // 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)) { if (options.reuseBlockNumbers) { @@ -709,7 +772,7 @@ namespace storm { return result; } else { // If there are more variables that belong to the non-block part of the encoding, we need to recursively descend. - + bool skippedBoth = true; BDD partitionThen; BDD partitionElse; @@ -725,22 +788,22 @@ namespace storm { isNondeterminismVariable = true; } - if (storm::dd::InternalAdd::matchesVariableIndex(partitionNode, sylvan_var(nonBlockVariablesNode), -offset)) { + if (sylvan_mtbdd_matches_variable_index(partitionNode, sylvan_var(nonBlockVariablesNode), -offset)) { partitionThen = sylvan_high(partitionNode); partitionElse = sylvan_low(partitionNode); skippedBoth = false; } else { partitionThen = partitionElse = partitionNode; } - - if (storm::dd::InternalAdd::matchesVariableIndex(signatureNode, sylvan_var(nonBlockVariablesNode))) { + + if (sylvan_mtbdd_matches_variable_index(signatureNode, sylvan_var(nonBlockVariablesNode))) { signatureThen = sylvan_high(signatureNode); signatureElse = sylvan_low(signatureNode); skippedBoth = false; } else { signatureThen = signatureElse = signatureNode; } - + // If both (signature and partition) skipped the next variable, we fast-forward. if (skippedBoth) { // If the current variable is a nondeterminism variable, we need to advance both variable sets otherwise just the non-block variables. @@ -750,20 +813,20 @@ 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 refine(partitionNode, signatureNode, nondeterminismVariablesNode, nonBlockVariablesNode); + return refineSequential(partitionNode, signatureNode, nondeterminismVariablesNode, nonBlockVariablesNode); } - - std::pair combinedThenResult = refine(partitionThen, signatureThen, isNondeterminismVariable ? sylvan_high(nondeterminismVariablesNode) : nondeterminismVariablesNode, sylvan_high(nonBlockVariablesNode)); + + std::pair combinedThenResult = refineSequential(partitionThen, signatureThen, isNondeterminismVariable ? sylvan_high(nondeterminismVariablesNode) : nondeterminismVariablesNode, sylvan_high(nonBlockVariablesNode)); BDD thenResult = combinedThenResult.first; bdd_refs_push(thenResult); BDD changedThenResult = combinedThenResult.second; if (options.createChangedStates) { bdd_refs_push(changedThenResult); } - std::pair combinedElseResult = refine(partitionElse, signatureElse, isNondeterminismVariable ? sylvan_high(nondeterminismVariablesNode) : nondeterminismVariablesNode, sylvan_high(nonBlockVariablesNode)); + std::pair combinedElseResult = refineSequential(partitionElse, signatureElse, isNondeterminismVariable ? sylvan_high(nondeterminismVariablesNode) : nondeterminismVariablesNode, sylvan_high(nonBlockVariablesNode)); BDD elseResult = combinedElseResult.first; bdd_refs_push(elseResult); BDD changedElseResult = combinedElseResult.second; @@ -798,49 +861,134 @@ namespace storm { // Store the result in the cache. signatureCache[nodePair] = result; - + return result; } } - storm::dd::DdManager const& manager; - storm::dd::InternalDdManager const& internalDdManager; - storm::expressions::Variable blockVariable; - std::set stateVariables; + }; + + TASK_IMPL_5(BDD, refine_double, BDD, partitionNode, MTBDD, signatureNode, BDD, nondeterminismVariablesNode, BDD, nonBlockVariablesNode, void*, refinerPtr) + { + auto& refiner = *static_cast*>(refinerPtr); + std::unique_lock lock(refiner.mutex, std::defer_lock); + + // 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 == sylvan_false) { + return sylvan_false; + } - storm::dd::Bdd nondeterminismVariables; - storm::dd::Bdd nonBlockVariables; + STORM_LOG_ASSERT(partitionNode != mtbdd_false, "Expected non-false node."); - // The provided options. - InternalSignatureRefinerOptions options; + BDD result; - uint64_t numberOfBlockVariables; + if (sylvan_isconst(nonBlockVariablesNode)) { + // Get the lock so we can modify the signature cache. + lock.lock(); + + // Check the signature cache whether we have seen this signature before. + auto nodePair = std::make_pair(signatureNode, partitionNode); + auto it = refiner.signatureCacheSingle.find(nodePair); + if (it != refiner.signatureCacheSingle.end()) { + return it->second; + } + + if (refiner.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 = refiner.reuseBlocksCache[partitionNode]; + if (!reuseBlockEntry.isReused()) { + reuseBlockEntry.setReused(); + refiner.reuseBlocksCache.emplace(partitionNode, true); + refiner.signatureCacheSingle[nodePair] = partitionNode; + return partitionNode; + } + } + + // Encode new block and give up lock before + result = refiner.encodeBlock(refiner.nextFreeBlockIndex++); + refiner.signatureCacheSingle[nodePair] = result; + lock.unlock(); + return result; + } - storm::dd::Bdd blockCube; + // Check the cache whether we have seen the same node before. + if (cache_get(signatureNode|(256LL<<42), nonBlockVariablesNode, partitionNode|(refiner.numberOfRefinements<<40), &result)) { + return result; + } - // The current number of blocks of the new partition. - uint64_t nextFreeBlockIndex; + sylvan_gc_test(); - // The number of completed refinements. - uint64_t numberOfRefinements; + // If there are more variables that belong to the non-block part of the encoding, we need to recursively descend. - // The cache used to identify states with identical signature. - spp::sparse_hash_map, std::pair, SylvanMTBDDPairHash> signatureCache; + bool skippedBoth = true; + BDD partitionThen; + BDD partitionElse; + MTBDD signatureThen; + MTBDD signatureElse; + short offset; + bool isNondeterminismVariable = false; + while (skippedBoth && !sylvan_isconst(nonBlockVariablesNode)) { + // Remember an offset that indicates whether the top variable is a nondeterminism variable or not. + offset = refiner.options.shiftStateVariables ? 1 : 0; + if (!sylvan_isconst(nondeterminismVariablesNode) && sylvan_var(nondeterminismVariablesNode) == sylvan_var(nonBlockVariablesNode)) { + offset = 0; + isNondeterminismVariable = true; + } + + if (sylvan_mtbdd_matches_variable_index(partitionNode, sylvan_var(nonBlockVariablesNode), -offset)) { + partitionThen = sylvan_high(partitionNode); + partitionElse = sylvan_low(partitionNode); + skippedBoth = false; + } else { + partitionThen = partitionElse = partitionNode; + } + + if (sylvan_mtbdd_matches_variable_index(signatureNode, sylvan_var(nonBlockVariablesNode))) { + signatureThen = sylvan_high(signatureNode); + signatureElse = sylvan_low(signatureNode); + skippedBoth = false; + } else { + signatureThen = signatureElse = signatureNode; + } + + // If both (signature and partition) skipped the next variable, we fast-forward. + if (skippedBoth) { + // 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); + } + } + } - // The cache used to identify which old block numbers have already been reused. - spp::sparse_hash_map reuseBlocksCache; + // If there are no more non-block variables remaining, make a recursive call to enter the base case. + if (sylvan_isconst(nonBlockVariablesNode)) { + return CALL(refine_double, partitionNode, signatureNode, nondeterminismVariablesNode, nonBlockVariablesNode, refinerPtr); + } - // Performance counters. -// uint64_t signatureCacheLookups; -// uint64_t signatureCacheHits; -// uint64_t numberOfVisitedNodes; -// std::chrono::high_resolution_clock::duration totalSignatureCacheLookupTime; -// std::chrono::high_resolution_clock::duration totalSignatureCacheStoreTime; -// std::chrono::high_resolution_clock::duration totalReuseBlocksLookupTime; -// std::chrono::high_resolution_clock::duration totalLevelLookupTime; -// std::chrono::high_resolution_clock::duration totalBlockEncodingTime; -// std::chrono::high_resolution_clock::duration totalMakeNodeTime; - }; + BDD nextNondeterminismVariables = isNondeterminismVariable ? sylvan_set_next(nondeterminismVariablesNode) : nondeterminismVariablesNode; + BDD nextNonBlockVariables = sylvan_set_next(nonBlockVariablesNode); + bdd_refs_spawn(SPAWN(refine_double, partitionThen, signatureThen, nextNondeterminismVariables, nextNonBlockVariables, refinerPtr)); + + BDD elseResult = bdd_refs_push(CALL(refine_double, partitionElse, signatureElse, nextNondeterminismVariables, nextNonBlockVariables, refinerPtr)); + BDD thenResult = bdd_refs_sync(SYNC(refine_double)); + bdd_refs_pop(1); + + if (thenResult == elseResult) { + result = thenResult; + } else { + // Get the node to connect the subresults. + result = sylvan_makenode(sylvan_var(nonBlockVariablesNode) + offset, elseResult, thenResult); + } + + // Store the result in the cache. + cache_put(signatureNode|(256LL<<42), nonBlockVariablesNode, partitionNode|(refiner.numberOfRefinements<<40), result); + + return result; + } template SignatureRefiner::SignatureRefiner(storm::dd::DdManager const& manager, storm::expressions::Variable const& blockVariable, std::set const& stateRowVariables, std::set const& stateColumnVariables, bool shiftStateVariables, std::set const& nondeterminismVariables) : manager(&manager) { diff --git a/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp b/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp index ce1576956..b3723a4c4 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp +++ b/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp @@ -79,12 +79,7 @@ namespace storm { return negated ? -(*rationalFunction) : (*rationalFunction); } #endif - - template - bool InternalAdd::matchesVariableIndex(MTBDD const& node, uint64_t variableIndex, int64_t offset) { - return !mtbdd_isleaf(node) && static_cast(sylvan_var(node) + offset) == variableIndex; - } - + template bool InternalAdd::operator==(InternalAdd const& other) const { return this->sylvanMtbdd == other.sylvanMtbdd; diff --git a/src/storm/storage/dd/sylvan/InternalSylvanAdd.h b/src/storm/storage/dd/sylvan/InternalSylvanAdd.h index 139d39ee4..c4374c2b1 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanAdd.h +++ b/src/storm/storage/dd/sylvan/InternalSylvanAdd.h @@ -618,16 +618,6 @@ namespace storm { * @return The value of the leaf. */ static ValueType getValue(MTBDD const& node); - - /*! - * Retrieves whether the topmost variable in the MTBDD is the one with the given index. - * - * @param The top node of the MTBDD. - * @param variableIndex The variable index. - * @param offset An offset that is applied to the index of the top variable in the MTBDD. - * @return True iff the MTBDD's top variable has the given index. - */ - static bool matchesVariableIndex(MTBDD const& node, uint64_t variableIndex, int64_t offset = 0); private: /*! diff --git a/src/storm/storage/dd/sylvan/InternalSylvanBdd.cpp b/src/storm/storage/dd/sylvan/InternalSylvanBdd.cpp index 00e12dfdb..97252476a 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanBdd.cpp +++ b/src/storm/storage/dd/sylvan/InternalSylvanBdd.cpp @@ -527,10 +527,6 @@ namespace storm { return newNodeVariable; } - bool InternalBdd::matchesVariableIndex(BDD const& node, uint64_t variableIndex, int64_t offset) { - return !sylvan_isconst(node) && static_cast(sylvan_var(node) + offset) == variableIndex; - } - template InternalAdd InternalBdd::toAdd() const; template InternalAdd InternalBdd::toAdd() const; template InternalAdd InternalBdd::toAdd() const; diff --git a/src/storm/storage/dd/sylvan/InternalSylvanBdd.h b/src/storm/storage/dd/sylvan/InternalSylvanBdd.h index 6c07449c7..a1160654c 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanBdd.h +++ b/src/storm/storage/dd/sylvan/InternalSylvanBdd.h @@ -373,16 +373,6 @@ namespace storm { * @param targetValues The vector to which to write the selected values. */ void filterExplicitVector(Odd const& odd, std::vector const& ddVariableIndices, storm::storage::BitVector const& sourceValues, storm::storage::BitVector& targetValues) const; - - /*! - * Retrieves whether the topmost variable in the BDD is the one with the given index. - * - * @param The top node of the BDD. - * @param variableIndex The variable index. - * @param offset An offset that is applied to the index of the top variable in the BDD. - * @return True iff the BDD's top variable has the given index. - */ - static bool matchesVariableIndex(BDD const& node, uint64_t variableIndex, int64_t offset = 0); friend struct std::hash>; diff --git a/src/storm/utility/sylvan.h b/src/storm/utility/sylvan.h index 5f351b946..f7495bedb 100644 --- a/src/storm/utility/sylvan.h +++ b/src/storm/utility/sylvan.h @@ -17,5 +17,35 @@ #include "sylvan_storm_rational_number.h" #include "sylvan_storm_rational_function.h" +namespace storm { + namespace dd { + + /*! + * Retrieves whether the topmost variable in the BDD is the one with the given index. + * + * @param node The top node of the BDD. + * @param variableIndex The variable index. + * @param offset An offset that is applied to the index of the top variable in the BDD. + * @return True iff the BDD's top variable has the given index. + */ + bool sylvan_bdd_matches_variable_index(BDD node, uint64_t variableIndex, int64_t offset = 0) { + return !sylvan_isconst(node) && static_cast(sylvan_var(node) + offset) == variableIndex; + } + + /*! + * Retrieves whether the topmost variable in the MTBDD is the one with the given index. + * + * @param node The top node of the BDD. + * @param variableIndex The variable index. + * @param offset An offset that is applied to the index of the top variable in the BDD. + * @return True iff the BDD's top variable has the given index. + */ + bool sylvan_mtbdd_matches_variable_index(MTBDD node, uint64_t variableIndex, int64_t offset = 0) { + return !mtbdd_isleaf(node) && static_cast(sylvan_var(node) + offset) == variableIndex; + } + + } +} + #pragma GCC diagnostic pop #pragma clang diagnostic pop