From a9f03779483ee7d404ed616cda6a309385833410 Mon Sep 17 00:00:00 2001 From: sp Date: Thu, 7 Sep 2023 15:19:14 +0200 Subject: [PATCH] fixed incorrect handling of choiceValues in helper --- .../prctl/helper/SparseMdpPrctlHelper.cpp | 38 +++---------------- 1 file changed, 6 insertions(+), 32 deletions(-) diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index c1d0071e2..760cdce42 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -676,41 +676,15 @@ namespace storm { extractSchedulerChoices(*scheduler, resultForMaybeStates.getScheduler(), qualitativeStateSets.maybeStates); } } - if (goal.isShieldingTask()) { - std::vector subResult; - uint sizeChoiceValues = 0; - for(uint counter = 0; counter < qualitativeStateSets.maybeStates.size(); counter++) { - if(qualitativeStateSets.maybeStates.get(counter)) { - subResult.push_back(result.at(counter)); - } - } - - submatrix = transitionMatrix.getSubmatrix(true, qualitativeStateSets.maybeStates, qualitativeStateSets.maybeStates, false); - auto sub_multiplier = storm::solver::MultiplierFactory().create(env, submatrix); - sub_multiplier->multiply(env, subResult, &b, maybeStateChoiceValues); - - } } } - std::vector choiceValues = std::vector(transitionMatrix.getRowGroupIndices().at(transitionMatrix.getRowGroupIndices().size() - 1), storm::utility::zero()); - auto choice_it = maybeStateChoiceValues.begin(); - // TODO THIS IS BUGGY!! - for(uint state = 0; state < transitionMatrix.getRowGroupIndices().size() - 1; state++) { - uint rowGroupSize = transitionMatrix.getRowGroupIndices().at(state + 1) - transitionMatrix.getRowGroupIndices().at(state); - if (qualitativeStateSets.maybeStates.get(state)) { - for(uint choice = 0; choice < rowGroupSize; choice++, choice_it++) { - choiceValues.at(transitionMatrix.getRowGroupIndices().at(state) + choice) = *choice_it; - } - } else if (qualitativeStateSets.statesWithProbability0.get(state)) { - for(uint choice = 0; choice < rowGroupSize; choice++) { - choiceValues.at(transitionMatrix.getRowGroupIndices().at(state) + choice) = 0; - } - } else if (qualitativeStateSets.statesWithProbability1.get(state)) { - for(uint choice = 0; choice < rowGroupSize; choice++) { - choiceValues.at(transitionMatrix.getRowGroupIndices().at(state) + choice) = 1; - } - } + std::vector choiceValues; + if(goal.isShieldingTask()) { + choiceValues = std::vector(transitionMatrix.getRowGroupIndices().at(transitionMatrix.getRowGroupIndices().size() - 1), storm::utility::zero()); + std::vector b = std::vector(transitionMatrix.getRowCount(), storm::utility::zero()); + auto multiplier = storm::solver::MultiplierFactory().create(env, transitionMatrix); + multiplier->multiply(env, result, &b, choiceValues); } // Extend scheduler with choices for the states in the qualitative state sets.