sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

printing timing information

tempestpy_adaptions
TimQu 7 years ago
parent
61a6b178b7
commit
90a7ea4907
4 changed files with 56 additions and 14 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 15
      src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp
  2. 15
      src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.h
  3. 19
      src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp
  4. 21
      src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h

15
src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp
View File

@ -16,17 +16,15 @@
#include "storm/exceptions/NotSupportedException.h" #include "storm/exceptions/NotSupportedException.h"
#include "storm/exceptions/UnexpectedException.h" #include "storm/exceptions/UnexpectedException.h"
namespace storm { namespace storm {
namespace modelchecker { namespace modelchecker {
namespace multiobjective { namespace multiobjective {
template <class SparseMdpModelType> template <class SparseMdpModelType>
SparseMdpRewardBoundedPcaaWeightVectorChecker<SparseMdpModelType>::SparseMdpRewardBoundedPcaaWeightVectorChecker(SparseMultiObjectivePreprocessorResult<SparseMdpModelType> const& preprocessorResult) : PcaaWeightVectorChecker<SparseMdpModelType>(preprocessorResult.objectives), rewardUnfolding(*preprocessorResult.preprocessedModel, this->objectives, storm::storage::BitVector(preprocessorResult.preprocessedModel->getNumberOfChoices(), true), preprocessorResult.reward0EStates) {
SparseMdpRewardBoundedPcaaWeightVectorChecker<SparseMdpModelType>::SparseMdpRewardBoundedPcaaWeightVectorChecker(SparseMultiObjectivePreprocessorResult<SparseMdpModelType> const& preprocessorResult) : PcaaWeightVectorChecker<SparseMdpModelType>(preprocessorResult.objectives), swAll(true), rewardUnfolding(*preprocessorResult.preprocessedModel, this->objectives, storm::storage::BitVector(preprocessorResult.preprocessedModel->getNumberOfChoices(), true), preprocessorResult.reward0EStates) {
STORM_LOG_THROW(preprocessorResult.rewardFinitenessType == SparseMultiObjectivePreprocessorResult<SparseMdpModelType>::RewardFinitenessType::AllFinite, storm::exceptions::NotSupportedException, "There is a scheduler that yields infinite reward for one objective. This is not supported."); STORM_LOG_THROW(preprocessorResult.rewardFinitenessType == SparseMultiObjectivePreprocessorResult<SparseMdpModelType>::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."); STORM_LOG_THROW(preprocessorResult.preprocessedModel->getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::NotSupportedException, "The model has multiple initial states.");
} }
template <class SparseMdpModelType> template <class SparseMdpModelType>
@ -47,6 +45,7 @@ namespace storm {
template <class SparseMdpModelType> template <class SparseMdpModelType>
void SparseMdpRewardBoundedPcaaWeightVectorChecker<SparseMdpModelType>::computeEpochSolution(typename MultiDimensionalRewardUnfolding<ValueType>::Epoch const& epoch, std::vector<ValueType> const& weightVector) { void SparseMdpRewardBoundedPcaaWeightVectorChecker<SparseMdpModelType>::computeEpochSolution(typename MultiDimensionalRewardUnfolding<ValueType>::Epoch const& epoch, std::vector<ValueType> const& weightVector) {
auto const& epochModel = rewardUnfolding.setCurrentEpoch(epoch); auto const& epochModel = rewardUnfolding.setCurrentEpoch(epoch);
swEqBuilding.start();
std::vector<typename MultiDimensionalRewardUnfolding<ValueType>::SolutionType> result(epochModel.epochMatrix.getRowGroupCount()); std::vector<typename MultiDimensionalRewardUnfolding<ValueType>::SolutionType> result(epochModel.epochMatrix.getRowGroupCount());
@ -74,7 +73,11 @@ namespace storm {
minMaxSolver->setTrackScheduler(true); minMaxSolver->setTrackScheduler(true);
//minMaxSolver->setCachingEnabled(true); //minMaxSolver->setCachingEnabled(true);
std::vector<ValueType> x(result.size(), storm::utility::zero<ValueType>()); std::vector<ValueType> x(result.size(), storm::utility::zero<ValueType>());
swEqBuilding.stop();
swMinMaxSolving.start();
minMaxSolver->solveEquations(x, b); minMaxSolver->solveEquations(x, b);
swMinMaxSolving.stop();
swEqBuilding.start();
for (uint64_t state = 0; state < x.size(); ++state) { for (uint64_t state = 0; state < x.size(); ++state) {
result[state].weightedValue = x[state]; result[state].weightedValue = x[state];
} }
@ -101,12 +104,16 @@ namespace storm {
b[state] += epochModel.stepSolutions[epochModel.stepChoices.getNumberOfSetBitsBeforeIndex(choice)].objectiveValues[objIndex]; b[state] += epochModel.stepSolutions[epochModel.stepChoices.getNumberOfSetBitsBeforeIndex(choice)].objectiveValues[objIndex];
} }
} }
swEqBuilding.stop();
swLinEqSolving.start();
linEqSolver->solveEquations(x, b); linEqSolver->solveEquations(x, b);
swLinEqSolving.stop();
swEqBuilding.start();
for (uint64_t state = 0; state < choices.size(); ++state) { for (uint64_t state = 0; state < choices.size(); ++state) {
result[state].objectiveValues.push_back(x[state]); result[state].objectiveValues.push_back(x[state]);
} }
} }
swEqBuilding.stop();
rewardUnfolding.setSolutionForCurrentEpoch(result); rewardUnfolding.setSolutionForCurrentEpoch(result);
} }

15
src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.h
View File

@ -5,6 +5,8 @@
#include "storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.h" #include "storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.h"
#include "storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h" #include "storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h"
#include "storm/utility/Stopwatch.h"
namespace storm { namespace storm {
namespace modelchecker { namespace modelchecker {
namespace multiobjective { namespace multiobjective {
@ -23,7 +25,17 @@ namespace storm {
SparseMdpRewardBoundedPcaaWeightVectorChecker(SparseMultiObjectivePreprocessorResult<SparseMdpModelType> const& preprocessorResult); SparseMdpRewardBoundedPcaaWeightVectorChecker(SparseMultiObjectivePreprocessorResult<SparseMdpModelType> 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 * - 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<ValueType>::Epoch const& epoch, std::vector<ValueType> const& weightVector); void computeEpochSolution(typename MultiDimensionalRewardUnfolding<ValueType>::Epoch const& epoch, std::vector<ValueType> const& weightVector);
storm::utility::Stopwatch swAll, swEqBuilding, swLinEqSolving, swMinMaxSolving;
MultiDimensionalRewardUnfolding<ValueType> rewardUnfolding; MultiDimensionalRewardUnfolding<ValueType> rewardUnfolding;

19
src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp
View File

@ -27,12 +27,12 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
void MultiDimensionalRewardUnfolding<ValueType>::initialize() { void MultiDimensionalRewardUnfolding<ValueType>::initialize() {
swInit.start();
std::vector<std::vector<uint64_t>> epochSteps; std::vector<std::vector<uint64_t>> epochSteps;
initializeObjectives(epochSteps); initializeObjectives(epochSteps);
initializePossibleEpochSteps(epochSteps); initializePossibleEpochSteps(epochSteps);
initializeMemoryProduct(epochSteps); initializeMemoryProduct(epochSteps);
swInit.stop();
} }
template<typename ValueType> template<typename ValueType>
@ -214,12 +214,12 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
typename MultiDimensionalRewardUnfolding<ValueType>::EpochModel const& MultiDimensionalRewardUnfolding<ValueType>::setCurrentEpoch(Epoch const& epoch) { typename MultiDimensionalRewardUnfolding<ValueType>::EpochModel const& MultiDimensionalRewardUnfolding<ValueType>::setCurrentEpoch(Epoch const& epoch) {
// Check if we need to update the current epoch class // Check if we need to update the current epoch class
if (!currentEpoch || getClassOfEpoch(epoch) != getClassOfEpoch(currentEpoch.get())) { if (!currentEpoch || getClassOfEpoch(epoch) != getClassOfEpoch(currentEpoch.get())) {
setCurrentEpochClass(epoch); setCurrentEpochClass(epoch);
} }
swSetEpoch.start();
// Find out which objective rewards are earned in this particular epoch // Find out which objective rewards are earned in this particular epoch
epochModel.objectiveRewardFilter = std::vector<storm::storage::BitVector>(objectives.size(), storm::storage::BitVector(epochModel.objectiveRewards.front().size(), true)); epochModel.objectiveRewardFilter = std::vector<storm::storage::BitVector>(objectives.size(), storm::storage::BitVector(epochModel.objectiveRewards.front().size(), true));
for (auto const& reducedChoice : epochModel.stepChoices) { for (auto const& reducedChoice : epochModel.stepChoices) {
@ -268,7 +268,7 @@ namespace storm {
assert(epochModel.stepChoices.getNumberOfSetBits() == epochModel.stepSolutions.size()); assert(epochModel.stepChoices.getNumberOfSetBits() == epochModel.stepSolutions.size());
currentEpoch = epoch; currentEpoch = epoch;
swSetEpoch.stop();
/* /*
std::cout << "Epoch model for epoch " << storm::utility::vector::toString(epoch) << std::endl; std::cout << "Epoch model for epoch " << storm::utility::vector::toString(epoch) << std::endl;
std::cout << "Matrix: " << std::endl << epochModel.epochMatrix << std::endl; std::cout << "Matrix: " << std::endl << epochModel.epochMatrix << std::endl;
@ -286,6 +286,7 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
void MultiDimensionalRewardUnfolding<ValueType>::setCurrentEpochClass(Epoch const& epoch) { void MultiDimensionalRewardUnfolding<ValueType>::setCurrentEpochClass(Epoch const& epoch) {
swSetEpochClass.start();
auto productObjectiveRewards = computeObjectiveRewardsForProduct(epoch); auto productObjectiveRewards = computeObjectiveRewardsForProduct(epoch);
storm::storage::BitVector stepChoices(memoryProduct.getProduct().getNumberOfChoices(), false); storm::storage::BitVector stepChoices(memoryProduct.getProduct().getNumberOfChoices(), false);
@ -334,7 +335,7 @@ namespace storm {
} }
epochModel.objectiveRewards.push_back(std::move(reducedModelObjRewards)); epochModel.objectiveRewards.push_back(std::move(reducedModelObjRewards));
} }
swSetEpochClass.stop();
} }
template<typename ValueType> template<typename ValueType>
@ -353,12 +354,14 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
void MultiDimensionalRewardUnfolding<ValueType>::setSolutionForCurrentEpoch(std::vector<SolutionType> const& reducedModelStateSolutions) { void MultiDimensionalRewardUnfolding<ValueType>::setSolutionForCurrentEpoch(std::vector<SolutionType> const& reducedModelStateSolutions) {
swInsertSol.start();
for (uint64_t productState = 0; productState < memoryProduct.getProduct().getNumberOfStates(); ++productState) { for (uint64_t productState = 0; productState < memoryProduct.getProduct().getNumberOfStates(); ++productState) {
uint64_t reducedModelState = ecElimResult.oldToNewStateMapping[productState]; uint64_t reducedModelState = ecElimResult.oldToNewStateMapping[productState];
if (reducedModelState < reducedModelStateSolutions.size()) { if (reducedModelState < reducedModelStateSolutions.size()) {
setSolutionForCurrentEpoch(productState, reducedModelStateSolutions[reducedModelState]); setSolutionForCurrentEpoch(productState, reducedModelStateSolutions[reducedModelState]);
} }
} }
swInsertSol.stop();
} }
template<typename ValueType> template<typename ValueType>
@ -370,16 +373,18 @@ namespace storm {
} }
template<typename ValueType> template<typename ValueType>
typename MultiDimensionalRewardUnfolding<ValueType>::SolutionType const& MultiDimensionalRewardUnfolding<ValueType>::getStateSolution(Epoch const& epoch, uint64_t const& productState) const {
typename MultiDimensionalRewardUnfolding<ValueType>::SolutionType const& MultiDimensionalRewardUnfolding<ValueType>::getStateSolution(Epoch const& epoch, uint64_t const& productState) {
swFindSol.start();
std::vector<int64_t> solutionKey = epoch; std::vector<int64_t> solutionKey = epoch;
solutionKey.push_back(productState); solutionKey.push_back(productState);
auto solutionIt = solutions.find(solutionKey); auto solutionIt = solutions.find(solutionKey);
STORM_LOG_ASSERT(solutionIt != solutions.end(), "Requested unexisting solution for epoch " << storm::utility::vector::toString(epoch) << "."); STORM_LOG_ASSERT(solutionIt != solutions.end(), "Requested unexisting solution for epoch " << storm::utility::vector::toString(epoch) << ".");
swFindSol.stop();
return solutionIt->second; return solutionIt->second;
} }
template<typename ValueType> template<typename ValueType>
typename MultiDimensionalRewardUnfolding<ValueType>::SolutionType const& MultiDimensionalRewardUnfolding<ValueType>::getInitialStateResult(Epoch const& epoch) const {
typename MultiDimensionalRewardUnfolding<ValueType>::SolutionType const& MultiDimensionalRewardUnfolding<ValueType>::getInitialStateResult(Epoch const& epoch) {
return getStateSolution(epoch, *memoryProduct.getProduct().getInitialStates().begin()); return getStateSolution(epoch, *memoryProduct.getProduct().getInitialStates().begin());
} }

21
src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h
View File

@ -11,6 +11,7 @@
#include "storm/storage/memorystructure/SparseModelMemoryProduct.h" #include "storm/storage/memorystructure/SparseModelMemoryProduct.h"
#include "storm/transformer/EndComponentEliminator.h" #include "storm/transformer/EndComponentEliminator.h"
#include "storm/utility/Stopwatch.h"
namespace storm { namespace storm {
namespace modelchecker { namespace modelchecker {
@ -51,6 +52,18 @@ namespace storm {
storm::storage::BitVector const& possibleECActions, storm::storage::BitVector const& possibleECActions,
storm::storage::BitVector const& allowedBottomStates); 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(); Epoch getStartEpoch();
std::vector<Epoch> getEpochComputationOrder(Epoch const& startEpoch); std::vector<Epoch> getEpochComputationOrder(Epoch const& startEpoch);
@ -58,7 +71,7 @@ namespace storm {
EpochModel const& setCurrentEpoch(Epoch const& epoch); EpochModel const& setCurrentEpoch(Epoch const& epoch);
void setSolutionForCurrentEpoch(std::vector<SolutionType> const& reducedModelStateSolutions); void setSolutionForCurrentEpoch(std::vector<SolutionType> const& reducedModelStateSolutions);
SolutionType const& getInitialStateResult(Epoch const& epoch) const;
SolutionType const& getInitialStateResult(Epoch const& epoch);
private: private:
@ -99,6 +112,7 @@ namespace storm {
void initializeObjectives(std::vector<std::vector<uint64_t>>& epochSteps); void initializeObjectives(std::vector<std::vector<uint64_t>>& epochSteps);
void initializePossibleEpochSteps(std::vector<std::vector<uint64_t>> const& epochSteps); void initializePossibleEpochSteps(std::vector<std::vector<uint64_t>> const& epochSteps);
void initializeMemoryProduct(std::vector<std::vector<uint64_t>> const& epochSteps); void initializeMemoryProduct(std::vector<std::vector<uint64_t>> const& epochSteps);
storm::storage::MemoryStructure computeMemoryStructure() const; storm::storage::MemoryStructure computeMemoryStructure() const;
std::vector<std::vector<ValueType>> computeObjectiveRewardsForProduct(Epoch const& epoch) const; std::vector<std::vector<ValueType>> computeObjectiveRewardsForProduct(Epoch const& epoch) const;
@ -111,7 +125,7 @@ namespace storm {
void addScaledSolution(SolutionType& solution, SolutionType const& solutionToAdd, ValueType const& scalingFactor) const; void addScaledSolution(SolutionType& solution, SolutionType const& solutionToAdd, ValueType const& scalingFactor) const;
void setSolutionForCurrentEpoch(uint64_t const& productState, SolutionType const& solution); 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<ValueType> const& model; storm::models::sparse::Mdp<ValueType> const& model;
std::vector<storm::modelchecker::multiobjective::Objective<ValueType>> const& objectives; std::vector<storm::modelchecker::multiobjective::Objective<ValueType>> const& objectives;
@ -133,6 +147,9 @@ namespace storm {
std::vector<ValueType> scalingFactors; std::vector<ValueType> scalingFactors;
std::map<std::vector<int64_t>, SolutionType> solutions; std::map<std::vector<int64_t>, SolutionType> solutions;
storm::utility::Stopwatch swInit, swFindSol, swInsertSol, swSetEpoch, swSetEpochClass;
}; };
} }
} }
Write Preview
Loading…
Cancel
Save