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

WIP helper functions in GameViHelper

tempestpy_adaptions
Lukas Posch 3 years ago
committed by Stefan Pranger
parent
c2d2c38c28
commit
fefd6b0951
2 changed files with 49 additions and 64 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. 85
      src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp
  2. 28
      src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h

85
src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp
View File

@ -114,9 +114,11 @@ namespace storm {
} }
template <typename ValueType> template <typename ValueType>
void GameViHelper<ValueType>::performValueIterationUpperBound(Environment const& env, std::vector<ValueType>& x, storm::solver::OptimizationDirection const dir, uint64_t upperBound, std::vector<ValueType>& constrainedChoiceValues) {
void GameViHelper<ValueType>::performValueIterationUpperBound(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> b, storm::solver::OptimizationDirection const dir, uint64_t upperBound, std::vector<ValueType>& constrainedChoiceValues) {
prepareSolversAndMultipliers(env); prepareSolversAndMultipliers(env);
_x = x; _x = x;
_b = b;
if (this->isProduceSchedulerSet()) { if (this->isProduceSchedulerSet()) {
if (!this->_producedOptimalChoices.is_initialized()) { if (!this->_producedOptimalChoices.is_initialized()) {
this->_producedOptimalChoices.emplace(); this->_producedOptimalChoices.emplace();
@ -125,10 +127,21 @@ namespace storm {
} }
for (uint64_t iter = 0; iter < upperBound; iter++) { for (uint64_t iter = 0; iter < upperBound; iter++) {
if(iter == upperBound - 1) { if(iter == upperBound - 1) {
_multiplier->multiply(env, _x, nullptr, constrainedChoiceValues);
STORM_LOG_DEBUG("before multipliing ...");
STORM_LOG_DEBUG("_x = " << _x);
STORM_LOG_DEBUG("_b = " << _b);
STORM_LOG_DEBUG("constrainedChoiceValues = " << constrainedChoiceValues);
_multiplier->multiply(env, _x, &_b, constrainedChoiceValues);
STORM_LOG_DEBUG("before multipliing ...");
STORM_LOG_DEBUG("_x = " << _x);
STORM_LOG_DEBUG("_b = " << _b);
STORM_LOG_DEBUG("constrainedChoiceValues = " << constrainedChoiceValues);
} }
performIterationStepUpperBound(env, dir); performIterationStepUpperBound(env, dir);
} }
x = _x; x = _x;
} }
@ -140,57 +153,13 @@ namespace storm {
// multiplyandreducegaussseidel // multiplyandreducegaussseidel
// Ax = x' // Ax = x'
if (choices == nullptr) { if (choices == nullptr) {
_multiplier->multiplyAndReduce(env, dir, _x, nullptr, _x, nullptr, &_statesOfCoalition);
_multiplier->multiplyAndReduce(env, dir, _x, &_b, _x, nullptr, &_statesOfCoalition);
} else { } else {
// Also keep track of the choices made. // Also keep track of the choices made.
_multiplier->multiplyAndReduce(env, dir, _x, nullptr, _x, choices, &_statesOfCoalition);
_multiplier->multiplyAndReduce(env, dir, _x, &_b, _x, choices, &_statesOfCoalition);
} }
} }
template <typename ValueType>
void GameViHelper<ValueType>::fillResultVector(std::vector<ValueType>& result, storm::storage::BitVector relevantStates) {
std::vector<ValueType> filledVector = std::vector<ValueType>(relevantStates.size(), storm::utility::zero<ValueType>());
uint bitIndex = 0;
for(uint i = 0; i < filledVector.size(); i++) {
if (relevantStates.get(i)) {
filledVector.at(i) = result.at(bitIndex);
bitIndex++;
}
}
result = filledVector;
}
template <typename ValueType>
void GameViHelper<ValueType>::fillResultVector(std::vector<ValueType>& result, storm::storage::BitVector relevantStates, storm::storage::BitVector psiStates) {
std::vector<ValueType> filledVector = std::vector<ValueType>(relevantStates.size(), storm::utility::zero<ValueType>());
uint bitIndex = 0;
for(uint i = 0; i < filledVector.size(); i++) {
if (relevantStates.get(i)) {
filledVector.at(i) = result.at(bitIndex);
bitIndex++;
}
else if (psiStates.get(i)) {
filledVector.at(i) = 1;
}
}
result = filledVector;
}
template <typename ValueType>
void GameViHelper<ValueType>::fillChoiceValuesVector(std::vector<ValueType>& choiceValues, storm::storage::BitVector psiStates, std::vector<storm::storage::SparseMatrix<double>::index_type> rowGroupIndices) {
std::vector<ValueType> allChoices = std::vector<ValueType>(rowGroupIndices.at(rowGroupIndices.size() - 1), storm::utility::zero<ValueType>());
auto choice_it = choiceValues.begin();
for(uint state = 0; state < rowGroupIndices.size() - 1; state++) {
uint rowGroupSize = rowGroupIndices[state + 1] - rowGroupIndices[state];
if (psiStates.get(state)) {
for(uint choice = 0; choice < rowGroupSize; choice++, choice_it++) {
allChoices.at(rowGroupIndices.at(state) + choice) = *choice_it;
}
}
}
choiceValues = allChoices;
}
template <typename ValueType> template <typename ValueType>
void GameViHelper<ValueType>::setProduceScheduler(bool value) { void GameViHelper<ValueType>::setProduceScheduler(bool value) {
_produceScheduler = value; _produceScheduler = value;
@ -201,6 +170,11 @@ namespace storm {
return _produceScheduler; return _produceScheduler;
} }
template <typename ValueType>
void GameViHelper<ValueType>::updateTransitionMatrix(storm::storage::SparseMatrix<ValueType> newTransitionMatrix) {
_transitionMatrix = newTransitionMatrix;
}
template <typename ValueType> template <typename ValueType>
std::vector<uint64_t> const& GameViHelper<ValueType>::getProducedOptimalChoices() const { std::vector<uint64_t> const& GameViHelper<ValueType>::getProducedOptimalChoices() const {
STORM_LOG_ASSERT(this->isProduceSchedulerSet(), "Trying to get the produced optimal choices although no scheduler was requested."); STORM_LOG_ASSERT(this->isProduceSchedulerSet(), "Trying to get the produced optimal choices although no scheduler was requested.");
@ -230,6 +204,21 @@ namespace storm {
_multiplier->multiply(env, x, &_b, choiceValues); _multiplier->multiply(env, x, &_b, choiceValues);
} }
template <typename ValueType>
void GameViHelper<ValueType>::fillChoiceValuesVector(std::vector<ValueType>& choiceValues, storm::storage::BitVector psiStates, std::vector<storm::storage::SparseMatrix<double>::index_type> rowGroupIndices) {
std::vector<ValueType> allChoices = std::vector<ValueType>(rowGroupIndices.at(rowGroupIndices.size() - 1), storm::utility::zero<ValueType>());
auto choice_it = choiceValues.begin();
for(uint state = 0; state < rowGroupIndices.size() - 1; state++) {
uint rowGroupSize = rowGroupIndices[state + 1] - rowGroupIndices[state];
if (psiStates.get(state)) {
for(uint choice = 0; choice < rowGroupSize; choice++, choice_it++) {
allChoices.at(rowGroupIndices.at(state) + choice) = *choice_it;
}
}
}
choiceValues = allChoices;
}
template <typename ValueType> template <typename ValueType>
std::vector<ValueType>& GameViHelper<ValueType>::xNew() { std::vector<ValueType>& GameViHelper<ValueType>::xNew() {
return _x1IsCurrent ? _x1 : _x2; return _x1IsCurrent ? _x1 : _x2;

28
src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h
View File

@ -31,22 +31,7 @@ namespace storm {
/*! /*!
* Perform value iteration until upper bound * Perform value iteration until upper bound
*/ */
void performValueIterationUpperBound(Environment const& env, std::vector<ValueType>& x, storm::solver::OptimizationDirection const dir, uint64_t upperBound, std::vector<ValueType>& constrainedChoiceValues);
/*!
* Fills the result vector to the original size with zeros for all states except the relevantStates
*/
void fillResultVector(std::vector<ValueType>& result, storm::storage::BitVector relevantStates);
/*!
* Fills the result vector to the original size with ones for being psiStates, zeros for being not phiStates
*/
void fillResultVector(std::vector<ValueType>& result, storm::storage::BitVector relevantStates, storm::storage::BitVector psiStates);
/*!
* Fills the choice values vector to the original size with zeros for ~psiState choices.
*/
void fillChoiceValuesVector(std::vector<ValueType>& choiceValues, storm::storage::BitVector psiStates, std::vector<storm::storage::SparseMatrix<double>::index_type> rowGroupIndices);
void performValueIterationUpperBound(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> b, storm::solver::OptimizationDirection const dir, uint64_t upperBound, std::vector<ValueType>& constrainedChoiceValues);
/*! /*!
* Sets whether an optimal scheduler shall be constructed during the computation * Sets whether an optimal scheduler shall be constructed during the computation
@ -58,9 +43,20 @@ namespace storm {
*/ */
bool isProduceSchedulerSet() const; bool isProduceSchedulerSet() const;
/*!
* Changes the transitionMatrix of the gameViHelper to the given one.
*/
void updateTransitionMatrix(storm::storage::SparseMatrix<ValueType> newTransitionMatrix);
storm::storage::Scheduler<ValueType> extractScheduler() const; storm::storage::Scheduler<ValueType> extractScheduler() const;
void getChoiceValues(Environment const& env, std::vector<ValueType> const& x, std::vector<ValueType>& choiceValues); void getChoiceValues(Environment const& env, std::vector<ValueType> const& x, std::vector<ValueType>& choiceValues);
/*!
* Fills the choice values vector to the original size with zeros for ~psiState choices.
*/
void fillChoiceValuesVector(std::vector<ValueType>& choiceValues, storm::storage::BitVector psiStates, std::vector<storm::storage::SparseMatrix<double>::index_type> rowGroupIndices);
private: private:
/*! /*!
* Performs one iteration step for value iteration * Performs one iteration step for value iteration

Write Preview
Loading…
Cancel
Save