From bb7f4dd6d7b8203efb8c00448ac1f13b5671fb92 Mon Sep 17 00:00:00 2001 From: TimQu Date: Fri, 28 Sep 2018 16:39:37 +0200 Subject: [PATCH] canHandle method of exact continuous time model checkers now return 'false' for time-bounded properties --- .../csl/HybridCtmcCslModelChecker.cpp | 2 +- .../csl/SparseCtmcCslModelChecker.cpp | 2 +- .../SparseMarkovAutomatonCslModelChecker.cpp | 21 +++++++++++++++++++ .../SparseMarkovAutomatonCslModelChecker.h | 6 ++++++ 4 files changed, 29 insertions(+), 2 deletions(-) diff --git a/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp b/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp index 4d2507288..d36680dea 100644 --- a/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp @@ -37,7 +37,7 @@ namespace storm { template::SupportsExponential, int>::type> bool HybridCtmcCslModelChecker::canHandleImplementation(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); - return formula.isInFragment(storm::logic::prctl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true)); + return formula.isInFragment(storm::logic::prctl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setTimeBoundedUntilFormulasAllowed(false).setCumulativeRewardFormulasAllowed(false)); } template diff --git a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp index 3cedc1fab..f35d7e41f 100644 --- a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp @@ -44,7 +44,7 @@ namespace storm { template::SupportsExponential, int>::type> bool SparseCtmcCslModelChecker::canHandleImplementation(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); - return formula.isInFragment(storm::logic::prctl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setTimeAllowed(true).setTotalRewardFormulasAllowed(true)); + return formula.isInFragment(storm::logic::prctl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setTimeAllowed(true).setTotalRewardFormulasAllowed(true).setTimeBoundedUntilFormulasAllowed(false).setCumulativeRewardFormulasAllowed(false)); } template diff --git a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp index 929ea8721..454de198b 100644 --- a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp @@ -28,6 +28,12 @@ namespace storm { 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))) { return true; @@ -40,6 +46,21 @@ namespace storm { } } + 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))) { + 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(false).setCumulativeRewardFormulasAllowed(false)); + } + } + template std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeBoundedUntilProbabilities(Environment const& env, CheckTask const& checkTask) { storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); diff --git a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h index 3bd557dd4..3bd220449 100644 --- a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h +++ b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h @@ -29,7 +29,13 @@ 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; }; } }