diff --git a/src/storage/DeterministicModelBisimulationDecomposition.cpp b/src/storage/DeterministicModelBisimulationDecomposition.cpp index 55060ead1..cb69ec209 100644 --- a/src/storage/DeterministicModelBisimulationDecomposition.cpp +++ b/src/storage/DeterministicModelBisimulationDecomposition.cpp @@ -746,7 +746,7 @@ namespace storm { static int callsToRefinePartition = 0; static int statesIteratedOverInRefinePartition = 0; - static std::vector refinementOrder; + static std::chrono::high_resolution_clock::duration refineBlockTime(0); template template @@ -758,6 +758,9 @@ namespace storm { std::deque splitterQueue; std::for_each(partition.getBlocks().begin(), partition.getBlocks().end(), [&] (Block& a) { splitterQueue.push_back(&a); a.markAsSplitter(); }); + std::chrono::high_resolution_clock::time_point refinePartitionStart; + std::chrono::high_resolution_clock::duration refinePartitionTime(0); + // Then perform the actual splitting until there are no more splitters. while (!splitterQueue.empty()) { // Optionally: sort the splitter queue according to some criterion (here: prefer small splitters). @@ -769,7 +772,9 @@ namespace storm { splitter->unmarkAsSplitter(); // Now refine the partition using the current splitter. + std::chrono::high_resolution_clock::time_point refinePartitionStart = std::chrono::high_resolution_clock::now(); refinePartition(model.getTransitionMatrix(), backwardTransitions, *splitter, partition, bisimulationType, splitterQueue); + refinePartitionTime += std::chrono::high_resolution_clock::now() - refinePartitionStart; } std::chrono::high_resolution_clock::duration refinementTime = std::chrono::high_resolution_clock::now() - refinementStart; @@ -796,11 +801,15 @@ namespace storm { if (storm::settings::generalSettings().isShowStatisticsSet()) { std::chrono::milliseconds refinementTimeInMilliseconds = std::chrono::duration_cast(refinementTime); + std::chrono::milliseconds refinePartitionTimeInMilliseconds = std::chrono::duration_cast(refinePartitionTime); + std::chrono::milliseconds refineBlockTimeInMilliseconds = std::chrono::duration_cast(refineBlockTime); std::chrono::milliseconds extractionTimeInMilliseconds = std::chrono::duration_cast(extractionTime); std::chrono::milliseconds totalTimeInMilliseconds = std::chrono::duration_cast(totalTime); std::cout << std::endl; std::cout << "Time breakdown:" << std::endl; std::cout << " * time for partitioning: " << refinementTimeInMilliseconds.count() << "ms" << std::endl; + std::cout << " * time spent in refining partition: " << refinePartitionTimeInMilliseconds.count() << "ms" << std::endl; + std::cout << " * time spent in refining block based on probabilities: " << refineBlockTimeInMilliseconds.count() << "ms" << std::endl; std::cout << " * time for extraction: " << extractionTimeInMilliseconds.count() << "ms" << std::endl; std::cout << "------------------------------------------" << std::endl; std::cout << " * total time: " << totalTimeInMilliseconds.count() << "ms" << std::endl; @@ -808,16 +817,13 @@ namespace storm { std::cout << "Other:" << std::endl; std::cout << " * calls to refine partition: " << callsToRefinePartition << std::endl; std::cout << " * states iterated over: " << statesIteratedOverInRefinePartition << std::endl; - std::cout << " * order: "; - for (auto const& element : refinementOrder) { - std::cout << element << ", "; - } std::cout << std::endl; } } template void DeterministicModelBisimulationDecomposition::refineBlockProbabilities(Block& block, Partition& partition, BisimulationType bisimulationType, std::deque& splitterQueue) { + std::chrono::high_resolution_clock::time_point refinePartitionStart = std::chrono::high_resolution_clock::now(); // Sort the states in the block based on their probabilities. std::sort(partition.getBegin(block), partition.getEnd(block), [&partition] (std::pair const& a, std::pair const& b) { return a.second < b.second; } ); @@ -864,6 +870,8 @@ namespace storm { block.markAsSplitter(); } } + + refineBlockTime += std::chrono::high_resolution_clock::now() - refinePartitionStart; } template @@ -1041,7 +1049,6 @@ namespace storm { template void DeterministicModelBisimulationDecomposition::refinePartition(storm::storage::SparseMatrix const& forwardTransitions, storm::storage::SparseMatrix const& backwardTransitions, Block& splitter, Partition& partition, BisimulationType bisimulationType, std::deque& splitterQueue) { ++callsToRefinePartition; - refinementOrder.push_back(splitter.getId()); std::list predecessorBlocks; // Iterate over all states of the splitter and check its predecessors.