From d9176dc867e4d9ed2ebf41dccd6f68a8d9883c5e Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Mon, 17 Feb 2020 09:29:51 +0100 Subject: [PATCH] all (core) modelcheckers: Devided the canHandle method into a static and a non-static part. This allows to detect incompatibility before building the model. --- .../csl/HybridCtmcCslModelChecker.cpp | 21 ++++----- .../csl/HybridCtmcCslModelChecker.h | 12 ++--- .../csl/SparseCtmcCslModelChecker.cpp | 23 ++++----- .../csl/SparseCtmcCslModelChecker.h | 10 ++-- .../SparseMarkovAutomatonCslModelChecker.cpp | 47 ++++++++----------- .../SparseMarkovAutomatonCslModelChecker.h | 13 +++-- .../prctl/HybridDtmcPrctlModelChecker.cpp | 9 +++- .../prctl/HybridDtmcPrctlModelChecker.h | 5 ++ .../prctl/HybridMdpPrctlModelChecker.cpp | 24 ++++++---- .../prctl/HybridMdpPrctlModelChecker.h | 6 +++ .../prctl/SparseDtmcPrctlModelChecker.cpp | 18 +++++-- .../prctl/SparseDtmcPrctlModelChecker.h | 6 +++ .../prctl/SparseMdpPrctlModelChecker.cpp | 29 ++++++++---- .../prctl/SparseMdpPrctlModelChecker.h | 6 +++ .../prctl/SymbolicDtmcPrctlModelChecker.cpp | 7 ++- .../prctl/SymbolicDtmcPrctlModelChecker.h | 3 ++ .../prctl/SymbolicMdpPrctlModelChecker.cpp | 7 ++- .../prctl/SymbolicMdpPrctlModelChecker.h | 3 ++ 18 files changed, 148 insertions(+), 101 deletions(-) diff --git a/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp b/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp index b6d65edf0..88f380bd4 100644 --- a/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp @@ -24,22 +24,17 @@ namespace storm { } template - bool HybridCtmcCslModelChecker::canHandle(CheckTask const& checkTask) const { - return HybridCtmcCslModelChecker::canHandleImplementation(checkTask); - } - - template - template::SupportsExponential, int>::type> - bool HybridCtmcCslModelChecker::canHandleImplementation(CheckTask const& checkTask) const { - storm::logic::Formula const& formula = checkTask.getFormula(); - return formula.isInFragment(storm::logic::csrl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setTimeAllowed(true).setTimeOperatorsAllowed(true).setRewardAccumulationAllowed(true)); + bool HybridCtmcCslModelChecker::canHandleStatic(CheckTask const& checkTask) { + auto fragment = storm::logic::csrl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setTimeAllowed(true).setTimeOperatorsAllowed(true).setRewardAccumulationAllowed(true); + if (!storm::NumberTraits::SupportsExponential) { + fragment.setBoundedUntilFormulasAllowed(false).setCumulativeRewardFormulasAllowed(false).setInstantaneousFormulasAllowed(false); + } + return checkTask.getFormula().isInFragment(fragment); } template - template::SupportsExponential, int>::type> - bool HybridCtmcCslModelChecker::canHandleImplementation(CheckTask const& checkTask) const { - storm::logic::Formula const& formula = checkTask.getFormula(); - return formula.isInFragment(storm::logic::csrl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setTimeAllowed(true).setTimeOperatorsAllowed(true).setBoundedUntilFormulasAllowed(false).setCumulativeRewardFormulasAllowed(false).setInstantaneousFormulasAllowed(false)); + bool HybridCtmcCslModelChecker::canHandle(CheckTask const& checkTask) const { + return canHandleStatic(checkTask); } template diff --git a/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.h b/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.h index eaa55d42e..f266e9fe4 100644 --- a/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.h +++ b/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.h @@ -20,6 +20,9 @@ namespace storm { static const storm::dd::DdType DdType = ModelType::DdType; explicit HybridCtmcCslModelChecker(ModelType const& model); + + // Returns false, if this task can certainly not be handled by this model checker (independent of the concrete model). + static bool canHandleStatic(CheckTask const& checkTask); // The implemented methods of the AbstractModelChecker interface. virtual bool canHandle(CheckTask const& checkTask) const override; @@ -33,14 +36,7 @@ namespace storm { virtual std::unique_ptr computeCumulativeRewards(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; virtual std::unique_ptr computeReachabilityTimes(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; - - private: - template::SupportsExponential, int>::type = 0> - bool canHandleImplementation(CheckTask const& checkTask) const; - - template::SupportsExponential, int>::type = 0> - bool canHandleImplementation(CheckTask const& checkTask) const; - + }; } // namespace modelchecker diff --git a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp index 05555b125..10f1600bc 100644 --- a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp @@ -29,23 +29,18 @@ namespace storm { // Intentionally left empty. } - template - bool SparseCtmcCslModelChecker::canHandle(CheckTask const& checkTask) const { - return SparseCtmcCslModelChecker::canHandleImplementation(checkTask); - } - - template - template::SupportsExponential, int>::type> - bool SparseCtmcCslModelChecker::canHandleImplementation(CheckTask const& checkTask) const { - storm::logic::Formula const& formula = checkTask.getFormula(); - return formula.isInFragment(storm::logic::csrl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setTimeAllowed(true).setTotalRewardFormulasAllowed(true).setRewardAccumulationAllowed(true)); + template + bool SparseCtmcCslModelChecker::canHandleStatic(CheckTask const& checkTask) { + auto fragment = storm::logic::csrl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setTimeAllowed(true).setTimeOperatorsAllowed(true).setTotalRewardFormulasAllowed(true).setRewardAccumulationAllowed(true); + if (!storm::NumberTraits::SupportsExponential) { + fragment.setBoundedUntilFormulasAllowed(false).setCumulativeRewardFormulasAllowed(false).setInstantaneousFormulasAllowed(false); + } + return checkTask.getFormula().isInFragment(fragment); } template - template::SupportsExponential, int>::type> - bool SparseCtmcCslModelChecker::canHandleImplementation(CheckTask const& checkTask) const { - storm::logic::Formula const& formula = checkTask.getFormula(); - return formula.isInFragment(storm::logic::csrl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setTimeAllowed(true).setTotalRewardFormulasAllowed(true).setBoundedUntilFormulasAllowed(false).setCumulativeRewardFormulasAllowed(false).setInstantaneousFormulasAllowed(false)); + bool SparseCtmcCslModelChecker::canHandle(CheckTask const& checkTask) const { + return canHandleStatic(checkTask); } template diff --git a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.h b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.h index d7f432f53..bdb896a7b 100644 --- a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.h +++ b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.h @@ -21,6 +21,9 @@ namespace storm { explicit SparseCtmcCslModelChecker(SparseCtmcModelType const& model); + // Returns false, if this task can certainly not be handled by this model checker (independent of the concrete model). + static bool canHandleStatic(CheckTask const& checkTask); + // The implemented methods of the AbstractModelChecker interface. virtual bool canHandle(CheckTask const& checkTask) const override; virtual std::unique_ptr computeBoundedUntilProbabilities(Environment const& env, CheckTask const& checkTask) override; @@ -40,13 +43,6 @@ namespace storm { */ std::vector computeAllTransientProbabilities(Environment const& env, CheckTask const& checkTask); - private: - template::SupportsExponential, int>::type = 0> - bool canHandleImplementation(CheckTask const& checkTask) const; - - template::SupportsExponential, int>::type = 0> - bool canHandleImplementation(CheckTask const& checkTask) const; - }; } // namespace modelchecker diff --git a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp index 28e2444d5..29c006c88 100644 --- a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp @@ -27,38 +27,31 @@ namespace storm { // Intentionally left empty. } - template - bool SparseMarkovAutomatonCslModelChecker::canHandle(CheckTask const& checkTask) const { - return SparseMarkovAutomatonCslModelChecker::canHandleImplementation(checkTask); - } - - template - template::SupportsExponential, int>::type> - bool SparseMarkovAutomatonCslModelChecker::canHandleImplementation(CheckTask const& checkTask) const { - storm::logic::Formula const& formula = checkTask.getFormula(); - if(formula.isInFragment(storm::logic::csl().setGloballyFormulasAllowed(false).setNextFormulasAllowed(false).setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setTotalRewardFormulasAllowed(true).setTimeAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setLongRunAverageRewardFormulasAllowed(true).setRewardAccumulationAllowed(true))) { + template + bool SparseMarkovAutomatonCslModelChecker::canHandleStatic(CheckTask const& checkTask, bool* requiresSingleInitialState) { + auto singleObjectiveFragment = storm::logic::csl().setGloballyFormulasAllowed(false).setNextFormulasAllowed(false).setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setTotalRewardFormulasAllowed(true).setTimeAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setLongRunAverageRewardFormulasAllowed(true).setRewardAccumulationAllowed(true); + auto multiObjectiveFragment = storm::logic::multiObjective().setTimeAllowed(true).setTimeBoundedUntilFormulasAllowed(true); + if (!storm::NumberTraits::SupportsExponential) { + singleObjectiveFragment.setBoundedUntilFormulasAllowed(false).setCumulativeRewardFormulasAllowed(false).setInstantaneousFormulasAllowed(false); + multiObjectiveFragment.setTimeBoundedUntilFormulasAllowed(false).setCumulativeRewardFormulasAllowed(false).setInstantaneousFormulasAllowed(false); + } + if (checkTask.getFormula().isInFragment(singleObjectiveFragment)) { return true; - } else { - // Check whether we consider a multi-objective formula - // For multi-objective model checking, each initial state requires an individual scheduler (in contrast to single objective model checking). Let's exclude multiple initial states. - if (this->getModel().getInitialStates().getNumberOfSetBits() > 1) return false; - if (!checkTask.isOnlyInitialStatesRelevantSet()) return false; - return formula.isInFragment(storm::logic::multiObjective().setTimeAllowed(true).setTimeBoundedUntilFormulasAllowed(true)); + } else if (checkTask.isOnlyInitialStatesRelevantSet() && checkTask.getFormula().isInFragment(multiObjectiveFragment)) { + if (requiresSingleInitialState) { + *requiresSingleInitialState = true; + } } + return false; } - template - template::SupportsExponential, int>::type> - bool SparseMarkovAutomatonCslModelChecker::canHandleImplementation(CheckTask const& checkTask) const { - storm::logic::Formula const& formula = checkTask.getFormula(); - if(formula.isInFragment(storm::logic::prctl().setGloballyFormulasAllowed(false).setNextFormulasAllowed(false).setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setTotalRewardFormulasAllowed(true).setTimeAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setLongRunAverageRewardFormulasAllowed(true).setTimeBoundedUntilFormulasAllowed(false).setCumulativeRewardFormulasAllowed(false).setInstantaneousFormulasAllowed(false))) { - return true; + template + bool SparseMarkovAutomatonCslModelChecker::canHandle(CheckTask const& checkTask) const { + bool requiresSingleInitialState = false; + if (canHandleStatic(checkTask, &requiresSingleInitialState)) { + return !requiresSingleInitialState || this->getModel().getInitialStates().getNumberOfSetBits() == 1; } else { - // Check whether we consider a multi-objective formula - // For multi-objective model checking, each initial state requires an individual scheduler (in contrast to single objective model checking). Let's exclude multiple initial states. - if (this->getModel().getInitialStates().getNumberOfSetBits() > 1) return false; - if (!checkTask.isOnlyInitialStatesRelevantSet()) return false; - return formula.isInFragment(storm::logic::multiObjective().setTimeAllowed(true).setTimeBoundedUntilFormulasAllowed(false).setCumulativeRewardFormulasAllowed(false).setInstantaneousFormulasAllowed(false)); + return false; } } diff --git a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h index 3bd220449..f18f4a374 100644 --- a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h +++ b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h @@ -19,6 +19,12 @@ namespace storm { explicit SparseMarkovAutomatonCslModelChecker(SparseMarkovAutomatonModelType const& model); + /*! + * Returns false, if this task can certainly not be handled by this model checker (independent of the concrete model). + * @param requiresSingleInitialState if not nullptr, this flag is set to true iff checking this formula requires a model with a single initial state + */ + 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 computeBoundedUntilProbabilities(Environment const& env, CheckTask const& checkTask) override; @@ -29,13 +35,6 @@ namespace storm { virtual std::unique_ptr computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; virtual std::unique_ptr computeReachabilityTimes(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; virtual std::unique_ptr checkMultiObjectiveFormula(Environment const& env, CheckTask const& checkTask) override; - - private: - template::SupportsExponential, int>::type = 0> - bool canHandleImplementation(CheckTask const& checkTask) const; - - template::SupportsExponential, int>::type = 0> - bool canHandleImplementation(CheckTask const& checkTask) const; }; } } diff --git a/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp index ecd57182f..266363662 100644 --- a/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp @@ -32,11 +32,16 @@ namespace storm { } template - bool HybridDtmcPrctlModelChecker::canHandle(CheckTask const& checkTask) const { + bool HybridDtmcPrctlModelChecker::canHandleStatic(CheckTask const& checkTask) { storm::logic::Formula const& formula = checkTask.getFormula(); return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setTimeOperatorsAllowed(true).setReachbilityTimeFormulasAllowed(true).setRewardAccumulationAllowed(true)); } - + + template + bool HybridDtmcPrctlModelChecker::canHandle(CheckTask const& checkTask) const { + return canHandleStatic(checkTask); + } + template std::unique_ptr HybridDtmcPrctlModelChecker::computeUntilProbabilities(Environment const& env, CheckTask const& checkTask) { storm::logic::UntilFormula const& pathFormula = checkTask.getFormula(); diff --git a/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.h b/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.h index 854fae195..f779e1920 100644 --- a/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.h +++ b/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.h @@ -19,6 +19,11 @@ namespace storm { explicit HybridDtmcPrctlModelChecker(ModelType const& model); + /*! + * Returns false, if this task can certainly not be handled by this model checker (independent of the concrete model). + */ + static bool canHandleStatic(CheckTask const& checkTask); + // The implemented methods of the AbstractModelChecker interface. virtual bool canHandle(CheckTask const& checkTask) const override; virtual std::unique_ptr computeBoundedUntilProbabilities(Environment const& env, CheckTask const& checkTask) override; diff --git a/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp index 270e99c47..c4099bb5b 100644 --- a/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp @@ -38,20 +38,28 @@ namespace storm { } template - bool HybridMdpPrctlModelChecker::canHandle(CheckTask const& checkTask) const { + bool HybridMdpPrctlModelChecker::canHandleStatic(CheckTask const& checkTask, bool* requiresSingleInitialState) { storm::logic::Formula const& formula = checkTask.getFormula(); if (formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false).setTimeOperatorsAllowed(true).setReachbilityTimeFormulasAllowed(true).setRewardAccumulationAllowed(true))) { return true; + } else if (checkTask.isOnlyInitialStatesRelevantSet() && formula.isInFragment(storm::logic::multiObjective().setCumulativeRewardFormulasAllowed(true))) { + if (requiresSingleInitialState) { + *requiresSingleInitialState = true; + } + } + return false; + } + + template + bool HybridMdpPrctlModelChecker::canHandle(CheckTask const& checkTask) const { + bool requiresSingleInitialState = false; + if (canHandleStatic(checkTask, &requiresSingleInitialState)) { + return !requiresSingleInitialState || this->getModel().getInitialStates().getNonZeroCount() == 1; } else { - // Check whether we consider a multi-objective formula - // For multi-objective model checking, each state requires an individual scheduler (in contrast to single-objective model checking). Let's exclude that multiple states are relevant - if(this->getModel().getInitialStates().getNonZeroCount() > 1) return false; - if(!checkTask.isOnlyInitialStatesRelevantSet()) return false; - return formula.isInFragment(storm::logic::multiObjective().setCumulativeRewardFormulasAllowed(true)); + return false; } - } - + template std::unique_ptr HybridMdpPrctlModelChecker::computeUntilProbabilities(Environment const& env, CheckTask const& checkTask) { storm::logic::UntilFormula const& pathFormula = checkTask.getFormula(); diff --git a/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.h b/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.h index 68eb12baa..cc253e753 100644 --- a/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.h +++ b/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.h @@ -26,6 +26,12 @@ namespace storm { explicit HybridMdpPrctlModelChecker(ModelType const& model); + /*! + * Returns false, if this task can certainly not be handled by this model checker (independent of the concrete model). + * @param requiresSingleInitialState if not nullptr, this flag is set to true iff checking this formula requires a model with a single initial state + */ + 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 computeBoundedUntilProbabilities(Environment const& env, CheckTask const& checkTask) override; diff --git a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index 9896f8ce4..541c51502 100644 --- a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -32,17 +32,29 @@ namespace storm { } template - bool SparseDtmcPrctlModelChecker::canHandle(CheckTask const& checkTask) const { + bool SparseDtmcPrctlModelChecker::canHandleStatic(CheckTask const& checkTask, bool* requiresSingleInitialState) { storm::logic::Formula const& formula = checkTask.getFormula(); if (formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setConditionalRewardFormulasAllowed(true).setTotalRewardFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true).setRewardBoundedUntilFormulasAllowed(true).setRewardBoundedCumulativeRewardFormulasAllowed(true).setMultiDimensionalBoundedUntilFormulasAllowed(true).setMultiDimensionalCumulativeRewardFormulasAllowed(true).setTimeOperatorsAllowed(true).setReachbilityTimeFormulasAllowed(true).setRewardAccumulationAllowed(true))) { return true; - } else if (formula.isInFragment(storm::logic::quantiles())) { - if (this->getModel().getInitialStates().getNumberOfSetBits() > 1) return false; + } else if (checkTask.isOnlyInitialStatesRelevantSet() && formula.isInFragment(storm::logic::quantiles())) { + if (requiresSingleInitialState) { + *requiresSingleInitialState = true; + } return true; } return false; } + template + bool SparseDtmcPrctlModelChecker::canHandle(CheckTask const& checkTask) const { + bool requiresSingleInitialState = false; + if (canHandleStatic(checkTask, &requiresSingleInitialState)) { + return !requiresSingleInitialState || this->getModel().getInitialStates().getNumberOfSetBits() == 1; + } else { + return false; + } + } + template std::unique_ptr SparseDtmcPrctlModelChecker::computeBoundedUntilProbabilities(Environment const& env, CheckTask const& checkTask) { storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); diff --git a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h index 1001b5572..8e72833d6 100644 --- a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h +++ b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h @@ -18,6 +18,12 @@ namespace storm { explicit SparseDtmcPrctlModelChecker(SparseDtmcModelType const& model); + /*! + * Returns false, if this task can certainly not be handled by this model checker (independent of the concrete model). + * @param requiresSingleInitialState if not nullptr, this flag is set to true iff checking this formula requires a model with a single initial state + */ + 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 computeBoundedUntilProbabilities(Environment const& env, CheckTask const& checkTask) override; diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index 11821a518..f62035f73 100644 --- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -39,23 +39,32 @@ namespace storm { } template - bool SparseMdpPrctlModelChecker::canHandle(CheckTask const& checkTask) const { + bool SparseMdpPrctlModelChecker::canHandleStatic(CheckTask const& checkTask, bool* requiresSingleInitialState) { storm::logic::Formula const& formula = checkTask.getFormula(); if (formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true).setTotalRewardFormulasAllowed(true).setRewardBoundedUntilFormulasAllowed(true).setRewardBoundedCumulativeRewardFormulasAllowed(true).setMultiDimensionalBoundedUntilFormulasAllowed(true).setMultiDimensionalCumulativeRewardFormulasAllowed(true).setTimeOperatorsAllowed(true).setReachbilityTimeFormulasAllowed(true).setRewardAccumulationAllowed(true))) { return true; - } else if (formula.isInFragment(storm::logic::multiObjective().setCumulativeRewardFormulasAllowed(true).setTimeBoundedCumulativeRewardFormulasAllowed(true).setStepBoundedCumulativeRewardFormulasAllowed(true).setRewardBoundedCumulativeRewardFormulasAllowed(true).setTimeBoundedUntilFormulasAllowed(true).setStepBoundedUntilFormulasAllowed(true).setRewardBoundedUntilFormulasAllowed(true).setMultiDimensionalBoundedUntilFormulasAllowed(true).setMultiDimensionalCumulativeRewardFormulasAllowed(true))) { - // Check whether we consider a multi-objective formula - // For multi-objective model checking, each initial state requires an individual scheduler (in contrast to single-objective model checking). Let's exclude multiple initial states. - if (this->getModel().getInitialStates().getNumberOfSetBits() > 1) return false; - if (!checkTask.isOnlyInitialStatesRelevantSet()) return false; - return true; - } else if (formula.isInFragment(storm::logic::quantiles())) { - if (this->getModel().getInitialStates().getNumberOfSetBits() > 1) return false; - return true; + } else if (checkTask.isOnlyInitialStatesRelevantSet()) { + auto multiObjectiveFragment = storm::logic::multiObjective().setCumulativeRewardFormulasAllowed(true).setTimeBoundedCumulativeRewardFormulasAllowed(true).setStepBoundedCumulativeRewardFormulasAllowed(true).setRewardBoundedCumulativeRewardFormulasAllowed(true).setTimeBoundedUntilFormulasAllowed(true).setStepBoundedUntilFormulasAllowed(true).setRewardBoundedUntilFormulasAllowed(true).setMultiDimensionalBoundedUntilFormulasAllowed(true).setMultiDimensionalCumulativeRewardFormulasAllowed(true); + if (formula.isInFragment(multiObjectiveFragment) || formula.isInFragment(storm::logic::quantiles())) { + if (requiresSingleInitialState) { + *requiresSingleInitialState = true; + } + return true; + } } return false; } + template + bool SparseMdpPrctlModelChecker::canHandle(CheckTask const& checkTask) const { + bool requiresSingleInitialState = false; + if (canHandleStatic(checkTask, &requiresSingleInitialState)) { + return !requiresSingleInitialState || this->getModel().getInitialStates().getNumberOfSetBits() == 1; + } else { + return false; + } + } + template std::unique_ptr SparseMdpPrctlModelChecker::computeBoundedUntilProbabilities(Environment const& env, CheckTask const& checkTask) { storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h index 38a0a090c..44916728b 100644 --- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h +++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h @@ -18,6 +18,12 @@ namespace storm { explicit SparseMdpPrctlModelChecker(SparseMdpModelType const& model); + /*! + * Returns false, if this task can certainly not be handled by this model checker (independent of the concrete model). + * @param requiresSingleInitialState if not nullptr, this flag is set to true iff checking this formula requires a model with a single initial state + */ + 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 computeBoundedUntilProbabilities(Environment const& env, CheckTask const& checkTask) override; diff --git a/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp index 8b0040b2f..f10639dd4 100644 --- a/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp @@ -29,11 +29,16 @@ namespace storm { } template - bool SymbolicDtmcPrctlModelChecker::canHandle(CheckTask const& checkTask) const { + bool SymbolicDtmcPrctlModelChecker::canHandleStatic(CheckTask const& checkTask) { storm::logic::Formula const& formula = checkTask.getFormula(); return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false).setTimeOperatorsAllowed(true).setReachbilityTimeFormulasAllowed(true).setRewardAccumulationAllowed(true)); } + template + bool SymbolicDtmcPrctlModelChecker::canHandle(CheckTask const& checkTask) const { + return canHandleStatic(checkTask); + } + template std::unique_ptr SymbolicDtmcPrctlModelChecker::computeUntilProbabilities(Environment const& env, CheckTask const& checkTask) { storm::logic::UntilFormula const& pathFormula = checkTask.getFormula(); diff --git a/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h b/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h index 1186c0271..1a115468f 100644 --- a/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h +++ b/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h @@ -17,6 +17,9 @@ namespace storm { explicit SymbolicDtmcPrctlModelChecker(ModelType const& model); + // Returns false, if this task can certainly not be handled by this model checker (independent of the concrete model). + static bool canHandleStatic(CheckTask const& checkTask); + // The implemented methods of the AbstractModelChecker interface. virtual bool canHandle(CheckTask const& checkTask) const override; virtual std::unique_ptr computeBoundedUntilProbabilities(Environment const& env, CheckTask const& checkTask) override; diff --git a/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp index a08546669..d4dcf3a04 100644 --- a/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp @@ -29,11 +29,16 @@ namespace storm { } template - bool SymbolicMdpPrctlModelChecker::canHandle(CheckTask const& checkTask) const { + bool SymbolicMdpPrctlModelChecker::canHandleStatic(CheckTask const& checkTask) { storm::logic::Formula const& formula = checkTask.getFormula(); return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false).setTimeOperatorsAllowed(true).setReachbilityTimeFormulasAllowed(true).setRewardAccumulationAllowed(true)); } + template + bool SymbolicMdpPrctlModelChecker::canHandle(CheckTask const& checkTask) const { + return canHandleStatic(checkTask); + } + template std::unique_ptr SymbolicMdpPrctlModelChecker::computeUntilProbabilities(Environment const& env, CheckTask const& checkTask) { storm::logic::UntilFormula const& pathFormula = checkTask.getFormula(); diff --git a/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h b/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h index bf259e8b7..4fda40be3 100644 --- a/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h +++ b/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h @@ -18,6 +18,9 @@ namespace storm { explicit SymbolicMdpPrctlModelChecker(ModelType const& model); + // Returns false, if this task can certainly not be handled by this model checker (independent of the concrete model). + static bool canHandleStatic(CheckTask const& checkTask); + // The implemented methods of the AbstractModelChecker interface. virtual bool canHandle(CheckTask const& checkTask) const override; virtual std::unique_ptr computeBoundedUntilProbabilities(Environment const& env, CheckTask const& checkTask) override;