From 90a7ea4907578192c0c88842a2b248c508c5f557 Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 5 Sep 2017 10:36:54 +0200 Subject: [PATCH] printing timing information --- ...dpRewardBoundedPcaaWeightVectorChecker.cpp | 15 +++++++++---- ...eMdpRewardBoundedPcaaWeightVectorChecker.h | 15 ++++++++++++- .../MultiDimensionalRewardUnfolding.cpp | 19 ++++++++++------- .../MultiDimensionalRewardUnfolding.h | 21 +++++++++++++++++-- 4 files changed, 56 insertions(+), 14 deletions(-) diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp index eb7ce0bd8..33c2301fa 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp @@ -16,17 +16,15 @@ #include "storm/exceptions/NotSupportedException.h" #include "storm/exceptions/UnexpectedException.h" - namespace storm { namespace modelchecker { namespace multiobjective { template - SparseMdpRewardBoundedPcaaWeightVectorChecker::SparseMdpRewardBoundedPcaaWeightVectorChecker(SparseMultiObjectivePreprocessorResult const& preprocessorResult) : PcaaWeightVectorChecker(preprocessorResult.objectives), rewardUnfolding(*preprocessorResult.preprocessedModel, this->objectives, storm::storage::BitVector(preprocessorResult.preprocessedModel->getNumberOfChoices(), true), preprocessorResult.reward0EStates) { + SparseMdpRewardBoundedPcaaWeightVectorChecker::SparseMdpRewardBoundedPcaaWeightVectorChecker(SparseMultiObjectivePreprocessorResult const& preprocessorResult) : PcaaWeightVectorChecker(preprocessorResult.objectives), swAll(true), rewardUnfolding(*preprocessorResult.preprocessedModel, this->objectives, storm::storage::BitVector(preprocessorResult.preprocessedModel->getNumberOfChoices(), true), preprocessorResult.reward0EStates) { STORM_LOG_THROW(preprocessorResult.rewardFinitenessType == SparseMultiObjectivePreprocessorResult::RewardFinitenessType::AllFinite, storm::exceptions::NotSupportedException, "There is a scheduler that yields infinite reward for one objective. This is not supported."); STORM_LOG_THROW(preprocessorResult.preprocessedModel->getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::NotSupportedException, "The model has multiple initial states."); - } template @@ -47,6 +45,7 @@ namespace storm { template void SparseMdpRewardBoundedPcaaWeightVectorChecker::computeEpochSolution(typename MultiDimensionalRewardUnfolding::Epoch const& epoch, std::vector const& weightVector) { auto const& epochModel = rewardUnfolding.setCurrentEpoch(epoch); + swEqBuilding.start(); std::vector::SolutionType> result(epochModel.epochMatrix.getRowGroupCount()); @@ -74,7 +73,11 @@ namespace storm { minMaxSolver->setTrackScheduler(true); //minMaxSolver->setCachingEnabled(true); std::vector x(result.size(), storm::utility::zero()); + swEqBuilding.stop(); + swMinMaxSolving.start(); minMaxSolver->solveEquations(x, b); + swMinMaxSolving.stop(); + swEqBuilding.start(); for (uint64_t state = 0; state < x.size(); ++state) { result[state].weightedValue = x[state]; } @@ -101,12 +104,16 @@ namespace storm { b[state] += epochModel.stepSolutions[epochModel.stepChoices.getNumberOfSetBitsBeforeIndex(choice)].objectiveValues[objIndex]; } } + swEqBuilding.stop(); + swLinEqSolving.start(); linEqSolver->solveEquations(x, b); + swLinEqSolving.stop(); + swEqBuilding.start(); for (uint64_t state = 0; state < choices.size(); ++state) { result[state].objectiveValues.push_back(x[state]); } } - + swEqBuilding.stop(); rewardUnfolding.setSolutionForCurrentEpoch(result); } diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.h index 55eaa0067..db507cc68 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.h +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.h @@ -5,6 +5,8 @@ #include "storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.h" #include "storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h" +#include "storm/utility/Stopwatch.h" + namespace storm { namespace modelchecker { namespace multiobjective { @@ -23,7 +25,17 @@ namespace storm { SparseMdpRewardBoundedPcaaWeightVectorChecker(SparseMultiObjectivePreprocessorResult const& preprocessorResult); - virtual ~SparseMdpRewardBoundedPcaaWeightVectorChecker() = default; + virtual ~SparseMdpRewardBoundedPcaaWeightVectorChecker() { + swAll.stop(); + std::cout << "WVC statistics: " << std::endl; + std::cout << " overall: " << swAll << " seconds." << std::endl; + std::cout << "---------------------------------------------" << std::endl; + std::cout << " eqSysBuilding: " << swEqBuilding << " seconds." << std::endl; + std::cout << " MinMaxSolving: " << swMinMaxSolving << " seconds." << std::endl; + std::cout << " LinEqSolving: " << swLinEqSolving << " seconds." << std::endl; + + } + /*! * - computes the optimal expected reward w.r.t. the weighted sum of the rewards of the individual objectives @@ -45,6 +57,7 @@ namespace storm { void computeEpochSolution(typename MultiDimensionalRewardUnfolding::Epoch const& epoch, std::vector const& weightVector); + storm::utility::Stopwatch swAll, swEqBuilding, swLinEqSolving, swMinMaxSolving; MultiDimensionalRewardUnfolding rewardUnfolding; diff --git a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp index e01900157..effb240bf 100644 --- a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp +++ b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp @@ -27,12 +27,12 @@ namespace storm { template void MultiDimensionalRewardUnfolding::initialize() { - + swInit.start(); std::vector> epochSteps; initializeObjectives(epochSteps); initializePossibleEpochSteps(epochSteps); initializeMemoryProduct(epochSteps); - + swInit.stop(); } template @@ -214,12 +214,12 @@ namespace storm { template typename MultiDimensionalRewardUnfolding::EpochModel const& MultiDimensionalRewardUnfolding::setCurrentEpoch(Epoch const& epoch) { - // Check if we need to update the current epoch class if (!currentEpoch || getClassOfEpoch(epoch) != getClassOfEpoch(currentEpoch.get())) { setCurrentEpochClass(epoch); } + swSetEpoch.start(); // Find out which objective rewards are earned in this particular epoch epochModel.objectiveRewardFilter = std::vector(objectives.size(), storm::storage::BitVector(epochModel.objectiveRewards.front().size(), true)); for (auto const& reducedChoice : epochModel.stepChoices) { @@ -268,7 +268,7 @@ namespace storm { assert(epochModel.stepChoices.getNumberOfSetBits() == epochModel.stepSolutions.size()); currentEpoch = epoch; - + swSetEpoch.stop(); /* std::cout << "Epoch model for epoch " << storm::utility::vector::toString(epoch) << std::endl; std::cout << "Matrix: " << std::endl << epochModel.epochMatrix << std::endl; @@ -286,6 +286,7 @@ namespace storm { template void MultiDimensionalRewardUnfolding::setCurrentEpochClass(Epoch const& epoch) { + swSetEpochClass.start(); auto productObjectiveRewards = computeObjectiveRewardsForProduct(epoch); storm::storage::BitVector stepChoices(memoryProduct.getProduct().getNumberOfChoices(), false); @@ -334,7 +335,7 @@ namespace storm { } epochModel.objectiveRewards.push_back(std::move(reducedModelObjRewards)); } - + swSetEpochClass.stop(); } template @@ -353,12 +354,14 @@ namespace storm { template void MultiDimensionalRewardUnfolding::setSolutionForCurrentEpoch(std::vector const& reducedModelStateSolutions) { + swInsertSol.start(); for (uint64_t productState = 0; productState < memoryProduct.getProduct().getNumberOfStates(); ++productState) { uint64_t reducedModelState = ecElimResult.oldToNewStateMapping[productState]; if (reducedModelState < reducedModelStateSolutions.size()) { setSolutionForCurrentEpoch(productState, reducedModelStateSolutions[reducedModelState]); } } + swInsertSol.stop(); } template @@ -370,16 +373,18 @@ namespace storm { } template - typename MultiDimensionalRewardUnfolding::SolutionType const& MultiDimensionalRewardUnfolding::getStateSolution(Epoch const& epoch, uint64_t const& productState) const { + typename MultiDimensionalRewardUnfolding::SolutionType const& MultiDimensionalRewardUnfolding::getStateSolution(Epoch const& epoch, uint64_t const& productState) { + swFindSol.start(); std::vector solutionKey = epoch; solutionKey.push_back(productState); auto solutionIt = solutions.find(solutionKey); STORM_LOG_ASSERT(solutionIt != solutions.end(), "Requested unexisting solution for epoch " << storm::utility::vector::toString(epoch) << "."); + swFindSol.stop(); return solutionIt->second; } template - typename MultiDimensionalRewardUnfolding::SolutionType const& MultiDimensionalRewardUnfolding::getInitialStateResult(Epoch const& epoch) const { + typename MultiDimensionalRewardUnfolding::SolutionType const& MultiDimensionalRewardUnfolding::getInitialStateResult(Epoch const& epoch) { return getStateSolution(epoch, *memoryProduct.getProduct().getInitialStates().begin()); } diff --git a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h index ee4be4279..e66dff69d 100644 --- a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h +++ b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h @@ -11,6 +11,7 @@ #include "storm/storage/memorystructure/SparseModelMemoryProduct.h" #include "storm/transformer/EndComponentEliminator.h" +#include "storm/utility/Stopwatch.h" namespace storm { namespace modelchecker { @@ -51,6 +52,18 @@ namespace storm { storm::storage::BitVector const& possibleECActions, storm::storage::BitVector const& allowedBottomStates); + ~MultiDimensionalRewardUnfolding() { + std::cout << "Unfolding statistics: " << std::endl; + std::cout << " init: " << swInit << " seconds." << std::endl; + std::cout << " setEpoch: " << swSetEpoch << " seconds." << std::endl; + std::cout << " setEpochClass: " << swSetEpochClass << " seconds." << std::endl; + std::cout << " findSolutions: " << swFindSol << " seconds." << std::endl; + std::cout << " insertSolutions: " << swInsertSol << " seconds." << std::endl; + std::cout << "---------------------------------------------" << std::endl; + std::cout << "---------------------------------------------" << std::endl; + std::cout << std::endl; + + } Epoch getStartEpoch(); std::vector getEpochComputationOrder(Epoch const& startEpoch); @@ -58,7 +71,7 @@ namespace storm { EpochModel const& setCurrentEpoch(Epoch const& epoch); void setSolutionForCurrentEpoch(std::vector const& reducedModelStateSolutions); - SolutionType const& getInitialStateResult(Epoch const& epoch) const; + SolutionType const& getInitialStateResult(Epoch const& epoch); private: @@ -99,6 +112,7 @@ namespace storm { void initializeObjectives(std::vector>& epochSteps); void initializePossibleEpochSteps(std::vector> const& epochSteps); + void initializeMemoryProduct(std::vector> const& epochSteps); storm::storage::MemoryStructure computeMemoryStructure() const; std::vector> computeObjectiveRewardsForProduct(Epoch const& epoch) const; @@ -111,7 +125,7 @@ namespace storm { void addScaledSolution(SolutionType& solution, SolutionType const& solutionToAdd, ValueType const& scalingFactor) const; void setSolutionForCurrentEpoch(uint64_t const& productState, SolutionType const& solution); - SolutionType const& getStateSolution(Epoch const& epoch, uint64_t const& productState) const; + SolutionType const& getStateSolution(Epoch const& epoch, uint64_t const& productState); storm::models::sparse::Mdp const& model; std::vector> const& objectives; @@ -133,6 +147,9 @@ namespace storm { std::vector scalingFactors; std::map, SolutionType> solutions; + + + storm::utility::Stopwatch swInit, swFindSol, swInsertSol, swSetEpoch, swSetEpochClass; }; } }