From 4367bdb37899fcb502d6fdeae682f6ab61c927b8 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 4 Feb 2016 21:48:21 +0100 Subject: [PATCH] properly introduced CheckTask in all model checkers and made it compile again (+ functional tests working) Former-commit-id: d44db3c3427170dfd4cd32b8110b3cebc1fa7f9c --- src/builder/ExplicitPrismModelBuilder.cpp | 6 +- src/cli/entrypoints.h | 2 +- src/logic/Formula.cpp | 12 ++ src/logic/Formula.h | 5 + src/logic/Formulas.h | 1 + src/logic/OperatorFormula.cpp | 4 + src/logic/OperatorFormula.h | 1 + src/modelchecker/CheckTask.h | 69 ++++---- .../csl/HybridCtmcCslModelChecker.cpp | 19 ++- .../csl/SparseCtmcCslModelChecker.cpp | 19 ++- .../SparseMarkovAutomatonCslModelChecker.cpp | 27 ++-- .../SparseMarkovAutomatonCslModelChecker.h | 2 +- .../prctl/HybridDtmcPrctlModelChecker.cpp | 20 ++- .../prctl/HybridMdpPrctlModelChecker.cpp | 35 ++-- .../prctl/SparseDtmcPrctlModelChecker.cpp | 25 ++- .../prctl/SparseMdpPrctlModelChecker.cpp | 65 ++++---- .../prctl/SymbolicDtmcPrctlModelChecker.cpp | 17 +- .../prctl/SymbolicMdpPrctlModelChecker.cpp | 35 ++-- .../prctl/helper/SymbolicMdpPrctlHelper.cpp | 32 ++-- .../prctl/helper/SymbolicMdpPrctlHelper.h | 15 +- .../SparsePropositionalModelChecker.cpp | 2 + .../SymbolicPropositionalModelChecker.cpp | 3 + .../SparseDtmcEliminationModelChecker.cpp | 153 +++++------------- .../SparseDtmcEliminationModelChecker.h | 8 +- .../SparseDtmcEliminationModelCheckerTest.cpp | 4 +- 25 files changed, 281 insertions(+), 300 deletions(-) diff --git a/src/builder/ExplicitPrismModelBuilder.cpp b/src/builder/ExplicitPrismModelBuilder.cpp index 9e5474061..d345d9f05 100644 --- a/src/builder/ExplicitPrismModelBuilder.cpp +++ b/src/builder/ExplicitPrismModelBuilder.cpp @@ -264,11 +264,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The program contains undefined constants that appear in some places other than update probabilities and reward value expressions, which is not admitted."); #endif } - - if (!std::is_same::value) { - doMagic(iasdfasdpfoy); - } - + // If the set of labels we are supposed to built is restricted, we need to remove the other labels from the program. if (options.labelsToBuild) { if (!options.buildAllLabels) { diff --git a/src/cli/entrypoints.h b/src/cli/entrypoints.h index 284aee708..c93279179 100644 --- a/src/cli/entrypoints.h +++ b/src/cli/entrypoints.h @@ -172,7 +172,7 @@ namespace storm { storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings(); STORM_LOG_THROW(settings.isExplicitSet(), storm::exceptions::InvalidStateException, "Unable to build explicit model without model files."); - std::shared_ptr model = buildExplicitModel(settings.getTransitionFilename(), settings.getLabelingFilename(), settings.isStateRewardsSet() ? settings.getStateRewardsFilename() : boost::none, settings.isTransitionRewardsSet() ? settings.getTransitionRewardsFilename() : boost::none, settings.isChoiceLabelingSet() ? settings.getChoiceLabelingFilename() : boost::none); + std::shared_ptr model = buildExplicitModel(settings.getTransitionFilename(), settings.getLabelingFilename(), settings.isStateRewardsSet() ? boost::optional(settings.getStateRewardsFilename()) : boost::none, settings.isTransitionRewardsSet() ? boost::optional(settings.getTransitionRewardsFilename()) : boost::none, settings.isChoiceLabelingSet() ? boost::optional(settings.getChoiceLabelingFilename()) : boost::none); // Preprocess the model if needed. BRANCH_ON_MODELTYPE(model, model, ValueType, storm::dd::DdType::CUDD, preprocessModel, formulas); diff --git a/src/logic/Formula.cpp b/src/logic/Formula.cpp index babf9edfc..5ba068af9 100644 --- a/src/logic/Formula.cpp +++ b/src/logic/Formula.cpp @@ -115,6 +115,10 @@ namespace storm { return false; } + bool Formula::isOperatorFormula() const { + return false; + } + bool Formula::isPctlPathFormula() const { return false; } @@ -379,6 +383,14 @@ namespace storm { return dynamic_cast(*this); } + OperatorFormula& Formula::asOperatorFormula() { + return dynamic_cast(*this); + } + + OperatorFormula const& Formula::asOperatorFormula() const { + return dynamic_cast(*this); + } + std::vector> Formula::getAtomicExpressionFormulas() const { std::vector> result; this->gatherAtomicExpressionFormulas(result); diff --git a/src/logic/Formula.h b/src/logic/Formula.h index 1a6933703..31ee7744a 100644 --- a/src/logic/Formula.h +++ b/src/logic/Formula.h @@ -38,6 +38,7 @@ namespace storm { class LongRunAverageRewardFormula; class ProbabilityOperatorFormula; class RewardOperatorFormula; + class OperatorFormula; // Also foward-declare base model checker class. class ModelChecker; @@ -80,6 +81,7 @@ namespace storm { virtual bool isLongRunAverageRewardFormula() const; virtual bool isProbabilityOperatorFormula() const; virtual bool isRewardOperatorFormula() const; + virtual bool isOperatorFormula() const; virtual bool isPctlPathFormula() const; virtual bool isPctlStateFormula() const; @@ -175,6 +177,9 @@ namespace storm { RewardOperatorFormula& asRewardOperatorFormula(); RewardOperatorFormula const& asRewardOperatorFormula() const; + OperatorFormula& asOperatorFormula(); + OperatorFormula const& asOperatorFormula() const; + std::vector> getAtomicExpressionFormulas() const; std::vector> getAtomicLabelFormulas() const; std::set getReferencedRewardModels() const; diff --git a/src/logic/Formulas.h b/src/logic/Formulas.h index faf4ca164..3671b2859 100644 --- a/src/logic/Formulas.h +++ b/src/logic/Formulas.h @@ -13,6 +13,7 @@ #include "src/logic/NextFormula.h" #include "src/logic/PathFormula.h" #include "src/logic/RewardPathFormula.h" +#include "src/logic/OperatorFormula.h" #include "src/logic/ProbabilityOperatorFormula.h" #include "src/logic/ReachabilityRewardFormula.h" #include "src/logic/LongRunAverageRewardFormula.h" diff --git a/src/logic/OperatorFormula.cpp b/src/logic/OperatorFormula.cpp index 39fad071d..768b6b3d0 100644 --- a/src/logic/OperatorFormula.cpp +++ b/src/logic/OperatorFormula.cpp @@ -34,6 +34,10 @@ namespace storm { return optimalityType.get(); } + bool OperatorFormula::isOperatorFormula() const { + return true; + } + std::ostream& OperatorFormula::writeToStream(std::ostream& out) const { if (hasOptimalityType()) { out << (getOptimalityType() == OptimizationDirection::Minimize ? "min" : "max"); diff --git a/src/logic/OperatorFormula.h b/src/logic/OperatorFormula.h index a059ddb8b..5c120bf2f 100644 --- a/src/logic/OperatorFormula.h +++ b/src/logic/OperatorFormula.h @@ -24,6 +24,7 @@ namespace storm { void setBound(double); bool hasOptimalityType() const; OptimizationDirection const& getOptimalityType() const; + virtual bool isOperatorFormula() const override; virtual std::ostream& writeToStream(std::ostream& out) const override; diff --git a/src/modelchecker/CheckTask.h b/src/modelchecker/CheckTask.h index 042daf40d..acd039b8b 100644 --- a/src/modelchecker/CheckTask.h +++ b/src/modelchecker/CheckTask.h @@ -22,56 +22,50 @@ namespace storm { template class CheckTask { public: - /*! - * Creates an empty task object with the default options. - */ - CheckTask() : CheckTask(boost::none, boost::none, boost::none, false, boost::none, false, false) { - // Intentionally left empty. - } + template + friend class CheckTask; /*! * Creates a task object with the default options for the given formula. */ - CheckTask(FormulaType const& formula) { + CheckTask(FormulaType const& formula) : formula(formula) { this->onlyInitialStatesRelevant = false; this->produceStrategies = true; this->qualitative = false; - if (formula.isProbabilityOperatorFormula()) { - storm::logic::ProbabilityOperatorFormula const& probabilityOperatorFormula = formula.asProbabilityOperatorFormula(); - if (probabilityOperatorFormula.hasOptimalityType()) { - this->optimizationDirection = probabilityOperatorFormula.getOptimalityType(); + if (formula.isOperatorFormula()) { + storm::logic::OperatorFormula const& operatorFormula = formula.asOperatorFormula(); + if (operatorFormula.hasOptimalityType()) { + this->optimizationDirection = operatorFormula.getOptimalityType(); } - if (probabilityOperatorFormula.hasBound()) { + if (operatorFormula.hasBound()) { if (onlyInitialStatesRelevant) { - this->initialStatesBound = std::make_pair(probabilityOperatorFormula.getComparisonType(), static_cast(probabilityOperatorFormula.getBound())); + this->bound = std::make_pair(operatorFormula.getComparisonType(), static_cast(operatorFormula.getBound())); } + + if (!optimizationDirection) { + this->optimizationDirection = operatorFormula.getComparisonType() == storm::logic::ComparisonType::Less || operatorFormula.getComparisonType() == storm::logic::ComparisonType::LessEqual ? OptimizationDirection::Maximize : OptimizationDirection::Minimize; + } + } + } + + if (formula.isProbabilityOperatorFormula()) { + storm::logic::ProbabilityOperatorFormula const& probabilityOperatorFormula = formula.asProbabilityOperatorFormula(); + + if (probabilityOperatorFormula.hasBound()) { if (probabilityOperatorFormula.getBound() == storm::utility::zero() || probabilityOperatorFormula.getBound() == storm::utility::one()) { this->qualitative = true; } - if (!optimizationDirection) { - this->optimizationDirection = probabilityOperatorFormula.getComparisonType() == storm::logic::ComparisonType::Less || probabilityOperatorFormula.getComparisonType() == storm::logic::ComparisonType::LessEqual ? OptimizationDirection::Maximize : OptimizationDirection::Minimize; - } } } else if (formula.isRewardOperatorFormula()) { storm::logic::RewardOperatorFormula const& rewardOperatorFormula = formula.asRewardOperatorFormula(); this->rewardModel = rewardOperatorFormula.getOptionalRewardModelName(); - if (rewardOperatorFormula.hasOptimalityType()) { - this->optimizationDirection = rewardOperatorFormula.getOptimalityType(); - } - if (rewardOperatorFormula.hasBound()) { - if (onlyInitialStatesRelevant) { - this->initialStatesBound = std::make_pair(rewardOperatorFormula.getComparisonType(), static_cast(rewardOperatorFormula.getBound())); - } if (rewardOperatorFormula.getBound() == storm::utility::zero()) { this->qualitative = true; } - if (!optimizationDirection) { - this->optimizationDirection = rewardOperatorFormula.getComparisonType() == storm::logic::ComparisonType::Less || rewardOperatorFormula.getComparisonType() == storm::logic::ComparisonType::LessEqual ? OptimizationDirection::Maximize : OptimizationDirection::Minimize; - } } } } @@ -82,21 +76,14 @@ namespace storm { */ template CheckTask replaceFormula(NewFormulaType const& newFormula) const { - return CheckTask(newFormula, this->optimizationDirection, this->rewardModel, this->onlyInitialStatesRelevant, this->initialStatesBound, this->qualitative, this->produceStrategies); - } - - /*! - * Retrieves whether this task is associated with a formula. - */ - bool hasFormula() const { - return static_cast(formula); + return CheckTask(newFormula, this->optimizationDirection, this->rewardModel, this->onlyInitialStatesRelevant, this->bound, this->qualitative, this->produceStrategies); } /*! * Retrieves the formula from this task. */ FormulaType const& getFormula() const { - return formula.get().get(); + return formula.get(); } /*! @@ -134,6 +121,14 @@ namespace storm { return onlyInitialStatesRelevant; } + /*! + * Sets whether only initial states are relevant. + */ + CheckTask& setOnlyInitialStatesRelevant(bool value = true) { + this->onlyInitialStatesRelevant = value; + return *this; + } + /*! * Retrieves whether there is a bound with which the values for the states will be compared. */ @@ -193,12 +188,12 @@ namespace storm { * @param produceStrategies If supported by the model checker and the model formalism, strategies to achieve * a value will be produced if this flag is set. */ - CheckTask(boost::optional> const& formula, boost::optional const& optimizationDirection, boost::optional const& rewardModel, bool onlyInitialStatesRelevant, boost::optional> const& bound, bool qualitative, bool produceStrategies) : formula(formula), optimizationDirection(optimizationDirection), rewardModel(rewardModel), onlyInitialStatesRelevant(onlyInitialStatesRelevant), bound(bound), qualitative(qualitative), produceStrategies(produceStrategies) { + CheckTask(std::reference_wrapper const& formula, boost::optional const& optimizationDirection, boost::optional const& rewardModel, bool onlyInitialStatesRelevant, boost::optional> const& bound, bool qualitative, bool produceStrategies) : formula(formula), optimizationDirection(optimizationDirection), rewardModel(rewardModel), onlyInitialStatesRelevant(onlyInitialStatesRelevant), bound(bound), qualitative(qualitative), produceStrategies(produceStrategies) { // Intentionally left empty. } // The formula that is to be checked. - boost::optional> formula; + std::reference_wrapper formula; // If set, the probabilities will be minimized/maximized. boost::optional optimizationDirection; diff --git a/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp b/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp index 03800aaec..bb03bc1fc 100644 --- a/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp +++ b/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp @@ -29,16 +29,18 @@ namespace storm { template std::unique_ptr HybridCtmcCslModelChecker::computeUntilProbabilities(CheckTask const& checkTask) { + storm::logic::UntilFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); SymbolicQualitativeCheckResult const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult(); SymbolicQualitativeCheckResult const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::HybridCtmcCslHelper::computeUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, *this->linearEquationSolverFactory); + return storm::modelchecker::helper::HybridCtmcCslHelper::computeUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); } template std::unique_ptr HybridCtmcCslModelChecker::computeNextProbabilities(CheckTask const& checkTask) { + storm::logic::NextFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); @@ -52,14 +54,16 @@ namespace storm { template std::unique_ptr HybridCtmcCslModelChecker::computeReachabilityRewards(CheckTask const& checkTask) { + storm::logic::ReachabilityRewardFormula const& rewardPathFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(rewardPathFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::HybridCtmcCslHelper::computeReachabilityRewards(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), qualitative, *linearEquationSolverFactory); + return storm::modelchecker::helper::HybridCtmcCslHelper::computeReachabilityRewards(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *linearEquationSolverFactory); } template std::unique_ptr HybridCtmcCslModelChecker::computeBoundedUntilProbabilities(CheckTask const& checkTask) { + storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); SymbolicQualitativeCheckResult const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult(); @@ -74,25 +78,28 @@ namespace storm { upperBound = pathFormula.getDiscreteTimeBound(); } - return storm::modelchecker::helper::HybridCtmcCslHelper::computeBoundedUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, lowerBound, upperBound, *linearEquationSolverFactory); + return storm::modelchecker::helper::HybridCtmcCslHelper::computeBoundedUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), lowerBound, upperBound, *linearEquationSolverFactory); } template std::unique_ptr HybridCtmcCslModelChecker::computeInstantaneousRewards(CheckTask const& checkTask) { - return storm::modelchecker::helper::HybridCtmcCslHelper::computeInstantaneousRewards(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), rewardPathFormula.getContinuousTimeBound(), *linearEquationSolverFactory); + storm::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula(); + return storm::modelchecker::helper::HybridCtmcCslHelper::computeInstantaneousRewards(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getContinuousTimeBound(), *linearEquationSolverFactory); } template std::unique_ptr HybridCtmcCslModelChecker::computeCumulativeRewards(CheckTask const& checkTask) { - return storm::modelchecker::helper::HybridCtmcCslHelper::computeCumulativeRewards(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), rewardPathFormula.getContinuousTimeBound(), *linearEquationSolverFactory); + storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); + return storm::modelchecker::helper::HybridCtmcCslHelper::computeCumulativeRewards(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getContinuousTimeBound(), *linearEquationSolverFactory); } template std::unique_ptr HybridCtmcCslModelChecker::computeLongRunAverageProbabilities(CheckTask const& checkTask) { + storm::logic::StateFormula const& stateFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(stateFormula); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::HybridCtmcCslHelper::computeLongRunAverageProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), subResult.getTruthValuesVector(), qualitative, *linearEquationSolverFactory); + return storm::modelchecker::helper::HybridCtmcCslHelper::computeLongRunAverageProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *linearEquationSolverFactory); } // Explicitly instantiate the model checker. diff --git a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp index fa1ed6aa9..5c1dd73ab 100644 --- a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp +++ b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp @@ -36,6 +36,7 @@ namespace storm { template std::unique_ptr SparseCtmcCslModelChecker::computeBoundedUntilProbabilities(CheckTask const& checkTask) { + storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult();; @@ -50,12 +51,13 @@ namespace storm { upperBound = pathFormula.getDiscreteTimeBound(); } - std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeBoundedUntilProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), this->getModel().getExitRateVector(), qualitative, lowerBound, upperBound, *linearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeBoundedUntilProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), this->getModel().getExitRateVector(), checkTask.isQualitativeSet(), lowerBound, upperBound, *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } template std::unique_ptr SparseCtmcCslModelChecker::computeNextProbabilities(CheckTask const& checkTask) { + storm::logic::NextFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeNextProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), subResult.getTruthValuesVector(), *linearEquationSolverFactory); @@ -64,42 +66,47 @@ namespace storm { template std::unique_ptr SparseCtmcCslModelChecker::computeUntilProbabilities(CheckTask const& checkTask) { + storm::logic::UntilFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeUntilProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRateVector(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, *this->linearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeUntilProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRateVector(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } template std::unique_ptr SparseCtmcCslModelChecker::computeInstantaneousRewards(CheckTask const& checkTask) { - std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeInstantaneousRewards(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), rewardPathFormula.getContinuousTimeBound(), *linearEquationSolverFactory); + storm::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula(); + std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeInstantaneousRewards(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getContinuousTimeBound(), *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } template std::unique_ptr SparseCtmcCslModelChecker::computeCumulativeRewards(CheckTask const& checkTask) { - std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeCumulativeRewards(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), rewardPathFormula.getContinuousTimeBound(), *linearEquationSolverFactory); + storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); + std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeCumulativeRewards(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getContinuousTimeBound(), *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } template std::unique_ptr SparseCtmcCslModelChecker::computeReachabilityRewards(CheckTask const& checkTask) { + storm::logic::ReachabilityRewardFormula const& rewardPathFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(rewardPathFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeReachabilityRewards(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRateVector(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), qualitative, *linearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeReachabilityRewards(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } template std::unique_ptr SparseCtmcCslModelChecker::computeLongRunAverageProbabilities(CheckTask const& checkTask) { + storm::logic::StateFormula const& stateFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(stateFormula); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); storm::storage::SparseMatrix probabilityMatrix = storm::modelchecker::helper::SparseCtmcCslHelper::computeProbabilityMatrix(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector()); - std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageProbabilities(probabilityMatrix, subResult.getTruthValuesVector(), &this->getModel().getExitRateVector(), qualitative, *linearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageProbabilities(probabilityMatrix, subResult.getTruthValuesVector(), &this->getModel().getExitRateVector(), checkTask.isQualitativeSet(), *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp index e8921177b..369f54878 100644 --- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp +++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp @@ -34,58 +34,63 @@ namespace storm { template std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeBoundedUntilProbabilities(CheckTask const& checkTask) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + storm::logic::BoundedUntilFormula 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."); STORM_LOG_THROW(pathFormula.getLeftSubformula().isTrueFormula(), storm::exceptions::NotImplementedException, "Only bounded properties of the form 'true U[t1, t2] phi' are currently supported."); STORM_LOG_THROW(this->getModel().isClosed(), storm::exceptions::InvalidPropertyException, "Unable to compute time-bounded reachability probabilities in non-closed Markov automaton."); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(optimalityType.get(), this->getModel().getTransitionMatrix(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), rightResult.getTruthValuesVector(), pathFormula.getIntervalBounds(), *minMaxLinearEquationSolverFactory); + std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), rightResult.getTruthValuesVector(), pathFormula.getIntervalBounds(), *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(result))); } template std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeUntilProbabilities(CheckTask const& checkTask) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + storm::logic::UntilFormula 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 leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeUntilProbabilities(optimalityType.get(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, *minMaxLinearEquationSolverFactory); + std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(result))); } template std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeReachabilityRewards(CheckTask const& checkTask) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + storm::logic::ReachabilityRewardFormula const& rewardPathFormula = 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."); STORM_LOG_THROW(this->getModel().isClosed(), storm::exceptions::InvalidPropertyException, "Unable to compute reachability rewards in non-closed Markov automaton."); std::unique_ptr subResultPointer = this->check(rewardPathFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeReachabilityRewards(optimalityType.get(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), qualitative, *minMaxLinearEquationSolverFactory); + std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeReachabilityRewards(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(result))); } template std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeLongRunAverageProbabilities(CheckTask const& checkTask) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + storm::logic::StateFormula const& stateFormula = 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."); STORM_LOG_THROW(this->getModel().isClosed(), storm::exceptions::InvalidPropertyException, "Unable to compute long-run average in non-closed Markov automaton."); std::unique_ptr subResultPointer = this->check(stateFormula); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeLongRunAverageProbabilities(optimalityType.get(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), subResult.getTruthValuesVector(), qualitative, *minMaxLinearEquationSolverFactory); + std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeLongRunAverageProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(result))); } template - std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeExpectedTimes(CheckTask const& const& checkTask) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeExpectedTimes(CheckTask const& checkTask) { + storm::logic::EventuallyFormula const& eventuallyFormula = 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."); STORM_LOG_THROW(this->getModel().isClosed(), storm::exceptions::InvalidPropertyException, "Unable to compute expected times in non-closed Markov automaton."); std::unique_ptr subResultPointer = this->check(eventuallyFormula.getSubformula()); ExplicitQualitativeCheckResult& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeExpectedTimes(optimalityType.get(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), subResult.getTruthValuesVector(), qualitative, *minMaxLinearEquationSolverFactory); + std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeExpectedTimes(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(result))); } diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h index 1b553ccef..576f730ec 100644 --- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h +++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h @@ -25,7 +25,7 @@ namespace storm { virtual std::unique_ptr computeUntilProbabilities(CheckTask const& checkTask) override; virtual std::unique_ptr computeReachabilityRewards(CheckTask const& checkTask) override; virtual std::unique_ptr computeLongRunAverageProbabilities(CheckTask const& checkTask) override; - virtual std::unique_ptr computeExpectedTimes(CheckTask const& const& checkTask) override; + virtual std::unique_ptr computeExpectedTimes(CheckTask const& checkTask) override; private: // An object that is used for retrieving solvers for systems of linear equations that are the result of nondeterministic choices. diff --git a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp index 495e828fe..f8b52b1aa 100644 --- a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp @@ -40,22 +40,25 @@ namespace storm { template std::unique_ptr HybridDtmcPrctlModelChecker::computeUntilProbabilities(CheckTask const& checkTask) { + storm::logic::UntilFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); SymbolicQualitativeCheckResult const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult(); SymbolicQualitativeCheckResult const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, *this->linearEquationSolverFactory); + return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); } template std::unique_ptr HybridDtmcPrctlModelChecker::computeGloballyProbabilities(CheckTask const& checkTask) { + storm::logic::GloballyFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeGloballyProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), qualitative, *this->linearEquationSolverFactory); + return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeGloballyProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); } template std::unique_ptr HybridDtmcPrctlModelChecker::computeNextProbabilities(CheckTask const& checkTask) { + storm::logic::NextFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeNextProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector()); @@ -63,6 +66,7 @@ namespace storm { template std::unique_ptr HybridDtmcPrctlModelChecker::computeBoundedUntilProbabilities(CheckTask const& checkTask) { + storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); STORM_LOG_THROW(pathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidArgumentException, "Formula needs to have a discrete time bound."); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); @@ -73,21 +77,24 @@ namespace storm { template std::unique_ptr HybridDtmcPrctlModelChecker::computeCumulativeRewards(CheckTask const& checkTask) { + storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidArgumentException, "Formula needs to have a discrete time bound."); - return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeCumulativeRewards(this->getModel(), this->getModel().getTransitionMatrix(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); + return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeCumulativeRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); } template std::unique_ptr HybridDtmcPrctlModelChecker::computeInstantaneousRewards(CheckTask const& checkTask) { + storm::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula(); STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidArgumentException, "Formula needs to have a discrete time bound."); - return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeInstantaneousRewards(this->getModel(), this->getModel().getTransitionMatrix(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); + return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeInstantaneousRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); } template std::unique_ptr HybridDtmcPrctlModelChecker::computeReachabilityRewards(CheckTask const& checkTask) { + storm::logic::ReachabilityRewardFormula const& rewardPathFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(rewardPathFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeReachabilityRewards(this->getModel(), this->getModel().getTransitionMatrix(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), qualitative, *this->linearEquationSolverFactory); + return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeReachabilityRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); } template @@ -97,6 +104,7 @@ namespace storm { template std::unique_ptr HybridDtmcPrctlModelChecker::computeLongRunAverageProbabilities(CheckTask const& checkTask) { + storm::logic::StateFormula const& stateFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(stateFormula); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); @@ -105,7 +113,7 @@ namespace storm { storm::storage::SparseMatrix explicitProbabilityMatrix = this->getModel().getTransitionMatrix().toMatrix(odd, odd); - std::vector result = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeLongRunAverageProbabilities(explicitProbabilityMatrix, subResult.getTruthValuesVector().toVector(odd), qualitative, *this->linearEquationSolverFactory); + std::vector result = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeLongRunAverageProbabilities(explicitProbabilityMatrix, subResult.getTruthValuesVector().toVector(odd), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); return std::unique_ptr(new HybridQuantitativeCheckResult(this->getModel().getReachableStates(), this->getModel().getManager().getBddZero(), this->getModel().getManager().template getAddZero(), this->getModel().getReachableStates(), std::move(odd), std::move(result))); } diff --git a/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp b/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp index 5255ed136..ec42dab64 100644 --- a/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp @@ -43,61 +43,68 @@ namespace storm { template std::unique_ptr HybridMdpPrctlModelChecker::computeUntilProbabilities(CheckTask const& checkTask) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + storm::logic::UntilFormula 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 leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); SymbolicQualitativeCheckResult const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult(); SymbolicQualitativeCheckResult const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::HybridMdpPrctlHelper::computeUntilProbabilities(optimalityType.get(), this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, *this->linearEquationSolverFactory); + return storm::modelchecker::helper::HybridMdpPrctlHelper::computeUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); } template std::unique_ptr HybridMdpPrctlModelChecker::computeGloballyProbabilities(CheckTask const& checkTask) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + 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(pathFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::HybridMdpPrctlHelper::computeGloballyProbabilities(optimalityType.get(), this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), qualitative, *this->linearEquationSolverFactory); + return storm::modelchecker::helper::HybridMdpPrctlHelper::computeGloballyProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); } template std::unique_ptr HybridMdpPrctlModelChecker::computeNextProbabilities(CheckTask const& checkTask) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + 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(pathFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::HybridMdpPrctlHelper::computeNextProbabilities(optimalityType.get(), this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector()); + return storm::modelchecker::helper::HybridMdpPrctlHelper::computeNextProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector()); } template std::unique_ptr HybridMdpPrctlModelChecker::computeBoundedUntilProbabilities(CheckTask const& checkTask) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + storm::logic::BoundedUntilFormula 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."); STORM_LOG_THROW(pathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); SymbolicQualitativeCheckResult const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult(); SymbolicQualitativeCheckResult const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::HybridMdpPrctlHelper::computeBoundedUntilProbabilities(optimalityType.get(), this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); + return storm::modelchecker::helper::HybridMdpPrctlHelper::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); } template std::unique_ptr HybridMdpPrctlModelChecker::computeCumulativeRewards(CheckTask const& checkTask) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + storm::logic::CumulativeRewardFormula const& rewardPathFormula = 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."); STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); - return storm::modelchecker::helper::HybridMdpPrctlHelper::computeCumulativeRewards(optimalityType.get(), this->getModel(), this->getModel().getTransitionMatrix(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); + return storm::modelchecker::helper::HybridMdpPrctlHelper::computeCumulativeRewards(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); } template std::unique_ptr HybridMdpPrctlModelChecker::computeInstantaneousRewards(CheckTask const& checkTask) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + storm::logic::InstantaneousRewardFormula const& rewardPathFormula = 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."); STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); - return storm::modelchecker::helper::HybridMdpPrctlHelper::computeInstantaneousRewards(optimalityType.get(), this->getModel(), this->getModel().getTransitionMatrix(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); + return storm::modelchecker::helper::HybridMdpPrctlHelper::computeInstantaneousRewards(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); } template std::unique_ptr HybridMdpPrctlModelChecker::computeReachabilityRewards(CheckTask const& checkTask) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + storm::logic::ReachabilityRewardFormula const& rewardPathFormula = 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(rewardPathFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::HybridMdpPrctlHelper::computeReachabilityRewards(optimalityType.get(), this->getModel(), this->getModel().getTransitionMatrix(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), qualitative, *this->linearEquationSolverFactory); + return storm::modelchecker::helper::HybridMdpPrctlHelper::computeReachabilityRewards(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); } template diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index 631abae7c..01a76bcfd 100644 --- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -53,6 +53,7 @@ namespace storm { template std::unique_ptr SparseDtmcPrctlModelChecker::computeBoundedUntilProbabilities(CheckTask const& checkTask) { + storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); STORM_LOG_THROW(pathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); @@ -65,6 +66,7 @@ namespace storm { template std::unique_ptr SparseDtmcPrctlModelChecker::computeNextProbabilities(CheckTask const& checkTask) { + storm::logic::NextFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeNextProbabilities(this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), *linearEquationSolverFactory); @@ -73,54 +75,61 @@ namespace storm { template std::unique_ptr SparseDtmcPrctlModelChecker::computeUntilProbabilities(CheckTask const& checkTask) { + storm::logic::UntilFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeUntilProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, *linearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeUntilProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } template std::unique_ptr SparseDtmcPrctlModelChecker::computeGloballyProbabilities(CheckTask const& checkTask) { + storm::logic::GloballyFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeGloballyProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), qualitative, *linearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeGloballyProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } template std::unique_ptr SparseDtmcPrctlModelChecker::computeCumulativeRewards(CheckTask const& checkTask) { + storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); - std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeCumulativeRewards(this->getModel().getTransitionMatrix(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *linearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeCumulativeRewards(this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } template std::unique_ptr SparseDtmcPrctlModelChecker::computeInstantaneousRewards(CheckTask const& checkTask) { + storm::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula(); STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); - std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeInstantaneousRewards(this->getModel().getTransitionMatrix(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *linearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeInstantaneousRewards(this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } template std::unique_ptr SparseDtmcPrctlModelChecker::computeReachabilityRewards(CheckTask const& checkTask) { + storm::logic::ReachabilityRewardFormula const& rewardPathFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(rewardPathFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeReachabilityRewards(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), qualitative, *linearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeReachabilityRewards(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } template std::unique_ptr SparseDtmcPrctlModelChecker::computeLongRunAverageProbabilities(CheckTask const& checkTask) { + storm::logic::StateFormula const& stateFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(stateFormula); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageProbabilities(this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), nullptr, qualitative, *linearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageProbabilities(this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), nullptr, checkTask.isQualitativeSet(), *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } template - std::unique_ptr SparseDtmcPrctlModelChecker::computeConditionalProbabilities(storm::logic::ConditionalPathFormula const& pathFormula, bool qualitative , boost::optional const& optimalityType) { + std::unique_ptr SparseDtmcPrctlModelChecker::computeConditionalProbabilities(CheckTask const& checkTask) { + storm::logic::ConditionalPathFormula const& pathFormula = checkTask.getFormula(); STORM_LOG_THROW(pathFormula.getLeftSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Illegal conditional probability formula."); STORM_LOG_THROW(pathFormula.getRightSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Illegal conditional probability formula."); @@ -129,7 +138,7 @@ namespace storm { ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeConditionalProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, *linearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeConditionalProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index 1dca55e2c..8991c845c 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -58,47 +58,52 @@ namespace storm { template std::unique_ptr SparseMdpPrctlModelChecker::computeBoundedUntilProbabilities(CheckTask const& checkTask) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + storm::logic::BoundedUntilFormula const& pathFormula = 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 leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeBoundedUntilProbabilities(optimalityType.get(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getDiscreteTimeBound(), *minMaxLinearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getDiscreteTimeBound(), *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } template std::unique_ptr SparseMdpPrctlModelChecker::computeNextProbabilities(CheckTask const& checkTask) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + storm::logic::NextFormula const& pathFormula = 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 subResultPointer = this->check(pathFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeNextProbabilities(optimalityType.get(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), *minMaxLinearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeNextProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } template std::unique_ptr SparseMdpPrctlModelChecker::computeUntilProbabilities(CheckTask const& checkTask) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + storm::logic::UntilFormula const& pathFormula = 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 leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper::computeUntilProbabilities(optimalityType.get(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, false, *minMaxLinearEquationSolverFactory); + auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper::computeUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), false, *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(ret.result))); } template std::unique_ptr SparseMdpPrctlModelChecker::computeGloballyProbabilities(CheckTask const& checkTask) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + storm::logic::GloballyFormula const& pathFormula = 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 subResultPointer = this->check(pathFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper::computeGloballyProbabilities(optimalityType.get(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), qualitative, *minMaxLinearEquationSolverFactory); + auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper::computeGloballyProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(ret))); } template std::unique_ptr SparseMdpPrctlModelChecker::computeConditionalProbabilities(CheckTask const& checkTask) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + storm::logic::ConditionalPathFormula const& pathFormula = 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."); STORM_LOG_THROW(this->getModel().getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::InvalidPropertyException, "Cannot compute conditional probabilities on MDPs with more than one initial state."); STORM_LOG_THROW(pathFormula.getLeftSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Illegal conditional probability formula."); STORM_LOG_THROW(pathFormula.getRightSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Illegal conditional probability formula."); @@ -108,60 +113,44 @@ namespace storm { ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - return storm::modelchecker::helper::SparseMdpPrctlHelper::computeConditionalProbabilities(optimalityType.get(), *this->getModel().getInitialStates().begin(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, *minMaxLinearEquationSolverFactory); - } - - template - std::unique_ptr SparseMdpPrctlModelChecker::computeUntilProbabilitiesForInitialStates(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType, boost::optional> const& bound) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); - std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); - std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); - ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); - ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - if(qualitative | !bound) { - // For qualitative checks, or if the , we use the standard approach. - auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper::computeUntilProbabilities(optimalityType.get(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, false, *minMaxLinearEquationSolverFactory); - return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(ret.result))); - } else { - // With a given bound, we only iterate until we pass the bound. - storm::solver::BoundedGoal boundedGoal(optimalityType.get(), bound.get(), this->getModel().getInitialStates() ); - auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper::computeUntilProbabilities(boundedGoal, this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, false, *minMaxLinearEquationSolverFactory); - return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(ret.result))); - } - + return storm::modelchecker::helper::SparseMdpPrctlHelper::computeConditionalProbabilities(checkTask.getOptimizationDirection(), *this->getModel().getInitialStates().begin(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *minMaxLinearEquationSolverFactory); } template std::unique_ptr SparseMdpPrctlModelChecker::computeCumulativeRewards(CheckTask const& checkTask) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + storm::logic::CumulativeRewardFormula const& rewardPathFormula = 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."); STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidArgumentException, "Formula needs to have a discrete time bound."); - std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeCumulativeRewards(optimalityType.get(), this->getModel().getTransitionMatrix(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *minMaxLinearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeCumulativeRewards(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } template std::unique_ptr SparseMdpPrctlModelChecker::computeInstantaneousRewards(CheckTask const& checkTask) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + storm::logic::InstantaneousRewardFormula const& rewardPathFormula = 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."); STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidArgumentException, "Formula needs to have a discrete time bound."); - std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeInstantaneousRewards(optimalityType.get(), this->getModel().getTransitionMatrix(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *minMaxLinearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeInstantaneousRewards(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } template std::unique_ptr SparseMdpPrctlModelChecker::computeReachabilityRewards(CheckTask const& checkTask) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + storm::logic::ReachabilityRewardFormula const& rewardPathFormula = 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 subResultPointer = this->check(rewardPathFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeReachabilityRewards(optimalityType.get(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), qualitative, *minMaxLinearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeReachabilityRewards(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } template std::unique_ptr SparseMdpPrctlModelChecker::computeLongRunAverageProbabilities(CheckTask const& checkTask) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + storm::logic::StateFormula const& stateFormula = 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 subResultPointer = this->check(stateFormula); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeLongRunAverageProbabilities(optimalityType.get(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), qualitative, *minMaxLinearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeLongRunAverageProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } diff --git a/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp index 5f9973eb1..dc9d22e1a 100644 --- a/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp @@ -45,24 +45,27 @@ namespace storm { template std::unique_ptr SymbolicDtmcPrctlModelChecker::computeUntilProbabilities(CheckTask const& checkTask) { + storm::logic::UntilFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); SymbolicQualitativeCheckResult const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult(); SymbolicQualitativeCheckResult const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult(); - storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, *this->linearEquationSolverFactory); + storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); return std::unique_ptr>(new SymbolicQuantitativeCheckResult(this->getModel().getReachableStates(), numericResult)); } template std::unique_ptr SymbolicDtmcPrctlModelChecker::computeGloballyProbabilities(CheckTask const& checkTask) { + storm::logic::GloballyFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); - storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeGloballyProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), qualitative, *this->linearEquationSolverFactory); + storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeGloballyProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); return std::unique_ptr>(new SymbolicQuantitativeCheckResult(this->getModel().getReachableStates(), numericResult)); } template std::unique_ptr SymbolicDtmcPrctlModelChecker::computeNextProbabilities(CheckTask const& checkTask) { + storm::logic::NextFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeNextProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector()); @@ -71,6 +74,7 @@ namespace storm { template std::unique_ptr SymbolicDtmcPrctlModelChecker::computeBoundedUntilProbabilities(CheckTask const& checkTask) { + storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); STORM_LOG_THROW(pathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); @@ -82,23 +86,26 @@ namespace storm { template std::unique_ptr SymbolicDtmcPrctlModelChecker::computeCumulativeRewards(CheckTask const& checkTask) { + storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); - storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeCumulativeRewards(this->getModel(), this->getModel().getTransitionMatrix(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); + storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeCumulativeRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); return std::unique_ptr>(new SymbolicQuantitativeCheckResult(this->getModel().getReachableStates(), numericResult)); } template std::unique_ptr SymbolicDtmcPrctlModelChecker::computeInstantaneousRewards(CheckTask const& checkTask) { + storm::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula(); STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); - storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeInstantaneousRewards(this->getModel(), this->getModel().getTransitionMatrix(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); + storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeInstantaneousRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); return std::unique_ptr>(new SymbolicQuantitativeCheckResult(this->getModel().getReachableStates(), numericResult)); } template std::unique_ptr SymbolicDtmcPrctlModelChecker::computeReachabilityRewards(CheckTask const& checkTask) { + storm::logic::ReachabilityRewardFormula const& rewardPathFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(rewardPathFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); - storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeReachabilityRewards(this->getModel(), this->getModel().getTransitionMatrix(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), qualitative, *this->linearEquationSolverFactory); + storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeReachabilityRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); return std::unique_ptr>(new SymbolicQuantitativeCheckResult(this->getModel().getReachableStates(), numericResult)); } diff --git a/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp b/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp index 376b4805f..76f7fbe4e 100644 --- a/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp @@ -45,61 +45,68 @@ namespace storm { template std::unique_ptr SymbolicMdpPrctlModelChecker::computeUntilProbabilities(CheckTask const& checkTask) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + storm::logic::UntilFormula 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 leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); SymbolicQualitativeCheckResult const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult(); SymbolicQualitativeCheckResult const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeUntilProbabilities(optimalityType.get() == OptimizationDirection::Minimize, this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, *this->linearEquationSolverFactory); + return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); } template std::unique_ptr SymbolicMdpPrctlModelChecker::computeGloballyProbabilities(CheckTask const& checkTask) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + storm::logic::GloballyFormula const& pathFormula = 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 subResultPointer = this->check(pathFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeGloballyProbabilities(optimalityType.get() == OptimizationDirection::Minimize, this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), qualitative, *this->linearEquationSolverFactory); + return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeGloballyProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); } template std::unique_ptr SymbolicMdpPrctlModelChecker::computeNextProbabilities(CheckTask const& checkTask) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + 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(pathFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeNextProbabilities(optimalityType.get() == OptimizationDirection::Minimize, this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector()); + return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeNextProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector()); } template std::unique_ptr SymbolicMdpPrctlModelChecker::computeBoundedUntilProbabilities(CheckTask const& checkTask) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + storm::logic::BoundedUntilFormula const& pathFormula = 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."); STORM_LOG_THROW(pathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); SymbolicQualitativeCheckResult const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult(); SymbolicQualitativeCheckResult const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeBoundedUntilProbabilities(optimalityType.get() == OptimizationDirection::Minimize, this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); + return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); } template std::unique_ptr SymbolicMdpPrctlModelChecker::computeCumulativeRewards(CheckTask const& checkTask) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + storm::logic::CumulativeRewardFormula const& rewardPathFormula = 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."); STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); - return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeCumulativeRewards(optimalityType.get() == OptimizationDirection::Minimize, this->getModel(), this->getModel().getTransitionMatrix(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); + return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeCumulativeRewards(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); } template std::unique_ptr SymbolicMdpPrctlModelChecker::computeInstantaneousRewards(CheckTask const& checkTask) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + storm::logic::InstantaneousRewardFormula const& rewardPathFormula = 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."); STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); - return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeInstantaneousRewards(optimalityType.get() == OptimizationDirection::Minimize, this->getModel(), this->getModel().getTransitionMatrix(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); + return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeInstantaneousRewards(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); } template std::unique_ptr SymbolicMdpPrctlModelChecker::computeReachabilityRewards(CheckTask const& checkTask) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + storm::logic::ReachabilityRewardFormula const& rewardPathFormula = 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(rewardPathFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeReachabilityRewards(optimalityType.get() == OptimizationDirection::Minimize, this->getModel(), this->getModel().getTransitionMatrix(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), qualitative, *this->linearEquationSolverFactory); + return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeReachabilityRewards(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); } template diff --git a/src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp b/src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp index 17705fdbb..52447c289 100644 --- a/src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp @@ -23,11 +23,11 @@ namespace storm { namespace helper { template - std::unique_ptr SymbolicMdpPrctlHelper::computeUntilProbabilities(bool minimize, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory) { + std::unique_ptr SymbolicMdpPrctlHelper::computeUntilProbabilities(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory) { // We need to identify the states which have to be taken out of the matrix, i.e. all states that have // probability 0 and 1 of satisfying the until-formula. std::pair, storm::dd::Bdd> statesWithProbability01; - if (minimize) { + if (dir == OptimizationDirection::Minimize) { statesWithProbability01 = storm::utility::graph::performProb01Min(model, phiStates, psiStates); } else { statesWithProbability01 = storm::utility::graph::performProb01Max(model, phiStates, psiStates); @@ -66,7 +66,7 @@ namespace storm { // Now solve the resulting equation system. std::unique_ptr> solver = linearEquationSolverFactory.create(submatrix, maybeStates, model.getIllegalMask() && maybeStates, model.getRowVariables(), model.getColumnVariables(), model.getNondeterminismVariables(), model.getRowColumnMetaVariablePairs()); - storm::dd::Add result = solver->solveEquationSystem(minimize, model.getManager().template getAddZero(), subvector); + storm::dd::Add result = solver->solveEquationSystem(dir == OptimizationDirection::Minimize, model.getManager().template getAddZero(), subvector); return std::unique_ptr(new storm::modelchecker::SymbolicQuantitativeCheckResult(model.getReachableStates(), statesWithProbability01.second.template toAdd() + result)); } else { @@ -76,24 +76,24 @@ namespace storm { } template - std::unique_ptr SymbolicMdpPrctlHelper::computeGloballyProbabilities(bool minimize, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory) { - std::unique_ptr result = computeUntilProbabilities(!minimize, model, transitionMatrix, model.getReachableStates(), !psiStates && model.getReachableStates(), qualitative, linearEquationSolverFactory); + std::unique_ptr SymbolicMdpPrctlHelper::computeGloballyProbabilities(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory) { + std::unique_ptr result = computeUntilProbabilities(dir == OptimizationDirection::Minimize ? OptimizationDirection::Maximize : OptimizationDirection::Minimize, model, transitionMatrix, model.getReachableStates(), !psiStates && model.getReachableStates(), qualitative, linearEquationSolverFactory); result->asQuantitativeCheckResult().oneMinus(); return result; } template - std::unique_ptr SymbolicMdpPrctlHelper::computeNextProbabilities(bool minimize, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& nextStates) { + std::unique_ptr SymbolicMdpPrctlHelper::computeNextProbabilities(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& nextStates) { storm::dd::Add result = transitionMatrix * nextStates.swapVariables(model.getRowColumnMetaVariablePairs()).template toAdd(); return std::unique_ptr(new SymbolicQuantitativeCheckResult(model.getReachableStates(), result.sumAbstract(model.getColumnVariables()))); } template - std::unique_ptr SymbolicMdpPrctlHelper::computeBoundedUntilProbabilities(bool minimize, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, uint_fast64_t stepBound, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory) { + std::unique_ptr SymbolicMdpPrctlHelper::computeBoundedUntilProbabilities(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, uint_fast64_t stepBound, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory) { // We need to identify the states which have to be taken out of the matrix, i.e. all states that have // probability 0 or 1 of satisfying the until-formula. storm::dd::Bdd statesWithProbabilityGreater0; - if (minimize) { + if (dir == OptimizationDirection::Minimize) { statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0A(model, transitionMatrix.notZero(), phiStates, psiStates); } else { statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0E(model, transitionMatrix.notZero(), phiStates, psiStates); @@ -118,7 +118,7 @@ namespace storm { submatrix *= maybeStatesAdd.swapVariables(model.getRowColumnMetaVariablePairs()); std::unique_ptr> solver = linearEquationSolverFactory.create(submatrix, maybeStates, model.getIllegalMask() && maybeStates, model.getRowVariables(), model.getColumnVariables(), model.getNondeterminismVariables(), model.getRowColumnMetaVariablePairs()); - storm::dd::Add result = solver->performMatrixVectorMultiplication(minimize, model.getManager().template getAddZero(), &subvector, stepBound); + storm::dd::Add result = solver->performMatrixVectorMultiplication(dir == OptimizationDirection::Minimize, model.getManager().template getAddZero(), &subvector, stepBound); return std::unique_ptr(new storm::modelchecker::SymbolicQuantitativeCheckResult(model.getReachableStates(), psiStates.template toAdd() + result)); } else { @@ -127,19 +127,19 @@ namespace storm { } template - std::unique_ptr SymbolicMdpPrctlHelper::computeInstantaneousRewards(bool minimize, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory) { + std::unique_ptr SymbolicMdpPrctlHelper::computeInstantaneousRewards(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory) { // Only compute the result if the model has at least one reward this->getModel(). STORM_LOG_THROW(rewardModel.hasStateRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); // Perform the matrix-vector multiplication. std::unique_ptr> solver = linearEquationSolverFactory.create(model.getTransitionMatrix(), model.getReachableStates(), model.getIllegalMask(), model.getRowVariables(), model.getColumnVariables(), model.getNondeterminismVariables(), model.getRowColumnMetaVariablePairs()); - storm::dd::Add result = solver->performMatrixVectorMultiplication(minimize, rewardModel.getStateRewardVector(), nullptr, stepBound); + storm::dd::Add result = solver->performMatrixVectorMultiplication(dir == OptimizationDirection::Minimize, rewardModel.getStateRewardVector(), nullptr, stepBound); return std::unique_ptr(new SymbolicQuantitativeCheckResult(model.getReachableStates(), result)); } template - std::unique_ptr SymbolicMdpPrctlHelper::computeCumulativeRewards(bool minimize, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory) { + std::unique_ptr SymbolicMdpPrctlHelper::computeCumulativeRewards(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory) { // Only compute the result if the model has at least one reward this->getModel(). STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); @@ -148,13 +148,13 @@ namespace storm { // Perform the matrix-vector multiplication. std::unique_ptr> solver = linearEquationSolverFactory.create(model.getTransitionMatrix(), model.getReachableStates(), model.getIllegalMask(), model.getRowVariables(), model.getColumnVariables(), model.getNondeterminismVariables(), model.getRowColumnMetaVariablePairs()); - storm::dd::Add result = solver->performMatrixVectorMultiplication(minimize, model.getManager().template getAddZero(), &totalRewardVector, stepBound); + storm::dd::Add result = solver->performMatrixVectorMultiplication(dir == OptimizationDirection::Minimize, model.getManager().template getAddZero(), &totalRewardVector, stepBound); return std::unique_ptr(new SymbolicQuantitativeCheckResult(model.getReachableStates(), result)); } template - std::unique_ptr SymbolicMdpPrctlHelper::computeReachabilityRewards(bool minimize, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, bool qualitative, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory) { + std::unique_ptr SymbolicMdpPrctlHelper::computeReachabilityRewards(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, bool qualitative, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory) { // Only compute the result if there is at least one reward model. STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); @@ -162,7 +162,7 @@ namespace storm { // Determine which states have a reward of infinity by definition. storm::dd::Bdd infinityStates; storm::dd::Bdd transitionMatrixBdd = transitionMatrix.notZero(); - if (minimize) { + if (dir == OptimizationDirection::Minimize) { infinityStates = storm::utility::graph::performProb1E(model, transitionMatrixBdd, model.getReachableStates(), targetStates, storm::utility::graph::performProbGreater0E(model, transitionMatrixBdd, model.getReachableStates(), targetStates)); } else { infinityStates = storm::utility::graph::performProb1A(model, transitionMatrixBdd, model.getReachableStates(), targetStates, storm::utility::graph::performProbGreater0A(model, transitionMatrixBdd, model.getReachableStates(), targetStates)); @@ -197,7 +197,7 @@ namespace storm { // Now solve the resulting equation system. std::unique_ptr> solver = linearEquationSolverFactory.create(submatrix, maybeStates, model.getIllegalMask() && maybeStates, model.getRowVariables(), model.getColumnVariables(), model.getNondeterminismVariables(), model.getRowColumnMetaVariablePairs()); - storm::dd::Add result = solver->solveEquationSystem(minimize, model.getManager().template getAddZero(), subvector); + storm::dd::Add result = solver->solveEquationSystem(dir == OptimizationDirection::Minimize, model.getManager().template getAddZero(), subvector); return std::unique_ptr(new storm::modelchecker::SymbolicQuantitativeCheckResult(model.getReachableStates(), infinityStates.ite(model.getManager().getConstant(storm::utility::infinity()), result))); } else { diff --git a/src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.h b/src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.h index 25b01d449..083840a00 100644 --- a/src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.h +++ b/src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.h @@ -7,6 +7,7 @@ #include "src/storage/dd/Bdd.h" #include "src/utility/solver.h" +#include "src/solver/SolveGoal.h" namespace storm { namespace modelchecker { @@ -20,19 +21,19 @@ namespace storm { public: typedef typename storm::models::symbolic::NondeterministicModel::RewardModelType RewardModelType; - static std::unique_ptr computeBoundedUntilProbabilities(bool minimize, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, uint_fast64_t stepBound, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory); + static std::unique_ptr computeBoundedUntilProbabilities(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, uint_fast64_t stepBound, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory); - static std::unique_ptr computeNextProbabilities(bool minimize, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& nextStates); + static std::unique_ptr computeNextProbabilities(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& nextStates); - static std::unique_ptr computeUntilProbabilities(bool minimize, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory); + static std::unique_ptr computeUntilProbabilities(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory); - static std::unique_ptr computeGloballyProbabilities(bool minimize, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory); + static std::unique_ptr computeGloballyProbabilities(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory); - static std::unique_ptr computeCumulativeRewards(bool minimize, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory); + static std::unique_ptr computeCumulativeRewards(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory); - static std::unique_ptr computeInstantaneousRewards(bool minimize, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory); + static std::unique_ptr computeInstantaneousRewards(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory); - static std::unique_ptr computeReachabilityRewards(bool minimize, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, bool qualitative, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory); + static std::unique_ptr computeReachabilityRewards(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, bool qualitative, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory); }; } diff --git a/src/modelchecker/propositional/SparsePropositionalModelChecker.cpp b/src/modelchecker/propositional/SparsePropositionalModelChecker.cpp index f309403cf..626835d6f 100644 --- a/src/modelchecker/propositional/SparsePropositionalModelChecker.cpp +++ b/src/modelchecker/propositional/SparsePropositionalModelChecker.cpp @@ -27,6 +27,7 @@ namespace storm { template std::unique_ptr SparsePropositionalModelChecker::checkBooleanLiteralFormula(CheckTask const& checkTask) { + storm::logic::BooleanLiteralFormula const& stateFormula = checkTask.getFormula(); if (stateFormula.isTrueFormula()) { return std::unique_ptr(new ExplicitQualitativeCheckResult(storm::storage::BitVector(model.getNumberOfStates(), true))); } else { @@ -36,6 +37,7 @@ namespace storm { template std::unique_ptr SparsePropositionalModelChecker::checkAtomicLabelFormula(CheckTask const& checkTask) { + storm::logic::AtomicLabelFormula const& stateFormula = checkTask.getFormula(); STORM_LOG_THROW(model.hasLabel(stateFormula.getLabel()), storm::exceptions::InvalidPropertyException, "The property refers to unknown label '" << stateFormula.getLabel() << "'."); return std::unique_ptr(new ExplicitQualitativeCheckResult(model.getStates(stateFormula.getLabel()))); } diff --git a/src/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp b/src/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp index 5c51c656d..1539d8efe 100644 --- a/src/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp +++ b/src/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp @@ -27,6 +27,7 @@ namespace storm { template std::unique_ptr SymbolicPropositionalModelChecker::checkBooleanLiteralFormula(CheckTask const& checkTask) { + storm::logic::BooleanLiteralFormula const& stateFormula = checkTask.getFormula(); if (stateFormula.isTrueFormula()) { return std::unique_ptr(new SymbolicQualitativeCheckResult(model.getReachableStates(), model.getReachableStates())); } else { @@ -36,12 +37,14 @@ namespace storm { template std::unique_ptr SymbolicPropositionalModelChecker::checkAtomicLabelFormula(CheckTask const& checkTask) { + storm::logic::AtomicLabelFormula const& stateFormula = checkTask.getFormula(); STORM_LOG_THROW(model.hasLabel(stateFormula.getLabel()), storm::exceptions::InvalidPropertyException, "The property refers to unknown label '" << stateFormula.getLabel() << "'."); return std::unique_ptr(new SymbolicQualitativeCheckResult(model.getReachableStates(), model.getStates(stateFormula.getLabel()))); } template std::unique_ptr SymbolicPropositionalModelChecker::checkAtomicExpressionFormula(CheckTask const& checkTask) { + storm::logic::AtomicExpressionFormula const& stateFormula = checkTask.getFormula(); return std::unique_ptr(new SymbolicQualitativeCheckResult(model.getReachableStates(), model.getStates(stateFormula.getExpression()))); } diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp index 08c492b72..adcb4dda1 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp @@ -75,7 +75,7 @@ namespace storm { } template - SparseDtmcEliminationModelChecker::SparseDtmcEliminationModelChecker(storm::models::sparse::Dtmc const& model, bool computeResultsForInitialStatesOnly) : SparsePropositionalModelChecker(model), computeResultsForInitialStatesOnly(computeResultsForInitialStatesOnly) { + SparseDtmcEliminationModelChecker::SparseDtmcEliminationModelChecker(storm::models::sparse::Dtmc const& model) : SparsePropositionalModelChecker(model) { // Intentionally left empty. } @@ -131,6 +131,7 @@ namespace storm { template std::unique_ptr SparseDtmcEliminationModelChecker::computeLongRunAverageProbabilities(CheckTask const& checkTask) { + storm::logic::StateFormula const& stateFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(stateFormula); storm::storage::BitVector const& psiStates = subResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector(); @@ -145,7 +146,7 @@ namespace storm { storm::storage::BitVector const& initialStates = this->getModel().getInitialStates(); STORM_LOG_THROW(initialStates.getNumberOfSetBits() == 1, storm::exceptions::IllegalArgumentException, "Input model is required to have exactly one initial state."); - STORM_LOG_THROW(this->computeResultsForInitialStatesOnly, storm::exceptions::IllegalArgumentException, "Cannot compute long-run probabilities for all states."); + STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::IllegalArgumentException, "Cannot compute long-run probabilities for all states."); storm::storage::SparseMatrix backwardTransitions = this->getModel().getBackwardTransitions(); storm::storage::BitVector maybeStates = storm::utility::graph::performProbGreater0(backwardTransitions, storm::storage::BitVector(transitionMatrix.getRowCount(), true), psiStates); @@ -154,7 +155,7 @@ namespace storm { // Determine whether we need to perform some further computation. bool furtherComputationNeeded = true; - if (computeResultsForInitialStatesOnly && initialStates.isDisjointFrom(maybeStates)) { + if (checkTask.isOnlyInitialStatesRelevantSet() && initialStates.isDisjointFrom(maybeStates)) { STORM_LOG_DEBUG("The long-run probability for all initial states was found in a preprocessing step."); furtherComputationNeeded = false; } @@ -164,7 +165,7 @@ namespace storm { } if (furtherComputationNeeded) { - if (computeResultsForInitialStatesOnly) { + if (checkTask.isOnlyInitialStatesRelevantSet()) { // Determine the set of states that is reachable from the initial state without jumping over a target state. storm::storage::BitVector reachableStates = storm::utility::graph::getReachableStates(transitionMatrix, initialStates, storm::storage::BitVector(numberOfStates, true), storm::storage::BitVector(numberOfStates, false)); @@ -174,12 +175,12 @@ namespace storm { std::vector stateValues(maybeStates.size(), storm::utility::zero()); storm::utility::vector::setVectorValues(stateValues, psiStates, storm::utility::one()); - result = computeLongRunValues(transitionMatrix, backwardTransitions, initialStates, maybeStates, computeResultsForInitialStatesOnly, stateValues); + result = computeLongRunValues(transitionMatrix, backwardTransitions, initialStates, maybeStates, checkTask.isOnlyInitialStatesRelevantSet(), stateValues); } // Construct check result based on whether we have computed values for all states or just the initial states. std::unique_ptr checkResult(new ExplicitQuantitativeCheckResult(result)); - if (computeResultsForInitialStatesOnly) { + if (checkTask.isOnlyInitialStatesRelevantSet()) { // If we computed the results for the initial states only, we need to filter the result to only // communicate these results. checkResult->filter(ExplicitQualitativeCheckResult(initialStates)); @@ -188,14 +189,14 @@ namespace storm { } template - std::unique_ptr SparseDtmcEliminationModelChecker::computeLongRunAverageRewards(storm::logic::LongRunAverageRewardFormula const& rewardPathFormula, CheckSettings const& checkTask) { + std::unique_ptr SparseDtmcEliminationModelChecker::computeLongRunAverageRewards(CheckTask const& checkTask) { // Do some sanity checks to establish some required properties. - RewardModelType const& rewardModel = this->getModel().getRewardModel(rewardModelName ? rewardModelName.get() : ""); + RewardModelType const& rewardModel = this->getModel().getRewardModel(checkTask.isRewardModelSet() ? checkTask.getRewardModel() : ""); STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::IllegalArgumentException, "Input model does not have a reward model."); storm::storage::BitVector const& initialStates = this->getModel().getInitialStates(); STORM_LOG_THROW(initialStates.getNumberOfSetBits() == 1, storm::exceptions::IllegalArgumentException, "Input model is required to have exactly one initial state."); - STORM_LOG_THROW(this->computeResultsForInitialStatesOnly, storm::exceptions::IllegalArgumentException, "Cannot compute long-run probabilities for all states."); + STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::IllegalArgumentException, "Cannot compute long-run probabilities for all states."); storm::storage::SparseMatrix const& transitionMatrix = this->getModel().getTransitionMatrix(); uint_fast64_t numberOfStates = transitionMatrix.getRowCount(); @@ -221,12 +222,12 @@ namespace storm { // Determine whether we need to perform some further computation. bool furtherComputationNeeded = true; - if (computeResultsForInitialStatesOnly && initialStates.isDisjointFrom(maybeStates)) { + if (checkTask.isOnlyInitialStatesRelevantSet() && initialStates.isDisjointFrom(maybeStates)) { furtherComputationNeeded = false; } if (furtherComputationNeeded) { - if (computeResultsForInitialStatesOnly) { + if (checkTask.isOnlyInitialStatesRelevantSet()) { // Determine the set of states that is reachable from the initial state without jumping over a target state. storm::storage::BitVector reachableStates = storm::utility::graph::getReachableStates(transitionMatrix, initialStates, storm::storage::BitVector(numberOfStates, true), storm::storage::BitVector(numberOfStates, false)); @@ -234,12 +235,12 @@ namespace storm { maybeStates &= reachableStates; } - result = computeLongRunValues(transitionMatrix, backwardTransitions, initialStates, maybeStates, computeResultsForInitialStatesOnly, stateRewardValues); + result = computeLongRunValues(transitionMatrix, backwardTransitions, initialStates, maybeStates, checkTask.isOnlyInitialStatesRelevantSet(), stateRewardValues); } // Construct check result based on whether we have computed values for all states or just the initial states. std::unique_ptr checkResult(new ExplicitQuantitativeCheckResult(result)); - if (computeResultsForInitialStatesOnly) { + if (checkTask.isOnlyInitialStatesRelevantSet()) { // If we computed the results for the initial states only, we need to filter the result to only // communicate these results. checkResult->filter(ExplicitQualitativeCheckResult(initialStates)); @@ -411,6 +412,8 @@ namespace storm { template std::unique_ptr SparseDtmcEliminationModelChecker::computeBoundedUntilProbabilities(CheckTask const& checkTask) { + storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); + // Retrieve the appropriate bitvectors by model checking the subformulas. std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); @@ -424,7 +427,7 @@ namespace storm { // Determine whether we need to perform some further computation. bool furtherComputationNeeded = true; - if (computeResultsForInitialStatesOnly && this->getModel().getInitialStates().isDisjointFrom(statesWithProbabilityGreater0)) { + if (checkTask.isOnlyInitialStatesRelevantSet() && this->getModel().getInitialStates().isDisjointFrom(statesWithProbabilityGreater0)) { STORM_LOG_DEBUG("The probability for all initial states was found in a preprocessing step."); furtherComputationNeeded = false; } else if (statesWithProbabilityGreater0.empty()) { @@ -440,7 +443,7 @@ namespace storm { if (furtherComputationNeeded) { uint_fast64_t timeBound = pathFormula.getDiscreteTimeBound(); - if (computeResultsForInitialStatesOnly) { + if (checkTask.isOnlyInitialStatesRelevantSet()) { // Determine the set of states that is reachable from the initial state without jumping over a target state. storm::storage::BitVector reachableStates = storm::utility::graph::getReachableStates(transitionMatrix, initialStates, phiStates, psiStates, true, timeBound); @@ -453,7 +456,7 @@ namespace storm { std::vector distancesFromInitialStates; storm::storage::BitVector relevantStates; - if (computeResultsForInitialStatesOnly) { + if (checkTask.isOnlyInitialStatesRelevantSet()) { // Determine the set of initial states of the sub-model. storm::storage::BitVector subInitialStates = this->getModel().getInitialStates() % statesWithProbabilityGreater0; @@ -482,7 +485,7 @@ namespace storm { // If we are computing the results for the initial states only, we can use the minimal distance from // each state to the initial states to determine whether we still need to consider the values for // these states. If not, we can null-out all their probabilities. - if (computeResultsForInitialStatesOnly) { + if (checkTask.isOnlyInitialStatesRelevantSet()) { for (auto state : relevantStates) { if (distancesFromInitialStates[state] > (timeBound - timeStep)) { for (auto& element : submatrix.getRow(state)) { @@ -502,7 +505,7 @@ namespace storm { // Construct check result based on whether we have computed values for all states or just the initial states. std::unique_ptr checkResult(new ExplicitQuantitativeCheckResult(result)); - if (computeResultsForInitialStatesOnly) { + if (checkTask.isOnlyInitialStatesRelevantSet()) { // If we computed the results for the initial (and prob 0 and prob1) states only, we need to filter the // result to only communicate these results. checkResult->filter(ExplicitQualitativeCheckResult(this->getModel().getInitialStates() | psiStates)); @@ -512,6 +515,8 @@ namespace storm { template std::unique_ptr SparseDtmcEliminationModelChecker::computeUntilProbabilities(CheckTask const& checkTask) { + storm::logic::UntilFormula const& pathFormula = checkTask.getFormula(); + // Retrieve the appropriate bitvectors by model checking the subformulas. std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); @@ -526,7 +531,7 @@ namespace storm { // Determine whether we need to perform some further computation. bool furtherComputationNeeded = true; - if (computeResultsForInitialStatesOnly && this->getModel().getInitialStates().isDisjointFrom(maybeStates)) { + if (checkTask.isOnlyInitialStatesRelevantSet() && this->getModel().getInitialStates().isDisjointFrom(maybeStates)) { STORM_LOG_DEBUG("The probability for all initial states was found in a preprocessing step."); furtherComputationNeeded = false; } else if (maybeStates.empty()) { @@ -538,7 +543,7 @@ namespace storm { if (furtherComputationNeeded) { // If we compute the results for the initial states only, we can cut off all maybe state that are not // reachable from them. - if (computeResultsForInitialStatesOnly) { + if (checkTask.isOnlyInitialStatesRelevantSet()) { // Determine the set of states that is reachable from the initial state without jumping over a target state. storm::storage::BitVector reachableStates = storm::utility::graph::getReachableStates(this->getModel().getTransitionMatrix(), this->getModel().getInitialStates(), maybeStates, statesWithProbability1); @@ -556,7 +561,7 @@ namespace storm { storm::storage::SparseMatrix submatrix = this->getModel().getTransitionMatrix().getSubmatrix(false, maybeStates, maybeStates); storm::storage::SparseMatrix submatrixTransposed = submatrix.transpose(); - std::vector subresult = computeReachabilityValues(submatrix, oneStepProbabilities, submatrixTransposed, newInitialStates, computeResultsForInitialStatesOnly, phiStates, psiStates, oneStepProbabilities); + std::vector subresult = computeReachabilityValues(submatrix, oneStepProbabilities, submatrixTransposed, newInitialStates, checkTask.isOnlyInitialStatesRelevantSet(), phiStates, psiStates, oneStepProbabilities); storm::utility::vector::setVectorValues(result, maybeStates, subresult); } @@ -566,7 +571,7 @@ namespace storm { // Construct check result based on whether we have computed values for all states or just the initial states. std::unique_ptr checkResult(new ExplicitQuantitativeCheckResult(result)); - if (computeResultsForInitialStatesOnly) { + if (checkTask.isOnlyInitialStatesRelevantSet()) { // If we computed the results for the initial (and prob 0 and prob1) states only, we need to filter the // result to only communicate these results. checkResult->filter(ExplicitQualitativeCheckResult(~maybeStates | this->getModel().getInitialStates())); @@ -576,13 +581,15 @@ namespace storm { template std::unique_ptr SparseDtmcEliminationModelChecker::computeReachabilityRewards(CheckTask const& checkTask) { + storm::logic::ReachabilityRewardFormula const& rewardPathFormula = checkTask.getFormula(); + // Retrieve the appropriate bitvectors by model checking the subformulas. std::unique_ptr subResultPointer = this->check(rewardPathFormula.getSubformula()); storm::storage::BitVector phiStates(this->getModel().getNumberOfStates(), true); storm::storage::BitVector const& psiStates = subResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector(); // Do some sanity checks to establish some required properties. - RewardModelType const& rewardModel = this->getModel().getRewardModel(rewardModelName ? rewardModelName.get() : ""); + RewardModelType const& rewardModel = this->getModel().getRewardModel(checkTask.isRewardModelSet() ? checkTask.getRewardModel() : ""); STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::IllegalArgumentException, "Input model does not have a reward model."); // Then, compute the subset of states that has a reachability reward less than infinity. @@ -593,7 +600,7 @@ namespace storm { // Determine whether we need to perform some further computation. bool furtherComputationNeeded = true; - if (computeResultsForInitialStatesOnly) { + if (checkTask.isOnlyInitialStatesRelevantSet()) { if (this->getModel().getInitialStates().isSubsetOf(infinityStates)) { STORM_LOG_DEBUG("The reward of all initial states was found in a preprocessing step."); furtherComputationNeeded = false; @@ -608,7 +615,7 @@ namespace storm { if (furtherComputationNeeded) { // If we compute the results for the initial states only, we can cut off all maybe state that are not // reachable from them. - if (computeResultsForInitialStatesOnly) { + if (checkTask.isOnlyInitialStatesRelevantSet()) { // Determine the set of states that is reachable from the initial state without jumping over a target state. storm::storage::BitVector reachableStates = storm::utility::graph::getReachableStates(this->getModel().getTransitionMatrix(), this->getModel().getInitialStates(), maybeStates, psiStates); @@ -626,7 +633,7 @@ namespace storm { // Project the state reward vector to all maybe-states. std::vector stateRewardValues = rewardModel.getTotalRewardVector(maybeStates.getNumberOfSetBits(), this->getModel().getTransitionMatrix(), maybeStates); - std::vector subresult = computeReachabilityValues(submatrix, stateRewardValues, submatrixTransposed, newInitialStates, computeResultsForInitialStatesOnly, phiStates, psiStates, this->getModel().getTransitionMatrix().getConstrainedRowSumVector(maybeStates, psiStates)); + std::vector subresult = computeReachabilityValues(submatrix, stateRewardValues, submatrixTransposed, newInitialStates, checkTask.isOnlyInitialStatesRelevantSet(), phiStates, psiStates, this->getModel().getTransitionMatrix().getConstrainedRowSumVector(maybeStates, psiStates)); storm::utility::vector::setVectorValues(result, maybeStates, subresult); } @@ -636,7 +643,7 @@ namespace storm { // Construct check result based on whether we have computed values for all states or just the initial states. std::unique_ptr checkResult(new ExplicitQuantitativeCheckResult(result)); - if (computeResultsForInitialStatesOnly) { + if (checkTask.isOnlyInitialStatesRelevantSet()) { // If we computed the results for the initial (and inf) states only, we need to filter the result to // only communicate these results. checkResult->filter(ExplicitQualitativeCheckResult(~maybeStates | this->getModel().getInitialStates())); @@ -646,7 +653,7 @@ namespace storm { template std::unique_ptr SparseDtmcEliminationModelChecker::computeConditionalProbabilities(CheckTask const& checkTask) { - std::chrono::high_resolution_clock::time_point totalTimeStart = std::chrono::high_resolution_clock::now(); + storm::logic::ConditionalPathFormula const& pathFormula = checkTask.getFormula(); // Retrieve the appropriate bitvectors by model checking the subformulas. STORM_LOG_THROW(pathFormula.getLeftSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Expected 'eventually' formula."); @@ -661,7 +668,7 @@ namespace storm { // Do some sanity checks to establish some required properties. // STORM_LOG_WARN_COND(storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationMethod() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationMethod::State, "The chosen elimination method is not available for computing conditional probabilities. Falling back to regular state elimination."); STORM_LOG_THROW(this->getModel().getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::IllegalArgumentException, "Input model is required to have exactly one initial state."); - STORM_LOG_THROW(this->computeResultsForInitialStatesOnly, storm::exceptions::IllegalArgumentException, "Cannot compute conditional probabilities for all states."); + STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::IllegalArgumentException, "Cannot compute conditional probabilities for all states."); storm::storage::sparse::state_type initialState = *this->getModel().getInitialStates().begin(); storm::storage::SparseMatrix backwardTransitions = this->getModel().getBackwardTransitions(); @@ -690,18 +697,10 @@ namespace storm { storm::storage::BitVector statesReachingPhi = storm::utility::graph::performProbGreater0(backwardTransitions, trueStates, phiStates); // The set of states we need to consider are those that have a non-zero probability to satisfy the condition or are on some path that has a psi state in it. - STORM_LOG_TRACE("Initial state: " << this->getModel().getInitialStates()); - STORM_LOG_TRACE("Phi states: " << phiStates); - STORM_LOG_TRACE("Psi state: " << psiStates); - STORM_LOG_TRACE("States with probability greater 0 of satisfying the condition: " << statesWithProbabilityGreater0); - STORM_LOG_TRACE("States with psi predecessor: " << statesWithPsiPredecessor); - STORM_LOG_TRACE("States reaching phi: " << statesReachingPhi); storm::storage::BitVector maybeStates = statesWithProbabilityGreater0 | (statesWithPsiPredecessor & statesReachingPhi); - STORM_LOG_TRACE("Found " << maybeStates.getNumberOfSetBits() << " relevant states: " << maybeStates); // Determine the set of initial states of the sub-DTMC. storm::storage::BitVector newInitialStates = this->getModel().getInitialStates() % maybeStates; - STORM_LOG_TRACE("Found new initial states: " << newInitialStates << " (old: " << this->getModel().getInitialStates() << ")"); // Create a dummy vector for the one-step probabilities. std::vector oneStepProbabilities(maybeStates.getNumberOfSetBits(), storm::utility::zero()); @@ -723,10 +722,7 @@ namespace storm { // Keep only the states that we do not eliminate in the maybe states. maybeStates = phiStates | psiStates; - STORM_LOG_TRACE("Phi states in reduced model " << phiStates); - STORM_LOG_TRACE("Psi states in reduced model " << psiStates); storm::storage::BitVector statesToEliminate = ~maybeStates & ~newInitialStates; - STORM_LOG_TRACE("Eliminating the states " << statesToEliminate); // Before starting the model checking process, we assign priorities to states so we can use them to // impose ordering constraints later. @@ -738,19 +734,11 @@ namespace storm { eliminationOrderNeedsReversedDistances(order)); } - std::chrono::high_resolution_clock::time_point conversionStart = std::chrono::high_resolution_clock::now(); FlexibleSparseMatrix flexibleMatrix = getFlexibleSparseMatrix(submatrix); FlexibleSparseMatrix flexibleBackwardTransitions = getFlexibleSparseMatrix(submatrixTransposed, true); - std::chrono::high_resolution_clock::time_point conversionEnd = std::chrono::high_resolution_clock::now(); std::unique_ptr statePriorities = createStatePriorityQueue(distanceBasedPriorities, flexibleMatrix, flexibleBackwardTransitions, oneStepProbabilities, statesToEliminate); - - STORM_LOG_INFO("Computing conditional probilities." << std::endl); - std::chrono::high_resolution_clock::time_point modelCheckingStart = std::chrono::high_resolution_clock::now(); - uint_fast64_t numberOfStatesToEliminate = statePriorities->size(); - STORM_LOG_INFO("Eliminating " << numberOfStatesToEliminate << " states using the state elimination technique." << std::endl); performPrioritizedStateElimination(statePriorities, flexibleMatrix, flexibleBackwardTransitions, oneStepProbabilities, this->getModel().getInitialStates(), true); - STORM_LOG_INFO("Eliminated " << numberOfStatesToEliminate << " states." << std::endl); // Prepare some callbacks for the elimination procedure. ValueUpdateCallback valueUpdateCallback = [&oneStepProbabilities] (storm::storage::sparse::state_type const& state, ValueType const& loopProbability) { oneStepProbabilities[state] = storm::utility::simplify(loopProbability * oneStepProbabilities[state]); }; @@ -866,25 +854,6 @@ namespace storm { numerator += trans1.getValue() * additiveTerm; } } - std::chrono::high_resolution_clock::time_point modelCheckingEnd = std::chrono::high_resolution_clock::now(); - std::chrono::high_resolution_clock::time_point totalTimeEnd = std::chrono::high_resolution_clock::now(); - - if (storm::settings::generalSettings().isShowStatisticsSet()) { - std::chrono::high_resolution_clock::duration conversionTime = conversionEnd - conversionStart; - std::chrono::milliseconds conversionTimeInMilliseconds = std::chrono::duration_cast(conversionTime); - std::chrono::high_resolution_clock::duration modelCheckingTime = modelCheckingEnd - modelCheckingStart; - std::chrono::milliseconds modelCheckingTimeInMilliseconds = std::chrono::duration_cast(modelCheckingTime); - std::chrono::high_resolution_clock::duration totalTime = totalTimeEnd - totalTimeStart; - std::chrono::milliseconds totalTimeInMilliseconds = std::chrono::duration_cast(totalTime); - - STORM_PRINT_AND_LOG(std::endl); - STORM_PRINT_AND_LOG("Time breakdown:" << std::endl); - STORM_PRINT_AND_LOG(" * time for conversion: " << conversionTimeInMilliseconds.count() << "ms" << std::endl); - STORM_PRINT_AND_LOG(" * time for checking: " << modelCheckingTimeInMilliseconds.count() << "ms" << std::endl); - STORM_PRINT_AND_LOG("------------------------------------------" << std::endl); - STORM_PRINT_AND_LOG(" * total time: " << totalTimeInMilliseconds.count() << "ms" << std::endl); - STORM_PRINT_AND_LOG(std::endl); - } return std::unique_ptr(new ExplicitQuantitativeCheckResult(initialState, numerator / denominator)); } @@ -988,15 +957,9 @@ namespace storm { template std::vector::ValueType> SparseDtmcEliminationModelChecker::computeReachabilityValues(storm::storage::SparseMatrix const& transitionMatrix, std::vector& values, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector const& oneStepProbabilitiesToTarget) { - std::chrono::high_resolution_clock::time_point totalTimeStart = std::chrono::high_resolution_clock::now(); - - std::chrono::high_resolution_clock::time_point conversionStart = std::chrono::high_resolution_clock::now(); // Then, we convert the reduced matrix to a more flexible format to be able to perform state elimination more easily. FlexibleSparseMatrix flexibleMatrix = getFlexibleSparseMatrix(transitionMatrix); FlexibleSparseMatrix flexibleBackwardTransitions = getFlexibleSparseMatrix(backwardTransitions); - auto conversionEnd = std::chrono::high_resolution_clock::now(); - - std::chrono::high_resolution_clock::time_point modelCheckingStart = std::chrono::high_resolution_clock::now(); storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder order = storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationOrder(); boost::optional> distanceBasedPriorities; @@ -1018,31 +981,6 @@ namespace storm { STORM_LOG_ASSERT(flexibleMatrix.empty(), "Not all transitions were eliminated."); STORM_LOG_ASSERT(flexibleBackwardTransitions.empty(), "Not all transitions were eliminated."); - std::chrono::high_resolution_clock::time_point modelCheckingEnd = std::chrono::high_resolution_clock::now(); - std::chrono::high_resolution_clock::time_point totalTimeEnd = std::chrono::high_resolution_clock::now(); - - if (storm::settings::generalSettings().isShowStatisticsSet()) { - std::chrono::high_resolution_clock::duration conversionTime = conversionEnd - conversionStart; - std::chrono::milliseconds conversionTimeInMilliseconds = std::chrono::duration_cast(conversionTime); - std::chrono::high_resolution_clock::duration modelCheckingTime = modelCheckingEnd - modelCheckingStart; - std::chrono::milliseconds modelCheckingTimeInMilliseconds = std::chrono::duration_cast(modelCheckingTime); - std::chrono::high_resolution_clock::duration totalTime = totalTimeEnd - totalTimeStart; - std::chrono::milliseconds totalTimeInMilliseconds = std::chrono::duration_cast(totalTime); - - STORM_PRINT_AND_LOG(std::endl); - STORM_PRINT_AND_LOG("Time breakdown:" << std::endl); - STORM_PRINT_AND_LOG(" * time for conversion: " << conversionTimeInMilliseconds.count() << "ms" << std::endl); - STORM_PRINT_AND_LOG(" * time for checking: " << modelCheckingTimeInMilliseconds.count() << "ms" << std::endl); - STORM_PRINT_AND_LOG("------------------------------------------" << std::endl); - STORM_PRINT_AND_LOG(" * total time: " << totalTimeInMilliseconds.count() << "ms" << std::endl); - STORM_PRINT_AND_LOG(std::endl); - STORM_PRINT_AND_LOG("Other:" << std::endl); - STORM_PRINT_AND_LOG(" * number of states eliminated: " << transitionMatrix.getRowCount() << std::endl); - if (storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationMethod() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationMethod::Hybrid) { - STORM_PRINT_AND_LOG(" * maximal depth of SCC decomposition: " << maximalDepth << std::endl); - } - } - // Now, we return the value for the only initial state. STORM_LOG_DEBUG("Simplifying and returning result."); for (auto& value : values) { @@ -1243,7 +1181,6 @@ namespace storm { auto successorEntry = storm::utility::simplify(std::move(*first2 * multiplyFactor)); *result = successorEntry; newBackwardProbabilities[successorOffsetInNewBackwardTransitions].emplace_back(predecessor, successorEntry.getValue()); -// std::cout << "(1) adding " << first2->getColumn() << " -> " << newBackwardProbabilities[successorOffsetInNewBackwardTransitions].back() << "[" << successorOffsetInNewBackwardTransitions << "]" << std::endl; ++first2; ++successorOffsetInNewBackwardTransitions; } else if (first1->getColumn() < first2->getColumn()) { @@ -1253,7 +1190,6 @@ namespace storm { auto probability = storm::utility::simplify(first1->getValue() + storm::utility::simplify(multiplyFactor * first2->getValue())); *result = storm::storage::MatrixEntry(first1->getColumn(), probability); newBackwardProbabilities[successorOffsetInNewBackwardTransitions].emplace_back(predecessor, probability); -// std::cout << "(2) adding " << first2->getColumn() << " -> " << newBackwardProbabilities[successorOffsetInNewBackwardTransitions].back() << "[" << successorOffsetInNewBackwardTransitions << "]" << std::endl; ++first1; ++first2; ++successorOffsetInNewBackwardTransitions; @@ -1264,7 +1200,6 @@ namespace storm { auto stateProbability = storm::utility::simplify(std::move(*first2 * multiplyFactor)); *result = stateProbability; newBackwardProbabilities[successorOffsetInNewBackwardTransitions].emplace_back(predecessor, stateProbability.getValue()); -// std::cout << "(3) adding " << first2->getColumn() << " -> " << newBackwardProbabilities[successorOffsetInNewBackwardTransitions].back() << "[" << successorOffsetInNewBackwardTransitions << "]" << std::endl; ++successorOffsetInNewBackwardTransitions; } } @@ -1289,10 +1224,6 @@ namespace storm { } typename FlexibleSparseMatrix::row_type& successorBackwardTransitions = backwardTransitions.getRow(successorEntry.getColumn()); -// std::cout << "old backward trans of " << successorEntry.getColumn() << std::endl; -// for (auto const& trans : successorBackwardTransitions) { -// std::cout << trans << std::endl; -// } // Delete the current state as a predecessor of the successor state only if we are going to remove the // current state's forward transitions. @@ -1307,11 +1238,6 @@ namespace storm { typename FlexibleSparseMatrix::row_type::iterator first2 = newBackwardProbabilities[successorOffsetInNewBackwardTransitions].begin(); typename FlexibleSparseMatrix::row_type::iterator last2 = newBackwardProbabilities[successorOffsetInNewBackwardTransitions].end(); -// std::cout << "adding backward trans " << successorEntry.getColumn() << "[" << successorOffsetInNewBackwardTransitions << "]" << std::endl; -// for (auto const& trans : newBackwardProbabilities[successorOffsetInNewBackwardTransitions]) { -// std::cout << trans << std::endl; -// } - typename FlexibleSparseMatrix::row_type newPredecessors; newPredecessors.reserve((last1 - first1) + (last2 - first2)); std::insert_iterator result(newPredecessors, newPredecessors.end()); @@ -1347,10 +1273,6 @@ namespace storm { // Now move the new predecessors in place. successorBackwardTransitions = std::move(newPredecessors); -// std::cout << "new backward trans of " << successorEntry.getColumn() << std::endl; -// for (auto const& trans : successorBackwardTransitions) { -// std::cout << trans << std::endl; -// } ++successorOffsetInNewBackwardTransitions; } STORM_LOG_TRACE("Fixed predecessor lists of successor states."); @@ -1649,9 +1571,6 @@ namespace storm { } if (!foundCorrespondingElement) { -// std::cout << "forward entry: " << forwardIndex << " -> " << forwardEntry << std::endl; -// transitionMatrix.print(); -// backwardTransitions.print(); return false; } } diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h index 956cd239e..cfaead9ed 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h @@ -19,16 +19,15 @@ namespace storm { * Creates an elimination-based model checker for the given model. * * @param model The model to analyze. - * @param computeResultsForInitialStatesOnly If set to true, the results are only computed for */ - explicit SparseDtmcEliminationModelChecker(storm::models::sparse::Dtmc const& model, bool computeResultsForInitialStatesOnly = true); + explicit SparseDtmcEliminationModelChecker(storm::models::sparse::Dtmc const& model); // The implemented methods of the AbstractModelChecker interface. virtual bool canHandle(storm::logic::Formula const& formula) const override; virtual std::unique_ptr computeBoundedUntilProbabilities(CheckTask const& checkTask) override; virtual std::unique_ptr computeUntilProbabilities(CheckTask const& checkTask) override; virtual std::unique_ptr computeReachabilityRewards(CheckTask const& checkTask) override; - virtual std::unique_ptr computeLongRunAverageRewards(storm::logic::LongRunAverageRewardFormula const& rewardPathFormula, CheckSettings const& checkTask) override; + virtual std::unique_ptr computeLongRunAverageRewards(CheckTask const& checkTask) override; virtual std::unique_ptr computeConditionalProbabilities(CheckTask const& checkTask) override; virtual std::unique_ptr computeLongRunAverageProbabilities(CheckTask const& checkTask) override; @@ -150,9 +149,6 @@ namespace storm { static bool checkConsistent(FlexibleSparseMatrix& transitionMatrix, FlexibleSparseMatrix& backwardTransitions); - // A flag that indicates whether this model checker is supposed to produce results for all states or just for the initial states. - bool computeResultsForInitialStatesOnly; - }; } // namespace modelchecker diff --git a/test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp b/test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp index 7ce394070..ad4d9ab3d 100644 --- a/test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp +++ b/test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp @@ -94,14 +94,14 @@ TEST(SparseDtmcEliminationModelCheckerTest, Crowds) { formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\" || F \"observeIGreater1\"]"); - result = checker.check(*formula); + result = checker.check(storm::modelchecker::CheckTask(*formula).setOnlyInitialStatesRelevant(true)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.15330064292476167, quantitativeResult4[0], storm::settings::generalSettings().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeOnlyTrueSender\" || F \"observe0Greater1\"]"); - result = checker.check(*formula); + result = checker.check(storm::modelchecker::CheckTask(*formula).setOnlyInitialStatesRelevant(true)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.96592521978041668, quantitativeResult5[0], storm::settings::generalSettings().getPrecision());