diff --git a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp index 6c42b3e30..fbfcd796f 100644 --- a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp +++ b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp @@ -2,6 +2,8 @@ #include #include +#include +#include #include "storm/utility/macros.h" #include "storm/utility/FilteredRewardModel.h" @@ -12,6 +14,10 @@ #include "storm/modelchecker/helper/utility/SetInformationFromCheckTask.h" #include "storm/logic/FragmentSpecification.h" +#include "storm/logic/Coalition.h" + +#include "storm/storage/BitVector.h" +#include "storm/environment/solver/MultiplierEnvironment.h" #include "storm/models/sparse/StandardRewardModel.h" @@ -27,6 +33,8 @@ namespace storm { // Intentionally left empty. } + + template bool SparseSmgRpatlModelChecker::canHandleStatic(CheckTask const& checkTask, bool* requiresSingleInitialState) { storm::logic::Formula const& formula = checkTask.getFormula(); @@ -44,14 +52,46 @@ namespace storm { } } + + template std::unique_ptr SparseSmgRpatlModelChecker::checkGameFormula(Environment const& env, CheckTask const& checkTask) { storm::logic::GameFormula const& gameFormula = checkTask.getFormula(); storm::logic::Formula const& subFormula = gameFormula.getSubformula(); - if (subFormula.isOperatorFormula()) { - return this->checkStateFormula(env, checkTask.substituteFormula(subFormula.asStateFormula()).setPlayerCoalition(gameFormula.getCoalition())); + + if (subFormula.isRewardOperatorFormula()) { + return this->checkRewardOperatorFormula(solverEnv, checkTask.substituteFormula(subFormula.asRewardOperatorFormula())); + } else if (subFormula.isLongRunAverageOperatorFormula()) { + return this->checkLongRunAverageOperatorFormula(solverEnv, checkTask.substituteFormula(subFormula.asLongRunAverageOperatorFormula())); + } + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Cannot check this property (yet)."); + } + + template + std::unique_ptr SparseSmgRpatlModelChecker::checkRewardOperatorFormula(Environment const& env, CheckTask const& checkTask) { + storm::logic::RewardOperatorFormula const& formula = checkTask.getFormula(); + std::unique_ptr result = this->computeRewards(env, formula.getMeasureType(), checkTask.substituteFormula(formula.getSubformula())); + + return result; + } + + template + std::unique_ptr SparseSmgRpatlModelChecker::checkLongRunAverageOperatorFormula(Environment const& env, CheckTask const& checkTask) { + storm::logic::LongRunAverageOperatorFormula const& formula = checkTask.getFormula(); + std::unique_ptr result = this->computeLongRunAverageProbabilities(env, checkTask.substituteFormula(formula.getSubformula().asStateFormula())); + + return result; + } + + + + template + std::unique_ptr SparseSmgRpatlModelChecker::computeRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + storm::logic::Formula const& rewardFormula = checkTask.getFormula(); + if (rewardFormula.isLongRunAverageRewardFormula()) { + return this->computeLongRunAverageRewards(env, rewardMeasureType, checkTask.substituteFormula(rewardFormula.asLongRunAverageRewardFormula())); } - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Only game formulas with Operatorformulas as subformula are supported."); + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << rewardFormula << "' cannot (yet) be handled."); } template @@ -62,10 +102,15 @@ 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); - STORM_LOG_THROW(checkTask.isPlayerCoalitionSet(), storm::exceptions::InvalidPropertyException, "No player coalition was set."); - auto coalitionStates = this->getModel().computeStatesOfCoalition(checkTask.getPlayerCoalition()); - std::cout << "Found " << coalitionStates.getNumberOfSetBits() << " states in coalition." << std::endl; - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not implemented."); + storm::modelchecker::helper::SparseNondeterministicGameInfiniteHorizonHelper helper(this->getModel().getTransitionMatrix(), this->getModel().getPlayerActionIndices()); + storm::modelchecker::helper::setInformationFromCheckTaskNondeterministic(helper, checkTask, this->getModel()); + auto values = helper.computeLongRunAverageRewards(env, rewardModel.get()); + + std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(values))); + if (checkTask.isProduceSchedulersSet()) { + result->asExplicitQuantitativeCheckResult().setScheduler(std::make_unique>(helper.extractScheduler())); + } + return result; } template class SparseSmgRpatlModelChecker>;