Browse Source

fixed bug in reduce method in Multiplier.cpp for SMGs and MDPs

tempestpy_adaptions
Lukas Posch 3 years ago
committed by Stefan Pranger
parent
commit
d3b0046fa0
  1. 3
      src/storm/modelchecker/helper/finitehorizon/SparseNondeterministicStepBoundedHorizonHelper.cpp
  2. 4
      src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp
  3. 9
      src/storm/solver/Multiplier.cpp

3
src/storm/modelchecker/helper/finitehorizon/SparseNondeterministicStepBoundedHorizonHelper.cpp

@ -20,10 +20,11 @@ namespace storm {
template<typename ValueType>
void SparseNondeterministicStepBoundedHorizonHelper<ValueType>::getMaybeStatesRowGroupSizes(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& maybeStates, std::vector<uint64_t>& maybeStatesRowGroupSizes, uint& choiceValuesCounter) {
std::vector<uint64_t> rowGroupIndices = transitionMatrix.getRowGroupIndices();
choiceValuesCounter = 0;
for(uint counter = 0; counter < maybeStates.size(); counter++) {
if(maybeStates.get(counter)) {
maybeStatesRowGroupSizes.push_back(rowGroupIndices.at(counter));
choiceValuesCounter += transitionMatrix.getRowGroupSize(counter);
maybeStatesRowGroupSizes.push_back(choiceValuesCounter);
}
}
}

4
src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp

@ -110,7 +110,9 @@ namespace storm {
}
// Create a multiplier for reduction.
auto multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, transitionMatrix);
multiplier->reduce(env, goal.direction(), b, transitionMatrix.getRowGroupIndices(), result, &statesOfCoalition);
auto rowGroupIndices = transitionMatrix.getRowGroupIndices();
rowGroupIndices.erase(rowGroupIndices.begin());
multiplier->reduce(env, goal.direction(), b, rowGroupIndices, result, &statesOfCoalition);
if (goal.isShieldingTask()) {
choiceValues = b;
}

9
src/storm/solver/Multiplier.cpp

@ -92,8 +92,13 @@ namespace storm {
template<typename ValueType>
void Multiplier<ValueType>::reduce(Environment const& env, OptimizationDirection const& dir, std::vector<ValueType> const& choiceValues, std::vector<storm::storage::SparseMatrix<double>::index_type> rowGroupIndices, std::vector<ValueType>& result, storm::storage::BitVector const* dirOverride) const {
auto choice_it = choiceValues.begin();
for(uint state = 0; state < rowGroupIndices.size() - 1; state++) {
uint rowGroupSize = rowGroupIndices[state + 1] - rowGroupIndices[state];
for(uint state = 0; state < rowGroupIndices.size(); state++) {
uint rowGroupSize;
if(state == 0) {
rowGroupSize = rowGroupIndices[state];
} else {
rowGroupSize = rowGroupIndices[state] - rowGroupIndices[state-1];
}
if(dirOverride != nullptr) {
if((dir == storm::OptimizationDirection::Minimize && !dirOverride->get(state)) || (dir == storm::OptimizationDirection::Maximize && dirOverride->get(state))) {
result.at(state) = *std::min_element(choice_it, choice_it + rowGroupSize);

Loading…
Cancel
Save