From e5dd9ab90f865ed73dc704c6f84c8f820493768a Mon Sep 17 00:00:00 2001 From: lukpo Date: Wed, 4 Aug 2021 15:40:37 +0200 Subject: [PATCH] small cleanup SparseSmgRpatlModelChecker --- .../modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp | 7 ------- src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h | 2 +- 2 files changed, 1 insertion(+), 8 deletions(-) diff --git a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp index 1668bc440..b03d89b3c 100644 --- a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp +++ b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp @@ -39,8 +39,6 @@ namespace storm { // Intentionally left empty. } - - template bool SparseSmgRpatlModelChecker::canHandleStatic(CheckTask const& checkTask, bool* requiresSingleInitialState) { storm::logic::Formula const& formula = checkTask.getFormula(); @@ -57,8 +55,6 @@ namespace storm { } } - - template std::unique_ptr SparseSmgRpatlModelChecker::checkGameFormula(Environment const& env, CheckTask const& checkTask) { Environment solverEnv = env; @@ -97,7 +93,6 @@ namespace storm { 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; } @@ -105,7 +100,6 @@ namespace storm { 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; } @@ -216,7 +210,6 @@ namespace storm { } else if (checkTask.isProduceSchedulersSet()) { result->asExplicitQuantitativeCheckResult().setScheduler(std::make_unique>(helper.extractScheduler())); } - return result; } diff --git a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h index a27e580c5..44b55f868 100644 --- a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h +++ b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h @@ -28,6 +28,7 @@ namespace storm { // The implemented methods of the AbstractModelChecker interface. bool canHandle(CheckTask const& checkTask) const override; + std::unique_ptr checkGameFormula(Environment const& env, CheckTask const& checkTask) override; std::unique_ptr checkProbabilityOperatorFormula(Environment const& env, CheckTask const& checkTask) override; std::unique_ptr checkRewardOperatorFormula(Environment const& env, CheckTask const& checkTask) override; @@ -44,7 +45,6 @@ namespace storm { 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); private: storm::storage::BitVector statesOfCoalition; };