diff --git a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp
index 35464513d..e3f5d46fd 100644
--- a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp
+++ b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp
@@ -12,6 +12,7 @@
#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "storm/modelchecker/results/ExplicitParetoCurveCheckResult.h"
+#include "storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h"
#include "storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.h"
#include "storm/modelchecker/helper/utility/SetInformationFromCheckTask.h"
@@ -54,8 +55,6 @@ namespace storm {
}
}
-
-
template<typename SparseSmgModelType>
std::unique_ptr<CheckResult> SparseSmgRpatlModelChecker<SparseSmgModelType>::checkGameFormula(Environment const& env, CheckTask<storm::logic::GameFormula, ValueType> const& checkTask) {
Environment solverEnv = env;
@@ -69,10 +68,25 @@ namespace storm {
return this->checkRewardOperatorFormula(solverEnv, checkTask.substituteFormula(subFormula.asRewardOperatorFormula()));
} else if (subFormula.isLongRunAverageOperatorFormula()) {
return this->checkLongRunAverageOperatorFormula(solverEnv, checkTask.substituteFormula(subFormula.asLongRunAverageOperatorFormula()));
+ } else if (subFormula.isProbabilityOperatorFormula()) {
+ return this->checkProbabilityOperatorFormula(solverEnv, checkTask.substituteFormula(subFormula.asProbabilityOperatorFormula()));
}
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Cannot check this property (yet).");
}
+ template<typename ModelType>
+ std::unique_ptr<CheckResult> SparseSmgRpatlModelChecker<ModelType>::checkProbabilityOperatorFormula(Environment const& env, CheckTask<storm::logic::ProbabilityOperatorFormula, ValueType> const& checkTask) {
+ storm::logic::ProbabilityOperatorFormula const& stateFormula = checkTask.getFormula();
+ std::unique_ptr<CheckResult> result = this->computeProbabilities(env, checkTask.substituteFormula(stateFormula.getSubformula()));
+
+ if (checkTask.isBoundSet()) {
+ STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException, "Unable to perform comparison operation on non-quantitative result.");
+ return result->asQuantitativeCheckResult<ValueType>().compareAgainstBound(checkTask.getBoundComparisonType(), checkTask.getBoundThreshold());
+ } else {
+ return result;
+ }
+ }
+
template<typename ModelType>
std::unique_ptr<CheckResult> SparseSmgRpatlModelChecker<ModelType>::checkRewardOperatorFormula(Environment const& env, CheckTask<storm::logic::RewardOperatorFormula, ValueType> const& checkTask) {
storm::logic::RewardOperatorFormula const& formula = checkTask.getFormula();
@@ -89,7 +103,14 @@ namespace storm {
return result;
}
-
+ template<typename ModelType>
+ std::unique_ptr<CheckResult> SparseSmgRpatlModelChecker<ModelType>::computeProbabilities(Environment const& env, CheckTask<storm::logic::Formula, ValueType> const& checkTask) {
+ storm::logic::Formula const& formula = checkTask.getFormula();
+ if (formula.isReachabilityProbabilityFormula()) {
+ return this->computeReachabilityProbabilities(env, checkTask.substituteFormula(formula.asReachabilityProbabilityFormula()));
+ }
+ STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << formula << "' is invalid.");
+ }
template<typename ModelType>
std::unique_ptr<CheckResult> SparseSmgRpatlModelChecker<ModelType>::computeRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::Formula, ValueType> const& checkTask) {
@@ -100,6 +121,25 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << rewardFormula << "' cannot (yet) be handled.");
}
+ template<typename ModelType>
+ std::unique_ptr<CheckResult> SparseSmgRpatlModelChecker<ModelType>::computeUntilProbabilities(Environment const& env, CheckTask<storm::logic::UntilFormula, ValueType> const& checkTask) {
+ // Currently we only support computation of reachability probabilities, i.e. the left subformula will always be 'true' (for now).
+ storm::logic::UntilFormula 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> leftResultPointer = this->check(env, pathFormula.getLeftSubformula());
+ 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)));
+ if (checkTask.isProduceSchedulersSet() && ret.scheduler) {
+ result->asExplicitQuantitativeCheckResult<ValueType>().setScheduler(std::move(ret.scheduler));
+ }
+ 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");
@@ -119,41 +159,6 @@ namespace storm {
return result;
}
-
-
- //template<typename SparseSmgModelType>
- //void SparseSmgRpatlModelChecker<SparseSmgModelType>::coalitionIndicator(Environment& env, CheckTask<storm::logic::GameFormula, ValueType> const& checkTask) {
- // storm::storage::BitVector coalitionIndicators(this->getModel().getTransitionMatrix().getRowGroupCount());
-
- // std::vector<boost::variant<std::string, uint_fast64_t>> formulaPlayerIds = checkTask.getFormula().getCoalition().getPlayers();
- // std::vector<uint_fast64_t> playerIds;
- // std::vector<std::pair<std::string, uint_fast64_t>> playerActionIndices = this->getModel().getStatePlayerIndications();
-
- // for(auto const& player : formulaPlayerIds) {
- // // If the player is given via the player name we have to look up its index
- // if(player.type() == typeid(std::string)) {
- // auto it = std::find_if(playerActionIndices.begin(), playerActionIndices.end(),
- // [&player](const std::pair<std::string, uint_fast64_t>& element){ return element.first == boost::get<std::string>(player); });
- // playerIds.push_back(it->second);
- // // If the player is given by its index we have to shift it to match internal mappings
- // } else if(player.type() == typeid(uint_fast64_t)) {
- // playerIds.push_back(boost::get<uint_fast64_t>(player) - 1);
- // }
- // }
- // //for(auto const& p : playerActionIndices) std::cout << p.first << " - " << p.second << ", "; std::cout << std::endl;
- // //for(auto const& p : playerIds) std::cout << p << ", "; std::cout << std::endl;
-
- // for(uint i = 0; i < playerActionIndices.size(); i++) {
- // if(std::find(playerIds.begin(), playerIds.end(), playerActionIndices.at(i).second) != playerIds.end()) {
- // coalitionIndicators.set(i);
- // }
- // }
- // coalitionIndicators.complement();
-
- // //std::cout << "MINMAX OVERRIDE: " << coalitionIndicators << std::endl;
- // env.solver().multiplier().setOptimizationDirectionOverride(coalitionIndicators);
- //}
-
template class SparseSmgRpatlModelChecker<storm::models::sparse::Smg<double>>;
#ifdef STORM_HAVE_CARL
template class SparseSmgRpatlModelChecker<storm::models::sparse::Smg<storm::RationalNumber>>;
diff --git a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h
index 9f5889caf..dfbd47762 100644
--- a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h
+++ b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h
@@ -29,10 +29,14 @@ namespace storm {
// The implemented methods of the AbstractModelChecker interface.
bool canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const override;
std::unique_ptr<CheckResult> checkGameFormula(Environment const& env, CheckTask<storm::logic::GameFormula, ValueType> const& checkTask) override;
+ std::unique_ptr<CheckResult> checkProbabilityOperatorFormula(Environment const& env, CheckTask<storm::logic::ProbabilityOperatorFormula, ValueType> const& checkTask) override;
std::unique_ptr<CheckResult> checkRewardOperatorFormula(Environment const& env, CheckTask<storm::logic::RewardOperatorFormula, ValueType> const& checkTask) override;
std::unique_ptr<CheckResult> checkLongRunAverageOperatorFormula(Environment const& env, CheckTask<storm::logic::LongRunAverageOperatorFormula, ValueType> const& checkTask) override;
+ std::unique_ptr<CheckResult> computeProbabilities(Environment const& env, CheckTask<storm::logic::Formula, ValueType> const& checkTask) override;
std::unique_ptr<CheckResult> computeRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::Formula, ValueType> const& checkTask) override;
+
+ std::unique_ptr<CheckResult> computeUntilProbabilities(Environment const& env, CheckTask<storm::logic::UntilFormula, 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;
diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp
new file mode 100644
index 000000000..9bf5a10e8
--- /dev/null
+++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp
@@ -0,0 +1,97 @@
+#include "SparseSmgRpatlHelper.h"
+
+#include "storm/environment/Environment.h"
+#include "storm/environment/solver/MultiplierEnvironment.h"
+#include "storm/environment/solver/MinMaxSolverEnvironment.h"
+#include "storm/solver/MinMaxLinearEquationSolver.h"
+#include "storm/utility/vector.h"
+
+#include "storm/modelchecker/rpatl/helper/internal/GameViHelper.h"
+
+
+namespace storm {
+ namespace modelchecker {
+ namespace helper {
+
+ template<typename ValueType>
+ MDPSparseModelCheckingHelperReturnType<ValueType> SparseSmgRpatlHelper<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) {
+ // TODO add Kwiatkowska original reference
+ // TODO FIX solver min max mess
+
+ 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() - psiStates.getNumberOfSetBits(), storm::utility::zero<ValueType>());
+ std::vector<ValueType> b = transitionMatrix.getConstrainedRowGroupSumVector(~psiStates, psiStates);
+
+ // Reduce matrix to ~Prob1 states-
+ //STORM_LOG_DEBUG("\n" << transitionMatrix);
+ storm::storage::SparseMatrix<ValueType> submatrix = transitionMatrix.getSubmatrix(true, ~psiStates, ~psiStates, false);
+ //STORM_LOG_DEBUG("\n" << submatrix);
+
+
+ //STORM_LOG_DEBUG("x = " << storm::utility::vector::toString(x));
+ //STORM_LOG_DEBUG("b = " << storm::utility::vector::toString(b));
+
+ storm::storage::BitVector clippedStatesOfCoalition(statesOfCoalition.size() - psiStates.getNumberOfSetBits());
+ //STORM_LOG_DEBUG(psiStates);
+ //STORM_LOG_DEBUG(statesOfCoalition);
+ //STORM_LOG_DEBUG(clippedStatesOfCoalition);
+
+ // TODO move this to BitVector-class
+ auto clippedStatesCounter = 0;
+ for(uint i = 0; i < psiStates.size(); i++) {
+ std::cout << i << " : " << psiStates.get(i) << " -> " << statesOfCoalition[i] << std::endl;
+ if(!psiStates.get(i)) {
+ clippedStatesOfCoalition.set(clippedStatesCounter, statesOfCoalition[i]);
+ clippedStatesCounter++;
+ }
+ }
+ //STORM_LOG_DEBUG(clippedStatesOfCoalition);
+ clippedStatesOfCoalition.complement();
+ //STORM_LOG_DEBUG(clippedStatesOfCoalition);
+
+ storm::modelchecker::helper::internal::GameViHelper<ValueType> viHelper(submatrix, clippedStatesOfCoalition);
+ std::unique_ptr<storm::storage::Scheduler<ValueType>> scheduler;
+ if (produceScheduler) {
+ viHelper.setProduceScheduler(true);
+ }
+
+ viHelper.performValueIteration(env, x, b, goal.direction());
+
+ STORM_LOG_DEBUG(storm::utility::vector::toString(x));
+ if (produceScheduler) {
+ scheduler = std::make_unique<storm::storage::Scheduler<ValueType>>(expandScheduler(viHelper.extractScheduler(), psiStates));
+ STORM_LOG_DEBUG("IsPartial?" << scheduler->isPartialScheduler());
+ }
+ return MDPSparseModelCheckingHelperReturnType<ValueType>(std::move(x), std::move(scheduler));
+ }
+
+ template<typename ValueType>
+ storm::storage::Scheduler<ValueType> SparseSmgRpatlHelper<ValueType>::expandScheduler(storm::storage::Scheduler<ValueType> scheduler, storm::storage::BitVector psiStates) {
+ //STORM_LOG_DEBUG(psiStates.size());
+ for(uint i = 0; i < 2; i++) {
+ //STORM_LOG_DEBUG(scheduler.getChoice(i));
+ }
+ storm::storage::Scheduler<ValueType> completeScheduler(psiStates.size());
+ uint_fast64_t maybeStatesCounter = 0;
+ for(uint stateCounter = 0; stateCounter < psiStates.size(); stateCounter++) {
+ //STORM_LOG_DEBUG(stateCounter << " : " << psiStates.get(stateCounter));
+ if(psiStates.get(stateCounter)) {
+ completeScheduler.setChoice(0, stateCounter);
+ } else {
+ completeScheduler.setChoice(scheduler.getChoice(maybeStatesCounter), stateCounter);
+ maybeStatesCounter++;
+ }
+ }
+ return completeScheduler;
+ }
+
+ template class SparseSmgRpatlHelper<double>;
+#ifdef STORM_HAVE_CARL
+ template class SparseSmgRpatlHelper<storm::RationalNumber>;
+#endif
+ }
+ }
+}
diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h
new file mode 100644
index 000000000..9505bd51f
--- /dev/null
+++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h
@@ -0,0 +1,47 @@
+#pragma once
+
+#include <vector>
+
+#include "storm/modelchecker/hints/ModelCheckerHint.h"
+#include "storm/modelchecker/prctl/helper/SolutionType.h"
+#include "storm/storage/SparseMatrix.h"
+
+#include "storm/utility/solver.h"
+#include "storm/solver/SolveGoal.h"
+
+#include "storm/modelchecker/prctl/helper/MDPModelCheckingHelperReturnType.h"
+
+namespace storm {
+
+ class Environment;
+
+ namespace storage {
+ class BitVector;
+ }
+
+ namespace models {
+ namespace sparse {
+ template <typename ValueType>
+ class StandardRewardModel;
+ }
+ }
+
+ namespace modelchecker {
+ class CheckResult;
+
+ namespace helper {
+
+ template <typename ValueType>
+ class SparseSmgRpatlHelper {
+ public:
+ // TODO should probably be renamed in the future:
+
+ 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());
+
+ private:
+ static storm::storage::Scheduler<ValueType> expandScheduler(storm::storage::Scheduler<ValueType> scheduler, storm::storage::BitVector psiStates);
+
+ };
+ }
+ }
+}
diff --git a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp
new file mode 100644
index 000000000..4f6fc1e4e
--- /dev/null
+++ b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp
@@ -0,0 +1,198 @@
+#include "GameViHelper.h"
+
+#include "storm/environment/Environment.h"
+#include "storm/environment/solver/SolverEnvironment.h"
+#include "storm/environment/solver/GameSolverEnvironment.h"
+
+
+#include "storm/utility/SignalHandler.h"
+#include "storm/utility/vector.h"
+
+// TODO this will undergo major refactoring as soon as we implement model checking of further properties
+
+namespace storm {
+ namespace modelchecker {
+ namespace helper {
+ namespace internal {
+
+ template <typename ValueType>
+ GameViHelper<ValueType>::GameViHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector statesOfCoalition) : _transitionMatrix(transitionMatrix), _statesOfCoalition(statesOfCoalition) {
+ }
+
+ template <typename ValueType>
+ void GameViHelper<ValueType>::prepareSolversAndMultipliersReachability(const Environment& env) {
+ // TODO we get whole transitionmatrix and psistates DONE IN smgrpatlhelper
+ // -> clip statesofcoalition
+ // -> compute b vector from psiStates
+ // -> clip transitionmatrix and create multiplier
+ _multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, _transitionMatrix);
+ _multiplier->setOptimizationDirectionOverride(_statesOfCoalition);
+
+ _x1IsCurrent = false;
+ }
+
+ template <typename ValueType>
+ void GameViHelper<ValueType>::performValueIteration(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());
+ }
+
+ uint64_t iter = 0;
+ std::vector<ValueType> result = x;
+ while (iter < maxIter) {
+ ++iter;
+ performIterationStep(env, dir);
+
+ if (checkConvergence(precision)) {
+ break;
+ }
+ if (storm::utility::resources::isTerminate()) {
+ break;
+ }
+ }
+ x = xNew();
+
+ if (isProduceSchedulerSet()) {
+ // We will be doing one more iteration step and track scheduler choices this time.
+ performIterationStep(env, dir, &_producedOptimalChoices.get());
+ }
+ }
+
+ template <typename ValueType>
+ void GameViHelper<ValueType>::performIterationStep(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector<uint64_t>* choices) {
+ if (!_multiplier) {
+ prepareSolversAndMultipliersReachability(env);
+ }
+ _x1IsCurrent = !_x1IsCurrent;
+
+ // multiplyandreducegaussseidel
+ // Ax + b
+ if (choices == nullptr) {
+ //STORM_LOG_DEBUG("\n" << _transitionMatrix);
+ //STORM_LOG_DEBUG("xOld = " << storm::utility::vector::toString(xOld()));
+ //STORM_LOG_DEBUG("b = " << storm::utility::vector::toString(_b));
+ //STORM_LOG_DEBUG("xNew = " << storm::utility::vector::toString(xNew()));
+ _multiplier->multiplyAndReduce(env, dir, xOld(), &_b, xNew());
+ //std::cin.get();
+ } else {
+ // Also keep track of the choices made.
+ _multiplier->multiplyAndReduce(env, dir, xOld(), &_b, xNew(), choices);
+ }
+
+ // compare applyPointwise
+ storm::utility::vector::applyPointwise<ValueType, ValueType, ValueType>(xOld(), xNew(), xNew(), [&dir] (ValueType const& a, ValueType const& b) -> ValueType {
+ if(storm::solver::maximize(dir)) {
+ if(a > b) return a;
+ else return b;
+ } else {
+ if(a > b) return a;
+ else return b;
+ }
+ });
+ }
+
+ template <typename ValueType>
+ bool GameViHelper<ValueType>::checkConvergence(ValueType threshold) const {
+ STORM_LOG_ASSERT(_multiplier, "tried to check for convergence without doing an iteration first.");
+
+ // Now check whether the currently produced results are precise enough
+ STORM_LOG_ASSERT(threshold > storm::utility::zero<ValueType>(), "Did not expect a non-positive threshold.");
+ auto x1It = xOld().begin();
+ auto x1Ite = xOld().end();
+ auto x2It = xNew().begin();
+ ValueType maxDiff = (*x2It - *x1It);
+ ValueType minDiff = maxDiff;
+ // The difference between maxDiff and minDiff is zero at this point. Thus, it doesn't make sense to check the threshold now.
+ for (++x1It, ++x2It; x1It != x1Ite; ++x1It, ++x2It) {
+ ValueType diff = (*x2It - *x1It);
+ // Potentially update maxDiff or minDiff
+ bool skipCheck = false;
+ if (maxDiff < diff) {
+ maxDiff = diff;
+ } else if (minDiff > diff) {
+ minDiff = diff;
+ } else {
+ skipCheck = true;
+ }
+ // Check convergence
+ if (!skipCheck && (maxDiff - minDiff) > threshold) {
+ return false;
+ }
+ }
+ // TODO needs checking
+ return true;
+ }
+
+ template <typename ValueType>
+ void GameViHelper<ValueType>::setProduceScheduler(bool value) {
+ _produceScheduler = value;
+ }
+
+ template <typename ValueType>
+ bool GameViHelper<ValueType>::isProduceSchedulerSet() const {
+ return _produceScheduler;
+ }
+
+ template <typename ValueType>
+ std::vector<uint64_t> const& GameViHelper<ValueType>::getProducedOptimalChoices() const {
+ STORM_LOG_ASSERT(this->isProduceSchedulerSet(), "Trying to get the produced optimal choices although no scheduler was requested.");
+ STORM_LOG_ASSERT(this->_producedOptimalChoices.is_initialized(), "Trying to get the produced optimal choices but none were available. Was there a computation call before?");
+ return this->_producedOptimalChoices.get();
+ }
+
+ template <typename ValueType>
+ std::vector<uint64_t>& GameViHelper<ValueType>::getProducedOptimalChoices() {
+ STORM_LOG_ASSERT(this->isProduceSchedulerSet(), "Trying to get the produced optimal choices although no scheduler was requested.");
+ STORM_LOG_ASSERT(this->_producedOptimalChoices.is_initialized(), "Trying to get the produced optimal choices but none were available. Was there a computation call before?");
+ return this->_producedOptimalChoices.get();
+ }
+
+ template <typename ValueType>
+ storm::storage::Scheduler<ValueType> GameViHelper<ValueType>::extractScheduler() const{
+ auto const& optimalChoices = getProducedOptimalChoices();
+ storm::storage::Scheduler<ValueType> scheduler(optimalChoices.size());
+ for (uint64_t state = 0; state < optimalChoices.size(); ++state) {
+ scheduler.setChoice(optimalChoices[state], state);
+ }
+ return scheduler;
+ }
+
+ template <typename ValueType>
+ std::vector<ValueType>& GameViHelper<ValueType>::xNew() {
+ return _x1IsCurrent ? _x1 : _x2;
+ }
+
+ template <typename ValueType>
+ std::vector<ValueType> const& GameViHelper<ValueType>::xNew() const {
+ return _x1IsCurrent ? _x1 : _x2;
+ }
+
+ template <typename ValueType>
+ std::vector<ValueType>& GameViHelper<ValueType>::xOld() {
+ return _x1IsCurrent ? _x2 : _x1;
+ }
+
+ template <typename ValueType>
+ std::vector<ValueType> const& GameViHelper<ValueType>::xOld() const {
+ return _x1IsCurrent ? _x2 : _x1;
+ }
+
+ template class GameViHelper<double>;
+#ifdef STORM_HAVE_CARL
+ template class GameViHelper<storm::RationalNumber>;
+#endif
+ }
+ }
+ }
+}
diff --git a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h
new file mode 100644
index 000000000..92f963851
--- /dev/null
+++ b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h
@@ -0,0 +1,77 @@
+#pragma once
+
+#include "storm/storage/SparseMatrix.h"
+#include "storm/solver/LinearEquationSolver.h"
+#include "storm/solver/MinMaxLinearEquationSolver.h"
+#include "storm/solver/Multiplier.h"
+
+namespace storm {
+ class Environment;
+
+ namespace storage {
+ template <typename VT> class Scheduler;
+ }
+
+ namespace modelchecker {
+ namespace helper {
+ namespace internal {
+
+ template <typename ValueType>
+ class GameViHelper {
+ public:
+ GameViHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector statesOfCoalition);
+
+ void prepareSolversAndMultipliersReachability(const Environment& env);
+
+ void performValueIteration(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
+ */
+ void setProduceScheduler(bool value);
+
+ /*!
+ * @return whether an optimal scheduler shall be constructed during the computation
+ */
+ 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);
+
+ /*!
+ * Checks whether the curently computed value achieves the desired precision
+ */
+ bool checkConvergence(ValueType precision) const;
+
+ std::vector<ValueType>& xNew();
+ std::vector<ValueType> const& xNew() const;
+
+ std::vector<ValueType>& xOld();
+ std::vector<ValueType> const& xOld() const;
+ bool _x1IsCurrent;
+
+ /*!
+ * @pre before calling this, a computation call should have been performed during which scheduler production was enabled.
+ * @return the produced scheduler of the most recent call.
+ */
+ std::vector<uint64_t> const& getProducedOptimalChoices() const;
+
+ /*!
+ * @pre before calling this, a computation call should have been performed during which scheduler production was enabled.
+ * @return the produced scheduler of the most recent call.
+ */
+ std::vector<uint64_t>& getProducedOptimalChoices();
+
+ storm::storage::SparseMatrix<ValueType> _transitionMatrix;
+ storm::storage::BitVector _statesOfCoalition;
+ std::vector<ValueType> _x1, _x2, _b;
+ std::unique_ptr<storm::solver::Multiplier<ValueType>> _multiplier;
+
+ bool _produceScheduler = false;
+ boost::optional<std::vector<uint64_t>> _producedOptimalChoices;
+ };
+ }
+ }
+ }
+}