diff --git a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp index 6dac7d1bb..c3cb606f2 100644 --- a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp +++ b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp @@ -73,8 +73,6 @@ namespace storm { statesOfCoalition = this->getModel().computeStatesOfCoalition(gameFormula.getCoalition()); statesOfCoalition.complement(); - STORM_LOG_DEBUG("\n" << this->getModel().getTransitionMatrix()); - if (subFormula.isRewardOperatorFormula()) { return this->checkRewardOperatorFormula(solverEnv, checkTask.substituteFormula(subFormula.asRewardOperatorFormula())); } else if (subFormula.isLongRunAverageOperatorFormula()) { @@ -151,7 +149,6 @@ 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()); - STORM_LOG_DEBUG(ret.values); std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(ret.values))); if(checkTask.isShieldingTask()) { tempest::shields::createShield(std::make_shared>(this->getModel()), std::move(ret.choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), std::move(ret.relevantStates), statesOfCoalition); @@ -212,6 +209,7 @@ namespace storm { template std::unique_ptr SparseSmgRpatlModelChecker::computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); + // TODO //STORM_LOG_THROW(checkTask.isPlayerCoalitionSet(), storm::exceptions::InvalidPropertyException, "No player coalition was set."); //auto coalitionStates = this->getModel().computeStatesOfCoalition(checkTask.getPlayerCoalition()); std::cout << "Found " << statesOfCoalition.getNumberOfSetBits() << " states in coalition." << std::endl; diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index 4b015093b..a57a0ccef 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -16,14 +16,11 @@ namespace storm { template 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 - auto solverEnv = env; solverEnv.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration, false); // Initialize the solution vector. std::vector x = std::vector(transitionMatrix.getRowGroupCount() - psiStates.getNumberOfSetBits(), storm::utility::zero()); - // Relevant states are those states which are phiStates and not PsiStates. storm::storage::BitVector relevantStates = phiStates & ~psiStates; @@ -44,6 +41,7 @@ namespace storm { } viHelper.performValueIteration(env, x, b, goal.direction()); + //if(goal.isShieldingTask()) { if(true) { viHelper.getChoiceValues(env, x, constrainedChoiceValues); } @@ -109,6 +107,8 @@ namespace storm { // create multiplier and execute the calculation for 1 step auto multiplier = storm::solver::MultiplierFactory().create(env, transitionMatrix); std::vector choiceValues = std::vector(transitionMatrix.getRowCount(), storm::utility::zero()); + + //if(goal.isShieldingTask()) { if (true) { multiplier->multiply(env, x, &b, choiceValues); } @@ -124,7 +124,6 @@ namespace storm { // Relevant states are safe states - the psiStates. storm::storage::BitVector relevantStates = psiStates; - STORM_LOG_DEBUG(relevantStates); // Initialize the solution vector. std::vector x = std::vector(relevantStates.getNumberOfSetBits(), storm::utility::one()); @@ -149,16 +148,16 @@ namespace storm { if(upperBound > 0) { viHelper.performValueIteration(env, x, goal.direction(), upperBound, constrainedChoiceValues); -/* if (produceScheduler) { - scheduler = std::make_unique>(expandScheduler(viHelper.extractScheduler(), relevantStates, ~relevantStates)); - - }*/ } viHelper.fillChoiceValuesVector(constrainedChoiceValues, relevantStates, transitionMatrix.getRowGroupIndices()); viHelper.fillResultVector(x, relevantStates); viHelper.fillChoiceValuesVector(constrainedChoiceValues, relevantStates, transitionMatrix.getRowGroupIndices()); - STORM_LOG_DEBUG(x); + + if (produceScheduler) { + scheduler = std::make_unique>(expandScheduler(viHelper.extractScheduler(), relevantStates, ~relevantStates)); + } + return SMGSparseModelCheckingHelperReturnType(std::move(x), std::move(relevantStates), std::move(scheduler), std::move(constrainedChoiceValues)); } diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h index eb4eaf0cd..5258104dc 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h @@ -34,8 +34,6 @@ namespace storm { template class SparseSmgRpatlHelper { public: - // TODO should probably be renamed in the future: - 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 SMGSparseModelCheckingHelperReturnType 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 SMGSparseModelCheckingHelperReturnType 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);