From 66e08f9cd77a007113a2bc295fda4df9b96b35bf Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 2 Mar 2018 09:05:01 +0100 Subject: [PATCH] more time output in dd-based bisimulation --- .../storage/dd/BisimulationDecomposition.cpp | 2 +- .../NondeterministicModelPartitionRefiner.cpp | 3 ++- .../dd/bisimulation/PartitionRefiner.cpp | 19 ++++++++++++++++--- .../dd/bisimulation/PartitionRefiner.h | 3 +++ 4 files changed, 22 insertions(+), 5 deletions(-) diff --git a/src/storm/storage/dd/BisimulationDecomposition.cpp b/src/storm/storage/dd/BisimulationDecomposition.cpp index b19142b1d..682f5602d 100644 --- a/src/storm/storage/dd/BisimulationDecomposition.cpp +++ b/src/storm/storage/dd/BisimulationDecomposition.cpp @@ -93,7 +93,7 @@ namespace storm { } auto end = std::chrono::high_resolution_clock::now(); - STORM_LOG_INFO("Partition refinement completed in " << std::chrono::duration_cast(end - start).count() << "ms (" << iterations << " iterations)."); + STORM_LOG_INFO("Partition refinement completed in " << std::chrono::duration_cast(end - start).count() << "ms (" << iterations << " iterations, signature: " << std::chrono::duration_cast(refiner->getTotalSignatureTime()).count() << "ms, refinement: " << std::chrono::duration_cast(refiner->getTotalRefinementTime()).count() << "ms)."); } template diff --git a/src/storm/storage/dd/bisimulation/NondeterministicModelPartitionRefiner.cpp b/src/storm/storage/dd/bisimulation/NondeterministicModelPartitionRefiner.cpp index 1bf58a5ad..129c426c7 100644 --- a/src/storm/storage/dd/bisimulation/NondeterministicModelPartitionRefiner.cpp +++ b/src/storm/storage/dd/bisimulation/NondeterministicModelPartitionRefiner.cpp @@ -46,7 +46,8 @@ namespace storm { auto signatureStart = std::chrono::high_resolution_clock::now(); Signature stateSignature(choicePartitionAsBdd.existsAbstract(model.getNondeterminismVariables()).template toAdd()); auto signatureEnd = std::chrono::high_resolution_clock::now(); - + this->totalSignatureTime += (signatureEnd - signatureStart); + // If the choice partition changed, refine the state partition. STORM_LOG_TRACE("Refining state partition."); auto refinementStart = std::chrono::high_resolution_clock::now(); diff --git a/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp b/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp index 94a6d3666..87af0987b 100644 --- a/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp +++ b/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp @@ -12,7 +12,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(), model.getColumnVariables(), !model.isNondeterministicModel(), model.getNondeterminismVariables()) { + 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.getColumnVariables(), !model.isNondeterministicModel(), model.getNondeterminismVariables()), totalSignatureTime(0), totalRefinementTime(0) { // Intentionally left empty. } @@ -50,7 +50,7 @@ namespace storm { auto signatureEnd = std::chrono::high_resolution_clock::now(); totalSignatureTime += (signatureEnd - signatureStart); STORM_LOG_TRACE("Signature " << refinements << "[" << index << "] DD has " << signature.getSignatureAdd().getNodeCount() << " nodes."); - + auto refinementStart = std::chrono::high_resolution_clock::now(); newPartition = signatureRefiner.refine(oldPartition, signature); auto refinementEnd = std::chrono::high_resolution_clock::now(); @@ -78,8 +78,11 @@ namespace storm { Partition PartitionRefiner::internalRefine(Signature const& signature, SignatureRefiner& signatureRefiner, Partition const& oldPartition) { STORM_LOG_TRACE("Signature " << refinements << " DD has " << signature.getSignatureAdd().getNodeCount() << " nodes."); + auto refinementStart = std::chrono::high_resolution_clock::now(); auto newPartition = signatureRefiner.refine(oldPartition, signature); - + auto refinementEnd = std::chrono::high_resolution_clock::now(); + totalRefinementTime += (refinementEnd - refinementStart); + ++refinements; return newPartition; } @@ -132,6 +135,16 @@ namespace storm { return status; } + template + std::chrono::high_resolution_clock::duration PartitionRefiner::getTotalSignatureTime() const { + return totalSignatureTime; + } + + template + std::chrono::high_resolution_clock::duration PartitionRefiner::getTotalRefinementTime() const { + return totalRefinementTime; + } + template class PartitionRefiner; template class PartitionRefiner; diff --git a/src/storm/storage/dd/bisimulation/PartitionRefiner.h b/src/storm/storage/dd/bisimulation/PartitionRefiner.h index d4e59a207..4716a811a 100644 --- a/src/storm/storage/dd/bisimulation/PartitionRefiner.h +++ b/src/storm/storage/dd/bisimulation/PartitionRefiner.h @@ -53,6 +53,9 @@ namespace storm { */ Status getStatus() const; + std::chrono::high_resolution_clock::duration getTotalSignatureTime() const; + std::chrono::high_resolution_clock::duration getTotalRefinementTime() const; + protected: Partition internalRefine(SignatureComputer& stateSignatureComputer, SignatureRefiner& signatureRefiner, Partition const& oldPartition, Partition const& targetPartition, SignatureMode const& mode = SignatureMode::Eager); Partition internalRefine(Signature const& signature, SignatureRefiner& signatureRefiner, Partition const& oldPartition);