From 1599034b5c00acf003e16973b04c6864fd2d7edb Mon Sep 17 00:00:00 2001 From: lukpo Date: Tue, 20 Jul 2021 15:15:18 +0200 Subject: [PATCH] fixed shield handling --- .../prctl/SparseMdpPrctlModelChecker.cpp | 7 +++- .../prctl/helper/SparseMdpPrctlHelper.cpp | 42 +++++++++++-------- 2 files changed, 31 insertions(+), 18 deletions(-) diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index 6ed39870f..dfc23481d 100644 --- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -108,6 +108,7 @@ namespace storm { } 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); } + STORM_LOG_DEBUG(numericResult); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } } @@ -119,6 +120,7 @@ namespace storm { std::unique_ptr subResultPointer = this->check(env, pathFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper::computeNextProbabilities(env, storm::solver::SolveGoal(this->getModel(), checkTask), checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector()); + STORM_LOG_DEBUG(ret.values); std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(ret.values))); if(checkTask.isShieldingTask()) { 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)); @@ -137,6 +139,7 @@ namespace storm { ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); 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()); + STORM_LOG_DEBUG(ret.values); std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(ret.values))); if(checkTask.isShieldingTask()) { 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)); @@ -153,9 +156,11 @@ namespace storm { std::unique_ptr subResultPointer = this->check(env, pathFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); 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()); + STORM_LOG_DEBUG(ret.values); std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(ret.values))); if(checkTask.isShieldingTask()) { - 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)); + STORM_LOG_DEBUG(ret.choiceValues); + tempest::shields::createShield(std::make_shared>(this->getModel()), std::move(ret.choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(),subResult.getTruthValuesVector(), 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 c80b5647f..11f3bcaca 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -603,7 +603,7 @@ namespace storm { // We need to identify the maybe states (states which have a probability for satisfying the until formula // that is strictly between 0 and 1) and the states that satisfy the formula with probablity 1 and 0, respectively. QualitativeStateSetsUntilProbabilities qualitativeStateSets = getQualitativeStateSetsUntilProbabilities(goal, transitionMatrix, backwardTransitions, phiStates, psiStates, hint); - + STORM_LOG_INFO("Preprocessing: " << qualitativeStateSets.statesWithProbability1.getNumberOfSetBits() << " states with probability 1, " << qualitativeStateSets.statesWithProbability0.getNumberOfSetBits() << " with probability 0 (" << qualitativeStateSets.maybeStates.getNumberOfSetBits() << " states remaining)."); // Set values of resulting vector that are known exactly. @@ -621,14 +621,14 @@ namespace storm { // create multiplier and execute the calculation for 1 additional step auto multiplier = storm::solver::MultiplierFactory().create(env, transitionMatrix); - uint sizeChoiceValues = 0; + uint sizeMaybeStateChoiceValues = 0; for(uint counter = 0; counter < qualitativeStateSets.maybeStates.size(); counter++) { if(qualitativeStateSets.maybeStates.get(counter)) { - sizeChoiceValues += transitionMatrix.getRowGroupSize(counter); + sizeMaybeStateChoiceValues += transitionMatrix.getRowGroupSize(counter); } } - std::vector choiceValues = std::vector(sizeChoiceValues, storm::utility::zero()); + std::vector maybeStateChoiceValues = std::vector(sizeMaybeStateChoiceValues, storm::utility::zero()); // Check whether we need to compute exact probabilities for some states. if (qualitative || maybeStatesNotRelevant || !goal.isShieldingTask()) { @@ -681,19 +681,27 @@ namespace storm { submatrix = transitionMatrix.getSubmatrix(true, qualitativeStateSets.maybeStates, qualitativeStateSets.maybeStates, false); auto sub_multiplier = storm::solver::MultiplierFactory().create(env, submatrix); - sub_multiplier->multiply(env, subResult, &b, choiceValues); - - 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 (qualitativeStateSets.maybeStates.get(state)) { - for(uint choice = 0; choice < rowGroupSize; choice++, choice_it++) { - allChoices.at(transitionMatrix.getRowGroupIndices().at(state) + choice) = *choice_it; - } - } - } - choiceValues = allChoices; + 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(); + 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; } } }