Browse Source

cleaned up GameVi and LraViHelper

tempestpy_adaptions
Stefan Pranger 3 years ago
parent
commit
29fb202761
  1. 11
      src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp
  2. 24
      src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp

11
src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp

@ -221,13 +221,10 @@ namespace storm {
}
performIterationStep(env, dir, choices);
}
//std::cout << "result (" << iter << " steps):" << std::endl;
storm::utility::vector::applyPointwise<ValueType, ValueType>(xNew(), xNew(), [&iter] (ValueType const& x_i) -> ValueType { return x_i / (double)iter; });
//for(int i = 0; i < xNew().size() ; i++ ) {
// std::cout << std::setprecision(4) << i << "\t: " << xNew().at(i) << "\t" << xNew().at(i) * _uniformizationRate << "\t" << std::setprecision(16) << xOld().at(i) *_uniformizationRate << std::endl;
// //if(i == 50) {std::cout << "only showing top 50 lines"; break; }
//}
if(gameNondetTs()) result = (xOld().at(0) * _uniformizationRate)/(double)iter; // TODO is "init" always going to be .at(0) ?
if(gameNondetTs()) {
storm::utility::vector::applyPointwise<ValueType, ValueType>(xNew(), xNew(), [&iter] (ValueType const& x_i) -> ValueType { return x_i / (double)iter; });
result = (xOld().at(0) * _uniformizationRate)/(double)iter; // TODO is "init" always going to be .at(0) ?
}
return result;
}

24
src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp

@ -8,8 +8,6 @@
#include "storm/utility/SignalHandler.h"
#include "storm/utility/vector.h"
// TODO this will undergo major refactoring as soon as we implement model checking of further properties
namespace storm {
namespace modelchecker {
namespace helper {
@ -21,10 +19,6 @@ namespace storm {
template <typename ValueType>
void GameViHelper<ValueType>::prepareSolversAndMultipliers(const Environment& env) {
// TODO we get whole transitionmatrix and psistates DONE IN smgrpatlhelper
// -> clip statesofcoalition
// -> compute b vector from psiStates
// -> clip transitionmatrix and create multiplier
_multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, _transitionMatrix);
_x1IsCurrent = false;
@ -75,29 +69,16 @@ namespace storm {
}
_x1IsCurrent = !_x1IsCurrent;
// multiplyandreducegaussseidel
// Ax + b
if (choices == nullptr) {
//STORM_LOG_DEBUG("\n" << _transitionMatrix);
//STORM_LOG_DEBUG("xOld = " << storm::utility::vector::toString(xOld()));
//STORM_LOG_DEBUG("b = " << storm::utility::vector::toString(_b));
//STORM_LOG_DEBUG("xNew = " << storm::utility::vector::toString(xNew()));
_multiplier->multiplyAndReduce(env, dir, xOld(), &_b, xNew(), nullptr, &_statesOfCoalition);
//std::cin.get();
} else {
// Also keep track of the choices made.
_multiplier->multiplyAndReduce(env, dir, xOld(), &_b, xNew(), 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;
}
if(a > b) return a;
else return b;
});
}
@ -129,7 +110,6 @@ namespace storm {
return false;
}
}
// TODO needs checking
return true;
}

Loading…
Cancel
Save