From 40edc0ca4d51a78b94b27ba997cf620ca49babf5 Mon Sep 17 00:00:00 2001 From: TimQu Date: Fri, 1 Sep 2017 18:13:17 +0200 Subject: [PATCH] assert that there are no endcomponents with positive rewards --- .../rewardbounded/MultiDimensionalRewardUnfolding.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp index 4bd55afd9..f95ecb3ed 100644 --- a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp +++ b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp @@ -277,10 +277,10 @@ namespace storm { zeroObjRewardChoices &= storm::utility::vector::filterZero(objRewards); } - // todo - storm::storage::BitVector value0EStates(memoryProduct.getProduct().getNumberOfStates(), true); - - ecElimResult = storm::transformer::EndComponentEliminator::transform(epochModel.epochMatrix, storm::storage::BitVector(memoryProduct.getProduct().getNumberOfStates(), true), zeroObjRewardChoices & ~stepChoices, value0EStates); + storm::storage::BitVector allProductStates(memoryProduct.getProduct().getNumberOfStates(), true); + // We assume that there is no end component in which reward is earned + STORM_LOG_ASSERT(!storm::utility::graph::checkIfECWithChoiceExists(epochModel.epochMatrix, epochModel.epochMatrix.transpose(true), allProductStates, ~zeroObjRewardChoices & ~stepChoices), "There is a scheduler that yields infinite reward for one objective. This case should be excluded"); + ecElimResult = storm::transformer::EndComponentEliminator::transform(epochModel.epochMatrix, allProductStates, zeroObjRewardChoices & ~stepChoices, allProductStates); epochModel.epochMatrix = std::move(ecElimResult.matrix); epochModel.stepChoices = storm::storage::BitVector(epochModel.epochMatrix.getRowCount(), false);