diff --git a/src/storm/modelchecker/prctl/helper/MDPModelCheckingHelperReturnType.h b/src/storm/modelchecker/prctl/helper/MDPModelCheckingHelperReturnType.h index 7a8c7b320..97efcc3bc 100644 --- a/src/storm/modelchecker/prctl/helper/MDPModelCheckingHelperReturnType.h +++ b/src/storm/modelchecker/prctl/helper/MDPModelCheckingHelperReturnType.h @@ -29,9 +29,6 @@ namespace storm { // The values computed for the states. std::vector values; - // The values computed for the available choices. - std::vector choiceValues; - // A scheduler, if it was computed. std::unique_ptr> scheduler; }; diff --git a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp index 6dff7e419..489720e3e 100644 --- a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp +++ b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp @@ -72,6 +72,8 @@ namespace storm { statesOfCoalition = this->getModel().computeStatesOfCoalition(gameFormula.getCoalition()); + STORM_LOG_DEBUG("\n" << this->getModel().getTransitionMatrix()); + if (subFormula.isRewardOperatorFormula()) { return this->checkRewardOperatorFormula(solverEnv, checkTask.substituteFormula(subFormula.asRewardOperatorFormula())); } else if (subFormula.isLongRunAverageOperatorFormula()) { @@ -148,12 +150,9 @@ namespace storm { ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); auto ret = storm::modelchecker::helper::SparseSmgRpatlHelper::computeUntilProbabilities(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), statesOfCoalition, checkTask.isProduceSchedulersSet(), checkTask.getHint()); - for(auto const& x : ret.values) { - STORM_LOG_DEBUG("v: " << x); - } std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(ret.values))); if(checkTask.isShieldingTask()) { - result->asExplicitQuantitativeCheckResult().setScheduler(std::make_unique>(tempest::shields::createShield(this->getModel().getTransitionMatrix().getRowGroupIndices(), {}, checkTask.getShieldingExpression(), statesOfCoalition))); + result->asExplicitQuantitativeCheckResult().setScheduler(std::make_unique>(tempest::shields::createShield(this->getModel().getTransitionMatrix().getRowGroupIndices(), std::move(ret.choiceValues), checkTask.getShieldingExpression(), std::move(ret.relevantStates), statesOfCoalition))); } else if (checkTask.isProduceSchedulersSet() && ret.scheduler) { result->asExplicitQuantitativeCheckResult().setScheduler(std::move(ret.scheduler)); } @@ -215,7 +214,7 @@ namespace storm { std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(values))); if(checkTask.isShieldingTask()) { - result->asExplicitQuantitativeCheckResult().setScheduler(std::make_unique>(tempest::shields::createShield(this->getModel().getTransitionMatrix().getRowGroupIndices(), {}, checkTask.getShieldingExpression(), coalitionStates))); + //result->asExplicitQuantitativeCheckResult().setScheduler(std::make_unique>(tempest::shields::createShield(this->getModel().getTransitionMatrix().getRowGroupIndices(), {}, checkTask.getShieldingExpression(), coalitionStates))); } else if (checkTask.isProduceSchedulersSet()) { result->asExplicitQuantitativeCheckResult().setScheduler(std::make_unique>(helper.extractScheduler())); } diff --git a/src/storm/modelchecker/rpatl/helper/SMGModelCheckingHelperReturnType.h b/src/storm/modelchecker/rpatl/helper/SMGModelCheckingHelperReturnType.h new file mode 100644 index 000000000..dafb673dc --- /dev/null +++ b/src/storm/modelchecker/rpatl/helper/SMGModelCheckingHelperReturnType.h @@ -0,0 +1,43 @@ +#pragma once + +#include +#include +#include "storm/storage/Scheduler.h" + +namespace storm { + namespace storage { + class BitVector; + } + + namespace modelchecker { + namespace helper { + template + struct SMGSparseModelCheckingHelperReturnType { + + SMGSparseModelCheckingHelperReturnType(SMGSparseModelCheckingHelperReturnType const&) = delete; + SMGSparseModelCheckingHelperReturnType(SMGSparseModelCheckingHelperReturnType&&) = default; + + SMGSparseModelCheckingHelperReturnType(std::vector&& values, storm::storage::BitVector& relevantStates, std::unique_ptr>&& scheduler = nullptr, std::vector&& choiceValues = nullptr) : values(std::move(values)), relevantStates(relevantStates), scheduler(std::move(scheduler)), choiceValues(std::move(choiceValues)) { + // Intentionally left empty. + } + + virtual ~SMGSparseModelCheckingHelperReturnType() { + // Intentionally left empty. + } + + // The values computed for the states. + std::vector values; + + // The relevant states for which choice values have been computed. + storm::storage::BitVector relevantStates; + + // A scheduler, if it was computed. + std::unique_ptr> scheduler; + + // The values computed for the available choices. + std::vector choiceValues; + }; + } + + } +} diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index ca6e53ea2..852dca578 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -14,7 +14,7 @@ namespace storm { namespace helper { template - MDPSparseModelCheckingHelperReturnType SparseSmgRpatlHelper::computeUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint) { + SMGSparseModelCheckingHelperReturnType SparseSmgRpatlHelper::computeUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix 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 @@ -28,6 +28,7 @@ namespace storm { storm::storage::BitVector relevantStates = phiStates & ~psiStates; std::vector b = transitionMatrix.getConstrainedRowGroupSumVector(relevantStates, psiStates); + std::vector constrainedChoiceValues = std::vector(b.size(), storm::utility::zero()); // Reduce the matrix to relevant states storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, relevantStates, relevantStates, false); @@ -43,12 +44,15 @@ namespace storm { } viHelper.performValueIteration(env, x, b, goal.direction()); + if(true) { + viHelper.getChoiceValues(env, x, constrainedChoiceValues); + } viHelper.fillResultVector(x, relevantStates, psiStates); if (produceScheduler) { scheduler = std::make_unique>(expandScheduler(viHelper.extractScheduler(), psiStates, ~phiStates)); } - return MDPSparseModelCheckingHelperReturnType(std::move(x), std::move(scheduler)); + return SMGSparseModelCheckingHelperReturnType(std::move(x), relevantStates, std::move(scheduler), std::move(constrainedChoiceValues)); } template diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h index e6a36f2af..83e99423b 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h @@ -10,6 +10,7 @@ #include "storm/solver/SolveGoal.h" #include "storm/modelchecker/prctl/helper/MDPModelCheckingHelperReturnType.h" +#include "storm/modelchecker/rpatl/helper/SMGModelCheckingHelperReturnType.h" namespace storm { @@ -36,13 +37,14 @@ namespace storm { public: // TODO should probably be renamed in the future: - static MDPSparseModelCheckingHelperReturnType computeUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix 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 SMGSparseModelCheckingHelperReturnType computeUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix 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 computeGloballyProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint = ModelCheckerHint()); static MDPSparseModelCheckingHelperReturnType computeNextProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint); static MDPSparseModelCheckingHelperReturnType computeBoundedGloballyProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint, uint64_t lowerBound, uint64_t upperBound); private: static storm::storage::Scheduler expandScheduler(storm::storage::Scheduler scheduler, storm::storage::BitVector psiStates, storm::storage::BitVector notPhiStates); + static void expandChoiceValues(std::vector const& rowGroupIndices, storm::storage::BitVector const& relevantStates, std::vector const& constrainedChoiceValues, std::vector& choiceValues); }; } diff --git a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp index e0fd4eee8..5c3d95f12 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp @@ -134,8 +134,7 @@ namespace storm { } template - void GameViHelper::fillResultVector(std::vector& result, storm::storage::BitVector relevantStates, storm::storage::BitVector psiStates) - { + void GameViHelper::fillResultVector(std::vector& result, storm::storage::BitVector relevantStates, storm::storage::BitVector psiStates) { std::vector filledVector = std::vector(relevantStates.size(), storm::utility::zero()); uint bitIndex = 0; for(uint i = 0; i < filledVector.size(); i++) { @@ -184,6 +183,11 @@ namespace storm { return scheduler; } + template + void GameViHelper::getChoiceValues(Environment const& env, std::vector const& x, std::vector& choiceValues) { + _multiplier->multiply(env, x, &_b, choiceValues); + } + template std::vector& GameViHelper::xNew() { return _x1IsCurrent ? _x1 : _x2; diff --git a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h index 3a1343f90..d541bcd8e 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h +++ b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h @@ -42,6 +42,7 @@ namespace storm { storm::storage::Scheduler extractScheduler() const; + void getChoiceValues(Environment const& env, std::vector const& x, std::vector& choiceValues); private: void performIterationStep(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector* choices = nullptr);