start with next formulae

src/storm/logic/FragmentSpecification.cpp

@@ -67,6 +67,7 @@ namespace storm {
             rpatl.setReachabilityProbabilityFormulasAllowed(true);
             rpatl.setUntilFormulasAllowed(true);
             rpatl.setGloballyFormulasAllowed(true);
+            rpatl.setNextFormulasAllowed(true);
 
             return rpatl;
         }

src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp

@@ -114,6 +114,8 @@ namespace storm {
                 return this->computeUntilProbabilities(env, checkTask.substituteFormula(formula.asUntilFormula()));
             } else if (formula.isGloballyFormula()) {
                 return this->computeGloballyProbabilities(env, checkTask.substituteFormula(formula.asGloballyFormula()));
+            } else if (formula.isNextFormula()) {
+                return this->computeNextProbabilities(env, checkTask.substituteFormula(formula.asNextFormula()));
             }
             STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << formula << "' is invalid.");
         }
@@ -136,7 +138,6 @@ namespace storm {
             std::unique_ptr<CheckResult> rightResultPointer = this->check(env, pathFormula.getRightSubformula());
             ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult();
             ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult();
-            storm::solver::SolveGoal<ValueType> foo(this->getModel(), checkTask);
 
             auto ret = storm::modelchecker::helper::SparseSmgRpatlHelper<ValueType>::computeUntilProbabilities(env, storm::solver::SolveGoal<ValueType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), statesOfCoalition, checkTask.isProduceSchedulersSet(), checkTask.getHint());
             std::unique_ptr<CheckResult> result(new ExplicitQuantitativeCheckResult<ValueType>(std::move(ret.values)));
@@ -160,7 +161,19 @@ namespace storm {
             return result;
         }
 
-            template<typename SparseSmgModelType>
+        template<typename ModelType>
+        std::unique_ptr<CheckResult> SparseSmgRpatlModelChecker<ModelType>::computeNextProbabilities(Environment const& env, CheckTask<storm::logic::NextFormula, ValueType> const& checkTask) {
+            storm::logic::NextFormula const& pathFormula = checkTask.getFormula();
+            STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
+            std::unique_ptr<CheckResult> subResultPointer = this->check(env, pathFormula.getSubformula());
+            ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult();
+
+            auto ret = storm::modelchecker::helper::SparseSmgRpatlHelper<ValueType>::computeNextProbabilities(env, storm::solver::SolveGoal<ValueType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), statesOfCoalition, checkTask.isProduceSchedulersSet(), checkTask.getHint());
+            std::unique_ptr<CheckResult> result(new ExplicitQuantitativeCheckResult<ValueType>(std::move(ret.values)));
+            return result;
+        }
+
+        template<typename SparseSmgModelType>
         std::unique_ptr<CheckResult> SparseSmgRpatlModelChecker<SparseSmgModelType>::computeLongRunAverageProbabilities(Environment const& env, CheckTask<storm::logic::StateFormula, ValueType> const& checkTask) {
             STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "NYI");
         }

src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h

@@ -38,6 +38,8 @@ namespace storm {
 
             std::unique_ptr<CheckResult> computeUntilProbabilities(Environment const& env, CheckTask<storm::logic::UntilFormula, ValueType> const& checkTask) override;
             std::unique_ptr<CheckResult> computeGloballyProbabilities(Environment const& env, CheckTask<storm::logic::GloballyFormula, ValueType> const& checkTask) override;
+            std::unique_ptr<CheckResult> computeNextProbabilities(Environment const& env, CheckTask<storm::logic::NextFormula, ValueType> const& checkTask) override;
+
             std::unique_ptr<CheckResult> computeLongRunAverageProbabilities(Environment const& env, CheckTask<storm::logic::StateFormula, ValueType> const& checkTask) override;
             std::unique_ptr<CheckResult> computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::LongRunAverageRewardFormula, ValueType> const& checkTask) override;
 

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

@@ -85,6 +85,37 @@ namespace storm {
                 return result;
             }
 
+            template<typename ValueType>
+            MDPSparseModelCheckingHelperReturnType<ValueType> SparseSmgRpatlHelper<ValueType>::computeNextProbabilities(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) {
+
+                auto solverEnv = env;
+                solverEnv.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration, false);
+
+                // Initialize the solution vector.
+                std::vector<ValueType> x = std::vector<ValueType>(transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
+
+                auto allStates = storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true);
+
+                std::vector<ValueType> b = transitionMatrix.getConstrainedRowGroupSumVector(allStates, psiStates);
+
+                storm::storage::BitVector clippedStatesOfCoalition(transitionMatrix.getRowGroupCount());
+                clippedStatesOfCoalition.setClippedStatesOfCoalition(allStates, statesOfCoalition);
+                clippedStatesOfCoalition.complement();
+
+                storm::modelchecker::helper::internal::GameViHelper<ValueType> viHelper(transitionMatrix, clippedStatesOfCoalition);
+                std::unique_ptr<storm::storage::Scheduler<ValueType>> scheduler;
+                if (produceScheduler) {
+                    viHelper.setProduceScheduler(true);
+                }
+
+                viHelper.performNextIteration(env, x, b, goal.direction());
+
+                if (produceScheduler) {
+                    scheduler = std::make_unique<storm::storage::Scheduler<ValueType>>(expandScheduler(viHelper.extractScheduler(), psiStates, ~allStates));
+                }
+                return MDPSparseModelCheckingHelperReturnType<ValueType>(std::move(x), std::move(scheduler));
+            }
+
             template class SparseSmgRpatlHelper<double>;
 #ifdef STORM_HAVE_CARL
             template class SparseSmgRpatlHelper<storm::RationalNumber>;

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

@@ -38,6 +38,7 @@ namespace storm {
 
                 static MDPSparseModelCheckingHelperReturnType<ValueType> computeUntilProbabilities(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 = ModelCheckerHint());
                 static MDPSparseModelCheckingHelperReturnType<ValueType> computeGloballyProbabilities(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 = ModelCheckerHint());
+                static MDPSparseModelCheckingHelperReturnType<ValueType> computeNextProbabilities(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);
 
             private:
                 static storm::storage::Scheduler<ValueType> expandScheduler(storm::storage::Scheduler<ValueType> scheduler, storm::storage::BitVector psiStates, storm::storage::BitVector notPhiStates);

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

@@ -151,6 +151,31 @@ namespace storm {
                 }
 
                 template <typename ValueType>
+                void GameViHelper<ValueType>::performNextIteration(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> b, storm::solver::OptimizationDirection const dir) {
+                    prepareSolversAndMultipliersReachability(env);
+                    ValueType precision = storm::utility::convertNumber<ValueType>(env.solver().game().getPrecision());
+                    uint64_t maxIter = env.solver().game().getMaximalNumberOfIterations();
+                    _b = b;
+
+                    _x1.assign(_transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
+                    _x2 = _x1;
+
+                    if (this->isProduceSchedulerSet()) {
+                        if (!this->_producedOptimalChoices.is_initialized()) {
+                            this->_producedOptimalChoices.emplace();
+                        }
+                        this->_producedOptimalChoices->resize(this->_transitionMatrix.getRowGroupCount());
+                    }
+
+                    if (isProduceSchedulerSet()) {
+                        performIterationStep(env, dir, &_producedOptimalChoices.get());
+                    } else
+                        performIterationStep(env, dir);
+
+                    x = xNew();
+                }
+
+                        template <typename ValueType>
                 void GameViHelper<ValueType>::setProduceScheduler(bool value) {
                     _produceScheduler = value;
                 }

src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h

@@ -30,6 +30,8 @@ namespace storm {
                      */
                     void fillResultVector(std::vector<ValueType>& result, storm::storage::BitVector relevantStates, storm::storage::BitVector psiStates);
 
+                    void performNextIteration(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> b, storm::solver::OptimizationDirection const dir);
+
                     /*h
                      * Sets whether an optimal scheduler shall be constructed during the computation
                      */
@@ -41,6 +43,7 @@ namespace storm {
                     bool isProduceSchedulerSet() const;
 
                     storm::storage::Scheduler<ValueType> extractScheduler() const;
+
                 private:
                     void performIterationStep(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector<uint64_t>* choices = nullptr);