fixed choiceValues for MDP shields - Until and Globally

src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp

@@ -102,6 +102,8 @@ namespace storm {
                 storm::storage::BitVector resultMaybeStates;
                 std::vector<ValueType> choiceValues;
 
+                //TODO: check the result for shields
+
                 if(checkTask.isShieldingTask()) {
                     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);
                     tempest::shields::createShield<ValueType>(std::make_shared<storm::models::sparse::Mdp<ValueType>>(this->getModel()), std::move(choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), std::move(resultMaybeStates), storm::storage::BitVector(resultMaybeStates.size(), false));
@@ -121,7 +123,8 @@ namespace storm {
             auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeNextProbabilities(env, storm::solver::SolveGoal<ValueType>(this->getModel(), checkTask), checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector());
             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.values), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), std::move(ret.maybeStates), storm::storage::BitVector(ret.maybeStates.size(), false));
+                //TODO: creating a shield for NEXT does not work
+                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(), false));
             } else if (checkTask.isProduceSchedulersSet() && ret.scheduler) {
                 result->asExplicitQuantitativeCheckResult<ValueType>().setScheduler(std::move(ret.scheduler));
             }

src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp

@@ -620,10 +620,18 @@ namespace storm {
 
                 // create multiplier and execute the calculation for 1 additional step
                 auto multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, transitionMatrix);
-                std::vector<ValueType> choiceValues = std::vector<ValueType>(transitionMatrix.getRowCount(), storm::utility::zero<ValueType>());
+
+                uint sizeChoiceValues = 0;
+                for(uint counter = 0; counter < qualitativeStateSets.maybeStates.size(); counter++) {
+                    if(qualitativeStateSets.maybeStates.get(counter)) {
+                        sizeChoiceValues += transitionMatrix.getRowGroupSize(counter);
+                    }
+                }
+
+                std::vector<ValueType> choiceValues = std::vector<ValueType>(sizeChoiceValues, storm::utility::zero<ValueType>());
                 
                 // Check whether we need to compute exact probabilities for some states.
-                if (qualitative || maybeStatesNotRelevant) {
+                if (qualitative || maybeStatesNotRelevant || !goal.isShieldingTask()) {
                     // Set the values for all maybe-states to 0.5 to indicate that their probability values are neither 0 nor 1.
                     storm::utility::vector::setVectorValues<ValueType>(result, qualitativeStateSets.maybeStates, storm::utility::convertNumber<ValueType>(0.5));
                 } else {
@@ -663,8 +671,50 @@ namespace storm {
                             }
                         }
                         if (goal.isShieldingTask()) {
-                            multiplier->multiply(env, result, &b, choiceValues);
-                            multiplier->reduce(env, goal.direction(), choiceValues, transitionMatrix.getRowGroupIndices(), result, nullptr);
+                            STORM_LOG_DEBUG("SparseMdpPrctlHelper<ValueType>::computeUntilProbabilities: Before multiply()");
+                            STORM_LOG_DEBUG(result);
+
+                            std::vector<ValueType> subResult;
+                            uint sizeChoiceValues = 0;
+                            for(uint counter = 0; counter < qualitativeStateSets.maybeStates.size(); counter++) {
+                                if(qualitativeStateSets.maybeStates.get(counter)) {
+                                    subResult.push_back(result.at(counter));
+                                }
+                            }
+
+                            STORM_LOG_DEBUG(subResult);
+
+
+                            STORM_LOG_DEBUG(choiceValues);
+                            //std::vector<ValueType> 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<ValueType>().create(env, submatrix);
+
+
+                            sub_multiplier->multiply(env, subResult, &b, choiceValues);
+                            STORM_LOG_DEBUG(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;
+
+                            STORM_LOG_DEBUG(choiceValues);
+
+
+                            //TODO: fill up choiceValues with Zeros (dimension!)
+
                         }
                     }
                 }
@@ -703,6 +753,9 @@ namespace storm {
                     for (auto& element : result.values) {
                         element = storm::utility::one<ValueType>() - element;
                     }
+                    for (auto& choice : result.choiceValues) {
+                        choice = storm::utility::one<ValueType>() - choice;
+                    }
                     return result;
                 }
             }