From 7cbe2886eb7761aed9839e143ea9320636623131 Mon Sep 17 00:00:00 2001 From: lukpo Date: Tue, 20 Jul 2021 11:13:30 +0200 Subject: [PATCH] fixed shield handling for MDP Next and BoundedGlobally --- ...ndeterministicStepBoundedHorizonHelper.cpp | 61 ++++++++++++++++--- .../prctl/SparseMdpPrctlModelChecker.cpp | 13 ++-- .../prctl/helper/SparseMdpPrctlHelper.cpp | 33 ++-------- src/storm/solver/Multiplier.cpp | 3 - 4 files changed, 62 insertions(+), 48 deletions(-) diff --git a/src/storm/modelchecker/helper/finitehorizon/SparseNondeterministicStepBoundedHorizonHelper.cpp b/src/storm/modelchecker/helper/finitehorizon/SparseNondeterministicStepBoundedHorizonHelper.cpp index a37d11782..2340d9e76 100644 --- a/src/storm/modelchecker/helper/finitehorizon/SparseNondeterministicStepBoundedHorizonHelper.cpp +++ b/src/storm/modelchecker/helper/finitehorizon/SparseNondeterministicStepBoundedHorizonHelper.cpp @@ -63,18 +63,67 @@ namespace storm { if (lowerBound == 0) { if(goal.isShieldingTask()) { - multiplier->repeatedMultiplyAndReduceWithChoices(env, goal.direction(), subresult, &b, upperBound, nullptr, choiceValues, transitionMatrix.getRowGroupIndices()); + + std::vector::index_type> rowGroupIndices = transitionMatrix.getRowGroupIndices(); + std::vector::index_type> reducedRowGroupIndices; + uint sizeChoiceValues = 0; + for(uint counter = 0; counter < maybeStates.size(); counter++) { + if(maybeStates.get(counter)) { + sizeChoiceValues += transitionMatrix.getRowGroupSize(counter); + reducedRowGroupIndices.push_back(rowGroupIndices.at(counter)); + } + } + choiceValues = std::vector(sizeChoiceValues, storm::utility::zero()); + + multiplier->repeatedMultiplyAndReduceWithChoices(env, goal.direction(), subresult, &b, upperBound, nullptr, choiceValues, reducedRowGroupIndices); + + // fill up choicesValues for shields + std::vector allChoices = std::vector(transitionMatrix.getRowGroupIndices().at(transitionMatrix.getRowGroupIndices().size() - 1), storm::utility::zero()); + auto choice_it = choiceValues.begin(); + for(uint state = 0; state < transitionMatrix.getRowGroupIndices().size() - 1; state++) { + uint rowGroupSize = transitionMatrix.getRowGroupIndices().at(state + 1) - transitionMatrix.getRowGroupIndices().at(state); + if (maybeStates.get(state)) { + for(uint choice = 0; choice < rowGroupSize; choice++, choice_it++) { + allChoices.at(transitionMatrix.getRowGroupIndices().at(state) + choice) = *choice_it; + } + } + } + choiceValues = allChoices; } else { multiplier->repeatedMultiplyAndReduce(env, goal.direction(), subresult, &b, upperBound); } } else { if(goal.isShieldingTask()) { - multiplier->repeatedMultiplyAndReduceWithChoices(env, goal.direction(), subresult, &b, upperBound - lowerBound + 1, nullptr, choiceValues, transitionMatrix.getRowGroupIndices()); + std::vector::index_type> rowGroupIndices = transitionMatrix.getRowGroupIndices(); + std::vector::index_type> reducedRowGroupIndices; + uint sizeChoiceValues = 0; + for(uint counter = 0; counter < maybeStates.size(); counter++) { + if(maybeStates.get(counter)) { + sizeChoiceValues += transitionMatrix.getRowGroupSize(counter); + reducedRowGroupIndices.push_back(rowGroupIndices.at(counter)); + } + } + choiceValues = std::vector(sizeChoiceValues, storm::utility::zero()); + + multiplier->repeatedMultiplyAndReduceWithChoices(env, goal.direction(), subresult, &b, upperBound - lowerBound + 1, nullptr, choiceValues, reducedRowGroupIndices); storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, maybeStates, maybeStates, false); auto multiplier = storm::solver::MultiplierFactory().create(env, submatrix); b = std::vector(b.size(), storm::utility::zero()); - multiplier->repeatedMultiplyAndReduceWithChoices(env, goal.direction(), subresult, &b, lowerBound - 1, nullptr, choiceValues, transitionMatrix.getRowGroupIndices()); + multiplier->repeatedMultiplyAndReduceWithChoices(env, goal.direction(), subresult, &b, lowerBound - 1, nullptr, choiceValues, reducedRowGroupIndices); + + // fill up choicesValues for shields + std::vector allChoices = std::vector(transitionMatrix.getRowGroupIndices().at(transitionMatrix.getRowGroupIndices().size() - 1), storm::utility::zero()); + auto choice_it = choiceValues.begin(); + for(uint state = 0; state < transitionMatrix.getRowGroupIndices().size() - 1; state++) { + uint rowGroupSize = transitionMatrix.getRowGroupIndices().at(state + 1) - transitionMatrix.getRowGroupIndices().at(state); + if (maybeStates.get(state)) { + for(uint choice = 0; choice < rowGroupSize; choice++, choice_it++) { + allChoices.at(transitionMatrix.getRowGroupIndices().at(state) + choice) = *choice_it; + } + } + } + choiceValues = allChoices; } else { multiplier->repeatedMultiplyAndReduce(env, goal.direction(), subresult, &b, upperBound - lowerBound + 1); storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, maybeStates, maybeStates, false); @@ -90,11 +139,7 @@ namespace storm { storm::utility::vector::setVectorValues(result, psiStates, storm::utility::one()); } - //TODO: check if this works with nullptr as default for resultMaybeStates - if(!resultMaybeStates.empty()) - { - resultMaybeStates = maybeStates; - } + resultMaybeStates = maybeStates; return result; } diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index 39b2ea6e9..6ed39870f 100644 --- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -98,15 +98,13 @@ namespace storm { storm::modelchecker::helper::SparseNondeterministicStepBoundedHorizonHelper helper; std::vector numericResult; - //TODO: this does not work with nullptr as defaults for resultMaybeStates and choiceValues + //This works only with empty vectors, no nullptr storm::storage::BitVector resultMaybeStates; std::vector choiceValues; - //TODO: check the result for shields - if(checkTask.isShieldingTask()) { numericResult = helper.compute(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getNonStrictLowerBound(), pathFormula.getNonStrictUpperBound(), checkTask.getHint(), resultMaybeStates, choiceValues); - tempest::shields::createShield(std::make_shared>(this->getModel()), std::move(choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), std::move(resultMaybeStates), storm::storage::BitVector(resultMaybeStates.size(), false)); + tempest::shields::createShield(std::make_shared>(this->getModel()), std::move(choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), std::move(resultMaybeStates), storm::storage::BitVector(resultMaybeStates.size(), true)); } else { numericResult = helper.compute(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getNonStrictLowerBound(), pathFormula.getNonStrictUpperBound(), checkTask.getHint(), resultMaybeStates, choiceValues); } @@ -123,8 +121,7 @@ namespace storm { auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper::computeNextProbabilities(env, storm::solver::SolveGoal(this->getModel(), checkTask), checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector()); std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(ret.values))); if(checkTask.isShieldingTask()) { - //TODO: creating a shield for NEXT does not work - tempest::shields::createShield(std::make_shared>(this->getModel()), std::move(ret.choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), std::move(ret.maybeStates), storm::storage::BitVector(ret.maybeStates.size(), false)); + tempest::shields::createShield(std::make_shared>(this->getModel()), std::move(ret.choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), std::move(ret.maybeStates), storm::storage::BitVector(ret.maybeStates.size(), true)); } else if (checkTask.isProduceSchedulersSet() && ret.scheduler) { result->asExplicitQuantitativeCheckResult().setScheduler(std::move(ret.scheduler)); } @@ -142,7 +139,7 @@ namespace storm { auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper::computeUntilProbabilities(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), checkTask.isProduceSchedulersSet(), checkTask.getHint()); std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(ret.values))); if(checkTask.isShieldingTask()) { - tempest::shields::createShield(std::make_shared>(this->getModel()), std::move(ret.values), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), std::move(ret.maybeStates), storm::storage::BitVector(ret.maybeStates.size(), false)); + tempest::shields::createShield(std::make_shared>(this->getModel()), std::move(ret.choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), std::move(ret.maybeStates), storm::storage::BitVector(ret.maybeStates.size(), true)); } else if (checkTask.isProduceSchedulersSet() && ret.scheduler) { result->asExplicitQuantitativeCheckResult().setScheduler(std::move(ret.scheduler)); } @@ -158,7 +155,7 @@ namespace storm { auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper::computeGloballyProbabilities(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), checkTask.isProduceSchedulersSet()); std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(ret.values))); if(checkTask.isShieldingTask()) { - tempest::shields::createShield(std::make_shared>(this->getModel()), std::move(ret.values), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), std::move(ret.maybeStates), storm::storage::BitVector(ret.maybeStates.size(), false)); + tempest::shields::createShield(std::make_shared>(this->getModel()), std::move(ret.choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), std::move(ret.maybeStates), storm::storage::BitVector(ret.maybeStates.size(), true)); } else if (checkTask.isProduceSchedulersSet() && ret.scheduler) { result->asExplicitQuantitativeCheckResult().setScheduler(std::move(ret.scheduler)); } diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index 9ad693722..c80b5647f 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -637,14 +637,14 @@ namespace storm { } else { if (!qualitativeStateSets.maybeStates.empty()) { // In this case we have have to compute the remaining probabilities. - + // Obtain proper hint information either from the provided hint or from requirements of the solver. SparseMdpHintType hintInformation = computeHints(env, SolutionType::UntilProbabilities, hint, goal.direction(), transitionMatrix, backwardTransitions, qualitativeStateSets.maybeStates, phiStates, qualitativeStateSets.statesWithProbability1, produceScheduler); // Declare the components of the equation system we will solve. storm::storage::SparseMatrix submatrix; std::vector b; - + // If the hint information tells us that we have to eliminate MECs, we do so now. boost::optional> ecInformation; if (hintInformation.getEliminateEndComponents()) { @@ -671,9 +671,6 @@ namespace storm { } } if (goal.isShieldingTask()) { - STORM_LOG_DEBUG("SparseMdpPrctlHelper::computeUntilProbabilities: Before multiply()"); - STORM_LOG_DEBUG(result); - std::vector subResult; uint sizeChoiceValues = 0; for(uint counter = 0; counter < qualitativeStateSets.maybeStates.size(); counter++) { @@ -682,21 +679,9 @@ namespace storm { } } - STORM_LOG_DEBUG(subResult); - - - STORM_LOG_DEBUG(choiceValues); - //std::vector b_complete = transitionMatrix.getConstrainedRowGroupSumVector(storm::storage::BitVector(qualitativeStateSets.maybeStates.size(), true), qualitativeStateSets.statesWithProbability1); - submatrix = transitionMatrix.getSubmatrix(true, qualitativeStateSets.maybeStates, qualitativeStateSets.maybeStates, false); - - //STORM_LOG_DEBUG(b_complete); - auto sub_multiplier = storm::solver::MultiplierFactory().create(env, submatrix); - - sub_multiplier->multiply(env, subResult, &b, choiceValues); - STORM_LOG_DEBUG(choiceValues); std::vector allChoices = std::vector(transitionMatrix.getRowGroupIndices().at(transitionMatrix.getRowGroupIndices().size() - 1), storm::utility::zero()); auto choice_it = choiceValues.begin(); @@ -709,12 +694,6 @@ namespace storm { } } choiceValues = allChoices; - - STORM_LOG_DEBUG(choiceValues); - - - //TODO: fill up choiceValues with Zeros (dimension!) - } } } @@ -745,7 +724,6 @@ namespace storm { statesInPsiMecs.set(stateActionsPair.first, true); } } - return computeUntilProbabilities(env, std::move(goal), transitionMatrix, backwardTransitions, psiStates, statesInPsiMecs, qualitative, produceScheduler); } else { goal.oneMinus(); @@ -1150,7 +1128,7 @@ namespace storm { // Prepare resulting vector. std::vector result(transitionMatrix.getRowGroupCount(), storm::utility::zero()); - + // Determine which states have a reward that is infinity or less than infinity. QualitativeStateSetsReachabilityRewards qualitativeStateSets = getQualitativeStateSetsReachabilityRewards(goal, transitionMatrix, backwardTransitions, targetStates, hint, zeroRewardStatesGetter, zeroRewardChoicesGetter); @@ -1242,10 +1220,7 @@ namespace storm { STORM_LOG_ASSERT((!produceScheduler && !scheduler) || scheduler->isDeterministicScheduler(), "Expected a deterministic scheduler"); STORM_LOG_ASSERT((!produceScheduler && !scheduler) || scheduler->isMemorylessScheduler(), "Expected a memoryless scheduler"); - - //TODO: keep nullvector for choiceValues in computeReachabilityRewardsHelper? - nullptr causes ERROR - //std::vector choiceValues = std::vector(transitionMatrix.getRowCount(), storm::utility::zero()); - std::vector choiceValues = std::vector(); + std::vector choiceValues; return MDPSparseModelCheckingHelperReturnType(std::move(result), std::move(qualitativeStateSets.maybeStates), std::move(scheduler), std::move(choiceValues)); } diff --git a/src/storm/solver/Multiplier.cpp b/src/storm/solver/Multiplier.cpp index 0cc159e75..2324b7833 100644 --- a/src/storm/solver/Multiplier.cpp +++ b/src/storm/solver/Multiplier.cpp @@ -74,11 +74,8 @@ namespace storm { progress.setMaxCount(n); progress.startNewMeasurement(0); for (uint64_t i = 0; i < n; ++i) { - multiply(env, x, b, choiceValues); reduce(env, dir, choiceValues, rowGroupIndices, x); - - multiplyAndReduce(env, dir, x, b, x); if (storm::utility::resources::isTerminate()) { STORM_LOG_WARN("Aborting after " << i << " of " << n << " multiplications"); break;