From af270dee8aec1f67fe54498ed868dd7641d28282 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 13 Oct 2014 17:24:52 +0200 Subject: [PATCH] Enabled bisimulation quotienting. Former-commit-id: 588827ec8d32cb9cd3e4d17222da6f328674ac99 --- src/models/Dtmc.h | 10 +++-- ...ministicModelBisimulationDecomposition.cpp | 38 ++++++++++++++----- src/storage/StateBlock.h | 10 ++++- src/utility/cli.h | 16 +++++--- src/utility/constants.h | 1 + 5 files changed, 55 insertions(+), 20 deletions(-) diff --git a/src/models/Dtmc.h b/src/models/Dtmc.h index 0252b7533..98792982a 100644 --- a/src/models/Dtmc.h +++ b/src/models/Dtmc.h @@ -45,8 +45,9 @@ public: * @param optionalChoiceLabeling A vector that represents the labels associated with the choices of each state. */ Dtmc(storm::storage::SparseMatrix const& probabilityMatrix, storm::models::AtomicPropositionsLabeling const& stateLabeling, - boost::optional> const& optionalStateRewardVector, boost::optional> const& optionalTransitionRewardMatrix, - boost::optional>> const& optionalChoiceLabeling) + boost::optional> const& optionalStateRewardVector = boost::optional>(), + boost::optional> const& optionalTransitionRewardMatrix = boost::optional>(), + boost::optional>> const& optionalChoiceLabeling = boost::optional>>()) : AbstractDeterministicModel(probabilityMatrix, stateLabeling, optionalStateRewardVector, optionalTransitionRewardMatrix, optionalChoiceLabeling) { if (!this->checkValidityOfProbabilityMatrix()) { LOG4CPLUS_ERROR(logger, "Probability matrix is invalid."); @@ -72,8 +73,9 @@ public: * @param optionalChoiceLabeling A vector that represents the labels associated with the choices of each state. */ Dtmc(storm::storage::SparseMatrix&& probabilityMatrix, storm::models::AtomicPropositionsLabeling&& stateLabeling, - boost::optional>&& optionalStateRewardVector, boost::optional>&& optionalTransitionRewardMatrix, - boost::optional>>&& optionalChoiceLabeling) + boost::optional>&& optionalStateRewardVector = boost::optional>(), + boost::optional>&& optionalTransitionRewardMatrix = boost::optional>(), + boost::optional>>&& optionalChoiceLabeling = boost::optional>>()) // The std::move call must be repeated here because otherwise this calls the copy constructor of the Base Class : AbstractDeterministicModel(std::move(probabilityMatrix), std::move(stateLabeling), std::move(optionalStateRewardVector), std::move(optionalTransitionRewardMatrix), std::move(optionalChoiceLabeling)) { diff --git a/src/storage/DeterministicModelBisimulationDecomposition.cpp b/src/storage/DeterministicModelBisimulationDecomposition.cpp index 6a11b3e9a..d9023d153 100644 --- a/src/storage/DeterministicModelBisimulationDecomposition.cpp +++ b/src/storage/DeterministicModelBisimulationDecomposition.cpp @@ -475,6 +475,7 @@ namespace storm { template DeterministicModelBisimulationDecomposition::DeterministicModelBisimulationDecomposition(storm::models::Dtmc const& dtmc, bool weak, bool buildQuotient) { + STORM_LOG_THROW(!dtmc.hasStateRewards() && !dtmc.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures."); computeBisimulationEquivalenceClasses(dtmc, weak, buildQuotient); } @@ -492,7 +493,7 @@ namespace storm { // (c) the new reward structures. // Prepare a matrix builder for (a). - storm::storage::SparseMatrixBuilder builder; + storm::storage::SparseMatrixBuilder builder(this->size(), this->size()); // Prepare the new state labeling for (b). storm::models::AtomicPropositionsLabeling newLabeling(this->size(), dtmc.getStateLabeling().getNumberOfAtomicPropositions()); @@ -509,7 +510,22 @@ namespace storm { // Pick one representative state. It doesn't matter which state it is, because they all behave equally. storm::storage::sparse::state_type representativeState = *block.begin(); - // Add the outgoing transitions + // Compute the outgoing transitions of the block. + std::map blockProbability; + for (auto const& entry : dtmc.getTransitionMatrix().getRow(representativeState)) { + storm::storage::sparse::state_type targetBlock = partition.getBlock(entry.getColumn()).getId(); + auto probIterator = blockProbability.find(targetBlock); + if (probIterator != blockProbability.end()) { + probIterator->second += entry.getValue(); + } else { + blockProbability[targetBlock] = entry.getValue(); + } + } + + // Now add them to the actual matrix. + for (auto const& probabilityEntry : blockProbability) { + builder.addNextValue(blockIndex, probabilityEntry.first, probabilityEntry.second); + } // Add all atomic propositions to the equivalence class that the representative state satisfies. for (auto const& ap : atomicPropositions) { @@ -525,7 +541,11 @@ namespace storm { newLabeling.addAtomicPropositionToState("init", initialBlock.getId()); } - this->quotient = nullptr; + // FIXME: + // If reward structures are allowed, the quotient structures need to be built here. + + // Finally construct the quotient model. + this->quotient = std::shared_ptr>(new storm::models::Dtmc(builder.build(), std::move(newLabeling))); } template @@ -555,16 +575,16 @@ namespace storm { splitterQueue.pop_front(); } - // If we are required to build the quotient model, do so now. - if (buildQuotient) { - this->buildQuotient(dtmc, partition); - } - // Now move the states from the internal partition into their final place in the decomposition. We do so in // a way that maintains the block IDs as indices. this->blocks.resize(partition.size()); for (auto const& block : partition.getBlocks()) { - this->blocks[block.getId()] = block_type(partition.getBeginOfStates(block), partition.getEndOfStates(block)); + this->blocks[block.getId()] = block_type(partition.getBeginOfStates(block), partition.getEndOfStates(block), true); + } + + // If we are required to build the quotient model, do so now. + if (buildQuotient) { + this->buildQuotient(dtmc, partition); } std::chrono::high_resolution_clock::duration totalTime = std::chrono::high_resolution_clock::now() - totalStart; diff --git a/src/storage/StateBlock.h b/src/storage/StateBlock.h index 8497f3a2f..e9a8d5ebe 100644 --- a/src/storage/StateBlock.h +++ b/src/storage/StateBlock.h @@ -2,6 +2,7 @@ #define STORM_STORAGE_BLOCK_H_ #include +#include #include "src/utility/OsDetection.h" #include "src/storage/sparse/StateType.h" @@ -35,10 +36,15 @@ namespace storm { * * @param first The first element of the range to insert. * @param last The last element of the range (that is itself not inserted). + * @param sortedAndUnique If set to true, the input range is assumed to be sorted and duplicate-free. */ template - StateBlock(InputIterator first, InputIterator last) : states(first, last) { - // Intentionally left empty. + StateBlock(InputIterator first, InputIterator last, bool sortedAndUnique = false) { + if (sortedAndUnique) { + this->states = container_type(boost::container::ordered_unique_range_t(), first, last); + } else { + this->states = container_type(first, last); + } } /*! diff --git a/src/utility/cli.h b/src/utility/cli.h index ed63f5086..ab99d4bda 100644 --- a/src/utility/cli.h +++ b/src/utility/cli.h @@ -258,11 +258,20 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model."); } + // Print some information about the model. + result->printModelInformationToStream(std::cout); + if (settings.isBisimulationSet()) { STORM_LOG_THROW(result->getType() == storm::models::DTMC, storm::exceptions::InvalidSettingsException, "Bisimulation minimization is currently only compatible with DTMCs."); std::shared_ptr> dtmc = result->template as>(); - storm::storage::DeterministicModelBisimulationDecomposition bisimulationDecomposition(*dtmc); - return bisimulationDecomposition.getQuotient(); + + STORM_PRINT(std::endl << "Performing bisimulation minimization..." << std::endl); + storm::storage::DeterministicModelBisimulationDecomposition bisimulationDecomposition(*dtmc, false, true); + + result = bisimulationDecomposition.getQuotient(); + + STORM_PRINT_AND_LOG(std::endl << "Model after minimization:" << std::endl); + result->printModelInformationToStream(std::cout); } return result; @@ -300,9 +309,6 @@ namespace storm { // Start by parsing/building the model. std::shared_ptr> model = buildModel(); - // Print some information about the model. - model->printModelInformationToStream(std::cout); - // If we were requested to generate a counterexample, we now do so. if (settings.isCounterexampleSet()) { STORM_LOG_THROW(settings.isPctlPropertySet(), storm::exceptions::InvalidSettingsException, "Unable to generate counterexample without a property."); diff --git a/src/utility/constants.h b/src/utility/constants.h index e8a194619..a857e40ba 100644 --- a/src/utility/constants.h +++ b/src/utility/constants.h @@ -202,6 +202,7 @@ inline storm::storage::LabeledValues constantInfinity() { /*! @endcond */ + } //namespace utility } //namespace storm