From e92e32239bbc1c37fd96ea5e9ceb9706f0f9dda5 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Mon, 9 Aug 2021 18:05:39 +0200 Subject: [PATCH] Support for globally and next formulae for Markov Automata and CTMC Conflicts: src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp --- .../csl/SparseCtmcCslModelChecker.cpp | 27 ++++++++++-------- .../csl/SparseCtmcCslModelChecker.h | 1 + .../SparseMarkovAutomatonCslModelChecker.cpp | 28 ++++++++++++++++++- .../SparseMarkovAutomatonCslModelChecker.h | 2 ++ 4 files changed, 46 insertions(+), 12 deletions(-) diff --git a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp index baa780223..f3c107c8b 100644 --- a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp @@ -19,7 +19,6 @@ #include "storm/modelchecker/helper/ltl/SparseLTLHelper.h" #include "storm/logic/FragmentSpecification.h" -#include "storm/logic/ExtractMaximalStateFormulasVisitor.h" #include "storm/adapters/RationalFunctionAdapter.h" @@ -27,10 +26,6 @@ #include "storm/exceptions/InvalidPropertyException.h" #include "storm/exceptions/NotImplementedException.h" -#include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/GeneralSettings.h" -#include "storm/settings/modules/DebugSettings.h" - namespace storm { namespace modelchecker { template @@ -40,7 +35,7 @@ namespace storm { template bool SparseCtmcCslModelChecker::canHandleStatic(CheckTask const& checkTask) { - auto fragment = storm::logic::csrlstar().setGloballyFormulasAllowed(true).setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setTimeAllowed(true).setTimeOperatorsAllowed(true).setTotalRewardFormulasAllowed(true).setRewardAccumulationAllowed(true); + auto fragment = storm::logic::csrlstar().setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setTimeAllowed(true).setTimeOperatorsAllowed(true).setTotalRewardFormulasAllowed(true).setRewardAccumulationAllowed(true); if (!storm::NumberTraits::SupportsExponential) { fragment.setBoundedUntilFormulasAllowed(false).setCumulativeRewardFormulasAllowed(false).setInstantaneousFormulasAllowed(false); } @@ -85,6 +80,16 @@ namespace storm { return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } + template + std::unique_ptr SparseCtmcCslModelChecker::computeGloballyProbabilities(Environment const& env, CheckTask const& checkTask) { + storm::logic::GloballyFormula const& pathFormula = checkTask.getFormula(); + std::unique_ptr subResultPointer = this->check(env, pathFormula.getSubformula()); + ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); + auto probabilisticTransitions = this->getModel().computeProbabilityMatrix(); + std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeGloballyProbabilities(env, storm::solver::SolveGoal(this->getModel(), checkTask), probabilisticTransitions, probabilisticTransitions.transpose(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet()); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + } + template std::unique_ptr SparseCtmcCslModelChecker::computeUntilProbabilities(Environment const& env, CheckTask const& checkTask) { storm::logic::UntilFormula const& pathFormula = checkTask.getFormula(); @@ -99,15 +104,15 @@ namespace storm { template std::unique_ptr SparseCtmcCslModelChecker::computeHOAPathProbabilities(Environment const& env, CheckTask const& checkTask) { storm::logic::HOAPathFormula const& pathFormula = checkTask.getFormula(); - + auto probabilisticTransitions = this->getModel().computeProbabilityMatrix(); storm::modelchecker::helper::SparseLTLHelper helper(probabilisticTransitions); storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, this->getModel()); - + auto formulaChecker = [&] (storm::logic::Formula const& formula) { return this->check(env, formula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); }; auto apSets = helper.computeApSets(pathFormula.getAPMapping(), formulaChecker); std::vector numericResult = helper.computeDAProductProbabilities(env, *pathFormula.readAutomaton(), apSets); - + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } @@ -118,13 +123,13 @@ namespace storm { auto probabilisticTransitions = this->getModel().computeProbabilityMatrix(); storm::modelchecker::helper::SparseLTLHelper helper(probabilisticTransitions); storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, this->getModel()); - + auto formulaChecker = [&] (storm::logic::Formula const& formula) { return this->check(env, formula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); }; std::vector numericResult = helper.computeLTLProbabilities(env, pathFormula, formulaChecker); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } - + template std::unique_ptr SparseCtmcCslModelChecker::computeInstantaneousRewards(Environment const& env, storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula(); diff --git a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.h b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.h index 40b487eff..1730aa327 100644 --- a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.h +++ b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.h @@ -28,6 +28,7 @@ namespace storm { virtual bool canHandle(CheckTask const& checkTask) const override; virtual std::unique_ptr computeBoundedUntilProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeNextProbabilities(Environment const& env, CheckTask const& checkTask) override; + virtual std::unique_ptr computeGloballyProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeUntilProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeLTLProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeHOAPathProbabilities(Environment const& env, CheckTask const& checkTask) override; diff --git a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp index 56a567359..358945d14 100644 --- a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp @@ -1,5 +1,6 @@ #include "storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h" #include "storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h" +#include "storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h" #include "storm/modelchecker/helper/infinitehorizon/SparseNondeterministicInfiniteHorizonHelper.h" #include "storm/modelchecker/helper/utility/SetInformationFromCheckTask.h" @@ -40,7 +41,7 @@ namespace storm { template bool SparseMarkovAutomatonCslModelChecker::canHandleStatic(CheckTask const& checkTask, bool* requiresSingleInitialState) { - auto singleObjectiveFragment = storm::logic::csl().setUnaryBooleanPathFormulasAllowed(true).setBinaryBooleanPathFormulasAllowed(true).setNestedPathFormulasAllowed(true).setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setTotalRewardFormulasAllowed(true).setTimeAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setLongRunAverageRewardFormulasAllowed(true).setRewardAccumulationAllowed(true).setInstantaneousFormulasAllowed(false); + auto singleObjectiveFragment = storm::logic::csrlstar().setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setTotalRewardFormulasAllowed(true).setTimeAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setLongRunAverageRewardFormulasAllowed(true).setRewardAccumulationAllowed(true).setInstantaneousFormulasAllowed(false); auto multiObjectiveFragment = storm::logic::multiObjective().setTimeAllowed(true).setTimeBoundedUntilFormulasAllowed(true).setRewardAccumulationAllowed(true); if (!storm::NumberTraits::SupportsExponential) { singleObjectiveFragment.setBoundedUntilFormulasAllowed(false).setCumulativeRewardFormulasAllowed(false); @@ -93,6 +94,31 @@ namespace storm { std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), std::make_pair(lowerBound, upperBound)); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(result))); } + + + template + std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeNextProbabilities(Environment const& env, CheckTask const& checkTask) { + storm::logic::NextFormula const& pathFormula = 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 subResultPointer = this->check(env, pathFormula.getSubformula()); + ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); + std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeNextProbabilities(env, checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector()); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + } + + template + std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeGloballyProbabilities(Environment const& env, CheckTask const& checkTask) { + storm::logic::GloballyFormula const& pathFormula = 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 subResultPointer = this->check(env, pathFormula.getSubformula()); + ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); + auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper::computeGloballyProbabilities(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), checkTask.isProduceSchedulersSet()); + std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(ret.values))); + if (checkTask.isProduceSchedulersSet() && ret.scheduler) { + result->asExplicitQuantitativeCheckResult().setScheduler(std::move(ret.scheduler)); + } + return result; + } template std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeUntilProbabilities(Environment const& env, CheckTask const& checkTask) { diff --git a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h index 81f94bd7e..093df17aa 100644 --- a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h +++ b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h @@ -28,7 +28,9 @@ namespace storm { // 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; + 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 computeLTLProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeHOAPathProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeReachabilityRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override;