From 6cd3cdcd6ba2417300b705b501f7f148f2d46d60 Mon Sep 17 00:00:00 2001 From: sjunges Date: Mon, 25 Jan 2016 13:21:40 +0100 Subject: [PATCH 1/9] fixed missing template instantations Former-commit-id: d26a2580e4f0c89a39f2223440554bbcecc93c1a --- src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index 4c9e1643e..fac6e5864 100644 --- a/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -503,7 +503,7 @@ namespace storm { } template class SparseMarkovAutomatonCslHelper; - //template std::vector SparseMarkovAutomatonCslHelper::computeReachabilityRewards(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + template std::vector SparseMarkovAutomatonCslHelper::computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); } } From 9b9468fbfda4b9a2c02284c1692f57168402c885 Mon Sep 17 00:00:00 2001 From: PBerger Date: Mon, 25 Jan 2016 15:18:34 +0100 Subject: [PATCH 2/9] Fixed issues in graph.cpp when CARL is not available. Former-commit-id: 513070f1940c78208abf920cfd228c1f2525c00b --- src/utility/graph.cpp | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) diff --git a/src/utility/graph.cpp b/src/utility/graph.cpp index 193b0ff28..bac64948f 100644 --- a/src/utility/graph.cpp +++ b/src/utility/graph.cpp @@ -986,9 +986,10 @@ namespace storm { template storm::storage::BitVector performProb0A(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - template storm::storage::BitVector performProb0A(storm::models::sparse::NondeterministicModel> const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; - template storm::storage::BitVector performProb0A(storm::models::sparse::NondeterministicModel> const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; - + template storm::storage::BitVector performProb0A(storm::models::sparse::NondeterministicModel> const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); +#ifdef STORM_HAVE_CARL + template storm::storage::BitVector performProb0A(storm::models::sparse::NondeterministicModel> const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); +#endif template storm::storage::BitVector performProb1E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); @@ -1004,19 +1005,24 @@ namespace storm { template storm::storage::BitVector performProb0E(storm::models::sparse::NondeterministicModel> const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); +#ifdef STORM_HAVE_CARL template storm::storage::BitVector performProb0E(storm::models::sparse::NondeterministicModel> const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); +#endif template storm::storage::BitVector performProb0E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; template storm::storage::BitVector performProb1A(storm::models::sparse::NondeterministicModel> const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); +#ifdef STORM_HAVE_CARL template storm::storage::BitVector performProb1A(storm::models::sparse::NondeterministicModel> const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); +#endif template storm::storage::BitVector performProb1A( storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); template std::pair performProb01Min(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; template std::pair performProb01Min(storm::models::sparse::NondeterministicModel> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - template std::pair performProb01Min(storm::models::sparse::NondeterministicModel> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - +#ifdef STORM_HAVE_CARL + template std::pair performProb01Min(storm::models::sparse::NondeterministicModel> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); +#endif template std::vector getTopologicalSort(storm::storage::SparseMatrix const& matrix) ; From 8eec3f230608f6e0e58c57da82c303e1be16e706 Mon Sep 17 00:00:00 2001 From: PBerger Date: Mon, 25 Jan 2016 15:31:07 +0100 Subject: [PATCH 3/9] Fixed issue in ExplicitPrismModelBuilder.cpp when CARL is not available. Former-commit-id: 08c6ec6dbeb033e1cf410cc036e5ca30ccc0f2fc --- src/builder/ExplicitPrismModelBuilder.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/builder/ExplicitPrismModelBuilder.cpp b/src/builder/ExplicitPrismModelBuilder.cpp index 96b6298d0..a3d80d067 100644 --- a/src/builder/ExplicitPrismModelBuilder.cpp +++ b/src/builder/ExplicitPrismModelBuilder.cpp @@ -244,7 +244,7 @@ namespace storm { // not only appear in the probabilities, we re if (!std::is_same::value && preparedProgram->hasUndefinedConstants()) { #else - if (preparedProgram.hasUndefinedConstants()) { + if (preparedProgram->hasUndefinedConstants()) { #endif std::vector> undefinedConstants = preparedProgram->getUndefinedConstants(); std::stringstream stream; From 5e9c42f2afa312bca8a359f36187ed783b651cbe Mon Sep 17 00:00:00 2001 From: sjunges Date: Mon, 25 Jan 2016 15:32:19 +0100 Subject: [PATCH 4/9] intermediate commit Former-commit-id: 6acb50ec6293fca2038a09a258796da635bf0f07 --- src/models/sparse/Model.cpp | 3 +++ src/models/sparse/Model.h | 1 + src/storage/SparseMatrix.h | 8 ++++++++ 3 files changed, 12 insertions(+) diff --git a/src/models/sparse/Model.cpp b/src/models/sparse/Model.cpp index 791062b54..a1e71c0b7 100644 --- a/src/models/sparse/Model.cpp +++ b/src/models/sparse/Model.cpp @@ -320,6 +320,9 @@ namespace storm { return this->rewardModels; } + std::set getProbabilityParameters(Model const& model) { + return storm::storage::getVariables(model.getTransitionMatrix()); + } template class Model; template class Model; diff --git a/src/models/sparse/Model.h b/src/models/sparse/Model.h index 3d7776800..7d36ebca3 100644 --- a/src/models/sparse/Model.h +++ b/src/models/sparse/Model.h @@ -345,6 +345,7 @@ namespace storm { boost::optional> choiceLabeling; }; + std::set getProbabilityParameters(Model const& model); } // namespace sparse } // namespace models } // namespace storm diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index 99eea1c06..21d675cab 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -969,6 +969,14 @@ namespace storm { std::vector rowGroupIndices; }; + + std::set getVariables(SparseMatrix const& matrix) { + std::set result; + for(auto const& entry : matrix) { + entry.probability.gatherVariables(result); + } + return result; + } } // namespace storage } // namespace storm From f0f3e8cbb3ee97af02ac12eea6aac4362ef86afb Mon Sep 17 00:00:00 2001 From: PBerger Date: Mon, 25 Jan 2016 16:01:55 +0100 Subject: [PATCH 5/9] Fixed test/functional/permissiveschedulers/SmtPermissiveSchedulerTest.cpp when MathSAT support is unavailable. Former-commit-id: c4b91a2ac5aa70a08c1327cdd23fd010011485db --- .../permissiveschedulers/SmtPermissiveSchedulerTest.cpp | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/test/functional/permissiveschedulers/SmtPermissiveSchedulerTest.cpp b/test/functional/permissiveschedulers/SmtPermissiveSchedulerTest.cpp index 04f706221..4d87796b8 100644 --- a/test/functional/permissiveschedulers/SmtPermissiveSchedulerTest.cpp +++ b/test/functional/permissiveschedulers/SmtPermissiveSchedulerTest.cpp @@ -10,6 +10,9 @@ #include "src/models/sparse/StandardRewardModel.h" #include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h" + +#ifdef STORM_HAVE_MSAT + TEST(SmtPermissiveSchedulerTest, DieSelection) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die_c1.nm"); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); @@ -58,3 +61,5 @@ TEST(SmtPermissiveSchedulerTest, DieSelection) { // } + +#endif // STORM_HAVE_MSAT From 3cda2d153aec8249d71d00bb01c7d1181071db20 Mon Sep 17 00:00:00 2001 From: PBerger Date: Mon, 25 Jan 2016 16:42:44 +0100 Subject: [PATCH 6/9] Fixed MathsatExpressionAdapter.h, where the adaption of std::hash was already wrapped in "namespace std" but the definition used std:: again. Former-commit-id: 1d8aaaeca9b5a8ce8c2e5d07ebf7709d2ba67a4c --- src/adapters/MathsatExpressionAdapter.h | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/adapters/MathsatExpressionAdapter.h b/src/adapters/MathsatExpressionAdapter.h index 854b20542..9fec0cf15 100644 --- a/src/adapters/MathsatExpressionAdapter.h +++ b/src/adapters/MathsatExpressionAdapter.h @@ -22,9 +22,9 @@ namespace std { // Define hashing operator for MathSAT's declarations. template <> - struct std::hash { - std::size_t operator()(msat_decl const& declaration) const { - return std::hash()(declaration.repr); + struct hash { + size_t operator()(msat_decl const& declaration) const { + return hash()(declaration.repr); } }; } From 93be84a4a82aeb23a4dd7fcec02fc6b7182ec22f Mon Sep 17 00:00:00 2001 From: sjunges Date: Mon, 25 Jan 2016 16:51:14 +0100 Subject: [PATCH 7/9] fix in get parameters from model Former-commit-id: c4c11b2b294d7fbc07548ba5b5a10a74051b829b --- src/models/sparse/Model.cpp | 2 +- src/storage/SparseMatrix.cpp | 13 +++++++++++++ src/storage/SparseMatrix.h | 14 +++++--------- 3 files changed, 19 insertions(+), 10 deletions(-) diff --git a/src/models/sparse/Model.cpp b/src/models/sparse/Model.cpp index a1e71c0b7..e30965998 100644 --- a/src/models/sparse/Model.cpp +++ b/src/models/sparse/Model.cpp @@ -320,7 +320,7 @@ namespace storm { return this->rewardModels; } - std::set getProbabilityParameters(Model const& model) { + std::set getProbabilityParameters(Model const& model) { return storm::storage::getVariables(model.getTransitionMatrix()); } diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp index 1bc2f9af0..253609210 100644 --- a/src/storage/SparseMatrix.cpp +++ b/src/storage/SparseMatrix.cpp @@ -1208,6 +1208,19 @@ namespace storm { return result; } + +#ifdef STORM_HAVE_CARL + std::set getVariables(SparseMatrix const& matrix) + { + std::set result; + for(auto const& entry : matrix) { + entry.getValue().gatherVariables(result); + } + return result; + } + +#endif + // Explicitly instantiate the entry, builder and the matrix. // double template class MatrixEntry::index_type, double>; diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index 21d675cab..f9d9916c4 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -8,7 +8,7 @@ #include #include "src/utility/OsDetection.h" - +#include "src/adapters/CarlAdapter.h" #include // Forward declaration for adapter classes. @@ -970,14 +970,10 @@ namespace storm { }; - std::set getVariables(SparseMatrix const& matrix) { - std::set result; - for(auto const& entry : matrix) { - entry.probability.gatherVariables(result); - } - return result; - } - +#ifdef STORM_HAVE_CARL + std::set getVariables(SparseMatrix const& matrix); +#endif + } // namespace storage } // namespace storm From ad01dfa6117aab6420110d9b07a9bcd22caa3316 Mon Sep 17 00:00:00 2001 From: sjunges Date: Tue, 26 Jan 2016 17:25:00 +0100 Subject: [PATCH 8/9] refactored bisimulation a bit (mainly the entry point as well as hidden some options) Former-commit-id: 5405a149304e17f8db74f310d2bd9aecae249212 --- .../BisimulationDecomposition.cpp | 14 ++-- .../bisimulation/BisimulationDecomposition.h | 84 ++++++++++++++++--- ...ministicModelBisimulationDecomposition.cpp | 18 ++-- ...ministicModelBisimulationDecomposition.cpp | 12 +-- src/utility/storm.h | 46 +++++----- ...sticModelBisimulationDecompositionTest.cpp | 6 +- 6 files changed, 121 insertions(+), 59 deletions(-) diff --git a/src/storage/bisimulation/BisimulationDecomposition.cpp b/src/storage/bisimulation/BisimulationDecomposition.cpp index 08845a24b..b6158ed06 100644 --- a/src/storage/bisimulation/BisimulationDecomposition.cpp +++ b/src/storage/bisimulation/BisimulationDecomposition.cpp @@ -44,7 +44,7 @@ namespace storm { } template - BisimulationDecomposition::Options::Options() : measureDrivenInitialPartition(false), phiStates(), psiStates(), respectedAtomicPropositions(), keepRewards(false), type(BisimulationType::Strong), bounded(false), buildQuotient(true) { + BisimulationDecomposition::Options::Options() : measureDrivenInitialPartition(false), phiStates(), psiStates(), respectedAtomicPropositions(), buildQuotient(true), keepRewards(false), type(BisimulationType::Strong), bounded(false) { // Intentionally left empty. } @@ -163,9 +163,9 @@ namespace storm { template BisimulationDecomposition::BisimulationDecomposition(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, Options const& options) : model(model), backwardTransitions(backwardTransitions), options(options), partition(), comparator(), quotient(nullptr) { - STORM_LOG_THROW(!options.keepRewards || !model.hasRewardModel() || model.hasUniqueRewardModel(), storm::exceptions::IllegalFunctionCallException, "Bisimulation currently only supports models with at most one reward model."); - STORM_LOG_THROW(!options.keepRewards || !model.hasRewardModel() || model.getUniqueRewardModel()->second.hasOnlyStateRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently supported for models with state rewards only. Consider converting the transition rewards to state rewards (via suitable function calls)."); - STORM_LOG_THROW(options.type != BisimulationType::Weak || !options.bounded, storm::exceptions::IllegalFunctionCallException, "Weak bisimulation cannot preserve bounded properties."); + STORM_LOG_THROW(!options.getKeepRewards() || !model.hasRewardModel() || model.hasUniqueRewardModel(), storm::exceptions::IllegalFunctionCallException, "Bisimulation currently only supports models with at most one reward model."); + STORM_LOG_THROW(!options.getKeepRewards() || !model.hasRewardModel() || model.getUniqueRewardModel()->second.hasOnlyStateRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently supported for models with state rewards only. Consider converting the transition rewards to state rewards (via suitable function calls)."); + STORM_LOG_THROW(options.getType() != BisimulationType::Weak || !options.getBounded(), storm::exceptions::IllegalFunctionCallException, "Weak bisimulation cannot preserve bounded properties."); // Fix the respected atomic propositions if they were not explicitly given. if (!this->options.respectedAtomicPropositions) { @@ -270,7 +270,7 @@ namespace storm { // If the model has state rewards, we need to consider them, because otherwise reward properties are not // preserved. - if (options.keepRewards && model.hasRewardModel()) { + if (options.getKeepRewards() && model.hasRewardModel()) { this->splitInitialPartitionBasedOnStateRewards(); } } @@ -284,11 +284,11 @@ namespace storm { representativePsiState = *options.psiStates.get().begin(); } - partition = storm::storage::bisimulation::Partition(model.getNumberOfStates(), statesWithProbability01.first, options.bounded || options.keepRewards ? options.psiStates.get() : statesWithProbability01.second, representativePsiState); + partition = storm::storage::bisimulation::Partition(model.getNumberOfStates(), statesWithProbability01.first, options.getBounded() || options.getKeepRewards() ? options.psiStates.get() : statesWithProbability01.second, representativePsiState); // If the model has state rewards, we need to consider them, because otherwise reward properties are not // preserved. - if (options.keepRewards && model.hasRewardModel()) { + if (options.getKeepRewards() && model.hasRewardModel()) { this->splitInitialPartitionBasedOnStateRewards(); } } diff --git a/src/storage/bisimulation/BisimulationDecomposition.h b/src/storage/bisimulation/BisimulationDecomposition.h index a7bd575b2..f7b2379de 100644 --- a/src/storage/bisimulation/BisimulationDecomposition.h +++ b/src/storage/bisimulation/BisimulationDecomposition.h @@ -3,6 +3,8 @@ #include +#include "src/settings/SettingsManager.h" +#include "src/settings/modules/BisimulationSettings.h" #include "src/storage/sparse/StateType.h" #include "src/storage/Decomposition.h" #include "src/storage/StateBlock.h" @@ -25,6 +27,23 @@ namespace storm { namespace storage { enum class BisimulationType { Strong, Weak }; + enum class BisimulationTypeChoice { Strong, Weak, FromSettings }; + + inline BisimulationType resolveBisimulationTypeChoice(BisimulationTypeChoice c) { + switch(c) { + case BisimulationTypeChoice::Strong: + return BisimulationType::Strong; + case BisimulationTypeChoice::Weak: + return BisimulationType::Weak; + case BisimulationTypeChoice::FromSettings: + if (storm::settings::bisimulationSettings().isWeakBisimulationSet()) { + return BisimulationType::Weak; + } else { + return BisimulationType::Strong; + } + + } + } /*! * This class is the superclass of all decompositions of a sparse model into its bisimulation quotient. @@ -37,6 +56,8 @@ namespace storm { // A class that offers the possibility to customize the bisimulation. struct Options { + + // Creates an object representing the default values for all options. Options(); @@ -68,33 +89,74 @@ namespace storm { */ void preserveFormula(ModelType const& model, storm::logic::Formula const& formula); + + /** + * Sets the bisimulation type. If the bisimulation type is set to weak, + * we also change the bounded flag (as bounded properties are not preserved under + * weak bisimulation). + */ + void setType(BisimulationType t) { + if(t == BisimulationType::Weak) { + bounded = false; + } + type = t; + } + + BisimulationType getType() const { + return this->type; + } + + bool getBounded() const { + return this->bounded; + } + + bool getKeepRewards() const { + return this->keepRewards; + } + + bool isOptimizationDirectionSet() const { + return static_cast(optimalityType); + } + + OptimizationDirection getOptimizationDirection() const { + assert(optimalityType); + return optimalityType.get(); + } // A flag that indicates whether a measure driven initial partition is to be used. If this flag is set // to true, the two optional pairs phiStatesAndLabel and psiStatesAndLabel must be set. Then, the // measure driven initial partition wrt. to the states phi and psi is taken. bool measureDrivenInitialPartition; boost::optional phiStates; boost::optional psiStates; - boost::optional optimalityType; - // An optional set of strings that indicate which of the atomic propositions of the model are to be - // respected and which may be ignored. If not given, all atomic propositions of the model are respected. + /// An optional set of strings that indicate which of the atomic propositions of the model are to be + /// respected and which may be ignored. If not given, all atomic propositions of the model are respected. boost::optional> respectedAtomicPropositions; - // A flag that indicates whether or not the state-rewards of the model are to be respected (and should - // be kept in the quotient model, if one is built). + /// A flag that governs whether the quotient model is actually built or only the decomposition is computed. + bool buildQuotient; + + private: + + boost::optional optimalityType; + + + + + /// A flag that indicates whether or not the state-rewards of the model are to be respected (and should + /// be kept in the quotient model, if one is built). bool keepRewards; - // A flag that indicates whether a strong or a weak bisimulation is to be computed. + /// A flag that indicates whether a strong or a weak bisimulation is to be computed. BisimulationType type; - // A flag that indicates whether step-bounded properties are to be preserved. This may only be set to tru - // when computing strong bisimulation equivalence. + /// A flag that indicates whether step-bounded properties are to be preserved. This may only be set to tru + /// when computing strong bisimulation equivalence. bool bounded; - // A flag that governs whether the quotient model is actually built or only the decomposition is computed. - bool buildQuotient; - private: + + /*! * Sets the options under the assumption that the given formula is the only one that is to be checked. * diff --git a/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp b/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp index f81519084..bc48fdffc 100644 --- a/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp +++ b/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp @@ -122,7 +122,7 @@ namespace storm { void DeterministicModelBisimulationDecomposition::initializeMeasureDrivenPartition() { BisimulationDecomposition::initializeMeasureDrivenPartition(); - if (this->options.type == BisimulationType::Weak && this->model.getType() == storm::models::ModelType::Dtmc) { + if (this->options.getType() == BisimulationType::Weak && this->model.getType() == storm::models::ModelType::Dtmc) { this->initializeWeakDtmcBisimulation(); } } @@ -131,7 +131,7 @@ namespace storm { void DeterministicModelBisimulationDecomposition::initializeLabelBasedPartition() { BisimulationDecomposition::initializeLabelBasedPartition(); - if (this->options.type == BisimulationType::Weak && this->model.getType() == storm::models::ModelType::Dtmc) { + if (this->options.getType() == BisimulationType::Weak && this->model.getType() == storm::models::ModelType::Dtmc) { this->initializeWeakDtmcBisimulation(); } } @@ -494,7 +494,7 @@ namespace storm { } // Finally, we split the block based on the precomputed probabilities and the chosen bisimulation type. - if (this->options.type == BisimulationType::Strong || this->model.getType() == storm::models::ModelType::Ctmc) { + if (this->options.getType() == BisimulationType::Strong || this->model.getType() == storm::models::ModelType::Ctmc) { refinePredecessorBlocksOfSplitterStrong(predecessorBlocks, splitterQueue); } else { // If the splitter is a predecessor of we can use the computed probabilities to update the silent @@ -528,7 +528,7 @@ namespace storm { // If the model had state rewards, we need to build the state rewards for the quotient as well. boost::optional> stateRewards; - if (this->options.keepRewards && this->model.hasRewardModel()) { + if (this->options.getKeepRewards() && this->model.hasRewardModel()) { stateRewards = std::vector(this->blocks.size()); } @@ -542,7 +542,7 @@ namespace storm { // However, for weak bisimulation, we need to make sure the representative state is a non-silent one (if // there is any such state). - if (this->options.type == BisimulationType::Weak) { + if (this->options.getType() == BisimulationType::Weak) { for (auto const& state : block) { if (!isSilent(state)) { representativeState = state; @@ -576,7 +576,7 @@ namespace storm { storm::storage::sparse::state_type targetBlock = this->partition.getBlock(entry.getColumn()).getId(); // If we are computing a weak bisimulation quotient, there is no need to add self-loops. - if ((this->options.type == BisimulationType::Weak) && targetBlock == blockIndex) { + if ((this->options.getType() == BisimulationType::Weak) && targetBlock == blockIndex) { continue; } @@ -590,7 +590,7 @@ namespace storm { // Now add them to the actual matrix. for (auto const& probabilityEntry : blockProbability) { - if (this->options.type == BisimulationType::Weak && this->model.getType() == storm::models::ModelType::Dtmc) { + if (this->options.getType() == BisimulationType::Weak && this->model.getType() == storm::models::ModelType::Dtmc) { builder.addNextValue(blockIndex, probabilityEntry.first, probabilityEntry.second / (storm::utility::one() - getSilentProbability(representativeState))); } else { builder.addNextValue(blockIndex, probabilityEntry.first, probabilityEntry.second); @@ -608,7 +608,7 @@ namespace storm { // If the model has state rewards, we simply copy the state reward of the representative state, because // all states in a block are guaranteed to have the same state reward. - if (this->options.keepRewards && this->model.hasRewardModel()) { + if (this->options.getKeepRewards() && this->model.hasRewardModel()) { typename std::unordered_map::const_iterator nameRewardModelPair = this->model.getUniqueRewardModel(); stateRewards.get()[blockIndex] = nameRewardModelPair->second.getStateRewardVector()[representativeState]; } @@ -622,7 +622,7 @@ namespace storm { // Construct the reward model mapping. std::unordered_map rewardModels; - if (this->options.keepRewards && this->model.hasRewardModel()) { + if (this->options.getKeepRewards() && this->model.hasRewardModel()) { typename std::unordered_map::const_iterator nameRewardModelPair = this->model.getUniqueRewardModel(); rewardModels.insert(std::make_pair(nameRewardModelPair->first, typename ModelType::RewardModelType(stateRewards))); } diff --git a/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp b/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp index 21dd36d89..2e7d54113 100644 --- a/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp +++ b/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp @@ -17,13 +17,13 @@ namespace storm { template NondeterministicModelBisimulationDecomposition::NondeterministicModelBisimulationDecomposition(ModelType const& model, typename BisimulationDecomposition::Options const& options) : BisimulationDecomposition(model, model.getTransitionMatrix().transpose(false), options), choiceToStateMapping(model.getNumberOfChoices()), quotientDistributions(model.getNumberOfChoices()), orderedQuotientDistributions(model.getNumberOfChoices()) { - STORM_LOG_THROW(options.type == BisimulationType::Strong, storm::exceptions::IllegalFunctionCallException, "Weak bisimulation is currently not supported for nondeterministic models."); + STORM_LOG_THROW(options.getType() == BisimulationType::Strong, storm::exceptions::IllegalFunctionCallException, "Weak bisimulation is currently not supported for nondeterministic models."); } template std::pair NondeterministicModelBisimulationDecomposition::getStatesWithProbability01() { - STORM_LOG_THROW(static_cast(this->options.optimalityType), storm::exceptions::IllegalFunctionCallException, "Can only compute states with probability 0/1 with an optimization direction (min/max)."); - if (this->options.optimalityType.get() == OptimizationDirection::Minimize) { + STORM_LOG_THROW(this->options.isOptimizationDirectionSet(), storm::exceptions::IllegalFunctionCallException, "Can only compute states with probability 0/1 with an optimization direction (min/max)."); + if (this->options.getOptimizationDirection() == OptimizationDirection::Minimize) { return storm::utility::graph::performProb01Min(this->model.getTransitionMatrix(), this->model.getTransitionMatrix().getRowGroupIndices(), this->model.getBackwardTransitions(), this->options.phiStates.get(), this->options.psiStates.get()); } else { return storm::utility::graph::performProb01Max(this->model.getTransitionMatrix(), this->model.getTransitionMatrix().getRowGroupIndices(), this->model.getBackwardTransitions(), this->options.phiStates.get(), this->options.psiStates.get()); @@ -109,7 +109,7 @@ namespace storm { // If the model had state rewards, we need to build the state rewards for the quotient as well. boost::optional> stateRewards; - if (this->options.keepRewards && this->model.hasRewardModel()) { + if (this->options.getKeepRewards() && this->model.hasRewardModel()) { stateRewards = std::vector(this->blocks.size()); } @@ -169,7 +169,7 @@ namespace storm { // If the model has state rewards, we simply copy the state reward of the representative state, because // all states in a block are guaranteed to have the same state reward. - if (this->options.keepRewards && this->model.hasRewardModel()) { + if (this->options.getKeepRewards() && this->model.hasRewardModel()) { typename std::unordered_map::const_iterator nameRewardModelPair = this->model.getUniqueRewardModel(); stateRewards.get()[blockIndex] = nameRewardModelPair->second.getStateRewardVector()[representativeState]; } @@ -183,7 +183,7 @@ namespace storm { // Construct the reward model mapping. std::unordered_map rewardModels; - if (this->options.keepRewards && this->model.hasRewardModel()) { + if (this->options.getKeepRewards() && this->model.hasRewardModel()) { typename std::unordered_map::const_iterator nameRewardModelPair = this->model.getUniqueRewardModel(); rewardModels.insert(std::make_pair(nameRewardModelPair->first, typename ModelType::RewardModelType(stateRewards))); } diff --git a/src/utility/storm.h b/src/utility/storm.h index 3f2173ecf..fb96b7420 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -137,16 +137,13 @@ namespace storm { } template - std::shared_ptr performDeterministicSparseBisimulationMinimization(std::shared_ptr model, std::vector> const& formulas) { + std::shared_ptr performDeterministicSparseBisimulationMinimization(std::shared_ptr model, std::vector> const& formulas, storm::storage::BisimulationType type) { std::cout << "Performing bisimulation minimization... "; typename storm::storage::DeterministicModelBisimulationDecomposition::Options options; if (!formulas.empty()) { options = typename storm::storage::DeterministicModelBisimulationDecomposition::Options(*model, formulas); } - if (storm::settings::bisimulationSettings().isWeakBisimulationSet()) { - options.type = storm::storage::BisimulationType::Weak; - options.bounded = false; - } + options.setType(type); storm::storage::DeterministicModelBisimulationDecomposition bisimulationDecomposition(*model, options); bisimulationDecomposition.computeBisimulationDecomposition(); @@ -156,16 +153,14 @@ namespace storm { } template - std::shared_ptr performNondeterministicSparseBisimulationMinimization(std::shared_ptr model, std::vector> const& formulas) { + std::shared_ptr performNondeterministicSparseBisimulationMinimization(std::shared_ptr model, std::vector> const& formulas, storm::storage::BisimulationType type) { std::cout << "Performing bisimulation minimization... "; typename storm::storage::DeterministicModelBisimulationDecomposition::Options options; if (!formulas.empty()) { options = typename storm::storage::NondeterministicModelBisimulationDecomposition::Options(*model, formulas); } - if (storm::settings::bisimulationSettings().isWeakBisimulationSet()) { - options.type = storm::storage::BisimulationType::Weak; - options.bounded = false; - } + options.setType(type); + storm::storage::NondeterministicModelBisimulationDecomposition bisimulationDecomposition(*model, options); bisimulationDecomposition.computeBisimulationDecomposition(); @@ -174,23 +169,30 @@ namespace storm { return model; } + template, ModelType>::value, bool>::type = 0> + std::shared_ptr performBisimulationMinimization(std::shared_ptr model, std::vector> const& formulas, storm::storage::BisimulationType type) { + STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Dtmc) || model->isOfType(storm::models::ModelType::Ctmc) || model->isOfType(storm::models::ModelType::Mdp), storm::exceptions::InvalidSettingsException, "Bisimulation minimization is currently only available for DTMCs, CTMCs and MDPs."); + model->reduceToStateBasedRewards(); + + if (model->isOfType(storm::models::ModelType::Dtmc)) { + return performDeterministicSparseBisimulationMinimization>(model->template as>(), formulas, type); + } else if (model->isOfType(storm::models::ModelType::Ctmc)) { + return performDeterministicSparseBisimulationMinimization>(model->template as>(), formulas, type); + } else { + return performNondeterministicSparseBisimulationMinimization>(model->template as>(), formulas, type); + } + } + template, ModelType>::value, bool>::type = 0> std::shared_ptr preprocessModel(std::shared_ptr model, std::vector> const& formulas) { if (storm::settings::generalSettings().isBisimulationSet()) { - - STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::InvalidSettingsException, "Bisimulation minimization is currently only available for sparse models."); - STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Dtmc) || model->isOfType(storm::models::ModelType::Ctmc) || model->isOfType(storm::models::ModelType::Mdp), storm::exceptions::InvalidSettingsException, "Bisimulation minimization is currently only available for DTMCs, CTMCs and MDPs."); - - model->reduceToStateBasedRewards(); - - if (model->isOfType(storm::models::ModelType::Dtmc)) { - return performDeterministicSparseBisimulationMinimization>(model->template as>(), formulas); - } else if (model->isOfType(storm::models::ModelType::Ctmc)) { - return performDeterministicSparseBisimulationMinimization>(model->template as>(), formulas); - } else { - return performNondeterministicSparseBisimulationMinimization>(model->template as>(), formulas); + storm::storage::BisimulationType bisimType = storm::storage::BisimulationType::Strong; + if (storm::settings::bisimulationSettings().isWeakBisimulationSet()) { + bisimType = storm::storage::BisimulationType::Weak; } + STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::InvalidSettingsException, "Bisimulation minimization is currently only available for sparse models."); + return performBisimulationMinimization(model, formulas, bisimType); } return model; } diff --git a/test/functional/storage/DeterministicModelBisimulationDecompositionTest.cpp b/test/functional/storage/DeterministicModelBisimulationDecompositionTest.cpp index a706475bd..6eed6ac92 100644 --- a/test/functional/storage/DeterministicModelBisimulationDecompositionTest.cpp +++ b/test/functional/storage/DeterministicModelBisimulationDecompositionTest.cpp @@ -35,8 +35,7 @@ TEST(DeterministicModelBisimulationDecomposition, Die) { EXPECT_EQ(5ul, result->getNumberOfStates()); EXPECT_EQ(8ul, result->getNumberOfTransitions()); - options.bounded = false; - options.type = storm::storage::BisimulationType::Weak; + options.setType(storm::storage::BisimulationType::Weak); storm::storage::DeterministicModelBisimulationDecomposition> bisim3(*dtmc, options); ASSERT_NO_THROW(bisim3.computeBisimulationDecomposition()); @@ -93,8 +92,7 @@ TEST(DeterministicModelBisimulationDecomposition, Crowds) { EXPECT_EQ(65ul, result->getNumberOfStates()); EXPECT_EQ(105ul, result->getNumberOfTransitions()); - options.bounded = false; - options.type = storm::storage::BisimulationType::Weak; + options.setType(storm::storage::BisimulationType::Weak); storm::storage::DeterministicModelBisimulationDecomposition> bisim3(*dtmc, options); ASSERT_NO_THROW(bisim3.computeBisimulationDecomposition()); From 1c7f5dae56848fc75f139dd39a50b2a6690574a3 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 26 Jan 2016 18:34:33 +0100 Subject: [PATCH 9/9] fixed a bug pointed out by Matthias Former-commit-id: 0a4355c5804b6febbdaf2783465a9776730dfd8b --- src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp | 4 ---- 1 file changed, 4 deletions(-) diff --git a/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp index 564b635bc..5043c8296 100644 --- a/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp +++ b/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp @@ -262,10 +262,6 @@ namespace storm { if (startingIteration == 0) { result = values; storm::utility::vector::scaleVectorInPlace(result, std::get<3>(foxGlynnResult)[0]); - std::function addAndScale = [&foxGlynnResult] (ValueType const& a, ValueType const& b) { return a + std::get<3>(foxGlynnResult)[0] * b; }; - if (addVector != nullptr) { - storm::utility::vector::applyPointwise(result, *addVector, result, addAndScale); - } ++startingIteration; } else { if (computeCumulativeReward) {