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

reducedMinimizerActions BitVec

main
Fabian Russold 1 year ago
committed by sp
parent
4c514cecdd
commit
61b59e64fc
3 changed files with 63 additions and 15 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. 6
      src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp
  2. 63
      src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp
  3. 9
      src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h

6
src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp
View File

@ -63,7 +63,7 @@ namespace storm {
template<typename ValueType>
SMGSparseModelCheckingHelperReturnType<ValueType> SparseSmgRpatlHelper<ValueType>::computeUntilProbabilitiesSound(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint) {
storm::modelchecker::helper::internal::SoundGameViHelper<ValueType> viHelper(transitionMatrix, statesOfCoalition);
storm::modelchecker::helper::internal::SoundGameViHelper<ValueType> viHelper(transitionMatrix, statesOfCoalition, goal.direction());
// Initialize the x vector and solution vector result.
// TODO Fabian: maybe relevant states (later)
@ -73,7 +73,7 @@ namespace storm {
assert(xL.size() == psiStates.size());
for (size_t i = 0; i < xL.size(); i++)
{
if (psiStates[xL.size() - i])
if (psiStates[i])
xL[i] = 1;
}
STORM_LOG_DEBUG("xL " << xL);
@ -81,7 +81,7 @@ namespace storm {
storm::storage::BitVector probGreater0 = storm::utility::graph::performProbGreater0(backwardTransitions, phiStates, psiStates);
// assigning 1s to the xU vector for all states except the states s where Prob(sEf) = 0 for all goal states f
assert(xU.size() == probGreater0.size());
for (size_t i = 0; i < xL.size(); i++)
for (size_t i = 0; i < xL.size(); i++) // TODO Fabian: do this more efficient
{
if (probGreater0[i])
xU[i] = 1;

63
src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp
View File

@ -14,7 +14,7 @@ namespace storm {
namespace internal {
template <typename ValueType>
SoundGameViHelper<ValueType>::SoundGameViHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector statesOfCoalition) : _transitionMatrix(transitionMatrix), _statesOfCoalition(statesOfCoalition) {
SoundGameViHelper<ValueType>::SoundGameViHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector statesOfCoalition, OptimizationDirection const& optimizationDirection) : _transitionMatrix(transitionMatrix), _statesOfCoalition(statesOfCoalition), _optimizationDirection(optimizationDirection) {
// Intentionally left empty.
}
@ -23,6 +23,7 @@ namespace storm {
STORM_LOG_DEBUG("\n" << _transitionMatrix);
_multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, _transitionMatrix);
_x1IsCurrent = false;
_minimizerStates = _optimizationDirection == OptimizationDirection::Maximize ? _statesOfCoalition : ~_statesOfCoalition;
}
template <typename ValueType>
@ -77,30 +78,70 @@ namespace storm {
template <typename ValueType>
void SoundGameViHelper<ValueType>::performIterationStep(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector<uint64_t>* choices) {
storm::storage::BitVector reducedMinimizerActions = {storm::storage::BitVector(this->_transitionMatrix.getRowCount(), true)};
// under approximation
if (!_multiplier) {
prepareSolversAndMultipliers(env);
}
_x1IsCurrent = !_x1IsCurrent;
if (choices == nullptr) {
_multiplier->multiplyAndReduce(env, dir, xOldL(), nullptr, xNewL(), nullptr, &_statesOfCoalition);
} else {
_multiplier->multiplyAndReduce(env, dir, xOldL(), nullptr, xNewL(), choices, &_statesOfCoalition);
}
std::vector<ValueType> choiceValues = xNewL();
choiceValues.resize(this->_transitionMatrix.getRowCount());
_multiplier->multiply(env, xOldL(), nullptr, choiceValues);
reduceChoiceValues(choiceValues, &reducedMinimizerActions);
xNewL() = choiceValues;
// over_approximation
if (choices == nullptr) {
_multiplier->multiplyAndReduce(env, dir, xOldU(), nullptr, xNewU(), nullptr, &_statesOfCoalition);
} else {
_multiplier->multiplyAndReduce(env, dir, xOldU(), nullptr, xNewU(), choices, &_statesOfCoalition);
}
_multiplier->multiplyAndReduce(env, dir, xOldU(), nullptr, xNewU(), nullptr, &_statesOfCoalition);
// TODO Fabian: find_MSECs() & deflate()
}
template <typename ValueType>
void SoundGameViHelper<ValueType>::reduceChoiceValues(std::vector<ValueType>& choiceValues, storm::storage::BitVector* result)
{
// result BitVec should be initialized with 1s outside the function
// restrict rows
auto rowGroupIndices = this->_transitionMatrix.getRowGroupIndices();
auto choice_it = choiceValues.begin();
STORM_LOG_DEBUG("MinStates " << _minimizerStates);
STORM_LOG_DEBUG("init choiceVal " << choiceValues);
for(uint state = 0; state < rowGroupIndices.size() - 1; state++) {
uint rowGroupSize = rowGroupIndices[state + 1] - rowGroupIndices[state];
ValueType optChoice;
if (_minimizerStates[state]) { // check if current state is minimizer state
// getting the optimal minimizer choice for the given state
optChoice = *std::min_element(choice_it, choice_it + rowGroupSize);
for (uint choice = 0; choice < rowGroupSize; choice++, choice_it++) {
if (*choice_it > optChoice) {
result->set(rowGroupIndices[state] + choice, 0);
}
}
// reducing the xNew() (choiceValues) vector for minimizer states
choiceValues[state] = optChoice;
}
else
{
optChoice = *std::max_element(choice_it, choice_it + rowGroupSize);
// reducing the xNew() (choiceValues) vector for maximizer states
choiceValues[state] = optChoice;
choice_it += rowGroupSize;
}
}
choiceValues.resize(this->_transitionMatrix.getRowGroupCount());
STORM_LOG_DEBUG("reduced BitVec: " << *result);
STORM_LOG_DEBUG("reduced x Vector: " << choiceValues);
}
template <typename ValueType>
bool SoundGameViHelper<ValueType>::checkConvergence(ValueType threshold) const {
STORM_LOG_ASSERT(_multiplier, "tried to check for convergence without doing an iteration first.");

9
src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h
View File

@ -19,7 +19,7 @@ namespace storm {
template <typename ValueType>
class SoundGameViHelper {
public:
SoundGameViHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector statesOfCoalition);
SoundGameViHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector statesOfCoalition, OptimizationDirection const& optimizationDirection);
void prepareSolversAndMultipliers(const Environment& env);
@ -73,6 +73,10 @@ namespace storm {
*/
void performIterationStep(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector<uint64_t>* choices = nullptr);
void reduceChoiceValues(std::vector<ValueType>& choiceValues, storm::storage::BitVector* result);
//
// für alle minimizer states -> reduce zu optimal actions
/*!
* Checks whether the curently computed value achieves the desired precision
*/
@ -92,6 +96,8 @@ namespace storm {
bool _x1IsCurrent;
storm::storage::BitVector _minimizerStates;
/*!
* @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.
@ -108,6 +114,7 @@ namespace storm {
storm::storage::BitVector _statesOfCoalition;
std::vector<ValueType> _x, _x1L, _x2L, _x1U, _x2U;
std::unique_ptr<storm::solver::Multiplier<ValueType>> _multiplier;
OptimizationDirection _optimizationDirection;
bool _produceScheduler = false;
bool _shieldingTask = false;

Write Preview
Loading…
Cancel
Save