Browse Source

Fixed flagging objectives for reward finiteness check incorrectly

tempestpy_adaptions
Tim Quatmann 4 years ago
parent
commit
ed1a5b6ced
  1. 2
      src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.cpp

2
src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.cpp

@ -584,7 +584,6 @@ namespace storm {
for (uint64_t i = 0; i < formula.getDimension(); ++i) { for (uint64_t i = 0; i < formula.getDimension(); ++i) {
auto oldTbr = formula.getTimeBoundReference(i); auto oldTbr = formula.getTimeBoundReference(i);
if (oldTbr.isRewardBound()) { if (oldTbr.isRewardBound()) {
onlyRewardBounds = false;
if (oldTbr.hasRewardAccumulation()) { if (oldTbr.hasRewardAccumulation()) {
auto filteredBoundRewards = storm::utility::createFilteredRewardModel(data.model->getRewardModel(oldTbr.getRewardName()), oldTbr.getRewardAccumulation(), data.model->isDiscreteTimeModel()); auto filteredBoundRewards = storm::utility::createFilteredRewardModel(data.model->getRewardModel(oldTbr.getRewardName()), oldTbr.getRewardAccumulation(), data.model->isDiscreteTimeModel());
if (filteredBoundRewards.isDifferentFromUnfilteredModel()) { if (filteredBoundRewards.isDifferentFromUnfilteredModel()) {
@ -599,6 +598,7 @@ namespace storm {
newTimeBoundReferences.push_back(oldTbr); newTimeBoundReferences.push_back(oldTbr);
} }
} else { } else {
onlyRewardBounds = false;
newTimeBoundReferences.push_back(oldTbr); newTimeBoundReferences.push_back(oldTbr);
} }
} }

Loading…
Cancel
Save