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

implemented caching of the EC elimination result in the standard weight vector checker

tempestpy_adaptions
TimQu 7 years ago
parent
9716289f6a
commit
31af523ea1
2 changed files with 36 additions and 19 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 48
      src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp
  2. 7
      src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h

48
src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp
View File

@ -8,7 +8,6 @@
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h"
#include "storm/solver/MinMaxLinearEquationSolver.h"
#include "storm/transformer/EndComponentEliminator.h"
#include "storm/utility/graph.h"
#include "storm/utility/macros.h"
#include "storm/utility/vector.h"
@ -154,26 +153,14 @@ namespace storm {
return;
}
// Only consider the states from which a transition with non-zero reward is reachable. (The remaining states always have reward zero).
storm::storage::BitVector zeroRewardActions = storm::utility::vector::filterZero(weightedRewardVector);
storm::storage::BitVector nonZeroRewardActions = ~zeroRewardActions;
storm::storage::BitVector nonZeroRewardStates(this->model.getNumberOfStates(), false);
for(uint_fast64_t state = 0; state < this->model.getNumberOfStates(); ++state){
if(nonZeroRewardActions.getNextSetIndex(this->model.getTransitionMatrix().getRowGroupIndices()[state]) < this->model.getTransitionMatrix().getRowGroupIndices()[state+1]) {
nonZeroRewardStates.set(state);
}
}
storm::storage::BitVector subsystemStates = storm::utility::graph::performProbGreater0E(this->model.getTransitionMatrix().transpose(true), storm::storage::BitVector(this->model.getNumberOfStates(), true), nonZeroRewardStates);
// Remove neutral end components, i.e., ECs in which no reward is earned.
auto ecEliminatorResult = storm::transformer::EndComponentEliminator<ValueType>::transform(this->model.getTransitionMatrix(), subsystemStates, possibleECActions & zeroRewardActions, possibleBottomStates);
updateEcElimResult(weightedRewardVector);
std::vector<ValueType> subRewardVector(ecEliminatorResult.newToOldRowMapping.size());
storm::utility::vector::selectVectorValues(subRewardVector, ecEliminatorResult.newToOldRowMapping, weightedRewardVector);
std::vector<ValueType> subResult(ecEliminatorResult.matrix.getRowGroupCount());
std::vector<ValueType> subRewardVector(cachedEcElimResult->newToOldRowMapping.size());
storm::utility::vector::selectVectorValues(subRewardVector, cachedEcElimResult->newToOldRowMapping, weightedRewardVector);
std::vector<ValueType> subResult(cachedEcElimResult->matrix.getRowGroupCount());
storm::solver::GeneralMinMaxLinearEquationSolverFactory<ValueType> solverFactory;
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = solverFactory.create(ecEliminatorResult.matrix);
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = solverFactory.create(cachedEcElimResult->matrix);
solver->setOptimizationDirection(storm::solver::OptimizationDirection::Maximize);
solver->setTrackScheduler(true);
if (lowerResultBound) {
@ -186,7 +173,7 @@ namespace storm {
this->weightedResult = std::vector<ValueType>(this->model.getNumberOfStates());
transformReducedSolutionToOriginalModel(ecEliminatorResult.matrix, subResult, solver->getSchedulerChoices(), ecEliminatorResult.newToOldRowMapping, ecEliminatorResult.oldToNewStateMapping, this->weightedResult, this->optimalChoices);
transformReducedSolutionToOriginalModel(cachedEcElimResult->matrix, subResult, solver->getSchedulerChoices(), cachedEcElimResult->newToOldRowMapping, cachedEcElimResult->oldToNewStateMapping, this->weightedResult, this->optimalChoices);
}
template <class SparseModelType>
@ -274,6 +261,29 @@ namespace storm {
}
}
template <class SparseModelType>
void SparsePcaaWeightVectorChecker<SparseModelType>::updateEcElimResult(std::vector<ValueType> const& weightedRewardVector) {
// Check whether we need to update the currently cached ecElimResult
storm::storage::BitVector newZeroRewardChoices = storm::utility::vector::filterZero(weightedRewardVector);
if (!cachedZeroRewardChoices || cachedZeroRewardChoices.get() != newZeroRewardChoices) {
cachedZeroRewardChoices = std::move(newZeroRewardChoices);
// It is sufficient to consider the states from which a transition with non-zero reward is reachable. (The remaining states always have reward zero).
storm::storage::BitVector nonZeroRewardStates(this->model.getNumberOfStates(), false);
for (uint_fast64_t state = 0; state < this->model.getNumberOfStates(); ++state){
if (cachedZeroRewardChoices->getNextUnsetIndex(this->model.getTransitionMatrix().getRowGroupIndices()[state]) < this->model.getTransitionMatrix().getRowGroupIndices()[state+1]) {
nonZeroRewardStates.set(state);
}
}
storm::storage::BitVector subsystemStates = storm::utility::graph::performProbGreater0E(this->model.getTransitionMatrix().transpose(true), storm::storage::BitVector(this->model.getNumberOfStates(), true), nonZeroRewardStates);
// Remove neutral end components, i.e., ECs in which no reward is earned.
cachedEcElimResult = storm::transformer::EndComponentEliminator<ValueType>::transform(this->model.getTransitionMatrix(), subsystemStates, possibleECActions & cachedZeroRewardChoices.get(), possibleBottomStates);
}
STORM_LOG_ASSERT(cachedEcElimResult, "Updating the ecElimResult was not successfull.");
}
template <class SparseModelType>
void SparsePcaaWeightVectorChecker<SparseModelType>::transformReducedSolutionToOriginalModel(storm::storage::SparseMatrix<ValueType> const& reducedMatrix,
std::vector<ValueType> const& reducedSolution,

7
src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h
View File

@ -3,6 +3,7 @@
#include "storm/storage/BitVector.h"
#include "storm/storage/SparseMatrix.h"
#include "storm/storage/Scheduler.h"
#include "storm/transformer/EndComponentEliminator.h"
#include "storm/modelchecker/multiobjective/Objective.h"
#include "storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.h"
#include "storm/utility/vector.h"
@ -90,6 +91,8 @@ namespace storm {
*/
virtual void boundedPhase(std::vector<ValueType> const& weightVector, std::vector<ValueType>& weightedRewardVector) = 0;
void updateEcElimResult(std::vector<ValueType> const& weightedRewardVector);
/*!
* Transforms the results of a min-max-solver that considers a reduced model (without end components) to a result for the original (unreduced) model
*/
@ -127,6 +130,10 @@ namespace storm {
std::vector<ValueType> offsetsToOverApproximation;
// The scheduler choices that optimize the weighted rewards of undounded objectives.
std::vector<uint_fast64_t> optimalChoices;
// Caches the result of the ec elimination (avoiding recomputations for each weightvector)
boost::optional<typename storm::transformer::EndComponentEliminator<ValueType>::EndComponentEliminatorReturnType> cachedEcElimResult;
// Stores which choices are considered to have zero reward in the current cachedEcElimiResult.
boost::optional<storm::storage::BitVector> cachedZeroRewardChoices;
};

Write Preview
Loading…
Cancel
Save