From 472eaffabc38e723053fbc5ed8e95b2bb63b0aa0 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 3 Aug 2017 16:57:11 +0200 Subject: [PATCH] more work on refiners that deal with nondeterminism variables --- .../dd/bisimulation/SignatureRefiner.cpp | 287 ++++++++++-------- .../dd/bisimulation/SignatureRefiner.h | 2 +- 2 files changed, 153 insertions(+), 136 deletions(-) diff --git a/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp b/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp index 028fb7767..4595b5fd0 100644 --- a/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp +++ b/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp @@ -10,6 +10,7 @@ #include "storm/utility/macros.h" #include "storm/exceptions/InvalidSettingsException.h" #include "storm/exceptions/NotImplementedException.h" +#include "storm/exceptions/InvalidArgumentException.h" #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/BisimulationSettings.h" @@ -79,7 +80,7 @@ namespace storm { template class InternalSignatureRefiner { public: - InternalSignatureRefiner(storm::dd::DdManager const& manager, storm::expressions::Variable const& blockVariable, uint64_t lastStateLevel) : manager(manager), internalDdManager(manager.getInternalDdManager()), blockVariable(blockVariable), lastStateLevel(lastStateLevel), nextFreeBlockIndex(0), numberOfRefinements(0), lastNumberOfVisitedNodes(10000), signatureCache(lastNumberOfVisitedNodes), reuseBlocksCache(lastNumberOfVisitedNodes) { + InternalSignatureRefiner(storm::dd::DdManager const& manager, storm::expressions::Variable const& blockVariable, storm::dd::Bdd const& nondeterminismVariables, storm::dd::Bdd const& nonBlockVariables) : manager(manager), internalDdManager(manager.getInternalDdManager()), blockVariable(blockVariable), nondeterminismVariables(nondeterminismVariables), nonBlockVariables(nonBlockVariables), nextFreeBlockIndex(0), numberOfRefinements(0), lastNumberOfVisitedNodes(10000), signatureCache(lastNumberOfVisitedNodes), reuseBlocksCache(lastNumberOfVisitedNodes) { // Intentionally left empty. } @@ -97,18 +98,22 @@ namespace storm { signatureCache.clear(); reuseBlocksCache.clear(); nextFreeBlockIndex = oldPartition.getNextFreeBlockIndex(); - + + internalDdManager.debugCheck(); + // Perform the actual recursive refinement step. - DdNodePtr result = refine(oldPartition.asAdd().getInternalAdd().getCuddDdNode(), signatureAdd.getInternalAdd().getCuddDdNode()); + DdNodePtr result = refine(oldPartition.asAdd().getInternalAdd().getCuddDdNode(), signatureAdd.getInternalAdd().getCuddDdNode(), nondeterminismVariables.getInternalBdd().getCuddDdNode(), nonBlockVariables.getInternalBdd().getCuddDdNode()); // Construct resulting ADD from the obtained node and the meta information. storm::dd::InternalAdd internalNewPartitionAdd(&internalDdManager, cudd::ADD(internalDdManager.getCuddManager(), result)); storm::dd::Add newPartitionAdd(oldPartition.asAdd().getDdManager(), internalNewPartitionAdd, oldPartition.asAdd().getContainedMetaVariables()); + internalDdManager.debugCheck(); + return newPartitionAdd; } - DdNodePtr refine(DdNode* partitionNode, DdNode* signatureNode) { + DdNodePtr refine(DdNode* partitionNode, DdNode* signatureNode, DdNode* nondeterminismVariablesNode, DdNode* nonBlockVariablesNode) { ::DdManager* ddman = internalDdManager.getCuddManager().getManager(); // If we arrived at the constant zero node, then this was an illegal state encoding (we require @@ -118,45 +123,66 @@ namespace storm { } // Check the cache whether we have seen the same node before. - std::unique_ptr& sigCacheEntrySmartPtr = signatureCache[std::make_pair(signatureNode, partitionNode)]; - if (sigCacheEntrySmartPtr) { + auto nodePair = std::make_pair(signatureNode, partitionNode); + auto it = signatureCache.find(nodePair); + if (it != signatureCache.end()) { // If so, we return the corresponding result. - return *sigCacheEntrySmartPtr; + return it->second; } - DdNode** newEntryPtr = new DdNode*; - sigCacheEntrySmartPtr.reset(newEntryPtr); - - // Determine the levels in the DDs. - uint64_t partitionVariable = Cudd_NodeReadIndex(partitionNode) - 1; - uint64_t signatureVariable = Cudd_NodeReadIndex(signatureNode); - uint64_t partitionLevel = Cudd_ReadPerm(ddman, partitionVariable); - uint64_t signatureLevel = Cudd_ReadPerm(ddman, signatureVariable); - uint64_t topLevel = std::min(partitionLevel, signatureLevel); - uint64_t topVariable = topLevel == partitionLevel ? partitionVariable : signatureVariable; - - // Check whether the top variable is still within the state encoding. - if (topLevel <= lastStateLevel) { - // Determine subresults by recursive descent. - DdNodePtr thenResult; - DdNodePtr elseResult; - if (partitionLevel < signatureLevel) { - thenResult = refine(Cudd_T(partitionNode), signatureNode); - Cudd_Ref(thenResult); - elseResult = refine(Cudd_E(partitionNode), signatureNode); - Cudd_Ref(elseResult); - } else if (partitionLevel > signatureLevel) { - thenResult = refine(partitionNode, Cudd_T(signatureNode)); - Cudd_Ref(thenResult); - elseResult = refine(partitionNode, Cudd_E(signatureNode)); - Cudd_Ref(elseResult); + // If there are no more non-block variables, we hit the signature. + if (Cudd_IsConstant(nonBlockVariablesNode)) { + // If this is the first time (in this traversal) that we encounter this signature, we check + // whether we can assign the old block number to it. + auto& reuseEntry = reuseBlocksCache[partitionNode]; + if (!reuseEntry.isReused()) { + reuseEntry.setReused(); + signatureCache[nodePair] = partitionNode; + return partitionNode; } else { - thenResult = refine(Cudd_T(partitionNode), Cudd_T(signatureNode)); - Cudd_Ref(thenResult); - elseResult = refine(Cudd_E(partitionNode), Cudd_E(signatureNode)); - Cudd_Ref(elseResult); + DdNode* result; + { + storm::dd::Add blockEncoding = manager.getEncoding(blockVariable, nextFreeBlockIndex, false).template toAdd(); + ++nextFreeBlockIndex; + result = blockEncoding.getInternalAdd().getCuddDdNode(); + Cudd_Ref(result); + } + signatureCache[nodePair] = result; + Cudd_Deref(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 (!Cudd_IsConstant(nondeterminismVariablesNode) && Cudd_NodeReadIndex(nondeterminismVariablesNode) == Cudd_NodeReadIndex(nonBlockVariablesNode)) { + offset = 0; + } + + 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; + } + + DdNode* thenResult = refine(partitionThen, signatureThen, offset == 0 ? Cudd_T(nondeterminismVariablesNode) : nondeterminismVariablesNode, Cudd_T(nonBlockVariablesNode)); + Cudd_Ref(thenResult); + DdNode* elseResult = refine(partitionElse, signatureElse, offset == 0 ? Cudd_T(nondeterminismVariablesNode) : nondeterminismVariablesNode, Cudd_T(nonBlockVariablesNode)); + Cudd_Ref(elseResult); + DdNode* result; if (thenResult == elseResult) { Cudd_Deref(thenResult); @@ -164,7 +190,7 @@ namespace storm { result = thenResult; } else { // Get the node to connect the subresults. - DdNode* var = Cudd_addIthVar(ddman, topVariable + 1); + DdNode* var = Cudd_addIthVar(ddman, Cudd_NodeReadIndex(nonBlockVariablesNode) + offset); Cudd_Ref(var); result = Cudd_addIte(ddman, var, thenResult, elseResult); Cudd_Ref(result); @@ -174,33 +200,10 @@ namespace storm { } // Store the result in the cache. - *newEntryPtr = result; + signatureCache[nodePair] = result; Cudd_Deref(result); return result; - } else { - - // If we are not within the state encoding any more, we hit the signature itself. - - // 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(); - *newEntryPtr = partitionNode; - return partitionNode; - } else { - DdNode* result; - { - storm::dd::Add blockEncoding = manager.getEncoding(blockVariable, nextFreeBlockIndex, false).template toAdd(); - ++nextFreeBlockIndex; - result = blockEncoding.getInternalAdd().getCuddDdNode(); - Cudd_Ref(result); - } - *newEntryPtr = result; - Cudd_Deref(result); - return result; - } } } @@ -208,8 +211,9 @@ namespace storm { storm::dd::InternalDdManager const& internalDdManager; storm::expressions::Variable const& blockVariable; - // The last level that belongs to the state encoding in the DDs. - uint64_t lastStateLevel; + // The cubes representing all non-block and all nondeterminism variables, respectively. + storm::dd::Bdd nondeterminismVariables; + storm::dd::Bdd nonBlockVariables; // The current number of blocks of the new partition. uint64_t nextFreeBlockIndex; @@ -221,7 +225,7 @@ namespace storm { uint64_t lastNumberOfVisitedNodes; // The cache used to identify states with identical signature. - spp::sparse_hash_map, std::unique_ptr, CuddPointerPairHash> signatureCache; + spp::sparse_hash_map, DdNode*, CuddPointerPairHash> signatureCache; // The cache used to identify which old block numbers have already been reused. spp::sparse_hash_map reuseBlocksCache; @@ -230,7 +234,7 @@ namespace storm { template class InternalSignatureRefiner { public: - InternalSignatureRefiner(storm::dd::DdManager const& manager, storm::expressions::Variable const& blockVariable, uint64_t lastStateLevel) : manager(manager), internalDdManager(manager.getInternalDdManager()), blockVariable(blockVariable), numberOfBlockVariables(manager.getMetaVariable(blockVariable).getNumberOfDdVariables()), blockCube(manager.getMetaVariable(blockVariable).getCube()), lastStateLevel(lastStateLevel), nextFreeBlockIndex(0), numberOfRefinements(0), signatureCache() { + InternalSignatureRefiner(storm::dd::DdManager const& manager, storm::expressions::Variable const& blockVariable, storm::dd::Bdd const& nondeterminismVariables, storm::dd::Bdd const& nonBlockVariables) : manager(manager), internalDdManager(manager.getInternalDdManager()), blockVariable(blockVariable), nondeterminismVariables(nondeterminismVariables), nonBlockVariables(nonBlockVariables), 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(); @@ -270,7 +274,7 @@ namespace storm { // totalMakeNodeTime = std::chrono::high_resolution_clock::duration(0); // Perform the actual recursive refinement step. - BDD result = refine(oldPartition.asBdd().getInternalBdd().getSylvanBdd().GetBDD(), signatureAdd.getInternalAdd().getSylvanMtbdd().GetMTBDD()); + BDD result = refine(oldPartition.asBdd().getInternalBdd().getSylvanBdd().GetBDD(), signatureAdd.getInternalAdd().getSylvanMtbdd().GetMTBDD(), nondeterminismVariables.getInternalBdd().getSylvanBdd().GetBDD(), nonBlockVariables.getInternalBdd().getSylvanBdd().GetBDD()); // Construct resulting BDD from the obtained node and the meta information. storm::dd::InternalBdd internalNewPartitionBdd(&internalDdManager, sylvan::Bdd(result)); @@ -300,7 +304,7 @@ namespace storm { return sylvan_cube(blockCube.getInternalBdd().getSylvanBdd().GetBDD(), e.data()); } - BDD refine(BDD partitionNode, MTBDD signatureNode) { + BDD refine(BDD partitionNode, MTBDD signatureNode, BDD nondeterminismVariablesNode, BDD nonBlockVariablesNode) { LACE_ME; // If we arrived at the constant zero node, then this was an illegal state encoding (we require @@ -331,93 +335,98 @@ namespace storm { sigCacheEntrySmartPtr.reset(newEntryPtr); sylvan_gc_test(); - - // Determine levels in the DDs. -// start = std::chrono::high_resolution_clock::now(); - BDDVAR signatureVariable = sylvan_isconst(signatureNode) ? 0xffffffff : sylvan_var(signatureNode); - BDDVAR partitionVariable = sylvan_var(partitionNode) - 1; - BDDVAR topVariable = std::min(signatureVariable, partitionVariable); -// end = std::chrono::high_resolution_clock::now(); -// totalLevelLookupTime += end - start; - // Check whether the top variable is still within the state encoding. - if (topVariable <= lastStateLevel) { - // Determine subresults by recursive descent. - BDD thenResult; - BDD elseResult; - if (partitionVariable < signatureVariable) { - elseResult = refine(sylvan_low(partitionNode), signatureNode); - thenResult = refine(sylvan_high(partitionNode), signatureNode); - } else if (partitionVariable > signatureVariable) { - elseResult = refine(partitionNode, sylvan_low(signatureNode)); - thenResult = refine(partitionNode, sylvan_high(signatureNode)); - } else { - elseResult = refine(sylvan_low(partitionNode), sylvan_low(signatureNode)); - thenResult = refine(sylvan_high(partitionNode), sylvan_high(signatureNode)); - } - - BDD result; - if (thenResult == elseResult) { - result = thenResult; - } else { - // Get the node to connect the subresults. -// start = std::chrono::high_resolution_clock::now(); - result = sylvan_makenode(topVariable + 1, 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; - - return result; - } else { - - // If we are not within the state encoding any more, we hit the signature itself. - + // If there are no more non-block variables, we hit the signature. + if (sylvan_isconst(nonBlockVariablesNode)) { // If this is the first time (in this traversal) that we encounter this signature, we check // whether we can assign the old block number to it. -// start = std::chrono::high_resolution_clock::now(); + + // start = std::chrono::high_resolution_clock::now(); auto& reuseBlockEntry = reuseBlocksCache[partitionNode]; -// end = std::chrono::high_resolution_clock::now(); -// totalReuseBlocksLookupTime += end - start; + // 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(); + // start = std::chrono::high_resolution_clock::now(); *newEntryPtr = partitionNode; -// end = std::chrono::high_resolution_clock::now(); -// totalSignatureCacheStoreTime += end - start; + // end = std::chrono::high_resolution_clock::now(); + // totalSignatureCacheStoreTime += end - start; return partitionNode; } else { -// start = std::chrono::high_resolution_clock::now(); + // start = std::chrono::high_resolution_clock::now(); BDD result = encodeBlock(nextFreeBlockIndex++); -// end = std::chrono::high_resolution_clock::now(); -// totalBlockEncodingTime += end - start; + // end = std::chrono::high_resolution_clock::now(); + // totalBlockEncodingTime += end - start; -// start = std::chrono::high_resolution_clock::now(); + // start = std::chrono::high_resolution_clock::now(); *newEntryPtr = result; -// end = std::chrono::high_resolution_clock::now(); -// totalSignatureCacheStoreTime += end - start; + // end = std::chrono::high_resolution_clock::now(); + // totalSignatureCacheStoreTime += end - start; 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; + } + + 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; + } + + BDD thenResult = refine(partitionThen, signatureThen, offset == 0 ? sylvan_high(nondeterminismVariablesNode) : nondeterminismVariablesNode, sylvan_high(nonBlockVariablesNode)); + BDD elseResult = refine(partitionElse, signatureElse, offset == 0 ? sylvan_high(nondeterminismVariablesNode) : nondeterminismVariablesNode, sylvan_high(nonBlockVariablesNode)); + + BDD result; + if (thenResult == elseResult) { + 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; + + return result; } } storm::dd::DdManager const& manager; storm::dd::InternalDdManager const& internalDdManager; storm::expressions::Variable const& blockVariable; + + storm::dd::Bdd nondeterminismVariables; + storm::dd::Bdd nonBlockVariables; uint64_t numberOfBlockVariables; storm::dd::Bdd blockCube; - // The last level that belongs to the state encoding in the DDs. - uint64_t lastStateLevel; - // The current number of blocks of the new partition. uint64_t nextFreeBlockIndex; @@ -444,13 +453,21 @@ namespace storm { }; template - SignatureRefiner::SignatureRefiner(storm::dd::DdManager const& manager, storm::expressions::Variable const& blockVariable, std::set const& stateVariables) : manager(&manager), stateVariables(stateVariables) { - uint64_t lastStateLevel = 0; - for (auto const& stateVariable : stateVariables) { - lastStateLevel = std::max(lastStateLevel, manager.getMetaVariable(stateVariable).getHighestLevel()); + SignatureRefiner::SignatureRefiner(storm::dd::DdManager const& manager, storm::expressions::Variable const& blockVariable, std::set const& stateVariables, std::set const& nondeterminismVariables) : manager(&manager), stateVariables(stateVariables) { + + storm::dd::Bdd nonBlockVariablesCube = manager.getBddOne(); + storm::dd::Bdd nondeterminismVariablesCube = manager.getBddOne(); + for (auto const& var : nondeterminismVariables) { + auto cube = manager.getMetaVariable(var).getCube(); + nonBlockVariablesCube &= cube; + nondeterminismVariablesCube &= cube; + } + for (auto const& var : stateVariables) { + auto cube = manager.getMetaVariable(var).getCube(); + nonBlockVariablesCube &= cube; } - internalRefiner = std::make_unique>(manager, blockVariable, lastStateLevel); + internalRefiner = std::make_unique>(manager, blockVariable, nondeterminismVariablesCube, nonBlockVariablesCube); } template diff --git a/src/storm/storage/dd/bisimulation/SignatureRefiner.h b/src/storm/storage/dd/bisimulation/SignatureRefiner.h index ba6777d13..64797bdd8 100644 --- a/src/storm/storage/dd/bisimulation/SignatureRefiner.h +++ b/src/storm/storage/dd/bisimulation/SignatureRefiner.h @@ -18,7 +18,7 @@ namespace storm { class SignatureRefiner { public: SignatureRefiner() = default; - SignatureRefiner(storm::dd::DdManager const& manager, storm::expressions::Variable const& blockVariable, std::set const& stateVariables); + SignatureRefiner(storm::dd::DdManager const& manager, storm::expressions::Variable const& blockVariable, std::set const& stateVariables, std::set const& nondeterminismVariables = std::set()); ~SignatureRefiner();