Browse Source

adapted to changes for Multiplier::reduce

tempestpy_adaptions
Stefan Pranger 3 years ago
parent
commit
7f5f6eeee0
  1. 2
      src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
  2. 2
      src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp

2
src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp

@ -146,7 +146,7 @@ namespace storm {
if(goal.isShieldingTask()) { if(goal.isShieldingTask()) {
multiplier->multiply(env, result, nullptr, choiceValues); multiplier->multiply(env, result, nullptr, choiceValues);
multiplier->reduce(env, goal.direction(), choiceValues, transitionMatrix.getRowGroupIndices(), result, nullptr);
multiplier->reduce(env, goal.direction(), transitionMatrix.getRowGroupIndices(), choiceValues, result);
} }
else { else {
multiplier->multiplyAndReduce(env, dir, result, nullptr, result); multiplier->multiplyAndReduce(env, dir, result, nullptr, result);

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

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

Loading…
Cancel
Save