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());