From 3a12b1cc103a709645bc9afa6150130d71553088 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Mon, 9 Aug 2021 15:22:22 +0200 Subject: [PATCH] Model Checkers: Reduced code duplications by using a single `computeStateFormulaProbabilities` method Conflicts: src/storm/modelchecker/AbstractModelChecker.h src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp --- src/storm/modelchecker/AbstractModelChecker.cpp | 16 +++++++++++++++- src/storm/modelchecker/AbstractModelChecker.h | 2 +- .../prctl/HybridDtmcPrctlModelChecker.cpp | 8 -------- .../prctl/HybridDtmcPrctlModelChecker.h | 1 - .../prctl/HybridMdpPrctlModelChecker.cpp | 9 --------- .../prctl/HybridMdpPrctlModelChecker.h | 1 - .../prctl/SparseDtmcPrctlModelChecker.cpp | 8 -------- .../prctl/SparseDtmcPrctlModelChecker.h | 1 - .../prctl/SparseMdpPrctlModelChecker.cpp | 9 --------- .../prctl/SparseMdpPrctlModelChecker.h | 1 - .../prctl/SymbolicDtmcPrctlModelChecker.cpp | 8 -------- .../prctl/SymbolicDtmcPrctlModelChecker.h | 1 - .../prctl/SymbolicMdpPrctlModelChecker.cpp | 10 ---------- .../prctl/SymbolicMdpPrctlModelChecker.h | 1 - 14 files changed, 16 insertions(+), 60 deletions(-) diff --git a/src/storm/modelchecker/AbstractModelChecker.cpp b/src/storm/modelchecker/AbstractModelChecker.cpp index fc1534585..5fb9fa6e0 100644 --- a/src/storm/modelchecker/AbstractModelChecker.cpp +++ b/src/storm/modelchecker/AbstractModelChecker.cpp @@ -2,6 +2,9 @@ #include "storm/modelchecker/results/QualitativeCheckResult.h" #include "storm/modelchecker/results/QuantitativeCheckResult.h" +#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" +#include "storm/modelchecker/results/SymbolicQuantitativeCheckResult.h" + #include "storm/utility/constants.h" #include "storm/utility/macros.h" #include "storm/exceptions/NotImplementedException.h" @@ -11,6 +14,7 @@ #include "storm/environment/Environment.h" +#include "storm/models/ModelRepresentation.h" #include "storm/models/sparse/Dtmc.h" #include "storm/models/sparse/Ctmc.h" #include "storm/models/sparse/Mdp.h" @@ -142,7 +146,17 @@ namespace storm { template std::unique_ptr AbstractModelChecker::computeStateFormulaProbabilities(Environment const& env, CheckTask const& checkTask) { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << "."); + // recurse + std::unique_ptr resultPointer = this->check(env, checkTask.getFormula()); + if (resultPointer->isExplicitQualitativeCheckResult()) { + STORM_LOG_ASSERT(ModelType::Representation == storm::models::ModelRepresentation::Sparse, "Unexpected model type."); + return std::make_unique>(resultPointer->asExplicitQualitativeCheckResult()); + } else { + STORM_LOG_ASSERT(resultPointer->isSymbolicQualitativeCheckResult(), "Unexpected result type."); + STORM_LOG_ASSERT(ModelType::Representation != storm::models::ModelRepresentation::Sparse, "Unexpected model type."); + auto const& qualRes = resultPointer->asSymbolicQualitativeCheckResult::ddType>(); + return std::make_unique::ddType, ValueType>>(qualRes); + } } template diff --git a/src/storm/modelchecker/AbstractModelChecker.h b/src/storm/modelchecker/AbstractModelChecker.h index 6eb3b0de8..2038e6361 100644 --- a/src/storm/modelchecker/AbstractModelChecker.h +++ b/src/storm/modelchecker/AbstractModelChecker.h @@ -65,7 +65,7 @@ namespace storm { virtual std::unique_ptr computeUntilProbabilities(Environment const& env, CheckTask const& checkTask); virtual std::unique_ptr computeHOAPathProbabilities(Environment const& env, CheckTask const& checkTask); virtual std::unique_ptr computeLTLProbabilities(Environment const& env, CheckTask const& checkTask); - virtual std::unique_ptr computeStateFormulaProbabilities(Environment const& env, CheckTask const& checkTask); + std::unique_ptr computeStateFormulaProbabilities(Environment const& env, CheckTask const& checkTask); // The methods to compute the rewards for path formulas. virtual std::unique_ptr computeRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask); diff --git a/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp index 44bd4ab3c..7bd2474de 100644 --- a/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp @@ -82,14 +82,6 @@ namespace storm { return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeBoundedUntilProbabilities(env, this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getNonStrictUpperBound()); } - template - std::unique_ptr HybridDtmcPrctlModelChecker::computeStateFormulaProbabilities(Environment const& env, CheckTask const& checkTask) { - storm::logic::Formula const& formula = checkTask.getFormula(); - std::unique_ptr resultPointer = this->check(env, formula); - SymbolicQualitativeCheckResult const& result = resultPointer->asSymbolicQualitativeCheckResult(); - return std::make_unique>(result); - } - template std::unique_ptr HybridDtmcPrctlModelChecker::computeCumulativeRewards(Environment const& env, storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); diff --git a/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.h b/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.h index 761d0168f..f779e1920 100644 --- a/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.h +++ b/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.h @@ -31,7 +31,6 @@ namespace storm { virtual std::unique_ptr computeUntilProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeGloballyProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeLongRunAverageProbabilities(Environment const& env, CheckTask const& checkTask) override; - virtual std::unique_ptr computeStateFormulaProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; virtual std::unique_ptr computeCumulativeRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; diff --git a/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp index 275527797..e74c921a8 100644 --- a/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp @@ -102,15 +102,6 @@ namespace storm { SymbolicQualitativeCheckResult const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult(); return storm::modelchecker::helper::HybridMdpPrctlHelper::computeBoundedUntilProbabilities(env, checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getNonStrictUpperBound()); } - - template - std::unique_ptr HybridMdpPrctlModelChecker::computeStateFormulaProbabilities(Environment const& env, CheckTask const& checkTask) { - storm::logic::Formula const& formula = checkTask.getFormula(); - std::unique_ptr resultPointer = this->check(env, formula); - SymbolicQualitativeCheckResult const& result = resultPointer->asSymbolicQualitativeCheckResult(); - // min/max does not matters - return std::make_unique>(result); - } template std::unique_ptr HybridMdpPrctlModelChecker::computeCumulativeRewards(Environment const& env, storm::logic::RewardMeasureType, CheckTask const& checkTask) { diff --git a/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.h b/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.h index 3fa76a65a..d3b87f3a2 100644 --- a/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.h +++ b/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.h @@ -38,7 +38,6 @@ namespace storm { virtual std::unique_ptr computeNextProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeUntilProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeGloballyProbabilities(Environment const& env, CheckTask const& checkTask) override; - virtual std::unique_ptr computeStateFormulaProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeCumulativeRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; virtual std::unique_ptr computeInstantaneousRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; diff --git a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index 870a9a09a..5ee8fe1ce 100644 --- a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -175,14 +175,6 @@ namespace storm { return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } - template - std::unique_ptr SparseDtmcPrctlModelChecker::computeStateFormulaProbabilities(Environment const& env, CheckTask const& checkTask) { - // recurse - std::unique_ptr resultPointer = this->check(env, checkTask.getFormula()); - ExplicitQualitativeCheckResult const& result = resultPointer->asExplicitQualitativeCheckResult(); - return std::make_unique>(result); - } - template std::unique_ptr SparseDtmcPrctlModelChecker::computeCumulativeRewards(Environment const& env, storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); diff --git a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h index 6f49a1a6d..e5ff0d5f4 100644 --- a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h +++ b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h @@ -34,7 +34,6 @@ namespace storm { virtual std::unique_ptr computeConditionalProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeLongRunAverageProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeLTLProbabilities(Environment const& env, CheckTask const& checkTask) override; - virtual std::unique_ptr computeStateFormulaProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeCumulativeRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; virtual std::unique_ptr computeInstantaneousRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index f386d416c..2b8750c7d 100644 --- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -167,15 +167,6 @@ namespace storm { return result; } - template - std::unique_ptr SparseMdpPrctlModelChecker::computeStateFormulaProbabilities(Environment const& env, CheckTask const& checkTask) { - storm::logic::Formula const& formula = checkTask.getFormula(); - STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); - std::unique_ptr resultPointer = this->check(env, formula); - ExplicitQualitativeCheckResult const& result = resultPointer->asExplicitQualitativeCheckResult(); - return std::make_unique>(result); - } - template std::unique_ptr SparseMdpPrctlModelChecker::computeLTLProbabilities(Environment const& env, CheckTask const& checkTask) { storm::logic::PathFormula const& pathFormula = checkTask.getFormula(); diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h index 2a09694c5..2a56528ba 100644 --- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h +++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h @@ -40,7 +40,6 @@ namespace storm { virtual std::unique_ptr computeReachabilityTimes(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, 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; - virtual std::unique_ptr computeStateFormulaProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeLTLProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr checkMultiObjectiveFormula(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr checkQuantileFormula(Environment const& env, CheckTask const& checkTask) override; diff --git a/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp index 6b68c945f..473a39cab 100644 --- a/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp @@ -58,14 +58,6 @@ namespace storm { storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeGloballyProbabilities(env, this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet()); return std::make_unique>(this->getModel().getReachableStates(), numericResult); } - - template - std::unique_ptr SymbolicDtmcPrctlModelChecker::computeStateFormulaProbabilities(Environment const& env, CheckTask const& checkTask) { - storm::logic::Formula const& formula = checkTask.getFormula(); - std::unique_ptr resultPointer = this->check(env, formula); - SymbolicQualitativeCheckResult const& result = resultPointer->asSymbolicQualitativeCheckResult(); - return std::make_unique>(result); - } template std::unique_ptr SymbolicDtmcPrctlModelChecker::computeNextProbabilities(Environment const& env, CheckTask const& checkTask) { diff --git a/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h b/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h index 17c96e927..1a115468f 100644 --- a/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h +++ b/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h @@ -26,7 +26,6 @@ namespace storm { virtual std::unique_ptr computeNextProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeUntilProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeGloballyProbabilities(Environment const& env, CheckTask const& checkTask) override; - virtual std::unique_ptr computeStateFormulaProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeCumulativeRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; virtual std::unique_ptr computeInstantaneousRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; virtual std::unique_ptr computeReachabilityRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; diff --git a/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp index 8f366034a..d9937001d 100644 --- a/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp @@ -58,16 +58,6 @@ namespace storm { SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeGloballyProbabilities(env, checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet()); } - - template - std::unique_ptr SymbolicMdpPrctlModelChecker::computeStateFormulaProbabilities(Environment const& env, CheckTask const& checkTask) { - storm::logic::Formula const& formula = checkTask.getFormula(); - STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); - std::unique_ptr resultPointer = this->check(env, formula); - SymbolicQualitativeCheckResult const& result = resultPointer->asSymbolicQualitativeCheckResult(); - // min/max does not matters - return std::make_unique>(result); - } template std::unique_ptr SymbolicMdpPrctlModelChecker::computeNextProbabilities(Environment const& env, CheckTask const& checkTask) { diff --git a/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h b/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h index e54f3579d..4fda40be3 100644 --- a/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h +++ b/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h @@ -27,7 +27,6 @@ namespace storm { virtual std::unique_ptr computeNextProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeUntilProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeGloballyProbabilities(Environment const& env, CheckTask const& checkTask) override; - virtual std::unique_ptr computeStateFormulaProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeCumulativeRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; virtual std::unique_ptr computeInstantaneousRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; virtual std::unique_ptr computeReachabilityRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override;