diff --git a/src/storm/storage/dd/Odd.cpp b/src/storm/storage/dd/Odd.cpp index af86aba1d..b94295f0e 100644 --- a/src/storm/storage/dd/Odd.cpp +++ b/src/storm/storage/dd/Odd.cpp @@ -13,7 +13,7 @@ namespace storm { namespace dd { Odd::Odd(std::shared_ptr elseNode, uint_fast64_t elseOffset, std::shared_ptr thenNode, uint_fast64_t thenOffset) : elseNode(elseNode), thenNode(thenNode), elseOffset(elseOffset), thenOffset(thenOffset) { - // Intentionally left empty. + STORM_LOG_ASSERT(this != elseNode.get() && this != thenNode.get(), "Cyclic ODD."); } Odd const& Odd::getThenSuccessor() const { @@ -105,30 +105,23 @@ namespace storm { dotFile << boost::join(levelNames, " -> ") << ";"; dotFile << "}" << std::endl; - std::map>> levelToOddNodesMap; + std::map> levelToOddNodesMap; this->addToLevelToOddNodesMap(levelToOddNodesMap); for (auto const& levelNodes : levelToOddNodesMap) { dotFile << "{ rank = same; \"" << levelNodes.first << "\"" << std::endl;; for (auto const& node : levelNodes.second) { - dotFile << "\"" << &node.get() << "\";" << std::endl; + dotFile << "\"" << node << "\";" << std::endl; } dotFile << "}" << std::endl; } - std::set printedNodes; for (auto const& levelNodes : levelToOddNodesMap) { for (auto const& node : levelNodes.second) { - if (printedNodes.find(&node.get()) != printedNodes.end()) { - continue; - } else { - printedNodes.insert(&node.get()); - } - - dotFile << "\"" << &node.get() << "\" [label=\"" << levelNodes.first << "\"];" << std::endl; - if (!node.get().isTerminalNode()) { - dotFile << "\"" << &node.get() << "\" -> \"" << &node.get().getElseSuccessor() << "\" [style=dashed, label=\"0\"];" << std::endl; - dotFile << "\"" << &node.get() << "\" -> \"" << &node.get().getThenSuccessor() << "\" [style=solid, label=\"" << node.get().getElseOffset() << "\"];" << std::endl; + dotFile << "\"" << node << "\" [label=\"" << node->getTotalOffset() << "\"];" << std::endl; + if (!node->isTerminalNode()) { + dotFile << "\"" << node << "\" -> \"" << &node->getElseSuccessor() << "\" [style=dashed, label=\"0\"];" << std::endl; + dotFile << "\"" << node << "\" -> \"" << &node->getThenSuccessor() << "\" [style=solid, label=\"" << node->getElseOffset() << "\"];" << std::endl; } } } @@ -137,11 +130,13 @@ namespace storm { storm::utility::closeFile(dotFile); } - void Odd::addToLevelToOddNodesMap(std::map>>& levelToOddNodesMap, uint_fast64_t level) const { - levelToOddNodesMap[level].push_back(*this); + void Odd::addToLevelToOddNodesMap(std::map>& levelToOddNodesMap, uint_fast64_t level) const { + levelToOddNodesMap[level].emplace(this); if (!this->isTerminalNode()) { this->getElseSuccessor().addToLevelToOddNodesMap(levelToOddNodesMap, level + 1); - this->getThenSuccessor().addToLevelToOddNodesMap(levelToOddNodesMap, level + 1); + if (this->thenNode != this->elseNode) { + this->getThenSuccessor().addToLevelToOddNodesMap(levelToOddNodesMap, level + 1); + } } } diff --git a/src/storm/storage/dd/Odd.h b/src/storm/storage/dd/Odd.h index 637e9ca6c..0cb4a307c 100644 --- a/src/storm/storage/dd/Odd.h +++ b/src/storm/storage/dd/Odd.h @@ -4,6 +4,7 @@ #include #include #include +#include namespace storm { namespace dd { @@ -125,7 +126,7 @@ namespace storm { * @param levelToOddNodesMap A mapping of the level to the ODD node. * @param The level of the current node. */ - void addToLevelToOddNodesMap(std::map>>& levelToOddNodesMap, uint_fast64_t level = 0) const; + void addToLevelToOddNodesMap(std::map>& levelToOddNodesMap, uint_fast64_t level = 0) const; /*! * Adds the values of the old explicit values to the new explicit values where the positions in the old vector diff --git a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp index fc6e289b1..5f4376ae7 100644 --- a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp +++ b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp @@ -214,89 +214,43 @@ namespace storm { template class InternalSparseQuotientExtractorBase { public: - InternalSparseQuotientExtractorBase(storm::dd::DdManager const& manager, std::set const& stateVariables, std::set const& nondeterminismVariables) : manager(manager) { - - // Initialize cubes. - stateVariablesCube = manager.getBddOne(); - allSourceVariablesCube = manager.getBddOne(); - nondeterminismVariablesCube = manager.getBddOne(); - + InternalSparseQuotientExtractorBase(storm::dd::DdManager const& manager, std::set const& rowVariables, std::set const& columnVariables, std::set const& nondeterminismVariables, Partition const& partition, storm::dd::Bdd const& representatives, storm::dd::Odd const& odd) : manager(manager), partition(partition), representatives(representatives), odd(odd) { // Create cubes. - for (auto const& variable : stateVariables) { + rowVariablesCube = manager.getBddOne(); + for (auto const& variable : rowVariables) { auto const& ddMetaVariable = manager.getMetaVariable(variable); - std::vector> indicesAndLevels = ddMetaVariable.getIndicesAndLevels(); - sourceVariablesIndicesAndLevels.insert(sourceVariablesIndicesAndLevels.end(), indicesAndLevels.begin(), indicesAndLevels.end()); - - allSourceVariablesCube &= ddMetaVariable.getCube(); - stateVariablesCube &= ddMetaVariable.getCube(); + rowVariablesCube &= ddMetaVariable.getCube(); + } + columnVariablesCube = manager.getBddOne(); + for (auto const& variable : columnVariables) { + auto const& ddMetaVariable = manager.getMetaVariable(variable); + columnVariablesCube &= ddMetaVariable.getCube(); } + nondeterminismVariablesCube = manager.getBddOne(); for (auto const& variable : nondeterminismVariables) { auto const& ddMetaVariable = manager.getMetaVariable(variable); - allSourceVariablesCube &= ddMetaVariable.getCube(); nondeterminismVariablesCube &= ddMetaVariable.getCube(); - - std::vector> indicesAndLevels = ddMetaVariable.getIndicesAndLevels(); - nondeterminismVariablesIndicesAndLevels.insert(nondeterminismVariablesIndicesAndLevels.end(), indicesAndLevels.begin(), indicesAndLevels.end()); } - - // Sort the indices by their levels. - std::sort(sourceVariablesIndicesAndLevels.begin(), sourceVariablesIndicesAndLevels.end(), [] (std::pair const& a, std::pair const& b) { return a.second < b.second; } ); - std::sort(nondeterminismVariablesIndicesAndLevels.begin(), nondeterminismVariablesIndicesAndLevels.end(), [] (std::pair const& a, std::pair const& b) { return a.second < b.second; } ); + allSourceVariablesCube = rowVariablesCube && nondeterminismVariablesCube; } protected: - storm::storage::SparseMatrix createMatrixFromEntries(Partition const& partition) { - if (!deterministicEntries.empty()) { - return createMatrixFromDeterministicEntries(partition); - } else { - return createMatrixFromNondeterministicEntries(partition); - } - } + // The manager responsible for the DDs. + storm::dd::DdManager const& manager; - storm::storage::SparseMatrix createMatrixFromNondeterministicEntries(Partition const& partition) { - bool nontrivialRowGrouping = false; - uint64_t numberOfChoices = 0; - for (auto& group : nondeterministicEntries) { - for (auto& choice : group) { - auto& row = choice.second; - std::sort(row.begin(), row.end(), - [] (storm::storage::MatrixEntry const& a, storm::storage::MatrixEntry const& b) { - return a.getColumn() < b.getColumn(); - }); - ++numberOfChoices; - } - nontrivialRowGrouping |= group.size() > 1; - } - - storm::storage::SparseMatrixBuilder builder(numberOfChoices, partition.getNumberOfBlocks(), 0, false, nontrivialRowGrouping); - uint64_t rowCounter = 0; - for (auto& group : nondeterministicEntries) { - for (auto& choice : group) { - auto& row = choice.second; - for (auto const& entry : row) { - builder.addNextValue(rowCounter, entry.getColumn(), entry.getValue()); - } - - // Free storage for row. - row.clear(); - row.shrink_to_fit(); - - ++rowCounter; - } - - group.clear(); - - if (nontrivialRowGrouping) { - builder.newRowGroup(rowCounter); - } - } - nondeterministicEntries.clear(); - nondeterministicEntries.shrink_to_fit(); - return builder.build(); - } - - storm::storage::SparseMatrix createMatrixFromDeterministicEntries(Partition const& partition) { - for (auto& row : deterministicEntries) { + // Useful cubes needed in the translation. + storm::dd::Bdd rowVariablesCube; + storm::dd::Bdd columnVariablesCube; + storm::dd::Bdd allSourceVariablesCube; + storm::dd::Bdd nondeterminismVariablesCube; + + // Information about the state partition. + Partition partition; + storm::dd::Bdd representatives; + storm::dd::Odd const& odd; + + storm::storage::SparseMatrix createMatrixFromEntries() { + for (auto& row : matrixEntries) { std::sort(row.begin(), row.end(), [] (storm::storage::MatrixEntry const& a, storm::storage::MatrixEntry const& b) { return a.getColumn() < b.getColumn(); @@ -305,7 +259,7 @@ namespace storm { storm::storage::SparseMatrixBuilder builder(partition.getNumberOfBlocks(), partition.getNumberOfBlocks()); uint64_t rowCounter = 0; - for (auto& row : deterministicEntries) { + for (auto& row : matrixEntries) { for (auto const& entry : row) { builder.addNextValue(rowCounter, entry.getColumn(), entry.getValue()); } @@ -317,483 +271,332 @@ namespace storm { ++rowCounter; } - deterministicEntries.clear(); - deterministicEntries.shrink_to_fit(); + matrixEntries.clear(); + matrixEntries.shrink_to_fit(); return builder.build(); } - - void addMatrixEntry(storm::storage::BitVector const& nondeterminismEncoding, uint64_t sourceBlockIndex, uint64_t targetBlockIndex, ValueType const& value) { - if (nondeterminismVariablesIndicesAndLevels.empty()) { - this->deterministicEntries[sourceBlockIndex].emplace_back(targetBlockIndex, value); - } else { - this->nondeterministicEntries[sourceBlockIndex][nondeterminismEncoding].emplace_back(targetBlockIndex, value); - } + + void addMatrixEntry(uint64_t sourceBlockIndex, uint64_t targetBlockIndex, ValueType const& value) { + this->matrixEntries[sourceBlockIndex].emplace_back(targetBlockIndex, value); } void reserveMatrixEntries(uint64_t numberOfStates) { - if (nondeterminismVariablesIndicesAndLevels.empty()) { - this->deterministicEntries.resize(numberOfStates); - } else { - this->nondeterministicEntries.resize(numberOfStates); - } + this->matrixEntries.resize(numberOfStates); } - // The manager responsible for the DDs. - storm::dd::DdManager const& manager; - - // The indices and levels of all state variables. - std::vector> sourceVariablesIndicesAndLevels; - - // The indices and levels of all state variables. - std::vector> nondeterminismVariablesIndicesAndLevels; - - // Useful cubes needed in the translation. - storm::dd::Bdd stateVariablesCube; - storm::dd::Bdd allSourceVariablesCube; - storm::dd::Bdd nondeterminismVariablesCube; - - // A hash map that stores the unique source state representative for each source block index. - spp::sparse_hash_map> uniqueSourceRepresentative; - // The entries of the matrix that is built if the model is deterministic (DTMC, CTMC). - std::vector>> deterministicEntries; - - // The entries of the matrix that is built if the model is nondeterministic (MDP). - std::vector>>> nondeterministicEntries; + std::vector>> matrixEntries; }; template class InternalSparseQuotientExtractor : public InternalSparseQuotientExtractorBase { public: - InternalSparseQuotientExtractor(storm::dd::DdManager const& manager, std::set const& stateVariables, std::set const& nondeterminismVariables) : InternalSparseQuotientExtractorBase(manager, stateVariables, nondeterminismVariables), ddman(this->manager.getInternalDdManager().getCuddManager().getManager()) { - // Intentionally left empty. + InternalSparseQuotientExtractor(storm::dd::DdManager const& manager, std::set const& rowVariables, std::set const& columnVariables, std::set const& nondeterminismVariables, Partition const& partition, storm::dd::Bdd const& representatives, storm::dd::Odd const& odd) : InternalSparseQuotientExtractorBase(manager, rowVariables, columnVariables, nondeterminismVariables, partition, representatives, odd), ddman(this->manager.getInternalDdManager().getCuddManager().getManager()) { + + STORM_LOG_ASSERT(this->partition.storedAsAdd(), "Expected partition to be stored as an ADD."); + this->partition.asAdd().exportToDot("part.dot"); + odd.exportToDot("odd.dot"); + this->representatives.exportToDot("reprbdd.dot"); + this->representatives.template toAdd().exportToDot("repr.dot"); + this->createBlockToOffsetMapping(); } - storm::storage::SparseMatrix extractTransitionMatrix(storm::dd::Add const& transitionMatrix, Partition const& partition) { - STORM_LOG_ASSERT(partition.storedAsAdd(), "Expected partition stored as ADD."); - + storm::storage::SparseMatrix extractTransitionMatrix(storm::dd::Add const& transitionMatrix) { // Create the number of rows necessary for the matrix. - this->reserveMatrixEntries(partition.getNumberOfBlocks()); - STORM_LOG_TRACE("Partition has " << partition.getNumberOfStates() << " states in " << partition.getNumberOfBlocks() << " blocks."); + this->reserveMatrixEntries(this->partition.getNumberOfBlocks()); + STORM_LOG_TRACE("Partition has " << this->partition.getNumberOfStates() << " states in " << this->partition.getNumberOfBlocks() << " blocks."); - storm::storage::BitVector stateEncoding(this->sourceVariablesIndicesAndLevels.size()); - storm::storage::BitVector nondeterminismEncoding(this->nondeterminismVariablesIndicesAndLevels.size()); - extractTransitionMatrixRec(transitionMatrix.getInternalAdd().getCuddDdNode(), partition.asAdd().getInternalAdd().getCuddDdNode(), partition.asAdd().getInternalAdd().getCuddDdNode(), 0, stateEncoding, nondeterminismEncoding); + extractTransitionMatrixRec(transitionMatrix.getInternalAdd().getCuddDdNode(), this->odd, 0, this->partition.asAdd().getInternalAdd().getCuddDdNode(), this->representatives.getInternalBdd().getCuddDdNode(), this->allSourceVariablesCube.getInternalBdd().getCuddDdNode()); - return this->createMatrixFromEntries(partition); + return this->createMatrixFromEntries(); } - storm::storage::BitVector extractStates(storm::dd::Bdd const& states, Partition const& partition) { - STORM_LOG_ASSERT(partition.storedAsAdd(), "Expected partition stored as ADD."); - - storm::storage::BitVector result(partition.getNumberOfBlocks()); - extractStatesRec(states.getInternalBdd().getCuddDdNode(), partition.asAdd().getInternalAdd().getCuddDdNode(), this->stateVariablesCube.getInternalBdd().getCuddDdNode(), result); - - return result; + private: + void createBlockToOffsetMapping() { + this->createBlockToOffsetMappingRec(this->partition.asAdd().getInternalAdd().getCuddDdNode(), this->representatives.getInternalBdd().getCuddDdNode(), this->rowVariablesCube.getInternalBdd().getCuddDdNode(), this->odd, 0); + STORM_LOG_ASSERT(blockToOffset.size() == this->partition.getNumberOfBlocks(), "Mismatching block-to-offset mapping: " << blockToOffset.size() << " vs. " << this->partition.getNumberOfBlocks() << "."); } - private: - uint64_t decodeBlockIndex(DdNode* blockEncoding) { - std::unique_ptr& blockCacheEntry = blockDecodeCache[blockEncoding]; - if (blockCacheEntry) { - return *blockCacheEntry; + void createBlockToOffsetMappingRec(DdNodePtr partitionNode, DdNodePtr representativesNode, DdNodePtr variables, storm::dd::Odd const& odd, uint64_t offset) { + if (representativesNode == Cudd_ReadLogicZero(ddman)) { + std::cout << "returning early" << std::endl; + return; } - -// FILE* fp = fopen("block.dot" , "w"); -// Cudd_DumpDot(ddman, 1, &blockEncoding, nullptr, nullptr, fp); -// fclose(fp); - uint64_t result = 0; - uint64_t offset = 0; - while (blockEncoding != Cudd_ReadOne(ddman)) { - DdNode* then = Cudd_T(blockEncoding); - if (then != Cudd_ReadZero(ddman)) { - blockEncoding = then; - result |= 1ull << offset; - } else { - blockEncoding = Cudd_E(blockEncoding); - } - ++offset; + if (representativesNode == Cudd_ReadOne(ddman)) { + std::cout << "repr is one" << std::endl; } - - blockCacheEntry.reset(new uint64_t(result)); - - return result; - } - - void extractStatesRec(DdNode* statesNode, DdNode* partitionNode, DdNode* stateVariablesNode, storm::storage::BitVector& result) { - if (statesNode == Cudd_ReadLogicZero(ddman)) { - return; + if (partitionNode == Cudd_ReadOne(ddman)) { + std::cout << "part is zero" << std::endl; + } else if (partitionNode == Cudd_ReadOne(ddman)) { + std::cout << "part is one" << std::endl; } - bool skippedBoth = true; - DdNode* tStates; - DdNode* eStates; - DdNode* tPartition; - DdNode* ePartition; - bool negate = false; - while (skippedBoth && !Cudd_IsConstant(stateVariablesNode)) { - if (Cudd_NodeReadIndex(statesNode) == Cudd_NodeReadIndex(stateVariablesNode)) { - tStates = Cudd_T(statesNode); - eStates = Cudd_E(statesNode); - negate = Cudd_IsComplement(statesNode); - skippedBoth = false; + std::cout << "got call " << partitionNode << ", " << representativesNode << ", " << variables << ", " << offset << ", " << Cudd_IsConstant(variables) << std::endl; + + if (Cudd_IsConstant(variables)) { + STORM_LOG_ASSERT(odd.isTerminalNode(), "Expected terminal node."); + std::cout << "inserting " << partitionNode << " -> " << offset << std::endl; + STORM_LOG_ASSERT(blockToOffset.find(partitionNode) == blockToOffset.end(), "Duplicate entry."); + blockToOffset[partitionNode] = offset; + } else { + STORM_LOG_ASSERT(!odd.isTerminalNode(), "Expected non-terminal node."); + DdNodePtr partitionT; + DdNodePtr partitionE; + if (Cudd_NodeReadIndex(partitionNode) == Cudd_NodeReadIndex(variables) + 1) { + partitionT = Cudd_T(partitionNode); + partitionE = Cudd_E(partitionNode); } else { - tStates = eStates = statesNode; + std::cout << "[1] skipped " << Cudd_NodeReadIndex(variables) << ", got " << Cudd_NodeReadIndex(partitionNode) << std::endl; + partitionT = partitionE = partitionNode; } - if (Cudd_NodeReadIndex(partitionNode) == Cudd_NodeReadIndex(stateVariablesNode) + 1) { - tPartition = Cudd_T(partitionNode); - ePartition = Cudd_E(partitionNode); - skippedBoth = false; + DdNodePtr representativesT; + DdNodePtr representativesE; + if (Cudd_NodeReadIndex(representativesNode) == Cudd_NodeReadIndex(variables)) { + representativesT = Cudd_T(representativesNode); + representativesE = Cudd_E(representativesNode); } else { - tPartition = ePartition = partitionNode; + std::cout << "[2] skipped " << Cudd_NodeReadIndex(variables) << ", got " << Cudd_NodeReadIndex(representativesNode) << std::endl; + representativesT = representativesE = representativesNode; } - if (skippedBoth) { - stateVariablesNode = Cudd_T(stateVariablesNode); + if (representativesT != representativesE && Cudd_IsComplement(representativesNode)) { + representativesE = Cudd_Not(representativesE); + representativesT = Cudd_Not(representativesT); } + + std::cout << "else" << std::endl; + createBlockToOffsetMappingRec(partitionE, representativesE, Cudd_T(variables), odd.getElseSuccessor(), offset); + std::cout << "then with offset " << odd.getElseOffset() << std::endl; + createBlockToOffsetMappingRec(partitionT, representativesT, Cudd_T(variables), odd.getThenSuccessor(), offset + odd.getElseOffset()); } - - if (Cudd_IsConstant(stateVariablesNode)) { - // If there is no more state variables, it means that we arrived at a block encoding in which there is a state in the state set. - result.set(decodeBlockIndex(partitionNode)); - return; - } else { - // Otherwise, we need to recursively descend. - extractStatesRec(negate ? Cudd_Not(tStates) : tStates, tPartition, Cudd_T(stateVariablesNode), result); - extractStatesRec(negate ? Cudd_Not(eStates) : eStates, ePartition, Cudd_T(stateVariablesNode), result); - } + std::cout << "returning" << std::endl; } - void extractTransitionMatrixRec(DdNode* transitionMatrixNode, DdNode* sourcePartitionNode, DdNode* targetPartitionNode, uint64_t sourceStateEncodingIndex, storm::storage::BitVector& sourceStateEncoding, storm::storage::BitVector const& nondeterminismEncoding, ValueType const& factor = 1) { + void extractTransitionMatrixRec(DdNodePtr transitionMatrixNode, storm::dd::Odd const& sourceOdd, uint64_t sourceOffset, DdNodePtr targetPartitionNode, DdNodePtr representativesNode, DdNodePtr variables) { // For the empty DD, we do not need to add any entries. Note that the partition nodes cannot be zero // as all states of the model have to be contained. - if (transitionMatrixNode == Cudd_ReadZero(ddman)) { + if (transitionMatrixNode == Cudd_ReadZero(ddman) || representativesNode == Cudd_ReadLogicZero(ddman)) { return; } // If we have moved through all source variables, we must have arrived at a target block encoding. - if (sourceStateEncodingIndex == sourceStateEncoding.size()) { - // Decode the source block. - uint64_t sourceBlockIndex = decodeBlockIndex(sourcePartitionNode); - - std::unique_ptr& sourceRepresentative = this->uniqueSourceRepresentative[sourceBlockIndex]; - if (sourceRepresentative && *sourceRepresentative != sourceStateEncoding) { - // In this case, we have picked a different representative and must not record any entries now. - return; - } - - // Otherwise, we record the new representative. - sourceRepresentative.reset(new storm::storage::BitVector(sourceStateEncoding)); - - // Decode the target block and add entry to matrix. - uint64_t targetBlockIndex = decodeBlockIndex(targetPartitionNode); - this->addMatrixEntry(nondeterminismEncoding, sourceBlockIndex, targetBlockIndex, factor * Cudd_V(transitionMatrixNode)); + if (Cudd_IsConstant(variables)) { + STORM_LOG_ASSERT(Cudd_IsConstant(transitionMatrixNode), "Expected constant node."); + this->addMatrixEntry(sourceOffset, blockToOffset.at(targetPartitionNode), Cudd_V(transitionMatrixNode)); } else { - // Determine the levels in the DDs. - uint64_t transitionMatrixVariable = Cudd_NodeReadIndex(transitionMatrixNode); - uint64_t sourcePartitionVariable = Cudd_NodeReadIndex(sourcePartitionNode) - 1; - uint64_t targetPartitionVariable = Cudd_NodeReadIndex(targetPartitionNode) - 1; + DdNodePtr t; + DdNodePtr tt; + DdNodePtr te; + DdNodePtr e; + DdNodePtr et; + DdNodePtr ee; + if (Cudd_NodeReadIndex(transitionMatrixNode) == Cudd_NodeReadIndex(variables)) { + // Source node was not skipped in transition matrix. + t = Cudd_T(transitionMatrixNode); + e = Cudd_E(transitionMatrixNode); + } else { + t = e = transitionMatrixNode; + } - // Move through transition matrix. - bool skippedSourceInMatrix = false; - bool skippedTargetTInMatrix = false; - bool skippedTargetEInMatrix = false; - DdNode* tt = transitionMatrixNode; - DdNode* te = transitionMatrixNode; - DdNode* et = transitionMatrixNode; - DdNode* ee = transitionMatrixNode; - STORM_LOG_ASSERT(transitionMatrixVariable >= this->sourceVariablesIndicesAndLevels[sourceStateEncodingIndex].first, "Illegal top variable of transition matrix."); - if (transitionMatrixVariable == this->sourceVariablesIndicesAndLevels[sourceStateEncodingIndex].first) { - DdNode* t = Cudd_T(transitionMatrixNode); - uint64_t tVariable = Cudd_NodeReadIndex(t); - if (tVariable == this->sourceVariablesIndicesAndLevels[sourceStateEncodingIndex].first + 1) { - tt = Cudd_T(t); - te = Cudd_E(t); - } else { - tt = te = t; - skippedTargetTInMatrix = true; - } - - DdNode* e = Cudd_E(transitionMatrixNode); - uint64_t eVariable = Cudd_NodeReadIndex(e); - if (eVariable == this->sourceVariablesIndicesAndLevels[sourceStateEncodingIndex].first + 1) { + if (Cudd_NodeReadIndex(t) == Cudd_NodeReadIndex(variables) + 1) { + // Target node was not skipped in transition matrix. + tt = Cudd_T(t); + te = Cudd_E(t); + } else { + // Target node was skipped in transition matrix. + tt = te = t; + } + if (t != e) { + if (Cudd_NodeReadIndex(e) == Cudd_NodeReadIndex(variables) + 1) { + // Target node was not skipped in transition matrix. et = Cudd_T(e); ee = Cudd_E(e); } else { + // Target node was skipped in transition matrix. et = ee = e; - skippedTargetEInMatrix = true; } } else { - skippedSourceInMatrix = true; - if (transitionMatrixVariable == this->sourceVariablesIndicesAndLevels[sourceStateEncodingIndex].first + 1) { - tt = et = Cudd_T(transitionMatrixNode); - te = ee = Cudd_E(transitionMatrixNode); - } else { - tt = te = et = ee = transitionMatrixNode; - skippedTargetTInMatrix = skippedTargetEInMatrix = true; - } - } - - // Move through partition (for source state). - bool skippedInSourcePartition = false; - DdNode* sourceT; - DdNode* sourceE; - STORM_LOG_ASSERT(sourcePartitionVariable >= this->sourceVariablesIndicesAndLevels[sourceStateEncodingIndex].first, "Illegal top variable of source partition."); - if (sourcePartitionVariable == this->sourceVariablesIndicesAndLevels[sourceStateEncodingIndex].first) { - sourceT = Cudd_T(sourcePartitionNode); - sourceE = Cudd_E(sourcePartitionNode); - } else { - sourceT = sourceE = sourcePartitionNode; - skippedInSourcePartition = true; + et = tt; + ee = te; } - // Move through partition (for target state). - bool skippedInTargetPartition = false; - DdNode* targetT; - DdNode* targetE; - STORM_LOG_ASSERT(targetPartitionVariable >= this->sourceVariablesIndicesAndLevels[sourceStateEncodingIndex].first, "Illegal top variable of source partition."); - if (targetPartitionVariable == this->sourceVariablesIndicesAndLevels[sourceStateEncodingIndex].first) { + DdNodePtr targetT; + DdNodePtr targetE; + if (Cudd_NodeReadIndex(targetPartitionNode) == Cudd_NodeReadIndex(variables) + 1) { + // Node was not skipped in target partition. targetT = Cudd_T(targetPartitionNode); targetE = Cudd_E(targetPartitionNode); } else { + // Node was skipped in target partition. targetT = targetE = targetPartitionNode; - skippedInTargetPartition = true; } - // If we skipped the variable in the source partition, we only have to choose one of the two representatives. - if (!skippedInSourcePartition) { - sourceStateEncoding.set(sourceStateEncodingIndex, true); - if (!skippedInTargetPartition) { - extractTransitionMatrixRec(tt, sourceT, targetT, sourceStateEncodingIndex + 1, sourceStateEncoding, nondeterminismEncoding, factor); - } - extractTransitionMatrixRec(te, sourceT, targetE, sourceStateEncodingIndex + 1, sourceStateEncoding, nondeterminismEncoding, skippedTargetTInMatrix && skippedInTargetPartition ? 2 * factor : factor); + DdNodePtr representativesT; + DdNodePtr representativesE; + if (Cudd_NodeReadIndex(representativesNode) == Cudd_NodeReadIndex(variables)) { + // Node was not skipped in representatives. + representativesT = Cudd_T(representativesNode); + representativesE = Cudd_E(representativesNode); + } else { + // Node was skipped in representatives. + representativesT = representativesE = representativesNode; } - sourceStateEncoding.set(sourceStateEncodingIndex, false); - // If we skipped the variable in the target partition, just count the one representative twice. - if (!skippedInTargetPartition) { - extractTransitionMatrixRec(et, sourceE, targetT, sourceStateEncodingIndex + 1, sourceStateEncoding, nondeterminismEncoding, factor); + if (representativesT != representativesE && Cudd_IsComplement(representativesNode)) { + representativesT = Cudd_Not(representativesT); + representativesE = Cudd_Not(representativesE); } - extractTransitionMatrixRec(ee, sourceE, targetE, sourceStateEncodingIndex + 1, sourceStateEncoding, nondeterminismEncoding, skippedTargetEInMatrix && skippedInTargetPartition ? 2 * factor : factor); + + extractTransitionMatrixRec(ee, sourceOdd.getElseSuccessor(), sourceOffset, targetE, representativesE, Cudd_T(variables)); + extractTransitionMatrixRec(et, sourceOdd.getElseSuccessor(), sourceOffset, targetT, representativesE, Cudd_T(variables)); + extractTransitionMatrixRec(te, sourceOdd.getThenSuccessor(), sourceOffset + sourceOdd.getElseOffset(), targetE, representativesT, Cudd_T(variables)); + extractTransitionMatrixRec(tt, sourceOdd.getThenSuccessor(), sourceOffset + sourceOdd.getElseOffset(), targetT, representativesT, Cudd_T(variables)); } } ::DdManager* ddman; - spp::sparse_hash_map> blockDecodeCache; + // A mapping from blocks (stored in terms of a DD node) to the offset of the corresponding block. + spp::sparse_hash_map blockToOffset; }; template class InternalSparseQuotientExtractor : public InternalSparseQuotientExtractorBase { public: - InternalSparseQuotientExtractor(storm::dd::DdManager const& manager, std::set const& stateVariables, std::set const& nondeterminismVariables) : InternalSparseQuotientExtractorBase(manager, stateVariables, nondeterminismVariables) { - // Intentionally left empty. - } - - storm::storage::SparseMatrix extractTransitionMatrix(storm::dd::Add const& transitionMatrix, Partition const& partition) { - STORM_LOG_ASSERT(partition.storedAsBdd(), "Expected partition stored as BDD."); + InternalSparseQuotientExtractor(storm::dd::DdManager const& manager, std::set const& rowVariables, std::set const& columnVariables, std::set const& nondeterminismVariables, Partition const& partition, storm::dd::Bdd const& representatives, storm::dd::Odd const& odd) : InternalSparseQuotientExtractorBase(manager, rowVariables, columnVariables, nondeterminismVariables, partition, representatives, odd) { - // Create the number of rows necessary for the matrix. - this->reserveMatrixEntries(partition.getNumberOfBlocks()); - - storm::storage::BitVector stateEncoding(this->sourceVariablesIndicesAndLevels.size()); - storm::storage::BitVector nondeterminismEncoding; - extractTransitionMatrixRec(transitionMatrix.getInternalAdd().getSylvanMtbdd().GetMTBDD(), partition.asBdd().getInternalBdd().getSylvanBdd().GetBDD(), partition.asBdd().getInternalBdd().getSylvanBdd().GetBDD(), 0, stateEncoding, nondeterminismEncoding); - - return this->createMatrixFromEntries(partition); - } - - storm::storage::BitVector extractStates(storm::dd::Bdd const& states, Partition const& partition) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Möööp"); STORM_LOG_ASSERT(partition.storedAsBdd(), "Expected partition stored as BDD."); - - storm::storage::BitVector result(partition.getNumberOfBlocks()); - extractStatesRec(states.getInternalBdd().getSylvanBdd().GetBDD(), partition.asBdd().getInternalBdd().getSylvanBdd().GetBDD(), this->stateVariablesCube.getInternalBdd().getSylvanBdd().GetBDD(), result); - - return result; - } - - private: - uint64_t decodeBlockIndex(BDD blockEncoding) { - std::unique_ptr& blockCacheEntry = blockDecodeCache[blockEncoding]; - if (blockCacheEntry) { - return *blockCacheEntry; - } - - uint64_t result = 0; - uint64_t offset = 0; - while (blockEncoding != sylvan_true) { - if (sylvan_high(blockEncoding) != sylvan_false) { - blockEncoding = sylvan_high(blockEncoding); - result |= 1ull << offset; - } else { - blockEncoding = sylvan_low(blockEncoding); - } - ++offset; - } - - blockCacheEntry.reset(new uint64_t(result)); - - return result; } - void extractStatesRec(BDD statesNode, BDD partitionNode, BDD stateVariablesNode, storm::storage::BitVector& result) { - if (statesNode == sylvan_false) { - return; - } - - bool skippedBoth = true; - BDD tStates; - BDD eStates; - BDD tPartition; - BDD ePartition; - while (skippedBoth && !sylvan_isconst(stateVariablesNode)) { - if (sylvan_var(statesNode) == sylvan_var(stateVariablesNode)) { - tStates = sylvan_high(statesNode); - eStates = sylvan_low(statesNode); - skippedBoth = false; - } else { - tStates = eStates = statesNode; - } - - if (sylvan_var(partitionNode) == sylvan_var(stateVariablesNode) + 1) { - tPartition = sylvan_high(partitionNode); - ePartition = sylvan_low(partitionNode); - skippedBoth = false; - } else { - tPartition = ePartition = partitionNode; - } - - if (skippedBoth) { - stateVariablesNode = sylvan_high(stateVariablesNode); - } - } - - if (sylvan_isconst(stateVariablesNode)) { - // If there is no more state variables, it means that we arrived at a block encoding in which there is a state in the state set. - result.set(decodeBlockIndex(partitionNode)); - return; - } else { - // Otherwise, we need to recursively descend. - extractStatesRec(tStates, tPartition, sylvan_high(stateVariablesNode), result); - extractStatesRec(eStates, ePartition, sylvan_high(stateVariablesNode), result); - } + storm::storage::SparseMatrix extractTransitionMatrix(storm::dd::Add const& transitionMatrix) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Möööp"); +// // Create the number of rows necessary for the matrix. +// this->reserveMatrixEntries(partition.getNumberOfBlocks()); +// +// storm::storage::BitVector stateEncoding(this->sourceVariablesIndicesAndLevels.size()); +// storm::storage::BitVector nondeterminismEncoding; +// extractTransitionMatrixRec(transitionMatrix.getInternalAdd().getSylvanMtbdd().GetMTBDD(), partition.asBdd().getInternalBdd().getSylvanBdd().GetBDD(), partition.asBdd().getInternalBdd().getSylvanBdd().GetBDD(), 0, stateEncoding, nondeterminismEncoding); +// +// return this->createMatrixFromEntries(partition); } - void extractTransitionMatrixRec(MTBDD transitionMatrixNode, BDD sourcePartitionNode, BDD targetPartitionNode, uint64_t currentIndex, storm::storage::BitVector& sourceState, storm::storage::BitVector const& nondeterminismEncoding, ValueType const& factor = storm::utility::one()) { - // For the empty DD, we do not need to add any entries. Note that the partition nodes cannot be zero - // as all states of the model have to be contained. - if (mtbdd_iszero(transitionMatrixNode)) { - return; - } - - // If we have moved through all source variables, we must have arrived at a target block encoding. - if (currentIndex == sourceState.size()) { - // Decode the source block. - uint64_t sourceBlockIndex = decodeBlockIndex(sourcePartitionNode); - - std::unique_ptr& sourceRepresentative = this->uniqueSourceRepresentative[sourceBlockIndex]; - if (sourceRepresentative && *sourceRepresentative != sourceState) { - // In this case, we have picked a different representative and must not record any entries now. - return; - } - - // Otherwise, we record the new representative. - sourceRepresentative.reset(new storm::storage::BitVector(sourceState)); - - // Decode the target block and add matrix entry. - uint64_t targetBlockIndex = decodeBlockIndex(targetPartitionNode); - this->addMatrixEntry(nondeterminismEncoding, sourceBlockIndex, targetBlockIndex, factor * storm::dd::InternalAdd::getValue(transitionMatrixNode)); - } else { - // Determine the levels in the DDs. - uint64_t transitionMatrixVariable = sylvan_isconst(transitionMatrixNode) ? 0xffffffff : sylvan_var(transitionMatrixNode); - uint64_t sourcePartitionVariable = sylvan_var(sourcePartitionNode) - 1; - uint64_t targetPartitionVariable = sylvan_var(targetPartitionNode) - 1; - - // Move through transition matrix. - bool skippedSourceInMatrix = false; - bool skippedTargetTInMatrix = false; - bool skippedTargetEInMatrix = false; - MTBDD tt = transitionMatrixNode; - MTBDD te = transitionMatrixNode; - MTBDD et = transitionMatrixNode; - MTBDD ee = transitionMatrixNode; - if (transitionMatrixVariable == this->sourceVariablesIndicesAndLevels[currentIndex].first) { - MTBDD t = sylvan_high(transitionMatrixNode); - MTBDD e = sylvan_low(transitionMatrixNode); - - uint64_t tVariable = sylvan_isconst(t) ? 0xffffffff : sylvan_var(t); - if (tVariable == this->sourceVariablesIndicesAndLevels[currentIndex].first + 1) { - tt = sylvan_high(t); - te = sylvan_low(t); - } else { - tt = te = t; - skippedTargetTInMatrix = true; - } - - uint64_t eVariable = sylvan_isconst(e) ? 0xffffffff : sylvan_var(e); - if (eVariable == this->sourceVariablesIndicesAndLevels[currentIndex].first + 1) { - et = sylvan_high(e); - ee = sylvan_low(e); - } else { - et = ee = e; - skippedTargetEInMatrix = true; - } - } else { - skippedSourceInMatrix = true; - if (transitionMatrixVariable == this->sourceVariablesIndicesAndLevels[currentIndex].first + 1) { - tt = et = sylvan_high(transitionMatrixNode); - te = ee = sylvan_low(transitionMatrixNode); - } else { - tt = te = et = ee = transitionMatrixNode; - skippedTargetTInMatrix = skippedTargetEInMatrix = true; - } - } - - // Move through partition (for source state). - bool skippedInSourcePartition = false; - MTBDD sourceT; - MTBDD sourceE; - if (sourcePartitionVariable == this->sourceVariablesIndicesAndLevels[currentIndex].first) { - sourceT = sylvan_high(sourcePartitionNode); - sourceE = sylvan_low(sourcePartitionNode); - } else { - sourceT = sourceE = sourcePartitionNode; - skippedInSourcePartition = true; - } - - // Move through partition (for target state). - bool skippedInTargetPartition = false; - MTBDD targetT; - MTBDD targetE; - if (targetPartitionVariable == this->sourceVariablesIndicesAndLevels[currentIndex].first) { - targetT = sylvan_high(targetPartitionNode); - targetE = sylvan_low(targetPartitionNode); - } else { - targetT = targetE = targetPartitionNode; - skippedInTargetPartition = true; - } - - // If we skipped the variable in the source partition, we only have to choose one of the two representatives. - if (!skippedInSourcePartition) { - sourceState.set(currentIndex, true); - // If we skipped the variable in the target partition, just count the one representative twice. - if (!skippedInTargetPartition) { - extractTransitionMatrixRec(tt, sourceT, targetT, currentIndex + 1, sourceState, nondeterminismEncoding, factor); - } - extractTransitionMatrixRec(te, sourceT, targetE, currentIndex + 1, sourceState, nondeterminismEncoding, skippedTargetTInMatrix && skippedInTargetPartition ? 2 * factor : factor); - } - - sourceState.set(currentIndex, false); - // If we skipped the variable in the target partition, just count the one representative twice. - if (!skippedInTargetPartition) { - extractTransitionMatrixRec(et, sourceE, targetT, currentIndex + 1, sourceState, nondeterminismEncoding, factor); - } - extractTransitionMatrixRec(ee, sourceE, targetE, currentIndex + 1, sourceState, nondeterminismEncoding, skippedTargetEInMatrix && skippedInTargetPartition ? 2 * factor : factor); - } - } + private: +// void extractTransitionMatrixRec(MTBDD transitionMatrixNode, BDD sourcePartitionNode, BDD targetPartitionNode, uint64_t currentIndex, storm::storage::BitVector& sourceState, storm::storage::BitVector const& nondeterminismEncoding, ValueType const& factor = storm::utility::one()) { +// // For the empty DD, we do not need to add any entries. Note that the partition nodes cannot be zero +// // as all states of the model have to be contained. +// if (mtbdd_iszero(transitionMatrixNode)) { +// return; +// } +// +// // If we have moved through all source variables, we must have arrived at a target block encoding. +// if (currentIndex == sourceState.size()) { +// // Decode the source block. +// uint64_t sourceBlockIndex = decodeBlockIndex(sourcePartitionNode); +// +// std::unique_ptr& sourceRepresentative = this->uniqueSourceRepresentative[sourceBlockIndex]; +// if (sourceRepresentative && *sourceRepresentative != sourceState) { +// // In this case, we have picked a different representative and must not record any entries now. +// return; +// } +// +// // Otherwise, we record the new representative. +// sourceRepresentative.reset(new storm::storage::BitVector(sourceState)); +// +// // Decode the target block and add matrix entry. +// uint64_t targetBlockIndex = decodeBlockIndex(targetPartitionNode); +// this->addMatrixEntry(nondeterminismEncoding, sourceBlockIndex, targetBlockIndex, factor * storm::dd::InternalAdd::getValue(transitionMatrixNode)); +// } else { +// // Determine the levels in the DDs. +// uint64_t transitionMatrixVariable = sylvan_isconst(transitionMatrixNode) ? 0xffffffff : sylvan_var(transitionMatrixNode); +// uint64_t sourcePartitionVariable = sylvan_var(sourcePartitionNode) - 1; +// uint64_t targetPartitionVariable = sylvan_var(targetPartitionNode) - 1; +// +// // Move through transition matrix. +// bool skippedSourceInMatrix = false; +// bool skippedTargetTInMatrix = false; +// bool skippedTargetEInMatrix = false; +// MTBDD tt = transitionMatrixNode; +// MTBDD te = transitionMatrixNode; +// MTBDD et = transitionMatrixNode; +// MTBDD ee = transitionMatrixNode; +// if (transitionMatrixVariable == this->sourceVariablesIndicesAndLevels[currentIndex].first) { +// MTBDD t = sylvan_high(transitionMatrixNode); +// MTBDD e = sylvan_low(transitionMatrixNode); +// +// uint64_t tVariable = sylvan_isconst(t) ? 0xffffffff : sylvan_var(t); +// if (tVariable == this->sourceVariablesIndicesAndLevels[currentIndex].first + 1) { +// tt = sylvan_high(t); +// te = sylvan_low(t); +// } else { +// tt = te = t; +// skippedTargetTInMatrix = true; +// } +// +// uint64_t eVariable = sylvan_isconst(e) ? 0xffffffff : sylvan_var(e); +// if (eVariable == this->sourceVariablesIndicesAndLevels[currentIndex].first + 1) { +// et = sylvan_high(e); +// ee = sylvan_low(e); +// } else { +// et = ee = e; +// skippedTargetEInMatrix = true; +// } +// } else { +// skippedSourceInMatrix = true; +// if (transitionMatrixVariable == this->sourceVariablesIndicesAndLevels[currentIndex].first + 1) { +// tt = et = sylvan_high(transitionMatrixNode); +// te = ee = sylvan_low(transitionMatrixNode); +// } else { +// tt = te = et = ee = transitionMatrixNode; +// skippedTargetTInMatrix = skippedTargetEInMatrix = true; +// } +// } +// +// // Move through partition (for source state). +// bool skippedInSourcePartition = false; +// MTBDD sourceT; +// MTBDD sourceE; +// if (sourcePartitionVariable == this->sourceVariablesIndicesAndLevels[currentIndex].first) { +// sourceT = sylvan_high(sourcePartitionNode); +// sourceE = sylvan_low(sourcePartitionNode); +// } else { +// sourceT = sourceE = sourcePartitionNode; +// skippedInSourcePartition = true; +// } +// +// // Move through partition (for target state). +// bool skippedInTargetPartition = false; +// MTBDD targetT; +// MTBDD targetE; +// if (targetPartitionVariable == this->sourceVariablesIndicesAndLevels[currentIndex].first) { +// targetT = sylvan_high(targetPartitionNode); +// targetE = sylvan_low(targetPartitionNode); +// } else { +// targetT = targetE = targetPartitionNode; +// skippedInTargetPartition = true; +// } +// +// // If we skipped the variable in the source partition, we only have to choose one of the two representatives. +// if (!skippedInSourcePartition) { +// sourceState.set(currentIndex, true); +// // If we skipped the variable in the target partition, just count the one representative twice. +// if (!skippedInTargetPartition || !skippedTargetTInMatrix) { +// extractTransitionMatrixRec(tt, sourceT, targetT, currentIndex + 1, sourceState, nondeterminismEncoding, factor); +// } +// extractTransitionMatrixRec(te, sourceT, targetE, currentIndex + 1, sourceState, nondeterminismEncoding, skippedTargetTInMatrix && skippedInTargetPartition ? 2 * factor : factor); +// } +// +// sourceState.set(currentIndex, false); +// // If we skipped the variable in the target partition, just count the one representative twice. +// if (!skippedInTargetPartition || !skippedTargetEInMatrix) { +// extractTransitionMatrixRec(et, sourceE, targetT, currentIndex + 1, sourceState, nondeterminismEncoding, factor); +// } +// extractTransitionMatrixRec(ee, sourceE, targetE, currentIndex + 1, sourceState, nondeterminismEncoding, skippedTargetEInMatrix && skippedInTargetPartition ? 2 * factor : factor); +// } +// } spp::sparse_hash_map> blockDecodeCache; }; @@ -824,30 +627,29 @@ namespace storm { template std::shared_ptr> QuotientExtractor::extractSparseQuotient(storm::models::symbolic::Model const& model, Partition const& partition, PreservationInformation const& preservationInformation) { - InternalSparseQuotientExtractor sparseExtractor(model.getManager(), model.getRowVariables(), model.getNondeterminismVariables()); auto states = partition.getStates().swapVariables(model.getRowColumnMetaVariablePairs()); storm::dd::Bdd partitionAsBdd = partition.storedAsAdd() ? partition.asAdd().toBdd() : partition.asBdd(); partitionAsBdd = partitionAsBdd.renameVariables(model.getColumnVariables(), model.getRowVariables()); - partitionAsBdd.template toAdd().exportToDot("partition.dot"); auto start = std::chrono::high_resolution_clock::now(); // FIXME: Use partition as BDD in representative computation. auto representatives = InternalRepresentativeComputer(partition, model.getRowVariables(), model.getColumnVariables()).getRepresentatives(); - representatives.template toAdd().exportToDot("repr.dot"); - (model.getTransitionMatrix() * representatives.template toAdd()).exportToDot("extract.dot"); - storm::storage::SparseMatrix quotientTransitionMatrix = sparseExtractor.extractTransitionMatrix(model.getTransitionMatrix() * representatives.template toAdd(), partition); + STORM_LOG_ASSERT(representatives.getNonZeroCount() == partition.getNumberOfBlocks(), "Representatives size does not match that of the partition: " << representatives.getNonZeroCount() << " vs. " << partition.getNumberOfBlocks() << "."); + storm::dd::Odd odd = representatives.createOdd(); + STORM_LOG_ASSERT(odd.getTotalOffset() == representatives.getNonZeroCount(), "Mismatching ODD."); + InternalSparseQuotientExtractor sparseExtractor(model.getManager(), model.getRowVariables(), model.getColumnVariables(), model.getNondeterminismVariables(), partition, representatives, odd); + storm::storage::SparseMatrix quotientTransitionMatrix = sparseExtractor.extractTransitionMatrix(model.getTransitionMatrix()); auto end = std::chrono::high_resolution_clock::now(); STORM_LOG_TRACE("Quotient transition matrix extracted in " << std::chrono::duration_cast(end - start).count() << "ms."); start = std::chrono::high_resolution_clock::now(); - storm::dd::Odd odd = representatives.createOdd(); storm::models::sparse::StateLabeling quotientStateLabeling(partition.getNumberOfBlocks()); quotientStateLabeling.addLabel("init", ((model.getInitialStates() && partitionAsBdd).existsAbstract(model.getRowVariables()) && partitionAsBdd && representatives).existsAbstract({partition.getBlockVariable()}).toVector(odd)); - quotientStateLabeling.addLabel("deadlock", sparseExtractor.extractStates(model.getDeadlockStates(), partition)); + quotientStateLabeling.addLabel("deadlock", ((model.getDeadlockStates() && partitionAsBdd).existsAbstract(model.getRowVariables()) && partitionAsBdd && representatives).existsAbstract({partition.getBlockVariable()}).toVector(odd)); for (auto const& label : preservationInformation.getLabels()) { - quotientStateLabeling.addLabel(label, sparseExtractor.extractStates(model.getStates(label), partition)); + quotientStateLabeling.addLabel(label, (model.getStates(label) && representatives).toVector(odd)); } for (auto const& expression : preservationInformation.getExpressions()) { std::stringstream stream; @@ -857,7 +659,7 @@ namespace storm { if (quotientStateLabeling.containsLabel(expressionAsString)) { STORM_LOG_WARN("Duplicate label '" << expressionAsString << "', dropping second label definition."); } else { - quotientStateLabeling.addLabel(stream.str(), sparseExtractor.extractStates(model.getStates(expression), partition)); + quotientStateLabeling.addLabel(stream.str(), (model.getStates(expression) && representatives).toVector(odd)); } } end = std::chrono::high_resolution_clock::now(); diff --git a/src/storm/storage/dd/cudd/InternalCuddBdd.cpp b/src/storm/storage/dd/cudd/InternalCuddBdd.cpp index acdd67e63..8d8264dd7 100644 --- a/src/storm/storage/dd/cudd/InternalCuddBdd.cpp +++ b/src/storm/storage/dd/cudd/InternalCuddBdd.cpp @@ -313,10 +313,10 @@ namespace storm { Odd InternalBdd::createOdd(std::vector const& ddVariableIndices) const { // Prepare a unique table for each level that keeps the constructed ODD nodes unique. - std::vector, std::shared_ptr, HashFunctor>> uniqueTableForLevels(ddVariableIndices.size() + 1); + std::vector>> uniqueTableForLevels(ddVariableIndices.size() + 1); // Now construct the ODD structure from the BDD. - std::shared_ptr rootOdd = createOddRec(Cudd_Regular(this->getCuddDdNode()), ddManager->getCuddManager(), 0, Cudd_IsComplement(this->getCuddDdNode()), ddVariableIndices.size(), ddVariableIndices, uniqueTableForLevels); + std::shared_ptr rootOdd = createOddRec(this->getCuddDdNode(), ddManager->getCuddManager(), 0, ddVariableIndices.size(), ddVariableIndices, uniqueTableForLevels); // Return a copy of the root node to remove the shared_ptr encapsulation. return Odd(*rootOdd); @@ -329,57 +329,44 @@ namespace storm { return result; } - std::shared_ptr InternalBdd::createOddRec(DdNode const* dd, cudd::Cudd const& manager, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel, std::vector const& ddVariableIndices, std::vector, std::shared_ptr, HashFunctor>>& uniqueTableForLevels) { + std::shared_ptr InternalBdd::createOddRec(DdNode const* dd, cudd::Cudd const& manager, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector const& ddVariableIndices, std::vector>>& uniqueTableForLevels) { // Check whether the ODD for this node has already been computed (for this level) and if so, return this instead. - auto const& iterator = uniqueTableForLevels[currentLevel].find(std::make_pair(dd, complement)); - if (iterator != uniqueTableForLevels[currentLevel].end()) { - return iterator->second; + auto it = uniqueTableForLevels[currentLevel].find(dd); + if (it != uniqueTableForLevels[currentLevel].end()) { + return it->second; } else { // Otherwise, we need to recursively compute the ODD. // If we are already at the maximal level that is to be considered, we can simply create an Odd without // successors if (currentLevel == maxLevel) { - uint_fast64_t elseOffset = 0; - uint_fast64_t thenOffset = 0; - - // If the DD is not the zero leaf, then the then-offset is 1. - if (dd != Cudd_ReadZero(manager.getManager())) { - thenOffset = 1; - } - - // If we need to complement the 'terminal' node, we need to negate its offset. - if (complement) { - thenOffset = 1 - thenOffset; - } - - auto oddNode = std::make_shared(nullptr, elseOffset, nullptr, thenOffset); - uniqueTableForLevels[currentLevel].emplace(std::make_pair(dd, complement), oddNode); + auto oddNode = std::make_shared(nullptr, 0, nullptr, dd != Cudd_ReadLogicZero(manager.getManager()) ? 1 : 0); + uniqueTableForLevels[currentLevel].emplace(dd, oddNode); return oddNode; } else if (ddVariableIndices[currentLevel] < Cudd_NodeReadIndex(dd)) { // If we skipped the level in the DD, we compute the ODD just for the else-successor and use the same // node for the then-successor as well. - std::shared_ptr elseNode = createOddRec(dd, manager, currentLevel + 1, complement, maxLevel, ddVariableIndices, uniqueTableForLevels); + std::shared_ptr elseNode = createOddRec(dd, manager, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels); std::shared_ptr thenNode = elseNode; - uint_fast64_t totalOffset = elseNode->getElseOffset() + elseNode->getThenOffset(); - auto oddNode = std::make_shared(elseNode, totalOffset, thenNode, totalOffset); - uniqueTableForLevels[currentLevel].emplace(std::make_pair(dd, complement), oddNode); + auto oddNode = std::make_shared(elseNode, elseNode->getTotalOffset(), thenNode, elseNode->getTotalOffset()); + uniqueTableForLevels[currentLevel].emplace(dd, oddNode); return oddNode; } else { // Otherwise, we compute the ODDs for both the then- and else successors. DdNode const* thenDdNode = Cudd_T_const(dd); DdNode const* elseDdNode = Cudd_E_const(dd); - // Determine whether we have to evaluate the successors as if they were complemented. - bool elseComplemented = Cudd_IsComplement(elseDdNode) ^ complement; - bool thenComplemented = Cudd_IsComplement(thenDdNode) ^ complement; + if (Cudd_IsComplement(dd)) { + thenDdNode = Cudd_Not(thenDdNode); + elseDdNode = Cudd_Not(elseDdNode); + } - std::shared_ptr elseNode = createOddRec(Cudd_Regular(elseDdNode), manager, currentLevel + 1, elseComplemented, maxLevel, ddVariableIndices, uniqueTableForLevels); - std::shared_ptr thenNode = createOddRec(Cudd_Regular(thenDdNode), manager, currentLevel + 1, thenComplemented, maxLevel, ddVariableIndices, uniqueTableForLevels); + std::shared_ptr elseNode = createOddRec(elseDdNode, manager, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels); + std::shared_ptr thenNode = createOddRec(thenDdNode, manager, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels); - auto oddNode = std::make_shared(elseNode, elseNode->getElseOffset() + elseNode->getThenOffset(), thenNode, thenNode->getElseOffset() + thenNode->getThenOffset()); - uniqueTableForLevels[currentLevel].emplace(std::make_pair(dd, complement), oddNode); + auto oddNode = std::make_shared(elseNode, elseNode->getTotalOffset(), thenNode, thenNode->getTotalOffset()); + uniqueTableForLevels[currentLevel].emplace(dd, oddNode); return oddNode; } } diff --git a/src/storm/storage/dd/cudd/InternalCuddBdd.h b/src/storm/storage/dd/cudd/InternalCuddBdd.h index 005404e8e..36a200a56 100644 --- a/src/storm/storage/dd/cudd/InternalCuddBdd.h +++ b/src/storm/storage/dd/cudd/InternalCuddBdd.h @@ -443,14 +443,13 @@ namespace storm { * @param dd The DD for which to build the ODD. * @param manager The manager responsible for the DD. * @param currentLevel The currently considered level in the DD. - * @param complement A flag indicating whether or not the given node is to be considered as complemented. * @param maxLevel The number of levels that need to be considered. * @param ddVariableIndices The (sorted) indices of all DD variables that need to be considered. * @param uniqueTableForLevels A vector of unique tables, one for each level to be considered, that keeps * ODD nodes for the same DD and level unique. * @return A pointer to the constructed ODD for the given arguments. */ - static std::shared_ptr createOddRec(DdNode const* dd, cudd::Cudd const& manager, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel, std::vector const& ddVariableIndices, std::vector, std::shared_ptr, HashFunctor>>& uniqueTableForLevels); + static std::shared_ptr createOddRec(DdNode const* dd, cudd::Cudd const& manager, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector const& ddVariableIndices, std::vector>>& uniqueTableForLevels); /*! * Adds the selected values the target vector.