produceShield: small fix, produceScheduler: implemented

src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp

@@ -114,16 +114,24 @@ namespace storm {
 
                 storm::modelchecker::helper::internal::SoundGameViHelper<ValueType> viHelper(submatrix, submatrix.transpose(), b, clippedStatesOfCoalition, clippedPsiStates, goal.direction());
 
+                if (produceScheduler) {
+                    viHelper.setProduceScheduler(true);
+                }
+
                 viHelper.performValueIteration(env, xL, xU, goal.direction(), constrainedChoiceValues);
 
                 viHelper.fillChoiceValuesVector(constrainedChoiceValues, relevantStates, transitionMatrix.getRowGroupIndices());
                 storm::utility::vector::setVectorValues(result, relevantStates, xL);
 
+                if (produceScheduler) {
+                    scheduler = std::make_unique<storm::storage::Scheduler<ValueType>>(expandScheduler(viHelper.extractScheduler(), psiStates, ~phiStates));
+                }
+
                 return SMGSparseModelCheckingHelperReturnType<ValueType>(std::move(result), std::move(relevantStates), std::move(scheduler), std::move(constrainedChoiceValues));
             }
 
             template<typename ValueType>
-            storm::storage::Scheduler<ValueType> SparseSmgRpatlHelper<ValueType>::expandScheduler(storm::storage::Scheduler<ValueType> scheduler, storm::storage::BitVector psiStates, storm::storage::BitVector notPhiStates) {
+            storm::storage::Scheduler<ValueType> SparseSmgRpatlHelper<ValueType>::expandScheduler(storm::storage::Scheduler<ValueType> scheduler, storm::storage::BitVector psiStates, storm::storage::BitVector notPhiStates, bool sound) {
                 storm::storage::Scheduler<ValueType> completeScheduler(psiStates.size());
                 uint_fast64_t maybeStatesCounter = 0;
                 uint schedulerSize = psiStates.size();
@@ -131,6 +139,9 @@ namespace storm {
                     // psiStates already fulfill formulae so we can set an arbitrary action
                     if(psiStates.get(stateCounter)) {
                         completeScheduler.setChoice(0, stateCounter);
+                        if (sound) {
+                            maybeStatesCounter++;
+                        }
                     // ~phiStates do not fulfill formulae so we can set an arbitrary action
                     } else if(notPhiStates.get(stateCounter)) {
                         completeScheduler.setChoice(0, stateCounter);
@@ -149,7 +160,7 @@ namespace storm {
                 storm::storage::BitVector notPsiStates = ~psiStates;
                 statesOfCoalition.complement();
 
-                auto result = computeUntilProbabilities(env, std::move(goal), transitionMatrix, backwardTransitions, storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true), notPsiStates, qualitative, statesOfCoalition, produceScheduler, hint);
+                auto result = computeUntilProbabilitiesSound(env, std::move(goal), transitionMatrix, backwardTransitions, storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true), notPsiStates, qualitative, statesOfCoalition, produceScheduler, hint);
                 for (auto& element : result.values) {
                     element = storm::utility::one<ValueType>() - element;
                 }

src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h

@@ -41,7 +41,7 @@ namespace storm {
                 static SMGSparseModelCheckingHelperReturnType<ValueType> computeBoundedGloballyProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint, uint64_t lowerBound, uint64_t upperBound);
                 static SMGSparseModelCheckingHelperReturnType<ValueType> computeBoundedUntilProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint, uint64_t lowerBound, uint64_t upperBound, bool computeBoundedGlobally = false);
             private:
-                static storm::storage::Scheduler<ValueType> expandScheduler(storm::storage::Scheduler<ValueType> scheduler, storm::storage::BitVector psiStates, storm::storage::BitVector notPhiStates);
+                static storm::storage::Scheduler<ValueType> expandScheduler(storm::storage::Scheduler<ValueType> scheduler, storm::storage::BitVector psiStates, storm::storage::BitVector notPhiStates, bool sound = false);
                 static void expandChoiceValues(std::vector<uint_fast64_t> const& rowGroupIndices, storm::storage::BitVector const& relevantStates, std::vector<ValueType> const& constrainedChoiceValues, std::vector<ValueType>& choiceValues);
             };
         }

src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp

@@ -50,7 +50,7 @@ namespace storm {
                     }
 
                     uint64_t iter = 0;
-                    constrainedChoiceValues = std::vector<ValueType>(xL.size(), storm::utility::zero<ValueType>());
+                    constrainedChoiceValues = std::vector<ValueType>(_transitionMatrix.getRowCount(), storm::utility::zero<ValueType>());
 
                     while (iter < maxIter) {
                         performIterationStep(env, dir);
@@ -73,10 +73,18 @@ namespace storm {
                     xL = xNewL();
                     xU = xNewU();
 
-                    /* if (isProduceSchedulerSet()) {
+                     if (isProduceSchedulerSet()) {
                         // We will be doing one more iteration step and track scheduler choices this time.
-                        performIterationStep(env, dir, &_producedOptimalChoices.get());
-                    } */
+                        _x1IsCurrent = !_x1IsCurrent;
+                        _multiplier->multiplyAndReduce(env, dir, xOldL(), nullptr, xNewL(), &_producedOptimalChoices.get(), &_statesOfCoalition);
+                        storm::storage::BitVector psiStates = _psiStates;
+                        auto xL_begin = xNewL().begin();
+                        std::for_each(xNewL().begin(), xNewL().end(), [&psiStates, &xL_begin](ValueType &it)
+                                      {
+                                          if (psiStates[&it - &(*xL_begin)])
+                                              it = 1;
+                                      });
+                    }
                 }
 
                 template <typename ValueType>
@@ -84,7 +92,6 @@ namespace storm {
                     storm::storage::BitVector reducedMinimizerActions = {storm::storage::BitVector(this->_transitionMatrix.getRowCount(), true)};
 
                     // under approximation
-                    auto start = std::chrono::steady_clock::now();
                     if (!_multiplier) {
                         prepareSolversAndMultipliers(env);
                     }
@@ -114,8 +121,6 @@ namespace storm {
                                   });
 
                     if (reducedMinimizerActions != _oldPolicy) { // new MECs only if Policy changed
-                        start = std::chrono::steady_clock::now();
-
                         // restricting the none optimal minimizer choices
                         _restrictedTransitions = this->_transitionMatrix.restrictRows(reducedMinimizerActions);