diff --git a/src/storm/settings/modules/BisimulationSettings.cpp b/src/storm/settings/modules/BisimulationSettings.cpp index d048a35ca..8ed66dbdf 100644 --- a/src/storm/settings/modules/BisimulationSettings.cpp +++ b/src/storm/settings/modules/BisimulationSettings.cpp @@ -19,6 +19,7 @@ namespace storm { const std::string BisimulationSettings::signatureModeOptionName = "sigmode"; const std::string BisimulationSettings::reuseOptionName = "reuse"; const std::string BisimulationSettings::initialPartitionOptionName = "init"; + const std::string BisimulationSettings::refinementModeOptionName = "refine"; BisimulationSettings::BisimulationSettings() : ModuleSettings(moduleName) { std::vector types = { "strong", "weak" }; @@ -43,6 +44,12 @@ namespace storm { .addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(initialPartitionModes)) .setDefaultValueString("finer").build()) .build()); + + std::vector refinementModes = {"full", "changed"}; + this->addOption(storm::settings::OptionBuilder(moduleName, refinementModeOptionName, true, "Sets which refinement mode to use.") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(refinementModes)) + .setDefaultValueString("full").build()) + .build()); } bool BisimulationSettings::isStrongBisimulationSet() const { @@ -100,7 +107,17 @@ namespace storm { } return InitialPartitionMode::Finer; } - + + BisimulationSettings::RefinementMode BisimulationSettings::getRefinementMode() const { + std::string refinementModeAsString = this->getOption(refinementModeOptionName).getArgumentByName("mode").getValueAsString(); + if (refinementModeAsString == "full") { + return RefinementMode::Full; + } else if (refinementModeAsString == "changed") { + return RefinementMode::ChangedStates; + } + return RefinementMode::Full; + } + 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 ed1a15c6d..46deac738 100644 --- a/src/storm/settings/modules/BisimulationSettings.h +++ b/src/storm/settings/modules/BisimulationSettings.h @@ -23,6 +23,8 @@ namespace storm { enum class InitialPartitionMode { Regular, Finer }; + enum class RefinementMode { Full, ChangedStates }; + /*! * Creates a new set of bisimulation settings. */ @@ -69,6 +71,11 @@ namespace storm { */ InitialPartitionMode getInitialPartitionMode() const; + /*! + * Retrieves the refinement mode to use. + */ + RefinementMode getRefinementMode() const; + virtual bool check() const override; // The name of the module. @@ -82,6 +89,7 @@ namespace storm { static const std::string signatureModeOptionName; static const std::string reuseOptionName; static const std::string initialPartitionOptionName; + static const std::string refinementModeOptionName; }; } // namespace modules } // namespace settings diff --git a/src/storm/storage/dd/bisimulation/Partition.cpp b/src/storm/storage/dd/bisimulation/Partition.cpp index 46a265fd6..d3708c6a5 100644 --- a/src/storm/storage/dd/bisimulation/Partition.cpp +++ b/src/storm/storage/dd/bisimulation/Partition.cpp @@ -32,12 +32,12 @@ namespace storm { } template - Partition::Partition(storm::dd::Add const& partitionAdd, std::pair const& blockVariables, uint64_t numberOfBlocks, uint64_t nextFreeBlockIndex) : partition(partitionAdd), blockVariables(blockVariables), numberOfBlocks(numberOfBlocks), nextFreeBlockIndex(nextFreeBlockIndex) { + Partition::Partition(storm::dd::Add const& partitionAdd, std::pair const& blockVariables, uint64_t numberOfBlocks, uint64_t nextFreeBlockIndex, boost::optional> const& changedStates) : partition(partitionAdd), changedStates(changedStates), blockVariables(blockVariables), numberOfBlocks(numberOfBlocks), nextFreeBlockIndex(nextFreeBlockIndex) { // Intentionally left empty. } template - Partition::Partition(storm::dd::Bdd const& partitionBdd, std::pair const& blockVariables, uint64_t numberOfBlocks, uint64_t nextFreeBlockIndex) : partition(partitionBdd), blockVariables(blockVariables), numberOfBlocks(numberOfBlocks), nextFreeBlockIndex(nextFreeBlockIndex) { + Partition::Partition(storm::dd::Bdd const& partitionBdd, std::pair const& blockVariables, uint64_t numberOfBlocks, uint64_t nextFreeBlockIndex, boost::optional> const& changedStates) : partition(partitionBdd), changedStates(changedStates), blockVariables(blockVariables), numberOfBlocks(numberOfBlocks), nextFreeBlockIndex(nextFreeBlockIndex) { // Intentionally left empty. } @@ -47,13 +47,13 @@ namespace storm { } template - Partition Partition::replacePartition(storm::dd::Add const& newPartitionAdd, uint64_t numberOfBlocks, uint64_t nextFreeBlockIndex) const { - return Partition(newPartitionAdd, blockVariables, numberOfBlocks, nextFreeBlockIndex); + Partition Partition::replacePartition(storm::dd::Add const& newPartitionAdd, uint64_t numberOfBlocks, uint64_t nextFreeBlockIndex, boost::optional> const& changedStates) const { + return Partition(newPartitionAdd, blockVariables, numberOfBlocks, nextFreeBlockIndex, changedStates); } template - Partition Partition::replacePartition(storm::dd::Bdd const& newPartitionBdd, uint64_t numberOfBlocks, uint64_t nextFreeBlockIndex) const { - return Partition(newPartitionBdd, blockVariables, numberOfBlocks, nextFreeBlockIndex); + Partition Partition::replacePartition(storm::dd::Bdd const& newPartitionBdd, uint64_t numberOfBlocks, uint64_t nextFreeBlockIndex, boost::optional> const& changedStates) const { + return Partition(newPartitionBdd, blockVariables, numberOfBlocks, nextFreeBlockIndex, changedStates); } template @@ -227,6 +227,21 @@ namespace storm { } } + template + bool Partition::hasChangedStates() const { + return static_cast(changedStates); + } + + template + storm::dd::Add const& Partition::changedStatesAsAdd() const { + return boost::get>(changedStates.get()); + } + + template + storm::dd::Bdd const& Partition::changedStatesAsBdd() const { + return boost::get>(changedStates.get()); + } + template uint64_t Partition::getNumberOfBlocks() const { return numberOfBlocks; diff --git a/src/storm/storage/dd/bisimulation/Partition.h b/src/storm/storage/dd/bisimulation/Partition.h index 8b5f16365..ef824898c 100644 --- a/src/storm/storage/dd/bisimulation/Partition.h +++ b/src/storm/storage/dd/bisimulation/Partition.h @@ -31,8 +31,8 @@ namespace storm { bool operator==(Partition const& other); - Partition replacePartition(storm::dd::Add const& newPartitionAdd, uint64_t numberOfBlocks, uint64_t nextFreeBlockIndex) const; - Partition replacePartition(storm::dd::Bdd const& newPartitionBdd, uint64_t numberOfBlocks, uint64_t nextFreeBlockIndex) const; + Partition replacePartition(storm::dd::Add const& newPartitionAdd, uint64_t numberOfBlocks, uint64_t nextFreeBlockIndex, boost::optional> const& changedStates = boost::none) const; + Partition replacePartition(storm::dd::Bdd const& newPartitionBdd, uint64_t numberOfBlocks, uint64_t nextFreeBlockIndex, boost::optional> const& changedStates = boost::none) const; static Partition create(storm::models::symbolic::Model const& model, storm::storage::BisimulationType const& bisimulationType, PreservationInformation const& preservationInformation); static Partition create(storm::models::symbolic::Model const& model, storm::storage::BisimulationType const& bisimulationType, std::vector> const& formulas); @@ -55,7 +55,18 @@ namespace storm { uint64_t getNodeCount() const; storm::dd::Bdd getStates() const; - + + /*! + * Retrieves whether this partition has information about the states whose partition block assignment changed. + */ + bool hasChangedStates() const; + + /*! + * Retrieves the DD representing the states whose partition block assignment changed. + */ + storm::dd::Add const& changedStatesAsAdd() const; + storm::dd::Bdd const& changedStatesAsBdd() const; + private: /*! * Creates a new partition from the given data. @@ -66,8 +77,9 @@ namespace storm { * greater or equal than the number of states in the partition. * @param numberOfBlocks The number of blocks in this partition. * @param nextFreeBlockIndex The next free block index. + * @param changedStates If given, this DD indicates the block assignment for which states has changed. */ - Partition(storm::dd::Add const& partitionAdd, std::pair const& blockVariables, uint64_t numberOfBlocks, uint64_t nextFreeBlockIndex); + Partition(storm::dd::Add const& partitionAdd, std::pair const& blockVariables, uint64_t numberOfBlocks, uint64_t nextFreeBlockIndex, boost::optional> const& changedStates = boost::none); /*! * Creates a new partition from the given data. @@ -78,8 +90,9 @@ namespace storm { * greater or equal than the number of states in the partition. * @param numberOfBlocks The number of blocks in this partition. * @param nextFreeBlockIndex The next free block index. + * @param changedStates If given, this DD indicates the block assignment for which states has changed. */ - Partition(storm::dd::Bdd const& partitionBdd, std::pair const& blockVariables, uint64_t numberOfBlocks, uint64_t nextFreeBlockIndex); + Partition(storm::dd::Bdd const& partitionBdd, std::pair const& blockVariables, uint64_t numberOfBlocks, uint64_t nextFreeBlockIndex, boost::optional> const& changedStates = boost::none); /*! * Creates a partition from the given model that respects the given expressions. @@ -98,6 +111,9 @@ namespace storm { /// The DD representing the partition. The DD is over the row variables of the model and the block variable. boost::variant, storm::dd::Add> partition; + /// A DD representing the states whose block assignment in the partition was changed from the last partition. + boost::optional, storm::dd::Add>> changedStates; + /// The meta variables used to encode the block of each state in this partition. std::pair blockVariables; diff --git a/src/storm/storage/dd/bisimulation/SignatureComputer.cpp b/src/storm/storage/dd/bisimulation/SignatureComputer.cpp index b4336adc8..1d31137a7 100644 --- a/src/storm/storage/dd/bisimulation/SignatureComputer.cpp +++ b/src/storm/storage/dd/bisimulation/SignatureComputer.cpp @@ -101,9 +101,17 @@ namespace storm { template Signature SignatureComputer::getFullSignature(Partition const& partition) const { if (partition.storedAsBdd()) { - return Signature(this->transitionMatrix.multiplyMatrix(partition.asBdd(), columnVariables)); + if (partition.hasChangedStates()) { + return Signature(this->transitionMatrix.multiplyMatrix(partition.asBdd() && partition.changedStatesAsBdd(), columnVariables)); + } else { + return Signature(this->transitionMatrix.multiplyMatrix(partition.asBdd(), columnVariables)); + } } else { - return Signature(this->transitionMatrix.multiplyMatrix(partition.asAdd(), columnVariables)); + if (partition.hasChangedStates()) { + return Signature(this->transitionMatrix.multiplyMatrix(partition.asAdd() * partition.changedStatesAsAdd(), columnVariables)); + } else { + return Signature(this->transitionMatrix.multiplyMatrix(partition.asAdd(), columnVariables)); + } } } diff --git a/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp b/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp index 2db026aa8..f9df015bd 100644 --- a/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp +++ b/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp @@ -43,9 +43,12 @@ namespace storm { InternalSignatureRefinerOptions(bool shiftStateVariables) : shiftStateVariables(shiftStateVariables), createChangedStates(true) { auto const& bisimulationSettings = storm::settings::getModule(); + storm::settings::modules::BisimulationSettings::ReuseMode reuseMode = bisimulationSettings.getReuseMode(); - this->reuseBlockNumbers = reuseMode == storm::settings::modules::BisimulationSettings::ReuseMode::BlockNumbers; + + storm::settings::modules::BisimulationSettings::RefinementMode refinementMode = bisimulationSettings.getRefinementMode(); + this->createChangedStates = refinementMode == storm::settings::modules::BisimulationSettings::RefinementMode::ChangedStates; } bool shiftStateVariables; @@ -78,7 +81,7 @@ namespace storm { template class InternalSignatureRefiner { public: - InternalSignatureRefiner(storm::dd::DdManager const& manager, storm::expressions::Variable const& blockVariable, std::set const& stateColumnVariables, storm::dd::Bdd const& nondeterminismVariables, storm::dd::Bdd const& nonBlockVariables, InternalSignatureRefinerOptions const& options = InternalSignatureRefinerOptions()) : manager(manager), internalDdManager(manager.getInternalDdManager()), ddman(internalDdManager.getCuddManager().getManager()), blockVariable(blockVariable), stateColumnVariables(stateColumnVariables), nondeterminismVariables(nondeterminismVariables), nonBlockVariables(nonBlockVariables), options(options), nextFreeBlockIndex(0), numberOfRefinements(0), lastNumberOfVisitedNodes(10000), signatureCache(lastNumberOfVisitedNodes), reuseBlocksCache(lastNumberOfVisitedNodes) { + 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 = InternalSignatureRefinerOptions()) : manager(manager), internalDdManager(manager.getInternalDdManager()), ddman(internalDdManager.getCuddManager().getManager()), blockVariable(blockVariable), stateVariables(stateVariables), nondeterminismVariables(nondeterminismVariables), nonBlockVariables(nonBlockVariables), options(options), nextFreeBlockIndex(0), numberOfRefinements(0), lastNumberOfVisitedNodes(10000), signatureCache(lastNumberOfVisitedNodes), reuseBlocksCache(lastNumberOfVisitedNodes) { // Initialize precomputed data. auto const& ddMetaVariable = manager.getMetaVariable(blockVariable); @@ -89,9 +92,9 @@ namespace storm { } Partition refine(Partition const& oldPartition, Signature const& signature) { - storm::dd::Add newPartitionAdd = refine(oldPartition, signature.getSignatureAdd());; + std::pair, boost::optional>> newPartitionDds = refine(oldPartition, signature.getSignatureAdd());; ++numberOfRefinements; - return oldPartition.replacePartition(newPartitionAdd, nextFreeBlockIndex, nextFreeBlockIndex); + return oldPartition.replacePartition(newPartitionDds.first, nextFreeBlockIndex, nextFreeBlockIndex, newPartitionDds.second); } private: @@ -100,9 +103,7 @@ namespace storm { reuseBlocksCache.clear(); } - int i = 0; - - storm::dd::Add refine(Partition const& oldPartition, storm::dd::Add const& signatureAdd) { + std::pair, boost::optional>> refine(Partition const& oldPartition, storm::dd::Add const& signatureAdd) { STORM_LOG_ASSERT(oldPartition.storedAsAdd(), "Expecting partition to be stored as ADD for CUDD."); nextFreeBlockIndex = options.reuseBlockNumbers ? oldPartition.getNextFreeBlockIndex() : 0; @@ -114,13 +115,15 @@ namespace storm { storm::dd::InternalAdd internalNewPartitionAdd(&internalDdManager, cudd::ADD(internalDdManager.getCuddManager(), result.first)); storm::dd::Add newPartitionAdd(oldPartition.asAdd().getDdManager(), internalNewPartitionAdd, oldPartition.asAdd().getContainedMetaVariables()); + boost::optional> optionalChangedAdd; if (result.second) { - storm::dd::InternalBdd internalChangedBdd(&internalDdManager, cudd::BDD(internalDdManager.getCuddManager(), result.second)); - storm::dd::Bdd changedBdd(oldPartition.asAdd().getDdManager(), internalChangedBdd, stateColumnVariables); + storm::dd::InternalAdd internalChangedAdd(&internalDdManager, cudd::ADD(internalDdManager.getCuddManager(), result.second)); + storm::dd::Add changedAdd(oldPartition.asAdd().getDdManager(), internalChangedAdd, stateVariables); + optionalChangedAdd = changedAdd; } clearCaches(); - return newPartitionAdd; + return std::make_pair(newPartitionAdd, optionalChangedAdd); } DdNodePtr encodeBlock(uint64_t blockIndex) { @@ -137,11 +140,156 @@ namespace storm { return result; } + std::pair reuseOrRelabel(DdNode* partitionNode, DdNode* nondeterminismVariablesNode, DdNode* nonBlockVariablesNode) { + // If we arrived at the constant zero node, then this was an illegal state encoding. + if (partitionNode == Cudd_ReadZero(ddman)) { + if (options.createChangedStates) { + return std::make_pair(partitionNode, Cudd_ReadZero(ddman)); + } else { + return std::make_pair(partitionNode, nullptr); + } + } + + // Check the cache whether we have seen the same node before. + auto nodePair = std::make_pair(nullptr, partitionNode); + + 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 (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(); + std::pair result = std::make_pair(partitionNode, options.createChangedStates ? Cudd_ReadZero(ddman) : nullptr); + signatureCache[nodePair] = result; + return result; + } + } + + std::pair result = std::make_pair(encodeBlock(nextFreeBlockIndex++), options.createChangedStates ? Cudd_ReadOne(ddman) : nullptr); + 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. + + bool skipped = true; + DdNode* partitionThen; + DdNode* partitionElse; + 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(partitionNode) - offset == Cudd_NodeReadIndex(nonBlockVariablesNode)) { + partitionThen = Cudd_T(partitionNode); + partitionElse = Cudd_E(partitionNode); + skipped = false; + } else { + partitionThen = partitionElse = partitionNode; + } + + // 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 reuseOrRelabel(partitionNode, nondeterminismVariablesNode, nonBlockVariablesNode); + } + + std::pair combinedThenResult = reuseOrRelabel(partitionThen, isNondeterminismVariable ? Cudd_T(nondeterminismVariablesNode) : nondeterminismVariablesNode, Cudd_T(nonBlockVariablesNode)); + DdNodePtr thenResult = combinedThenResult.first; + DdNodePtr changedThenResult = combinedThenResult.second; + Cudd_Ref(thenResult); + if (options.createChangedStates) { + Cudd_Ref(changedThenResult); + } else { + STORM_LOG_ASSERT(!changedThenResult, "Expected not changed state DD."); + } + std::pair combinedElseResult = reuseOrRelabel(partitionElse, isNondeterminismVariable ? Cudd_T(nondeterminismVariablesNode) : nondeterminismVariablesNode, Cudd_T(nonBlockVariablesNode)); + DdNodePtr elseResult = combinedElseResult.first; + DdNodePtr changedElseResult = combinedElseResult.second; + Cudd_Ref(elseResult); + if (options.createChangedStates) { + Cudd_Ref(changedElseResult); + } else { + STORM_LOG_ASSERT(!changedThenResult, "Expected not changed state DD."); + } + + DdNodePtr 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); + } + + DdNodePtr changedResult = nullptr; + if (options.createChangedStates) { + if (changedThenResult == changedElseResult) { + Cudd_Deref(changedThenResult); + Cudd_Deref(changedElseResult); + changedResult = changedThenResult; + } else { + // Get the node to connect the subresults. + bool complemented = Cudd_IsComplement(changedThenResult); + changedResult = cuddUniqueInter(ddman, Cudd_NodeReadIndex(nonBlockVariablesNode) + offset, Cudd_Regular(changedThenResult), complemented ? Cudd_Not(changedElseResult) : changedElseResult); + if (complemented) { + changedResult = Cudd_Not(changedResult); + } + Cudd_Deref(changedThenResult); + Cudd_Deref(changedElseResult); + } + } + + // Store the result in the cache. + auto pairResult = std::make_pair(result, changedResult); + signatureCache[nodePair] = pairResult; + return pairResult; + } + } + std::pair 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 we arrived at the constant zero node, then this was an illegal state encoding. if (partitionNode == Cudd_ReadZero(ddman)) { - return std::make_pair(partitionNode, Cudd_ReadLogicZero(ddman)); + if (options.createChangedStates) { + return std::make_pair(partitionNode, Cudd_ReadZero(ddman)); + } else { + return std::make_pair(partitionNode, nullptr); + } + } else if (signatureNode == Cudd_ReadZero(ddman)) { + std::pair result = reuseOrRelabel(partitionNode, nondeterminismVariablesNode, nonBlockVariablesNode); + signatureCache[std::make_pair(signatureNode, partitionNode)] = result; + return result; } // Check the cache whether we have seen the same node before. @@ -162,7 +310,7 @@ namespace storm { auto& reuseEntry = reuseBlocksCache[partitionNode]; if (!reuseEntry.isReused()) { reuseEntry.setReused(); - std::pair result = std::make_pair(partitionNode, options.createChangedStates ? Cudd_ReadLogicZero(ddman) : nullptr); + std::pair result = std::make_pair(partitionNode, options.createChangedStates ? Cudd_ReadZero(ddman) : nullptr); signatureCache[nodePair] = result; return result; } @@ -226,6 +374,8 @@ namespace storm { Cudd_Ref(thenResult); if (options.createChangedStates) { Cudd_Ref(changedThenResult); + } else { + STORM_LOG_ASSERT(!changedThenResult, "Expected not changed state DD."); } std::pair combinedElseResult = refine(partitionElse, signatureElse, isNondeterminismVariable ? Cudd_T(nondeterminismVariablesNode) : nondeterminismVariablesNode, Cudd_T(nonBlockVariablesNode)); DdNodePtr elseResult = combinedElseResult.first; @@ -233,8 +383,10 @@ namespace storm { Cudd_Ref(elseResult); if (options.createChangedStates) { Cudd_Ref(changedElseResult); + } else { + STORM_LOG_ASSERT(!changedThenResult, "Expected not changed state DD."); } - + DdNodePtr result; if (thenResult == elseResult) { Cudd_Deref(thenResult); @@ -260,7 +412,7 @@ namespace storm { } else { // Get the node to connect the subresults. bool complemented = Cudd_IsComplement(changedThenResult); - changedResult = cuddUniqueInter(ddman, Cudd_NodeReadIndex(nonBlockVariablesNode) + offset, Cudd_Regular(changedThenResult), complemented ? Cudd_Not(changedElseResult) : elseResult); + changedResult = cuddUniqueInter(ddman, Cudd_NodeReadIndex(nonBlockVariablesNode) + offset, Cudd_Regular(changedThenResult), complemented ? Cudd_Not(changedElseResult) : changedElseResult); if (complemented) { changedResult = Cudd_Not(changedResult); } @@ -279,8 +431,8 @@ namespace storm { storm::dd::DdManager const& manager; storm::dd::InternalDdManager const& internalDdManager; ::DdManager* ddman; - storm::expressions::Variable const& blockVariable; - std::set const& stateColumnVariables; + storm::expressions::Variable blockVariable; + std::set stateVariables; // The cubes representing all non-block and all nondeterminism variables, respectively. storm::dd::Bdd nondeterminismVariables; @@ -314,16 +466,16 @@ namespace storm { template class InternalSignatureRefiner { public: - InternalSignatureRefiner(storm::dd::DdManager const& manager, storm::expressions::Variable const& blockVariable, std::set const& stateColumnVariables, storm::dd::Bdd const& nondeterminismVariables, storm::dd::Bdd const& nonBlockVariables, InternalSignatureRefinerOptions const& options) : manager(manager), internalDdManager(manager.getInternalDdManager()), blockVariable(blockVariable), nondeterminismVariables(nondeterminismVariables), nonBlockVariables(nonBlockVariables), options(options), numberOfBlockVariables(manager.getMetaVariable(blockVariable).getNumberOfDdVariables()), blockCube(manager.getMetaVariable(blockVariable).getCube()), nextFreeBlockIndex(0), numberOfRefinements(0), signatureCache() { + 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() { // Perform garbage collection to clean up stuff not needed anymore. LACE_ME; sylvan_gc(); } Partition refine(Partition const& oldPartition, Signature const& signature) { - storm::dd::Bdd newPartitionBdd = refine(oldPartition, signature.getSignatureAdd()); + std::pair, boost::optional>> newPartitionDds = refine(oldPartition, signature.getSignatureAdd()); ++numberOfRefinements; - return oldPartition.replacePartition(newPartitionBdd, nextFreeBlockIndex, nextFreeBlockIndex); + return oldPartition.replacePartition(newPartitionDds.first, nextFreeBlockIndex, nextFreeBlockIndex, newPartitionDds.second); } private: @@ -332,20 +484,27 @@ namespace storm { reuseBlocksCache.clear(); } - storm::dd::Bdd refine(Partition const& oldPartition, storm::dd::Add const& signatureAdd) { + std::pair, boost::optional>> refine(Partition const& oldPartition, storm::dd::Add const& signatureAdd) { STORM_LOG_ASSERT(oldPartition.storedAsBdd(), "Expecting partition to be stored as BDD for Sylvan."); nextFreeBlockIndex = options.reuseBlockNumbers ? oldPartition.getNextFreeBlockIndex() : 0; // Perform the actual recursive refinement step. - BDD result = refine(oldPartition.asBdd().getInternalBdd().getSylvanBdd().GetBDD(), signatureAdd.getInternalAdd().getSylvanMtbdd().GetMTBDD(), nondeterminismVariables.getInternalBdd().getSylvanBdd().GetBDD(), nonBlockVariables.getInternalBdd().getSylvanBdd().GetBDD()); + std::pair 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)); + 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) { + storm::dd::InternalBdd internalChangedBdd(&internalDdManager, sylvan::Bdd(result.second)); + storm::dd::Bdd changedBdd(oldPartition.asBdd().getDdManager(), internalChangedBdd, stateVariables); + optionalChangedBdd = changedBdd; + } + clearCaches(); - return newPartitionBdd; + return std::make_pair(newPartitionBdd, optionalChangedBdd); } BDD encodeBlock(uint64_t blockIndex) { @@ -357,15 +516,158 @@ namespace storm { return sylvan_cube(blockCube.getInternalBdd().getSylvanBdd().GetBDD(), e.data()); } - BDD refine(BDD partitionNode, MTBDD signatureNode, BDD nondeterminismVariablesNode, BDD nonBlockVariablesNode) { + std::pair reuseOrRelabel(BDD partitionNode, BDD nondeterminismVariablesNode, BDD nonBlockVariablesNode) { LACE_ME; + + if (partitionNode == sylvan_false) { + if (options.createChangedStates) { + return std::make_pair(sylvan_false, sylvan_false); + } else { + return std::make_pair(sylvan_false, 0); + } + } + + // Check the cache whether we have seen the same node before. + auto nodePair = std::make_pair(0, partitionNode); + auto it = signatureCache.find(nodePair); + if (it != signatureCache.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)) { + 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); + std::pair result; + if (options.createChangedStates) { + result = std::make_pair(partitionNode, sylvan_false); + } else { + result = std::make_pair(partitionNode, 0); + } + signatureCache[nodePair] = result; + return result; + } + } + + std::pair result; + if (options.createChangedStates) { + result = std::make_pair(encodeBlock(nextFreeBlockIndex++), sylvan_true); + } else { + result = std::make_pair(encodeBlock(nextFreeBlockIndex++), 0); + } + 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. + + bool skipped = true; + BDD partitionThen; + BDD partitionElse; + 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(partitionNode, sylvan_var(nonBlockVariablesNode), -offset)) { + partitionThen = sylvan_high(partitionNode); + partitionElse = sylvan_low(partitionNode); + skipped = false; + } else { + partitionThen = partitionElse = partitionNode; + } + + // 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 reuseOrRelabel(partitionNode, nondeterminismVariablesNode, nonBlockVariablesNode); + } + + std::pair combinedThenResult = reuseOrRelabel(partitionThen, 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 = reuseOrRelabel(partitionElse, isNondeterminismVariable ? sylvan_high(nondeterminismVariablesNode) : nondeterminismVariablesNode, sylvan_high(nonBlockVariablesNode)); + BDD elseResult = combinedElseResult.first; + bdd_refs_push(elseResult); + BDD changedElseResult = combinedElseResult.second; + if (options.createChangedStates) { + bdd_refs_push(changedElseResult); + } + + std::pair result; + if (thenResult == elseResult) { + result.first = thenResult; + } else { + // Get the node to connect the subresults. + result.first = sylvan_makenode(sylvan_var(nonBlockVariablesNode) + offset, elseResult, thenResult); + } + + result.second = 0; + if (options.createChangedStates) { + if (changedThenResult == changedElseResult) { + result.second = changedThenResult; + } else { + // Get the node to connect the subresults. + result.second = sylvan_makenode(sylvan_var(nonBlockVariablesNode) + offset, changedElseResult, changedThenResult); + } + } + + // Dispose of the intermediate results. + if (options.createChangedStates) { + bdd_refs_pop(4); + } else { + bdd_refs_pop(2); + } + + // Store the result in the cache. + signatureCache[nodePair] = result; + return result; + } + } + + std::pair 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 // all states to be non-deadlock). if (partitionNode == sylvan_false) { - return partitionNode; + if (options.createChangedStates) { + return std::make_pair(sylvan_false, sylvan_false); + } else { + return std::make_pair(sylvan_false, 0); + } + } else if (mtbdd_iszero(signatureNode)) { + std::pair result = reuseOrRelabel(partitionNode, nondeterminismVariablesNode, nonBlockVariablesNode); + signatureCache[std::make_pair(signatureNode, partitionNode)] = result; + return result; } - + STORM_LOG_ASSERT(partitionNode != mtbdd_false, "Expected non-false node."); // Check the cache whether we have seen the same node before. @@ -388,12 +690,23 @@ namespace storm { if (!reuseBlockEntry.isReused()) { reuseBlockEntry.setReused(); reuseBlocksCache.emplace(partitionNode, true); - signatureCache[nodePair] = partitionNode; - return partitionNode; + std::pair result; + if (options.createChangedStates) { + result = std::make_pair(partitionNode, sylvan_false); + } else { + result = std::make_pair(partitionNode, 0); + } + signatureCache[nodePair] = result; + return result; } } - - BDD result = encodeBlock(nextFreeBlockIndex++); + + std::pair result; + if (options.createChangedStates) { + result = std::make_pair(encodeBlock(nextFreeBlockIndex++), sylvan_true); + } else { + result = std::make_pair(encodeBlock(nextFreeBlockIndex++), 0); + } signatureCache[nodePair] = result; return result; } else { @@ -445,22 +758,46 @@ namespace storm { return refine(partitionNode, signatureNode, nondeterminismVariablesNode, nonBlockVariablesNode); } - BDD thenResult = refine(partitionThen, signatureThen, isNondeterminismVariable ? sylvan_high(nondeterminismVariablesNode) : nondeterminismVariablesNode, sylvan_high(nonBlockVariablesNode)); + std::pair combinedThenResult = refine(partitionThen, signatureThen, isNondeterminismVariable ? sylvan_high(nondeterminismVariablesNode) : nondeterminismVariablesNode, sylvan_high(nonBlockVariablesNode)); + BDD thenResult = combinedThenResult.first; bdd_refs_push(thenResult); - BDD elseResult = refine(partitionElse, signatureElse, isNondeterminismVariable ? sylvan_high(nondeterminismVariablesNode) : nondeterminismVariablesNode, sylvan_high(nonBlockVariablesNode)); + 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)); + BDD elseResult = combinedElseResult.first; bdd_refs_push(elseResult); - - BDD result; + BDD changedElseResult = combinedElseResult.second; + if (options.createChangedStates) { + bdd_refs_push(changedElseResult); + } + + std::pair result; if (thenResult == elseResult) { - result = thenResult; + result.first = thenResult; } else { // Get the node to connect the subresults. - result = sylvan_makenode(sylvan_var(nonBlockVariablesNode) + offset, elseResult, thenResult); + result.first = sylvan_makenode(sylvan_var(nonBlockVariablesNode) + offset, elseResult, thenResult); } - + + result.second = 0; + if (options.createChangedStates) { + if (changedThenResult == changedElseResult) { + result.second = changedThenResult; + } else { + // Get the node to connect the subresults. + result.second = sylvan_makenode(sylvan_var(nonBlockVariablesNode) + offset, changedElseResult, changedThenResult); + } + } + // Dispose of the intermediate results. - bdd_refs_pop(2); - + if (options.createChangedStates) { + bdd_refs_pop(4); + } else { + bdd_refs_pop(2); + } + // Store the result in the cache. signatureCache[nodePair] = result; @@ -470,8 +807,9 @@ namespace storm { storm::dd::DdManager const& manager; storm::dd::InternalDdManager const& internalDdManager; - storm::expressions::Variable const& blockVariable; - + storm::expressions::Variable blockVariable; + std::set stateVariables; + storm::dd::Bdd nondeterminismVariables; storm::dd::Bdd nonBlockVariables; @@ -489,7 +827,7 @@ namespace storm { uint64_t numberOfRefinements; // The cache used to identify states with identical signature. - spp::sparse_hash_map, MTBDD, SylvanMTBDDPairHash> signatureCache; + spp::sparse_hash_map, std::pair, SylvanMTBDDPairHash> signatureCache; // The cache used to identify which old block numbers have already been reused. spp::sparse_hash_map reuseBlocksCache;