From 05f2f241cb69b9d4956dcbdcad2ccec7aa603ef3 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 9 Nov 2017 20:34:05 +0100 Subject: [PATCH] fixed some recently introduced issues --- .../storage/dd/BisimulationDecomposition.cpp | 4 +-- .../dd/bisimulation/SignatureRefiner.cpp | 29 ++++++++++--------- src/storm/utility/sylvan.cpp | 15 ++++++++++ src/storm/utility/sylvan.h | 8 ++--- 4 files changed, 35 insertions(+), 21 deletions(-) create mode 100644 src/storm/utility/sylvan.cpp diff --git a/src/storm/storage/dd/BisimulationDecomposition.cpp b/src/storm/storage/dd/BisimulationDecomposition.cpp index 8106243b7..6d649aede 100644 --- a/src/storm/storage/dd/BisimulationDecomposition.cpp +++ b/src/storm/storage/dd/BisimulationDecomposition.cpp @@ -94,7 +94,7 @@ namespace storm { } auto end = std::chrono::high_resolution_clock::now(); - STORM_LOG_DEBUG("Partition refinement completed in " << std::chrono::duration_cast(end - start).count() << "s (" << iterations << " iterations)."); + STORM_LOG_DEBUG("Partition refinement completed in " << std::chrono::duration_cast(end - start).count() << "ms (" << iterations << " iterations)."); } template @@ -117,7 +117,7 @@ namespace storm { auto durationSinceLastMessage = std::chrono::duration_cast(now - timeOfLastMessage).count(); if (static_cast(durationSinceLastMessage) >= showProgressDelay) { auto durationSinceStart = std::chrono::duration_cast(now - start).count(); - STORM_LOG_INFO("State partition after " << iterations << " iterations (" << durationSinceStart << "s) has " << refiner->getStatePartition().getNumberOfBlocks() << " blocks."); + STORM_LOG_INFO("State partition after " << iterations << " iterations (" << durationSinceStart << "ms) has " << refiner->getStatePartition().getNumberOfBlocks() << " blocks."); timeOfLastMessage = std::chrono::high_resolution_clock::now(); } } diff --git a/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp b/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp index dfc24ec0f..3083ea75d 100644 --- a/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp +++ b/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp @@ -466,7 +466,7 @@ namespace storm { spp::sparse_hash_map reuseBlocksCache; }; - TASK_DECL_5(BDD, refine_double, BDD, MTBDD, BDD, BDD, void*); + TASK_DECL_5(BDD, refine_parallel, BDD, MTBDD, BDD, BDD, void*); template class InternalSignatureRefinerBase; @@ -709,7 +709,7 @@ namespace storm { std::pair refineParallel(BDD partitionNode, MTBDD signatureNode, BDD nondeterminismVariablesNode, BDD nonBlockVariablesNode) { LACE_ME; - return std::make_pair(CALL(refine_double, partitionNode, signatureNode, nondeterminismVariablesNode, nonBlockVariablesNode, this), 0); + return std::make_pair(CALL(refine_parallel, partitionNode, signatureNode, nondeterminismVariablesNode, nonBlockVariablesNode, this), 0); } std::pair refineSequential(BDD partitionNode, MTBDD signatureNode, BDD nondeterminismVariablesNode, BDD nonBlockVariablesNode) { @@ -868,7 +868,7 @@ namespace storm { }; - TASK_IMPL_5(BDD, refine_double, BDD, partitionNode, MTBDD, signatureNode, BDD, nondeterminismVariablesNode, BDD, nonBlockVariablesNode, void*, refinerPtr) + TASK_IMPL_5(BDD, refine_parallel, BDD, partitionNode, MTBDD, signatureNode, BDD, nondeterminismVariablesNode, BDD, nonBlockVariablesNode, void*, refinerPtr) { auto& refiner = *static_cast*>(refinerPtr); std::unique_lock lock(refiner.mutex, std::defer_lock); @@ -881,8 +881,12 @@ namespace storm { STORM_LOG_ASSERT(partitionNode != mtbdd_false, "Expected non-false node."); + // Check the cache whether we have seen the same node before. BDD result; - + if (cache_get(signatureNode|(256LL<<42), nonBlockVariablesNode, partitionNode|(refiner.numberOfRefinements<<40), &result)) { + return result; + } + if (sylvan_isconst(nonBlockVariablesNode)) { // Get the lock so we can modify the signature cache. lock.lock(); @@ -911,11 +915,10 @@ namespace storm { result = refiner.encodeBlock(refiner.nextFreeBlockIndex++); refiner.signatureCacheSingle[nodePair] = result; lock.unlock(); - return result; - } - - // Check the cache whether we have seen the same node before. - if (cache_get(signatureNode|(256LL<<42), nonBlockVariablesNode, partitionNode|(refiner.numberOfRefinements<<40), &result)) { + + // Store the result in the cache. + cache_put(signatureNode|(256LL<<42), nonBlockVariablesNode, partitionNode|(refiner.numberOfRefinements<<40), result); + return result; } @@ -966,15 +969,15 @@ namespace storm { // If there are no more non-block variables remaining, make a recursive call to enter the base case. if (sylvan_isconst(nonBlockVariablesNode)) { - return CALL(refine_double, partitionNode, signatureNode, nondeterminismVariablesNode, nonBlockVariablesNode, refinerPtr); + return CALL(refine_parallel, partitionNode, signatureNode, nondeterminismVariablesNode, nonBlockVariablesNode, refinerPtr); } BDD nextNondeterminismVariables = isNondeterminismVariable ? sylvan_set_next(nondeterminismVariablesNode) : nondeterminismVariablesNode; BDD nextNonBlockVariables = sylvan_set_next(nonBlockVariablesNode); - bdd_refs_spawn(SPAWN(refine_double, partitionThen, signatureThen, nextNondeterminismVariables, nextNonBlockVariables, refinerPtr)); + bdd_refs_spawn(SPAWN(refine_parallel, partitionElse, signatureElse, nextNondeterminismVariables, nextNonBlockVariables, refinerPtr)); - BDD elseResult = bdd_refs_push(CALL(refine_double, partitionElse, signatureElse, nextNondeterminismVariables, nextNonBlockVariables, refinerPtr)); - BDD thenResult = bdd_refs_sync(SYNC(refine_double)); + BDD thenResult = bdd_refs_push(CALL(refine_parallel, partitionThen, signatureThen, nextNondeterminismVariables, nextNonBlockVariables, refinerPtr)); + BDD elseResult = bdd_refs_sync(SYNC(refine_parallel)); bdd_refs_pop(1); if (thenResult == elseResult) { diff --git a/src/storm/utility/sylvan.cpp b/src/storm/utility/sylvan.cpp new file mode 100644 index 000000000..769b125d2 --- /dev/null +++ b/src/storm/utility/sylvan.cpp @@ -0,0 +1,15 @@ +#include "storm/utility/sylvan.h" + +namespace storm { + namespace dd { + + bool sylvan_bdd_matches_variable_index(BDD node, uint64_t variableIndex, int64_t offset) { + return !sylvan_isconst(node) && static_cast(sylvan_var(node) + offset) == variableIndex; + } + + bool sylvan_mtbdd_matches_variable_index(MTBDD node, uint64_t variableIndex, int64_t offset) { + return !mtbdd_isleaf(node) && static_cast(sylvan_var(node) + offset) == variableIndex; + } + + } +} diff --git a/src/storm/utility/sylvan.h b/src/storm/utility/sylvan.h index f7495bedb..9d582e6b2 100644 --- a/src/storm/utility/sylvan.h +++ b/src/storm/utility/sylvan.h @@ -28,9 +28,7 @@ namespace storm { * @param offset An offset that is applied to the index of the top variable in the BDD. * @return True iff the BDD's top variable has the given index. */ - bool sylvan_bdd_matches_variable_index(BDD node, uint64_t variableIndex, int64_t offset = 0) { - return !sylvan_isconst(node) && static_cast(sylvan_var(node) + offset) == variableIndex; - } + bool sylvan_bdd_matches_variable_index(BDD node, uint64_t variableIndex, int64_t offset = 0); /*! * Retrieves whether the topmost variable in the MTBDD is the one with the given index. @@ -40,9 +38,7 @@ namespace storm { * @param offset An offset that is applied to the index of the top variable in the BDD. * @return True iff the BDD's top variable has the given index. */ - bool sylvan_mtbdd_matches_variable_index(MTBDD node, uint64_t variableIndex, int64_t offset = 0) { - return !mtbdd_isleaf(node) && static_cast(sylvan_var(node) + offset) == variableIndex; - } + bool sylvan_mtbdd_matches_variable_index(MTBDD node, uint64_t variableIndex, int64_t offset = 0); } }