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

deleted BoundedGloballyGameViHelper

tempestpy_adaptions
Lukas Posch 3 years ago
committed by Stefan Pranger
parent
e5dd9ab90f
commit
75bacaa6b2
2 changed files with 0 additions and 208 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. 132
      src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp
  2. 76
      src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h

132
src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp
View File

@ -1,132 +0,0 @@
#include "BoundedGloballyGameViHelper.h"
#include "storm/environment/Environment.h"
#include "storm/environment/solver/SolverEnvironment.h"
#include "storm/environment/solver/GameSolverEnvironment.h"
#include "storm/utility/SignalHandler.h"
#include "storm/utility/vector.h"
namespace storm {
namespace modelchecker {
namespace helper {
namespace internal {
template <typename ValueType>
BoundedGloballyGameViHelper<ValueType>::BoundedGloballyGameViHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector statesOfCoalition) : _transitionMatrix(transitionMatrix), _statesOfCoalition(statesOfCoalition) {
}
template <typename ValueType>
void BoundedGloballyGameViHelper<ValueType>::prepareSolversAndMultipliers(const Environment& env) {
_multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, _transitionMatrix);
}
template <typename ValueType>
void BoundedGloballyGameViHelper<ValueType>::performValueIteration(Environment const& env, std::vector<ValueType>& x, storm::solver::OptimizationDirection const dir, uint64_t upperBound, std::vector<ValueType>& constrainedChoiceValues) {
prepareSolversAndMultipliers(env);
_x = x;
if (this->isProduceSchedulerSet()) {
if (!this->_producedOptimalChoices.is_initialized()) {
this->_producedOptimalChoices.emplace();
}
this->_producedOptimalChoices->resize(this->_transitionMatrix.getRowGroupCount());
}
for (uint64_t iter = 0; iter < upperBound; iter++) {
if(iter == upperBound - 1) {
_multiplier->multiply(env, _x, nullptr, constrainedChoiceValues);
}
performIterationStep(env, dir);
}
x = _x;
}
template <typename ValueType>
void BoundedGloballyGameViHelper<ValueType>::performIterationStep(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector<uint64_t>* choices) {
if (!_multiplier) {
prepareSolversAndMultipliers(env);
}
// multiplyandreducegaussseidel
// Ax = x'
if (choices == nullptr) {
_multiplier->multiplyAndReduce(env, dir, _x, nullptr, _x, nullptr, &_statesOfCoalition);
} else {
// Also keep track of the choices made.
_multiplier->multiplyAndReduce(env, dir, _x, nullptr, _x, choices, &_statesOfCoalition);
}
}
template <typename ValueType>
void BoundedGloballyGameViHelper<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 BoundedGloballyGameViHelper<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>
void BoundedGloballyGameViHelper<ValueType>::setProduceScheduler(bool value) {
_produceScheduler = value;
}
template <typename ValueType>
bool BoundedGloballyGameViHelper<ValueType>::isProduceSchedulerSet() const {
return _produceScheduler;
}
template <typename ValueType>
std::vector<uint64_t> const& BoundedGloballyGameViHelper<ValueType>::getProducedOptimalChoices() const {
STORM_LOG_ASSERT(this->isProduceSchedulerSet(), "Trying to get the produced optimal choices although no scheduler was requested.");
STORM_LOG_ASSERT(this->_producedOptimalChoices.is_initialized(), "Trying to get the produced optimal choices but none were available. Was there a computation call before?");
return this->_producedOptimalChoices.get();
}
template <typename ValueType>
std::vector<uint64_t>& BoundedGloballyGameViHelper<ValueType>::getProducedOptimalChoices() {
STORM_LOG_ASSERT(this->isProduceSchedulerSet(), "Trying to get the produced optimal choices although no scheduler was requested.");
STORM_LOG_ASSERT(this->_producedOptimalChoices.is_initialized(), "Trying to get the produced optimal choices but none were available. Was there a computation call before?");
return this->_producedOptimalChoices.get();
}
template <typename ValueType>
storm::storage::Scheduler<ValueType> BoundedGloballyGameViHelper<ValueType>::extractScheduler() const{
auto const& optimalChoices = getProducedOptimalChoices();
storm::storage::Scheduler<ValueType> scheduler(optimalChoices.size());
for (uint64_t state = 0; state < optimalChoices.size(); ++state) {
scheduler.setChoice(optimalChoices[state], state);
}
return scheduler;
}
template class BoundedGloballyGameViHelper<double>;
#ifdef STORM_HAVE_CARL
template class BoundedGloballyGameViHelper<storm::RationalNumber>;
#endif
}
}
}
}

76
src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h
View File

@ -1,76 +0,0 @@
#pragma once
#include "storm/storage/SparseMatrix.h"
#include "storm/solver/LinearEquationSolver.h"
#include "storm/solver/MinMaxLinearEquationSolver.h"
#include "storm/solver/Multiplier.h"
namespace storm {
class Environment;
namespace storage {
template <typename VT> class Scheduler;
}
namespace modelchecker {
namespace helper {
namespace internal {
template <typename ValueType>
class BoundedGloballyGameViHelper {
public:
BoundedGloballyGameViHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector statesOfCoalition);
void prepareSolversAndMultipliers(const Environment& env);
void performValueIteration(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 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);
/*!
* Sets whether an optimal scheduler shall be constructed during the computation
*/
void setProduceScheduler(bool value);
/*!
* @return whether an optimal scheduler shall be constructed during the computation
*/
bool isProduceSchedulerSet() const;
storm::storage::Scheduler<ValueType> extractScheduler() const;
private:
void performIterationStep(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector<uint64_t>* choices = nullptr);
/*!
* @pre before calling this, a computation call should have been performed during which scheduler production was enabled.
* @return the produced scheduler of the most recent call.
*/
std::vector<uint64_t> const& getProducedOptimalChoices() const;
/*!
* @pre before calling this, a computation call should have been performed during which scheduler production was enabled.
* @return the produced scheduler of the most recent call.
*/
std::vector<uint64_t>& getProducedOptimalChoices();
storm::storage::SparseMatrix<ValueType> _transitionMatrix;
storm::storage::BitVector _statesOfCoalition;
std::vector<ValueType> _x;
std::unique_ptr<storm::solver::Multiplier<ValueType>> _multiplier;
bool _produceScheduler = false;
boost::optional<std::vector<uint64_t>> _producedOptimalChoices;
};
}
}
}
}
Write Preview
Loading…
Cancel
Save