From ea90c1ac7d96c766c1e4569bb601d3f5c46eeab5 Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Tue, 22 Dec 2020 16:30:40 +0100 Subject: [PATCH] added and finalized methods for rpatlMC --- .../rpatl/SparseSmgRpatlModelChecker.cpp | 65 +++++++++++-------- .../rpatl/SparseSmgRpatlModelChecker.h | 14 ++-- 2 files changed, 47 insertions(+), 32 deletions(-) diff --git a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp index a6c230625..3b217030e 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" @@ -14,6 +16,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" @@ -30,10 +36,11 @@ namespace storm { // Intentionally left empty. } + + template 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 { @@ -51,21 +58,22 @@ 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 + Environment solverEnv = env; + coalitionIndicator(solverEnv, checkTask); + 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())); + return this->checkRewardOperatorFormula(solverEnv, checkTask.substituteFormula(subFormula.asRewardOperatorFormula())); } else if (subFormula.isLongRunAverageOperatorFormula()) { - return this->checkLongRunAverageOperatorFormula(env, checkTask.substituteFormula(subFormula.asLongRunAverageOperatorFormula())); + return this->checkLongRunAverageOperatorFormula(solverEnv, checkTask.substituteFormula(subFormula.asLongRunAverageOperatorFormula())); } - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "checkGameFormula NYI"); + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Cannot check this property (yet)."); } template @@ -73,26 +81,26 @@ namespace storm { storm::logic::RewardOperatorFormula const& formula = checkTask.getFormula(); std::unique_ptr result = this->computeRewards(env, formula.getMeasureType(), checkTask.substituteFormula(formula.getSubformula())); - return nullptr; + return result; } 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())); - } - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << rewardFormula << "' is invalid."); + 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 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. + 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::InvalidArgumentException, "The given formula '" << rewardFormula << "' cannot (yet) be handled."); } template @@ -107,9 +115,15 @@ namespace storm { 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"); + std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(values))); + if (checkTask.isProduceSchedulersSet()) { + result->asExplicitQuantitativeCheckResult().setScheduler(std::make_unique>(helper.extractScheduler())); + } + return result; + } + + + template void SparseSmgRpatlModelChecker::coalitionIndicator(Environment& env, CheckTask const& checkTask) { storm::storage::BitVector coalitionIndicators(this->getModel().getTransitionMatrix().getRowGroupCount()); @@ -143,7 +157,6 @@ namespace storm { 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 0927fc618..9a194dbb7 100644 --- a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h +++ b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h @@ -25,12 +25,14 @@ namespace storm { static bool canHandleStatic(CheckTask const& checkTask, bool* requiresSingleInitialState = nullptr); // 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; + bool canHandle(CheckTask const& checkTask) const override; + std::unique_ptr checkGameFormula(Environment const& env, CheckTask const& checkTask) override; + std::unique_ptr checkRewardOperatorFormula(Environment const& env, CheckTask const& checkTask) override; + std::unique_ptr checkLongRunAverageOperatorFormula(Environment const& env, CheckTask const& checkTask) override; + + std::unique_ptr computeRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; + std::unique_ptr computeLongRunAverageProbabilities(Environment const& env, CheckTask const& checkTask) override; + std::unique_ptr computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; void coalitionIndicator(Environment& env, CheckTask const& checkTask); };