From 41828ca27d444668ecb45b2825fdc4940c4f1045 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 20 Oct 2017 15:38:24 +0200 Subject: [PATCH] more work on bisimulation-based abstraction-refinement --- src/storm/modelchecker/CheckTask.h | 7 + .../PartialBisimulationMdpModelChecker.cpp | 226 +++++++++++++++++- .../PartialBisimulationMdpModelChecker.h | 53 +++- .../prctl/helper/SymbolicMdpPrctlHelper.cpp | 2 +- .../SymbolicQuantitativeCheckResult.cpp | 10 + .../results/SymbolicQuantitativeCheckResult.h | 4 +- src/storm/models/ModelBase.h | 10 + src/storm/models/sparse/Model.cpp | 6 + src/storm/models/sparse/Model.h | 11 +- src/storm/models/symbolic/Model.h | 6 +- .../storage/dd/BisimulationDecomposition.cpp | 44 ++-- .../storage/dd/BisimulationDecomposition.h | 8 + 12 files changed, 349 insertions(+), 38 deletions(-) diff --git a/src/storm/modelchecker/CheckTask.h b/src/storm/modelchecker/CheckTask.h index cc0de06c0..093c40ca8 100644 --- a/src/storm/modelchecker/CheckTask.h +++ b/src/storm/modelchecker/CheckTask.h @@ -128,6 +128,13 @@ namespace storm { return optimizationDirection.get(); } + /*! + * Sets the optimization direction. + */ + void setOptimizationDirection(storm::OptimizationDirection const& dir) { + optimizationDirection = dir; + } + /*! * Retrieves whether a reward model was set. */ diff --git a/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.cpp index d52065969..d1ec80394 100644 --- a/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.cpp @@ -2,34 +2,252 @@ #include "storm/models/symbolic/Dtmc.h" #include "storm/models/symbolic/Mdp.h" +#include "storm/models/symbolic/StochasticTwoPlayerGame.h" #include "storm/modelchecker/results/CheckResult.h" +#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h" +#include "storm/modelchecker/results/SymbolicQuantitativeCheckResult.h" +#include "storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h" +#include "storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h" #include "storm/logic/FragmentSpecification.h" +#include "storm/storage/dd/Bdd.h" +#include "storm/storage/dd/BisimulationDecomposition.h" + +#include "storm/settings/SettingsManager.h" +#include "storm/settings/modules/AbstractionSettings.h" + +#include "storm/utility/macros.h" +#include "storm/exceptions/NotSupportedException.h" +#include "storm/exceptions/InvalidPropertyException.h" +#include "storm/exceptions/NotImplementedException.h" +#include "storm/exceptions/InvalidTypeException.h" + namespace storm { namespace modelchecker { template - PartialBisimulationMdpModelChecker::PartialBisimulationMdpModelChecker(ModelType const& model) : SymbolicPropositionalModelChecker(model) { + PartialBisimulationMdpModelChecker::PartialBisimulationMdpModelChecker(ModelType const& model) : AbstractModelChecker(), model(model) { // Intentionally left empty. } template bool PartialBisimulationMdpModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); - storm::logic::FragmentSpecification fragment = storm::logic::reachability(); + storm::logic::FragmentSpecification fragment = storm::logic::reachability().setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true); return formula.isInFragment(fragment) && checkTask.isOnlyInitialStatesRelevantSet(); } template std::unique_ptr PartialBisimulationMdpModelChecker::computeUntilProbabilities(CheckTask const& checkTask) { - return nullptr; + return computeValuesAbstractionRefinement(false, checkTask.substituteFormula(checkTask.getFormula())); } template std::unique_ptr PartialBisimulationMdpModelChecker::computeReachabilityProbabilities(CheckTask const& checkTask) { - return nullptr; + return computeValuesAbstractionRefinement(false, checkTask.substituteFormula(checkTask.getFormula())); + } + + template + std::unique_ptr PartialBisimulationMdpModelChecker::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + STORM_LOG_THROW(rewardMeasureType == storm::logic::RewardMeasureType::Expectation, storm::exceptions::InvalidPropertyException, "Can only compute reward expectations."); + return computeValuesAbstractionRefinement(true, checkTask.template substituteFormula(checkTask.getFormula())); + } + + template + std::unique_ptr PartialBisimulationMdpModelChecker::computeValuesAbstractionRefinement(bool rewards, CheckTask const& checkTask) { + + STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::InvalidPropertyException, "The game-based abstraction refinement model checker can only compute the result for the initial states."); + + // Create the appropriate preservation information. + storm::dd::bisimulation::PreservationInformation preservationInformation(model, storm::storage::BisimulationType::Strong); + if (checkTask.isRewardModelSet()) { + if (checkTask.getRewardModel() != "" || model.hasRewardModel(checkTask.getRewardModel())) { + preservationInformation.addRewardModel(checkTask.getRewardModel()); + } else if (model.hasUniqueRewardModel()) { + preservationInformation.addRewardModel(model.getUniqueRewardModelName()); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Property refers to illegal reward model '" << checkTask.getRewardModel() << "'."); + } + } + + // Create a bisimulation object that is used to obtain (partial) quotients. + storm::dd::BisimulationDecomposition bisimulation(this->model, {checkTask.getFormula().asSharedPointer()}, storm::storage::BisimulationType::Strong); + + auto start = std::chrono::high_resolution_clock::now(); + + uint64_t iterations = 0; + std::unique_ptr result; + while (!result) { + bool fullQuotient = bisimulation.getReachedFixedPoint(); + std::shared_ptr> quotient = bisimulation.getQuotient(); + STORM_LOG_TRACE("Model in iteration " << (iterations + 1) << " has " << quotient->getNumberOfStates() << " states and " << quotient->getNumberOfTransitions() << " transitions."); + + if (fullQuotient) { + STORM_LOG_TRACE("Reached final quotient."); + quotient->printModelInformationToStream(std::cout); + result = computeResultFullQuotient(*quotient, rewards, checkTask); + } else { + // Obtain lower and upper bounds from the partial quotient. + std::pair, std::unique_ptr> bounds = computeBoundsPartialQuotient(*quotient, rewards, checkTask); + + // Check whether the bounds are sufficiently close. + bool converged = checkBoundsSufficientlyClose(bounds); + if (converged) { + result = getAverageOfBounds(bounds); + } else { + printBoundsInformation(bounds); + + STORM_LOG_TRACE("Performing bisimulation step."); + bisimulation.compute(10); + } + } + + ++iterations; + } + + auto end = std::chrono::high_resolution_clock::now(); + STORM_LOG_TRACE("Completed abstraction-refinement in " << std::chrono::duration_cast(end - start).count() << "ms."); + + return result; + } + + template + void PartialBisimulationMdpModelChecker::printBoundsInformation(std::pair, std::unique_ptr> const& bounds) { + STORM_LOG_THROW(bounds.first->isSymbolicQuantitativeCheckResult(), storm::exceptions::InvalidTypeException, "Expected symbolic quantitative check result."); + storm::modelchecker::SymbolicQuantitativeCheckResult const& lowerBounds = bounds.first->asSymbolicQuantitativeCheckResult(); + STORM_LOG_THROW(bounds.second->isSymbolicQuantitativeCheckResult(), storm::exceptions::InvalidTypeException, "Expected symbolic quantitative check result."); + storm::modelchecker::SymbolicQuantitativeCheckResult const& upperBounds = bounds.second->asSymbolicQuantitativeCheckResult(); + + // If there is exactly one value that we stored, we print the current bounds as an interval. + if (lowerBounds.getStates().getNonZeroCount() == 1 && upperBounds.getStates().getNonZeroCount() == 1) { + STORM_LOG_TRACE("Obtained bounds [" << lowerBounds.getValueVector().getMax() << ", " << upperBounds.getValueVector().getMax() << "] on actual result."); + } else { + STORM_LOG_TRACE("Largest difference over initial states is " << getLargestDifference(bounds) << "."); + } + } + + template + typename PartialBisimulationMdpModelChecker::ValueType PartialBisimulationMdpModelChecker::getLargestDifference(std::pair, std::unique_ptr> const& bounds) { + STORM_LOG_THROW(bounds.first->isSymbolicQuantitativeCheckResult(), storm::exceptions::InvalidTypeException, "Expected symbolic quantitative check result."); + storm::modelchecker::SymbolicQuantitativeCheckResult const& lowerBounds = bounds.first->asSymbolicQuantitativeCheckResult(); + STORM_LOG_THROW(bounds.second->isSymbolicQuantitativeCheckResult(), storm::exceptions::InvalidTypeException, "Expected symbolic quantitative check result."); + storm::modelchecker::SymbolicQuantitativeCheckResult const& upperBounds = bounds.second->asSymbolicQuantitativeCheckResult(); + + return (upperBounds.getValueVector() - lowerBounds.getValueVector()).getMax(); + } + + template + bool PartialBisimulationMdpModelChecker::checkBoundsSufficientlyClose(std::pair, std::unique_ptr> const& bounds) { + STORM_LOG_THROW(bounds.first->isSymbolicQuantitativeCheckResult(), storm::exceptions::InvalidTypeException, "Expected symbolic quantitative check result."); + storm::modelchecker::SymbolicQuantitativeCheckResult const& lowerBounds = bounds.first->asSymbolicQuantitativeCheckResult(); + STORM_LOG_THROW(bounds.second->isSymbolicQuantitativeCheckResult(), storm::exceptions::InvalidTypeException, "Expected symbolic quantitative check result."); + storm::modelchecker::SymbolicQuantitativeCheckResult const& upperBounds = bounds.second->asSymbolicQuantitativeCheckResult(); + + return lowerBounds.getValueVector().equalModuloPrecision(upperBounds.getValueVector(), storm::settings::getModule().getPrecision(), false); + } + + template + std::unique_ptr PartialBisimulationMdpModelChecker::getAverageOfBounds(std::pair, std::unique_ptr> const& bounds) { + STORM_LOG_THROW(bounds.first->isSymbolicQuantitativeCheckResult(), storm::exceptions::InvalidTypeException, "Expected symbolic quantitative check result."); + storm::modelchecker::SymbolicQuantitativeCheckResult const& lowerBounds = bounds.first->asSymbolicQuantitativeCheckResult(); + STORM_LOG_THROW(bounds.second->isSymbolicQuantitativeCheckResult(), storm::exceptions::InvalidTypeException, "Expected symbolic quantitative check result."); + storm::modelchecker::SymbolicQuantitativeCheckResult const& upperBounds = bounds.second->asSymbolicQuantitativeCheckResult(); + + return std::make_unique>(lowerBounds.getReachableStates(), lowerBounds.getStates(), (lowerBounds.getValueVector() + upperBounds.getValueVector()) / lowerBounds.getValueVector().getDdManager().getConstant(storm::utility::convertNumber(std::string("2.0")))); + } + + static int i = 0; + + template + std::pair, std::unique_ptr> PartialBisimulationMdpModelChecker::computeBoundsPartialQuotient(storm::models::symbolic::Mdp const& quotient, bool rewards, CheckTask const& checkTask) { + + std::pair, std::unique_ptr> result; + + CheckTask newCheckTask(checkTask); + SymbolicMdpPrctlModelChecker> checker(quotient); + + newCheckTask.setOptimizationDirection(storm::OptimizationDirection::Minimize); + if (rewards) { + result.first = checker.computeRewards(storm::logic::RewardMeasureType::Expectation,newCheckTask); + } else { + result.first = checker.computeProbabilities(newCheckTask); + } + result.first->asSymbolicQuantitativeCheckResult().getValueVector().exportToDot("lower_values" + std::to_string(i) + ".dot"); + result.first->filter(storm::modelchecker::SymbolicQualitativeCheckResult(quotient.getReachableStates(), quotient.getInitialStates())); + + newCheckTask.setOptimizationDirection(storm::OptimizationDirection::Maximize); + if (rewards) { + result.first = checker.computeRewards(storm::logic::RewardMeasureType::Expectation, newCheckTask); + } else { + result.second = checker.computeProbabilities(newCheckTask); + } + result.first->asSymbolicQuantitativeCheckResult().getValueVector().exportToDot("upper_values" + std::to_string(i++) + ".dot"); + result.second->filter(storm::modelchecker::SymbolicQualitativeCheckResult(quotient.getReachableStates(), quotient.getInitialStates())); + + return result; + } + + template + std::pair, std::unique_ptr> PartialBisimulationMdpModelChecker::computeBoundsPartialQuotient(storm::models::symbolic::StochasticTwoPlayerGame const& quotient, bool rewards, CheckTask const& checkTask) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Currently not implemented."); + } + + template + std::pair, std::unique_ptr> PartialBisimulationMdpModelChecker::computeBoundsPartialQuotient(storm::models::Model const& quotient, bool rewards, CheckTask const& checkTask) { + + // Sanity checks. + STORM_LOG_THROW(quotient.isSymbolicModel(), storm::exceptions::NotSupportedException, "Expecting symbolic quotient."); + storm::models::ModelType modelType = quotient.getType(); + STORM_LOG_THROW(modelType == storm::models::ModelType::Mdp || modelType == storm::models::ModelType::S2pg, storm::exceptions::NotSupportedException, "Only MDPs and stochastic games are supported as partial quotients."); + + if (modelType == storm::models::ModelType::Mdp) { + return computeBoundsPartialQuotient(*quotient.template as>(), rewards, checkTask); + } else { + return computeBoundsPartialQuotient(*quotient.template as>(), rewards, checkTask); + } + } + + template + std::unique_ptr PartialBisimulationMdpModelChecker::computeResultFullQuotient(storm::models::symbolic::Dtmc const& quotient, bool rewards, CheckTask const& checkTask) { + SymbolicDtmcPrctlModelChecker> checker(quotient); + std::unique_ptr result; + if (rewards) { + result = checker.computeRewards(storm::logic::RewardMeasureType::Expectation, checkTask); + } else { + result = checker.computeProbabilities(checkTask); + } + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(quotient.getReachableStates(), quotient.getInitialStates())); + return result; + } + + template + std::unique_ptr PartialBisimulationMdpModelChecker::computeResultFullQuotient(storm::models::symbolic::Mdp const& quotient, bool rewards, CheckTask const& checkTask) { + SymbolicMdpPrctlModelChecker> checker(quotient); + std::unique_ptr result; + if (rewards) { + result = checker.computeRewards(storm::logic::RewardMeasureType::Expectation, checkTask); + } else { + result = checker.computeProbabilities(checkTask); + } + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(quotient.getReachableStates(), quotient.getInitialStates())); + return result; + } + + template + std::unique_ptr PartialBisimulationMdpModelChecker::computeResultFullQuotient(storm::models::Model const& quotient, bool rewards, CheckTask const& checkTask) { + + // Sanity checks. + STORM_LOG_THROW(quotient.isSymbolicModel(), storm::exceptions::NotSupportedException, "Expecting symbolic quotient."); + storm::models::ModelType modelType = quotient.getType(); + STORM_LOG_THROW(modelType == storm::models::ModelType::Dtmc || modelType == storm::models::ModelType::Mdp, storm::exceptions::NotSupportedException, "Only DTMCs and MDPs supported as full quotients."); + + if (modelType == storm::models::ModelType::Dtmc) { + return computeResultFullQuotient(*quotient.template as>(), rewards, checkTask); + } else { + return computeResultFullQuotient(*quotient.template as>(), rewards, checkTask); + } } template class PartialBisimulationMdpModelChecker>; diff --git a/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.h b/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.h index de8bc9e22..dacdb4be5 100644 --- a/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.h +++ b/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.h @@ -1,26 +1,71 @@ #pragma once -#include "storm/modelchecker/propositional/SymbolicPropositionalModelChecker.h" +#include "storm/modelchecker/AbstractModelChecker.h" #include "storm/storage/dd/DdType.h" namespace storm { + namespace dd { + template + class Bdd; + } + + namespace models { + template + class Model; + + namespace symbolic { + template + class Dtmc; + + template + class Mdp; + + template + class StochasticTwoPlayerGame; + } + } + namespace modelchecker { template - class PartialBisimulationMdpModelChecker : public SymbolicPropositionalModelChecker { + class PartialBisimulationMdpModelChecker : public AbstractModelChecker { public: typedef typename ModelType::ValueType ValueType; - + static const storm::dd::DdType DdType = ModelType::DdType; + /*! * Constructs a model checker for the given model. */ explicit PartialBisimulationMdpModelChecker(ModelType const& model); -// /// Overridden methods from super class. + /// Overridden methods from super class. virtual bool canHandle(CheckTask const& checkTask) const override; virtual std::unique_ptr computeUntilProbabilities(CheckTask const& checkTask) override; virtual std::unique_ptr computeReachabilityProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; + + private: + std::unique_ptr computeValuesAbstractionRefinement(bool rewards, CheckTask const& checkTask); + + // Methods to check for convergence and postprocessing the result. + bool checkBoundsSufficientlyClose(std::pair, std::unique_ptr> const& bounds); + std::unique_ptr getAverageOfBounds(std::pair, std::unique_ptr> const& bounds); + void printBoundsInformation(std::pair, std::unique_ptr> const& bounds); + ValueType getLargestDifference(std::pair, std::unique_ptr> const& bounds); + + // Methods to compute bounds on the partial quotient. + std::pair, std::unique_ptr> computeBoundsPartialQuotient(storm::models::symbolic::Mdp const& quotient, bool rewards, CheckTask const& checkTask); + std::pair, std::unique_ptr> computeBoundsPartialQuotient(storm::models::symbolic::StochasticTwoPlayerGame const& quotient, bool rewards, CheckTask const& checkTask); + std::pair, std::unique_ptr> computeBoundsPartialQuotient(storm::models::Model const& quotient, bool rewards, CheckTask const& checkTask); + + // Methods to solve the query on the full quotient. + std::unique_ptr computeResultFullQuotient(storm::models::symbolic::Dtmc const& quotient, bool rewards, CheckTask const& checkTask); + std::unique_ptr computeResultFullQuotient(storm::models::symbolic::Mdp const& quotient, bool rewards, CheckTask const& checkTask); + std::unique_ptr computeResultFullQuotient(storm::models::Model const& quotient, bool rewards, CheckTask const& checkTask); + + // The non-abstracted model. + ModelType const& model; }; } } diff --git a/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp index 518f50acc..59cb85256 100644 --- a/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp @@ -49,7 +49,7 @@ namespace storm { storm::dd::Bdd maybeStates = !statesWithProbability01.first && !statesWithProbability01.second && model.getReachableStates(); - STORM_LOG_INFO("Preprocessing: " << statesWithProbability01.first.getNonZeroCount() << " states with probability 1, " << statesWithProbability01.second.getNonZeroCount() << " with probability 0 (" << maybeStates.getNonZeroCount() << " states remaining)."); + STORM_LOG_INFO("Preprocessing: " << statesWithProbability01.first.getNonZeroCount() << " states with probability 0, " << statesWithProbability01.second.getNonZeroCount() << " with probability 1 (" << maybeStates.getNonZeroCount() << " states remaining)."); // Check whether we need to compute exact probabilities for some states. if (qualitative) { diff --git a/src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.cpp b/src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.cpp index b73190bab..52121ff70 100644 --- a/src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.cpp +++ b/src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.cpp @@ -57,6 +57,16 @@ namespace storm { return values; } + template + storm::dd::Bdd const& SymbolicQuantitativeCheckResult::getStates() const { + return states; + } + + template + storm::dd::Bdd const& SymbolicQuantitativeCheckResult::getReachableStates() const { + return reachableStates; + } + template void print(std::ostream& out, ValueType const& value) { if (value == storm::utility::infinity()) { diff --git a/src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.h b/src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.h index 34e0e0bc6..cf7e037a8 100644 --- a/src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.h +++ b/src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.h @@ -31,7 +31,9 @@ namespace storm { virtual bool isSymbolicQuantitativeCheckResult() const override; storm::dd::Add const& getValueVector() const; - + storm::dd::Bdd const& getStates() const; + storm::dd::Bdd const& getReachableStates() const; + virtual std::ostream& writeToStream(std::ostream& out) const override; virtual void filter(QualitativeCheckResult const& filter) override; diff --git a/src/storm/models/ModelBase.h b/src/storm/models/ModelBase.h index 614ebdcd5..9eace3911 100644 --- a/src/storm/models/ModelBase.h +++ b/src/storm/models/ModelBase.h @@ -130,6 +130,16 @@ namespace storm { */ virtual void reduceToStateBasedRewards() = 0; + /*! + * Retrieves whether the model has a reward model with the given name. + * + * @return True iff the model has a reward model with the given name. + */ + virtual bool hasRewardModel(std::string const& rewardModelName) const = 0; + + virtual bool hasUniqueRewardModel() const = 0; + virtual std::string const& getUniqueRewardModelName() const = 0; + private: // The type of the model. ModelType modelType; diff --git a/src/storm/models/sparse/Model.cpp b/src/storm/models/sparse/Model.cpp index 288b46a1a..34891500e 100644 --- a/src/storm/models/sparse/Model.cpp +++ b/src/storm/models/sparse/Model.cpp @@ -176,6 +176,12 @@ namespace storm { return this->getNumberOfRewardModels() == 1; } + template + std::string const& Model::getUniqueRewardModelName() const { + STORM_LOG_THROW(this->getNumberOfRewardModels() == 1, storm::exceptions::IllegalFunctionCallException, "The reward model is not unique."); + return this->rewardModels.begin()->first; + } + template bool Model::hasRewardModel() const { return !this->rewardModels.empty(); diff --git a/src/storm/models/sparse/Model.h b/src/storm/models/sparse/Model.h index 5e52a9e12..34a2863c7 100644 --- a/src/storm/models/sparse/Model.h +++ b/src/storm/models/sparse/Model.h @@ -134,7 +134,7 @@ namespace storm { * * @return True iff the model has a reward model with the given name. */ - bool hasRewardModel(std::string const& rewardModelName) const; + virtual bool hasRewardModel(std::string const& rewardModelName) const override; /*! * Retrieves the reward model with the given name, if one exists. Otherwise, an exception is thrown. @@ -162,7 +162,14 @@ namespace storm { * * @return True iff the model has a unique reward model. */ - bool hasUniqueRewardModel() const; + virtual bool hasUniqueRewardModel() const override; + + /*! + * Retrieves the name of the unique reward model, if there exists exactly one. Otherwise, an exception is thrown. + * + * @return The name of the unique reward model. + */ + virtual std::string const& getUniqueRewardModelName() const override; /*! * Retrieves whether the model has at least one reward model. diff --git a/src/storm/models/symbolic/Model.h b/src/storm/models/symbolic/Model.h index 1bebd7fe5..fd0839a2b 100644 --- a/src/storm/models/symbolic/Model.h +++ b/src/storm/models/symbolic/Model.h @@ -261,7 +261,7 @@ namespace storm { * * @return True iff the model has a reward model with the given name. */ - bool hasRewardModel(std::string const& rewardModelName) const; + virtual bool hasRewardModel(std::string const& rewardModelName) const override; /*! * Retrieves the reward model with the given name, if one exists. Otherwise, an exception is thrown. @@ -282,7 +282,7 @@ namespace storm { * * @return The name of the unique reward model. */ - std::string const& getUniqueRewardModelName() const; + virtual std::string const& getUniqueRewardModelName() const override; /*! * Retrieves the unique reward model, if there exists exactly one. Otherwise, an exception is thrown. @@ -296,7 +296,7 @@ namespace storm { * * @return True iff the model has a unique reward model. */ - bool hasUniqueRewardModel() const; + virtual bool hasUniqueRewardModel() const override; /*! * Retrieves whether the model has at least one reward model. diff --git a/src/storm/storage/dd/BisimulationDecomposition.cpp b/src/storm/storage/dd/BisimulationDecomposition.cpp index dbe2c5f26..2ee9088e0 100644 --- a/src/storm/storage/dd/BisimulationDecomposition.cpp +++ b/src/storm/storage/dd/BisimulationDecomposition.cpp @@ -33,32 +33,29 @@ namespace storm { template BisimulationDecomposition::BisimulationDecomposition(storm::models::symbolic::Model const& model, storm::storage::BisimulationType const& bisimulationType) : model(model), preservationInformation(model, bisimulationType), refiner(createRefiner(model, Partition::create(model, bisimulationType, preservationInformation))) { - auto const& generalSettings = storm::settings::getModule(); - showProgress = generalSettings.isVerboseSet(); - showProgressDelay = generalSettings.getShowProgressDelay(); - this->refineWrtRewardModels(); - - STORM_LOG_TRACE("Initial partition has " << refiner->getStatePartition().getNumberOfBlocks() << " blocks."); -#ifndef NDEBUG - STORM_LOG_TRACE("Initial partition has " << refiner->getStatePartition().getNodeCount() << " nodes."); -#endif + this->initialize(); } - + + template + BisimulationDecomposition::BisimulationDecomposition(storm::models::symbolic::Model const& model, storm::storage::BisimulationType const& bisimulationType, bisimulation::PreservationInformation const& preservationInformation) : model(model), preservationInformation(preservationInformation), refiner(createRefiner(model, Partition::create(model, bisimulationType, preservationInformation))) { + this->initialize(); + } + template BisimulationDecomposition::BisimulationDecomposition(storm::models::symbolic::Model const& model, std::vector> const& formulas, storm::storage::BisimulationType const& bisimulationType) : model(model), preservationInformation(model, formulas, bisimulationType), refiner(createRefiner(model, Partition::create(model, bisimulationType, preservationInformation))) { - auto const& generalSettings = storm::settings::getModule(); - showProgress = generalSettings.isVerboseSet(); - showProgressDelay = generalSettings.getShowProgressDelay(); - this->refineWrtRewardModels(); - - STORM_LOG_TRACE("Initial partition has " << refiner->getStatePartition().getNumberOfBlocks() << " blocks."); -#ifndef NDEBUG - STORM_LOG_TRACE("Initial partition has " << refiner->getStatePartition().getNodeCount() << " nodes."); -#endif + this->initialize(); } template BisimulationDecomposition::BisimulationDecomposition(storm::models::symbolic::Model const& model, Partition const& initialPartition, bisimulation::PreservationInformation const& preservationInformation) : model(model), preservationInformation(preservationInformation), refiner(createRefiner(model, initialPartition)) { + this->initialize(); + } + + template + BisimulationDecomposition::~BisimulationDecomposition() = default; + + template + void BisimulationDecomposition::initialize() { auto const& generalSettings = storm::settings::getModule(); showProgress = generalSettings.isVerboseSet(); showProgressDelay = generalSettings.getShowProgressDelay(); @@ -70,9 +67,6 @@ namespace storm { #endif } - template - BisimulationDecomposition::~BisimulationDecomposition() = default; - template void BisimulationDecomposition::compute(bisimulation::SignatureMode const& mode) { STORM_LOG_ASSERT(refiner, "No suitable refiner."); @@ -132,6 +126,11 @@ namespace storm { return !refined; } + template + bool BisimulationDecomposition::getReachedFixedPoint() const { + return this->refiner->getStatus() == Status::FixedPoint; + } + template std::shared_ptr> BisimulationDecomposition::getQuotient() const { std::shared_ptr> quotient; @@ -148,7 +147,6 @@ namespace storm { } quotient = partialQuotientExtractor->extract(refiner->getStatePartition(), preservationInformation); - STORM_LOG_TRACE("Quotient extraction done."); } STORM_LOG_TRACE("Quotient extraction done."); diff --git a/src/storm/storage/dd/BisimulationDecomposition.h b/src/storm/storage/dd/BisimulationDecomposition.h index ef9018f9a..21ff7de2a 100644 --- a/src/storm/storage/dd/BisimulationDecomposition.h +++ b/src/storm/storage/dd/BisimulationDecomposition.h @@ -37,6 +37,7 @@ namespace storm { class BisimulationDecomposition { public: BisimulationDecomposition(storm::models::symbolic::Model const& model, storm::storage::BisimulationType const& bisimulationType); + BisimulationDecomposition(storm::models::symbolic::Model const& model, storm::storage::BisimulationType const& bisimulationType, bisimulation::PreservationInformation const& preservationInformation); BisimulationDecomposition(storm::models::symbolic::Model const& model, std::vector> const& formulas, storm::storage::BisimulationType const& bisimulationType); BisimulationDecomposition(storm::models::symbolic::Model const& model, bisimulation::Partition const& initialPartition, bisimulation::PreservationInformation const& preservationInformation); @@ -54,12 +55,19 @@ namespace storm { */ bool compute(uint64_t steps, bisimulation::SignatureMode const& mode = bisimulation::SignatureMode::Eager); + /*! + * Retrieves whether a fixed point has been reached. Depending on this, extracting a quotient will either + * give a full quotient or a partial one. + */ + bool getReachedFixedPoint() const; + /*! * Retrieves the quotient model after the bisimulation decomposition was computed. */ std::shared_ptr> getQuotient() const; private: + void initialize(); void refineWrtRewardModels(); // The model for which to compute the bisimulation decomposition.