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

clean up BoundedGloballyGameViHelper

tempestpy_adaptions
Lukas Posch 4 years ago
parent
0fd952c6f7
commit
f6829dd109
3 changed files with 7 additions and 72 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. 66
      src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp
  2. 11
      src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h
  3. 2
      src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h

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

@ -19,23 +19,12 @@ namespace storm {
template <typename ValueType>
void BoundedGloballyGameViHelper<ValueType>::prepareSolversAndMultipliers(const Environment& env) {
_multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, _transitionMatrix);
/*
_x1IsCurrent = false;
*/
}
template <typename ValueType>
void BoundedGloballyGameViHelper<ValueType>::performValueIteration(Environment const& env, std::vector<ValueType>& x, storm::solver::OptimizationDirection const dir, uint64_t upperBound) {
prepareSolversAndMultipliers(env);
/*
_x1.assign(_transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
*/
_x1 = x;
_x2 = _x1;
/* STORM_LOG_DEBUG("_b = " << _b);
STORM_LOG_DEBUG("_x1 = " << _x1);
STORM_LOG_DEBUG("_x2 = " << _x2);*/
_x = x;
if (this->isProduceSchedulerSet()) {
if (!this->_producedOptimalChoices.is_initialized()) {
@ -46,24 +35,9 @@ namespace storm {
for (uint64_t iter = 0; iter < upperBound; iter++) {
performIterationStep(env, dir);
/* STORM_LOG_DEBUG("After iteration " << iter << ":");
STORM_LOG_DEBUG("_x1 = " << _x1);
STORM_LOG_DEBUG("_x2 = " << _x2);*/
/* if (storm::utility::resources::isTerminate()) {
break;
}*/
}
/*
x = xNew();
*/
x = _x1;
/* if (isProduceSchedulerSet()) {
// We will be doing one more iteration step and track scheduler choices this time.
performIterationStep(env, dir, &_producedOptimalChoices.get());
}*/
x = _x;
}
template <typename ValueType>
@ -71,27 +45,15 @@ namespace storm {
if (!_multiplier) {
prepareSolversAndMultipliers(env);
}
/* _x1IsCurrent = !_x1IsCurrent;*/
// multiplyandreducegaussseidel
// Ax + b
if (choices == nullptr) {
_multiplier->multiplyAndReduce(env, dir, _x1, nullptr, _x1, nullptr, &_statesOfCoalition);
_multiplier->multiplyAndReduce(env, dir, _x, nullptr, _x, nullptr, &_statesOfCoalition);
} else {
// Also keep track of the choices made.
_multiplier->multiplyAndReduce(env, dir, _x1, nullptr, _x1, choices, &_statesOfCoalition);
_multiplier->multiplyAndReduce(env, dir, _x, nullptr, _x, choices, &_statesOfCoalition);
}
/* // compare applyPointwise
storm::utility::vector::applyPointwise<ValueType, ValueType, ValueType>(xOld(), xNew(), xNew(), [&dir] (ValueType const& a, ValueType const& b) -> ValueType {
if(storm::solver::maximize(dir)) {
if(a > b) return a;
else return b;
} else {
if(a > b) return a;
else return b;
}
});*/
}
template <typename ValueType>
@ -142,26 +104,6 @@ namespace storm {
return scheduler;
}
/* template <typename ValueType>
std::vector<ValueType>& BoundedGloballyGameViHelper<ValueType>::xNew() {
return _x1IsCurrent ? _x1 : _x2;
}
template <typename ValueType>
std::vector<ValueType> const& BoundedGloballyGameViHelper<ValueType>::xNew() const {
return _x1IsCurrent ? _x1 : _x2;
}
template <typename ValueType>
std::vector<ValueType>& BoundedGloballyGameViHelper<ValueType>::xOld() {
return _x1IsCurrent ? _x2 : _x1;
}
template <typename ValueType>
std::vector<ValueType> const& BoundedGloballyGameViHelper<ValueType>::xOld() const {
return _x1IsCurrent ? _x2 : _x1;
}*/
template class BoundedGloballyGameViHelper<double>;
#ifdef STORM_HAVE_CARL
template class BoundedGloballyGameViHelper<storm::RationalNumber>;

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

@ -30,7 +30,7 @@ namespace storm {
*/
void fillResultVector(std::vector<ValueType>& result, storm::storage::BitVector psiStates);
/*h
/*!
* Sets whether an optimal scheduler shall be constructed during the computation
*/
void setProduceScheduler(bool value);
@ -45,13 +45,6 @@ namespace storm {
private:
void performIterationStep(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector<uint64_t>* choices = nullptr);
/* std::vector<ValueType>& xNew();
std::vector<ValueType> const& xNew() const;
std::vector<ValueType>& xOld();
std::vector<ValueType> const& xOld() const;
bool _x1IsCurrent;*/
/*!
* @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.
@ -66,7 +59,7 @@ namespace storm {
storm::storage::SparseMatrix<ValueType> _transitionMatrix;
storm::storage::BitVector _statesOfCoalition;
std::vector<ValueType> _x1, _x2;
std::vector<ValueType> _x;
std::unique_ptr<storm::solver::Multiplier<ValueType>> _multiplier;
bool _produceScheduler = false;

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

@ -30,7 +30,7 @@ namespace storm {
*/
void fillResultVector(std::vector<ValueType>& result, storm::storage::BitVector relevantStates, storm::storage::BitVector psiStates);
/*h
/*!
* Sets whether an optimal scheduler shall be constructed during the computation
*/
void setProduceScheduler(bool value);

Write Preview
Loading…
Cancel
Save