fixed shield handling

src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp

@@ -108,6 +108,7 @@ namespace storm {
                 } else {
                     numericResult = helper.compute(env, storm::solver::SolveGoal<ValueType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getNonStrictLowerBound<uint64_t>(), pathFormula.getNonStrictUpperBound<uint64_t>(), checkTask.getHint(), resultMaybeStates, choiceValues);
                 }
+                STORM_LOG_DEBUG(numericResult);
                 return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
             }
         }
@@ -119,6 +120,7 @@ namespace storm {
             std::unique_ptr<CheckResult> subResultPointer = this->check(env, pathFormula.getSubformula());
             ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult();
             auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeNextProbabilities(env, storm::solver::SolveGoal<ValueType>(this->getModel(), checkTask), checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector());
+            STORM_LOG_DEBUG(ret.values);
             std::unique_ptr<CheckResult> result(new ExplicitQuantitativeCheckResult<ValueType>(std::move(ret.values)));
             if(checkTask.isShieldingTask()) {
                 tempest::shields::createShield<ValueType>(std::make_shared<storm::models::sparse::Mdp<ValueType>>(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<ValueType>::computeUntilProbabilities(env, storm::solver::SolveGoal<ValueType>(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<CheckResult> result(new ExplicitQuantitativeCheckResult<ValueType>(std::move(ret.values)));
             if(checkTask.isShieldingTask()) {
                 tempest::shields::createShield<ValueType>(std::make_shared<storm::models::sparse::Mdp<ValueType>>(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<CheckResult> subResultPointer = this->check(env, pathFormula.getSubformula());
             ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult();
             auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeGloballyProbabilities(env, storm::solver::SolveGoal<ValueType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), checkTask.isProduceSchedulersSet());
+            STORM_LOG_DEBUG(ret.values);
             std::unique_ptr<CheckResult> result(new ExplicitQuantitativeCheckResult<ValueType>(std::move(ret.values)));
             if(checkTask.isShieldingTask()) {
-                tempest::shields::createShield<ValueType>(std::make_shared<storm::models::sparse::Mdp<ValueType>>(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<ValueType>(std::make_shared<storm::models::sparse::Mdp<ValueType>>(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<ValueType>().setScheduler(std::move(ret.scheduler));
             }

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<ValueType>().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<ValueType> choiceValues = std::vector<ValueType>(sizeChoiceValues, storm::utility::zero<ValueType>());
+                std::vector<ValueType> maybeStateChoiceValues = std::vector<ValueType>(sizeMaybeStateChoiceValues, storm::utility::zero<ValueType>());
                 
                 // 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<ValueType>().create(env, submatrix);
-                            sub_multiplier->multiply(env, subResult, &b, choiceValues);
-
-                            std::vector<ValueType> allChoices = std::vector<ValueType>(transitionMatrix.getRowGroupIndices().at(transitionMatrix.getRowGroupIndices().size() - 1), storm::utility::zero<ValueType>());
-                            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<ValueType> choiceValues = std::vector<ValueType>(transitionMatrix.getRowGroupIndices().at(transitionMatrix.getRowGroupIndices().size() - 1), storm::utility::zero<ValueType>());
+                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;
                         }
                     }
                 }