From 6c0cbe622ff345914e5d4f483ec71ebb1a661865 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Wed, 13 Jan 2021 12:55:04 +0100 Subject: [PATCH] Polished SparseSmgRpatlModelChecker --- .../rpatl/SparseSmgRpatlModelChecker.cpp | 61 +++---------------- .../rpatl/SparseSmgRpatlModelChecker.h | 1 - 2 files changed, 10 insertions(+), 52 deletions(-) diff --git a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp index f6161fac2..e9243c79d 100644 --- a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp +++ b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp @@ -34,11 +34,7 @@ namespace storm { bool SparseSmgRpatlModelChecker::canHandleStatic(CheckTask const& checkTask, bool* requiresSingleInitialState) { storm::logic::Formula const& formula = checkTask.getFormula(); - if (formula.isInFragment(storm::logic::rpatl().setCoalitionOperatorsAllowed(true).setRewardOperatorsAllowed(true).setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setLongRunAverageOperatorsAllowed(true))) { - return true; - } else { - return false; - } + return formula.isInFragment(storm::logic::rpatl()); } template @@ -53,69 +49,32 @@ namespace storm { template std::unique_ptr SparseSmgRpatlModelChecker::checkGameFormula(Environment const& env, CheckTask const& checkTask) { - STORM_LOG_DEBUG("checkGameFormula matrix: " << this->getModel().getTransitionMatrix().getDimensionsAsString()); - STORM_LOG_DEBUG("checkGameFormula playerindices:"); - STORM_LOG_DEBUG("checkGameFormula matrix: \n" << this->getModel().getTransitionMatrix()); - // TODO set min max row groups w.r.t. coalition storm::logic::GameFormula const& gameFormula = checkTask.getFormula(); storm::logic::Formula const& subFormula = gameFormula.getSubformula(); - STORM_LOG_DEBUG(gameFormula); - if (subFormula.isRewardOperatorFormula()) { - return this->checkRewardOperatorFormula(env, checkTask.substituteFormula(subFormula.asRewardOperatorFormula())); - } else if (subFormula.isLongRunAverageOperatorFormula()) { - return this->checkLongRunAverageOperatorFormula(env, checkTask.substituteFormula(subFormula.asLongRunAverageOperatorFormula())); - } - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "checkGameFormula NYI"); - } - - 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 nullptr; - } - - template - std::unique_ptr AbstractModelChecker::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())); + if (subFormula.isOperatorFormula()) { + return this->checkStateFormula(env, checkTask.substituteFormula(subFormula.asStateFormula()).setPlayerCoalition(gameFormula.getCoalition())); } - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << rewardFormula << "' is invalid."); - } - - template - std::unique_ptr AbstractModelChecker::checkLongRunAverageOperatorFormula(Environment const& env, CheckTask const& checkTask) { - storm::logic::LongRunAverageOperatorFormula const& formula = checkTask.getFormula(); - //STORM_LOG_THROW(formula.getSubformula().isStateFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid."); - - std::unique_ptr result = this->computeLongRunAverageProbabilities(env, checkTask.substituteFormula(formula.getSubformula().asStateFormula())); - - return result; //TODO check bounds. + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Only game formulas with Operatorformulas as subformula are supported."); } template std::unique_ptr SparseSmgRpatlModelChecker::computeLongRunAverageProbabilities(Environment const& env, CheckTask const& checkTask) { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "NYI"); + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not implemented."); } 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::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)); - //return result; - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "NYI"); + 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."); + } template class SparseSmgRpatlModelChecker>; #ifdef STORM_HAVE_CARL template class SparseSmgRpatlModelChecker>; - //template class SparseSmgRpatlModelChecker>; TODO are we going to need this? #endif } } diff --git a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h index 91bb09206..abf3243a5 100644 --- a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h +++ b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h @@ -27,7 +27,6 @@ namespace storm { // The implemented methods of the AbstractModelChecker interface. virtual bool canHandle(CheckTask const& checkTask) const override; virtual std::unique_ptr checkGameFormula(Environment const& env, CheckTask const& checkTask) override; - virtual std::unique_ptr checkRewardOperatorFormula(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeLongRunAverageProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override;