From 2b0911d627ffb0f20bf199e0499cdba9d6b68057 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 3 Aug 2017 18:20:30 +0200 Subject: [PATCH] more work on MDP bisimulation --- src/storm/models/symbolic/Model.cpp | 13 +- src/storm/models/symbolic/Model.h | 15 +- .../models/symbolic/NondeterministicModel.cpp | 14 -- .../models/symbolic/NondeterministicModel.h | 5 +- .../dd/bisimulation/PartitionRefiner.cpp | 6 +- .../dd/bisimulation/QuotientExtractor.cpp | 2 +- .../dd/bisimulation/SignatureRefiner.cpp | 162 +++++++++--------- 7 files changed, 112 insertions(+), 105 deletions(-) diff --git a/src/storm/models/symbolic/Model.cpp b/src/storm/models/symbolic/Model.cpp index 46c8ad35c..61f9932f4 100644 --- a/src/storm/models/symbolic/Model.cpp +++ b/src/storm/models/symbolic/Model.cpp @@ -174,12 +174,21 @@ namespace storm { template std::set Model::getRowAndNondeterminismVariables() const { - return rowVariables; + std::set result; + std::set_union(this->getRowVariables().begin(), this->getRowVariables().end(), this->getNondeterminismVariables().begin(), this->getNondeterminismVariables().end(), std::inserter(result, result.begin())); + return result; } template std::set Model::getColumnAndNondeterminismVariables() const { - return columnVariables; + std::set result; + std::set_union(this->getColumnVariables().begin(), this->getColumnVariables().end(), this->getNondeterminismVariables().begin(), this->getNondeterminismVariables().end(), std::inserter(result, result.begin())); + return result; + } + + template + std::set const& Model::getNondeterminismVariables() const { + return emptyVariableSet; } template diff --git a/src/storm/models/symbolic/Model.h b/src/storm/models/symbolic/Model.h index 395028ae9..1f0aee439 100644 --- a/src/storm/models/symbolic/Model.h +++ b/src/storm/models/symbolic/Model.h @@ -226,14 +226,21 @@ namespace storm { * * @return All meta variables used to encode rows and nondetermism. */ - virtual std::set getRowAndNondeterminismVariables() const; + std::set getRowAndNondeterminismVariables() const; /*! * Retrieves all meta variables used to encode columns and nondetermism. * * @return All meta variables used to encode columns and nondetermism. */ - virtual std::set getColumnAndNondeterminismVariables() const; + std::set getColumnAndNondeterminismVariables() const; + + /*! + * Retrieves all meta variables used to encode the nondeterminism. + * + * @return All meta variables used to encode the nondeterminism. + */ + virtual std::set const& getNondeterminismVariables() const; /*! * Retrieves the pairs of row and column meta variables. @@ -311,7 +318,6 @@ namespace storm { std::set const& getParameters() const; protected: - /*! * Sets the transition matrix of the model. * @@ -389,6 +395,9 @@ namespace storm { // The parameters. Only meaningful for models over rational functions. std::set parameters; + + // An empty variable set that can be used when references to non-existing sets need to be returned. + std::set emptyVariableSet; }; } // namespace symbolic diff --git a/src/storm/models/symbolic/NondeterministicModel.cpp b/src/storm/models/symbolic/NondeterministicModel.cpp index 32baf1cd2..6545e27c0 100644 --- a/src/storm/models/symbolic/NondeterministicModel.cpp +++ b/src/storm/models/symbolic/NondeterministicModel.cpp @@ -62,20 +62,6 @@ namespace storm { return nondeterminismVariables; } - template - std::set NondeterministicModel::getRowAndNondeterminismVariables() const { - std::set result; - std::set_union(this->getRowVariables().begin(), this->getRowVariables().end(), this->getNondeterminismVariables().begin(), this->getNondeterminismVariables().end(), std::inserter(result, result.begin())); - return result; - } - - template - std::set NondeterministicModel::getColumnAndNondeterminismVariables() const { - std::set result; - std::set_union(this->getColumnVariables().begin(), this->getColumnVariables().end(), this->getNondeterminismVariables().begin(), this->getNondeterminismVariables().end(), std::inserter(result, result.begin())); - return result; - } - template storm::dd::Bdd const& NondeterministicModel::getIllegalMask() const { return illegalMask; diff --git a/src/storm/models/symbolic/NondeterministicModel.h b/src/storm/models/symbolic/NondeterministicModel.h index b3d5b7cb6..ecbc2af94 100644 --- a/src/storm/models/symbolic/NondeterministicModel.h +++ b/src/storm/models/symbolic/NondeterministicModel.h @@ -97,10 +97,7 @@ namespace storm { * * @return The meta variables used to encode the nondeterminism in the model. */ - std::set const& getNondeterminismVariables() const; - - virtual std::set getRowAndNondeterminismVariables() const override; - virtual std::set getColumnAndNondeterminismVariables() const override; + virtual std::set const& getNondeterminismVariables() const override; /*! * Retrieves a BDD characterizing all illegal nondeterminism encodings in the model. diff --git a/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp b/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp index b3e19cdc2..8a5915004 100644 --- a/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp +++ b/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp @@ -5,7 +5,7 @@ namespace storm { namespace bisimulation { template - PartitionRefiner::PartitionRefiner(storm::models::symbolic::Model const& model, Partition const& initialStatePartition) : status(Status::Initialized), refinements(0), statePartition(initialStatePartition), signatureComputer(model), signatureRefiner(model.getManager(), statePartition.getBlockVariable(), model.getRowAndNondeterminismVariables()) { + PartitionRefiner::PartitionRefiner(storm::models::symbolic::Model const& model, Partition const& initialStatePartition) : status(Status::Initialized), refinements(0), statePartition(initialStatePartition), signatureComputer(model), signatureRefiner(model.getManager(), statePartition.getBlockVariable(), model.getRowAndNondeterminismVariables(), model.getNondeterminismVariables()) { // Intentionally left empty. } @@ -44,7 +44,7 @@ namespace storm { totalSignatureTime += (signatureEnd - signatureStart); STORM_LOG_DEBUG("Signature " << refinements << "[" << index << "] DD has " << signature.getSignatureAdd().getNodeCount() << " nodes."); - signature.getSignatureAdd().exportToDot("sig" + std::to_string(refinements) + ".dot"); +// signature.getSignatureAdd().exportToDot("sig" + std::to_string(refinements) + ".dot"); // if (refinements == 1) { // exit(-1); // } @@ -54,7 +54,7 @@ namespace storm { auto refinementEnd = std::chrono::high_resolution_clock::now(); totalRefinementTime += (refinementEnd - refinementStart); - newPartition.asAdd().exportToDot("newpart" + std::to_string(refinements) + ".dot"); +// newPartition.asAdd().exportToDot("newpart" + std::to_string(refinements) + ".dot"); signatureTime += std::chrono::duration_cast(signatureEnd - signatureStart).count(); refinementTime = std::chrono::duration_cast(refinementEnd - refinementStart).count(); diff --git a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp index ccaeaa774..b88524f6c 100644 --- a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp +++ b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp @@ -592,7 +592,7 @@ namespace storm { return std::shared_ptr>(new storm::models::symbolic::Ctmc(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, preservedLabelBdds, {})); } } else { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Cannot exctract quotient for this model type."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Cannot extract quotient for this model type."); } } diff --git a/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp b/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp index 4595b5fd0..e370a75bd 100644 --- a/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp +++ b/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp @@ -99,8 +99,6 @@ namespace storm { reuseBlocksCache.clear(); nextFreeBlockIndex = oldPartition.getNextFreeBlockIndex(); - internalDdManager.debugCheck(); - // Perform the actual recursive refinement step. DdNodePtr result = refine(oldPartition.asAdd().getInternalAdd().getCuddDdNode(), signatureAdd.getInternalAdd().getCuddDdNode(), nondeterminismVariables.getInternalBdd().getCuddDdNode(), nonBlockVariables.getInternalBdd().getCuddDdNode()); @@ -108,8 +106,6 @@ namespace storm { storm::dd::InternalAdd internalNewPartitionAdd(&internalDdManager, cudd::ADD(internalDdManager.getCuddManager(), result)); storm::dd::Add newPartitionAdd(oldPartition.asAdd().getDdManager(), internalNewPartitionAdd, oldPartition.asAdd().getContainedMetaVariables()); - internalDdManager.debugCheck(); - return newPartitionAdd; } @@ -154,28 +150,48 @@ namespace storm { } else { // If there are more variables that belong to the non-block part of the encoding, we need to recursively descend. - // Remember an offset that indicates whether the top variable is a nondeterminism variable or not. - short offset = 1; - if (!Cudd_IsConstant(nondeterminismVariablesNode) && Cudd_NodeReadIndex(nondeterminismVariablesNode) == Cudd_NodeReadIndex(nonBlockVariablesNode)) { - offset = 0; - } - + bool skippedBoth = true; DdNode* partitionThen; DdNode* partitionElse; - if (Cudd_NodeReadIndex(partitionNode) - offset == Cudd_NodeReadIndex(nonBlockVariablesNode)) { - partitionThen = Cudd_T(partitionNode); - partitionElse = Cudd_E(partitionNode); - } else { - partitionThen = partitionElse = partitionNode; - } - DdNode* signatureThen; DdNode* signatureElse; - if (Cudd_NodeReadIndex(signatureNode) == Cudd_NodeReadIndex(nonBlockVariablesNode)) { - signatureThen = Cudd_T(signatureNode); - signatureElse = Cudd_E(signatureNode); - } else { - signatureThen = signatureElse = signatureNode; + short offset = 1; + while (skippedBoth && !Cudd_IsConstant(nonBlockVariablesNode)) { + // Remember an offset that indicates whether the top variable is a nondeterminism variable or not. + offset = 1; + if (!Cudd_IsConstant(nondeterminismVariablesNode) && Cudd_NodeReadIndex(nondeterminismVariablesNode) == Cudd_NodeReadIndex(nonBlockVariablesNode)) { + offset = 0; + } + + if (Cudd_NodeReadIndex(partitionNode) - offset == Cudd_NodeReadIndex(nonBlockVariablesNode)) { + partitionThen = Cudd_T(partitionNode); + partitionElse = Cudd_E(partitionNode); + skippedBoth = false; + } else { + partitionThen = partitionElse = partitionNode; + } + + if (Cudd_NodeReadIndex(signatureNode) == Cudd_NodeReadIndex(nonBlockVariablesNode)) { + signatureThen = Cudd_T(signatureNode); + signatureElse = Cudd_E(signatureNode); + skippedBoth = false; + } else { + signatureThen = signatureElse = signatureNode; + } + + // If both (signature and partition) skipped the next variable, we fast-forward. + if (skippedBoth) { + // If the current variable is a nondeterminism variable, we need to advance both variable sets otherwise just the non-block variables. + nonBlockVariablesNode = Cudd_T(nonBlockVariablesNode); + if (offset == 0) { + 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 refine(partitionNode, signatureNode, nondeterminismVariablesNode, nonBlockVariablesNode); } DdNode* thenResult = refine(partitionThen, signatureThen, offset == 0 ? Cudd_T(nondeterminismVariablesNode) : nondeterminismVariablesNode, Cudd_T(nonBlockVariablesNode)); @@ -315,24 +331,13 @@ namespace storm { STORM_LOG_ASSERT(partitionNode != mtbdd_false, "Expected non-false node."); -// ++numberOfVisitedNodes; - // Check the cache whether we have seen the same node before. -// ++signatureCacheLookups; -// auto start = std::chrono::high_resolution_clock::now(); - std::unique_ptr& sigCacheEntrySmartPtr = signatureCache[std::make_pair(signatureNode, partitionNode)]; - if (sigCacheEntrySmartPtr) { -// ++signatureCacheHits; + auto nodePair = std::make_pair(signatureNode, partitionNode); + auto it = signatureCache.find(nodePair); + if (it != signatureCache.end()) { // If so, we return the corresponding result. -// auto end = std::chrono::high_resolution_clock::now(); -// totalSignatureCacheLookupTime += end - start; - return *sigCacheEntrySmartPtr; + return it->second; } -// auto end = std::chrono::high_resolution_clock::now(); -// totalSignatureCacheLookupTime += end - start; - - MTBDD* newEntryPtr = new MTBDD; - sigCacheEntrySmartPtr.reset(newEntryPtr); sylvan_gc_test(); @@ -341,55 +346,62 @@ namespace storm { // 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. - // start = std::chrono::high_resolution_clock::now(); auto& reuseBlockEntry = reuseBlocksCache[partitionNode]; - // end = std::chrono::high_resolution_clock::now(); - // totalReuseBlocksLookupTime += end - start; if (!reuseBlockEntry.isReused()) { reuseBlockEntry.setReused(); reuseBlocksCache.emplace(partitionNode, true); - // start = std::chrono::high_resolution_clock::now(); - *newEntryPtr = partitionNode; - // end = std::chrono::high_resolution_clock::now(); - // totalSignatureCacheStoreTime += end - start; + signatureCache[nodePair] = partitionNode; return partitionNode; } else { - // start = std::chrono::high_resolution_clock::now(); BDD result = encodeBlock(nextFreeBlockIndex++); - // end = std::chrono::high_resolution_clock::now(); - // totalBlockEncodingTime += end - start; - - // start = std::chrono::high_resolution_clock::now(); - *newEntryPtr = result; - // end = std::chrono::high_resolution_clock::now(); - // totalSignatureCacheStoreTime += end - start; + 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. - // Remember an offset that indicates whether the top variable is a nondeterminism variable or not. - short offset = 1; - if (!sylvan_isconst(nondeterminismVariablesNode) && sylvan_var(nondeterminismVariablesNode) == sylvan_var(nonBlockVariablesNode)) { - offset = 0; - } - + bool skippedBoth = true; BDD partitionThen; BDD partitionElse; - if (sylvan_var(partitionNode) - offset == sylvan_var(nonBlockVariablesNode)) { - partitionThen = sylvan_high(partitionNode); - partitionElse = sylvan_low(partitionNode); - } else { - partitionThen = partitionElse = partitionNode; - } - MTBDD signatureThen; MTBDD signatureElse; - if (sylvan_var(signatureNode) == sylvan_var(nonBlockVariablesNode)) { - signatureThen = sylvan_high(signatureNode); - signatureElse = sylvan_low(signatureNode); - } else { - signatureThen = signatureElse = signatureNode; + short offset = 1; + while (skippedBoth && !sylvan_isconst(nonBlockVariablesNode)) { + // Remember an offset that indicates whether the top variable is a nondeterminism variable or not. + offset = 1; + if (!sylvan_isconst(nondeterminismVariablesNode) && sylvan_var(nondeterminismVariablesNode) == sylvan_var(nonBlockVariablesNode)) { + offset = 0; + } + + if (sylvan_var(partitionNode) - offset == sylvan_var(nonBlockVariablesNode)) { + partitionThen = sylvan_high(partitionNode); + partitionElse = sylvan_low(partitionNode); + skippedBoth = false; + } else { + partitionThen = partitionElse = partitionNode; + } + + if (sylvan_var(signatureNode) == sylvan_var(nonBlockVariablesNode)) { + signatureThen = sylvan_high(signatureNode); + signatureElse = sylvan_low(signatureNode); + skippedBoth = false; + } else { + signatureThen = signatureElse = signatureNode; + } + + // If both (signature and partition) skipped the next variable, we fast-forward. + if (skippedBoth) { + // If the current variable is a nondeterminism variable, we need to advance both variable sets otherwise just the non-block variables. + nonBlockVariablesNode = sylvan_high(nonBlockVariablesNode); + if (offset == 0) { + 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 refine(partitionNode, signatureNode, nondeterminismVariablesNode, nonBlockVariablesNode); } BDD thenResult = refine(partitionThen, signatureThen, offset == 0 ? sylvan_high(nondeterminismVariablesNode) : nondeterminismVariablesNode, sylvan_high(nonBlockVariablesNode)); @@ -400,17 +412,11 @@ namespace storm { result = thenResult; } else { // Get the node to connect the subresults. - // start = std::chrono::high_resolution_clock::now(); result = sylvan_makenode(sylvan_var(nonBlockVariablesNode) + offset, elseResult, thenResult); - // end = std::chrono::high_resolution_clock::now(); - // totalMakeNodeTime += end - start; } // Store the result in the cache. - // start = std::chrono::high_resolution_clock::now(); - *newEntryPtr = result; - // end = std::chrono::high_resolution_clock::now(); - // totalSignatureCacheStoreTime += end - start; + signatureCache[nodePair] = result; return result; } @@ -434,7 +440,7 @@ namespace storm { uint64_t numberOfRefinements; // The cache used to identify states with identical signature. - spp::sparse_hash_map, std::unique_ptr, SylvanMTBDDPairHash> signatureCache; + spp::sparse_hash_map, MTBDD, SylvanMTBDDPairHash> signatureCache; // The cache used to identify which old block numbers have already been reused. spp::sparse_hash_map reuseBlocksCache;