From caa7335afa8c6af64e0edf82323ab3d17a4065cd Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Tue, 7 Oct 2014 20:16:25 +0200
Subject: [PATCH 01/14] Started work on sparse bisimulation decomposition.
Former-commit-id: 56840e4705586978856cf2b87fdc38219a8e8b7b
---
src/settings/modules/GeneralSettings.cpp | 9 ++-
src/settings/modules/GeneralSettings.h | 9 +++
src/storage/BisimulationDecomposition.cpp | 50 ++++++++++++++++
src/storage/BisimulationDecomposition.h | 28 +++++++++
src/storage/Distribution.cpp | 35 +++++++++++
src/storage/Distribution.h | 71 +++++++++++++++++++++++
6 files changed, 200 insertions(+), 2 deletions(-)
create mode 100644 src/storage/BisimulationDecomposition.cpp
create mode 100644 src/storage/BisimulationDecomposition.h
create mode 100644 src/storage/Distribution.cpp
create mode 100644 src/storage/Distribution.h
diff --git a/src/settings/modules/GeneralSettings.cpp b/src/settings/modules/GeneralSettings.cpp
index 585bcfdfb..b10204e29 100644
--- a/src/settings/modules/GeneralSettings.cpp
+++ b/src/settings/modules/GeneralSettings.cpp
@@ -42,6 +42,8 @@ namespace storm {
const std::string GeneralSettings::constantsOptionShortName = "const";
const std::string GeneralSettings::statisticsOptionName = "statistics";
const std::string GeneralSettings::statisticsOptionShortName = "stats";
+ const std::string GeneralSettings::bisimulationOptionName = "bisimulation";
+ const std::string GeneralSettings::bisimulationOptionShortName = "bisim";
GeneralSettings::GeneralSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) {
this->addOption(storm::settings::OptionBuilder(moduleName, helpOptionName, false, "Shows all available options, arguments and descriptions.").setShortName(helpOptionShortName)
@@ -72,7 +74,7 @@ namespace storm {
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the LTL formulas.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, counterexampleOptionName, false, "Generates a counterexample for the given PRCTL formulas if not satisfied by the model")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to which the counterexample is to be written.").setDefaultValueString("-").setIsOptional(true).build()).setShortName(counterexampleOptionShortName).build());
-
+ this->addOption(storm::settings::OptionBuilder(moduleName, bisimulationOptionName, true, "Sets whether to perform bisimulation minimization.").setShortName(bisimulationOptionShortName).build());
this->addOption(storm::settings::OptionBuilder(moduleName, transitionRewardsOptionName, "", "If given, the transition rewards are read from this file and added to the explicit model. Note that this requires the model to be given as an explicit model (i.e., via --" + explicitOptionName + ").")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the transition rewards.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, stateRewardsOptionName, false, "If given, the state rewards are read from this file and added to the explicit model. Note that this requires the model to be given as an explicit model (i.e., via --" + explicitOptionName + ").")
@@ -91,7 +93,6 @@ namespace storm {
this->addOption(storm::settings::OptionBuilder(moduleName, constantsOptionName, false, "Specifies the constant replacements to use in symbolic models. Note that Note that this requires the model to be given as an symbolic model (i.e., via --" + symbolicOptionName + ").").setShortName(constantsOptionShortName)
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("values", "A comma separated list of constants and their value, e.g. a=1,b=2,c=3.").setDefaultValueString("").build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, statisticsOptionName, true, "Sets whether to display statistics if available.").setShortName(statisticsOptionShortName).build());
-
}
bool GeneralSettings::isHelpSet() const {
@@ -278,6 +279,10 @@ namespace storm {
return true;
}
+ bool GeneralSettings::isBisimulationSet() const {
+ return this->getOption(bisimulationOptionName).getHasOptionBeenSet();
+ }
+
} // namespace modules
} // namespace settings
} // namespace storm
\ No newline at end of file
diff --git a/src/settings/modules/GeneralSettings.h b/src/settings/modules/GeneralSettings.h
index 75f48d8f1..f4cdf96d0 100644
--- a/src/settings/modules/GeneralSettings.h
+++ b/src/settings/modules/GeneralSettings.h
@@ -314,6 +314,13 @@ namespace storm {
*/
bool isShowStatisticsSet() const;
+ /*!
+ * Retrieves whether the option to perform bisimulation minimization is set.
+ *
+ * @return True iff the option was set.
+ */
+ bool isBisimulationSet() const;
+
bool check() const override;
// The name of the module.
@@ -354,6 +361,8 @@ namespace storm {
static const std::string constantsOptionShortName;
static const std::string statisticsOptionName;
static const std::string statisticsOptionShortName;
+ static const std::string bisimulationOptionName;
+ static const std::string bisimulationOptionShortName;
};
} // namespace modules
diff --git a/src/storage/BisimulationDecomposition.cpp b/src/storage/BisimulationDecomposition.cpp
new file mode 100644
index 000000000..ba2e4111b
--- /dev/null
+++ b/src/storage/BisimulationDecomposition.cpp
@@ -0,0 +1,50 @@
+#include "src/storage/BisimulationDecomposition.h"
+
+#include <queue>
+
+namespace storm {
+ namespace storage {
+
+ template<typename ValueType>
+ BisimulationDecomposition<ValueType>::BisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, bool weak) {
+ computeBisimulationEquivalenceClasses(model, weak);
+ }
+
+ template<typename ValueType>
+ void BisimulationDecomposition<ValueType>::computeBisimulationEquivalenceClasses(storm::models::Dtmc<ValueType> const& model, bool weak) {
+ // We start by computing the initial partition. In particular, we also keep a mapping of states to their blocks.
+ std::vector<std::size_t> stateToBlockMapping(model.getNumberOfStates());
+ storm::storage::BitVector labeledStates = model.getLabeledStates("one");
+ this->blocks.emplace_back(labeledStates.begin(), labeledStates.end());
+ std::for_each(labeledStates.begin(), labeledStates.end(), [&] (storm::storage::sparse::state_type const& state) { stateToBlockMapping[state] = 0; } );
+ labeledStates.complement();
+ this->blocks.emplace_back(labeledStates.begin(), labeledStates.end());
+ std::for_each(labeledStates.begin(), labeledStates.end(), [&] (storm::storage::sparse::state_type const& state) { stateToBlockMapping[state] = 1; } );
+
+ // Retrieve the backward transitions to allow for better checking of states that need to be re-examined.
+ storm::storage::SparseMatrix<ValueType> const& backwardTransitions = model.getBackwardTransitions();
+
+ // Initially, both blocks are potential splitters.
+ std::queue<std::size_t> splitterQueue;
+ splitterQueue.push(0);
+ splitterQueue.push(1);
+
+ // As long as there is a splitter, we keep refining the current partition.
+ while (!splitterQueue.empty()) {
+
+ }
+
+ // While there is a splitter...
+ //
+ // check the predecessors of the splitter:
+ // * if they still have the same signature as before, then they remain unsplit
+ // * otherwise, split off the states that now behave differently
+ // and mark the smaller block as a splitter
+
+ //
+
+ }
+
+ template class BisimulationDecomposition<double>;
+ }
+}
\ No newline at end of file
diff --git a/src/storage/BisimulationDecomposition.h b/src/storage/BisimulationDecomposition.h
new file mode 100644
index 000000000..1d2535b2e
--- /dev/null
+++ b/src/storage/BisimulationDecomposition.h
@@ -0,0 +1,28 @@
+#ifndef STORM_STORAGE_BISIMULATIONDECOMPOSITION_H_
+#define STORM_STORAGE_BISIMULATIONDECOMPOSITION_H_
+
+#include "src/storage/Decomposition.h"
+#include "src/models/Dtmc.h"
+
+namespace storm {
+ namespace storage {
+
+ /*!
+ * This class represents the decomposition model into its bisimulation quotient.
+ */
+ template <typename ValueType>
+ class BisimulationDecomposition : public Decomposition<StateBlock> {
+ public:
+ /*!
+ * Decomposes the given DTMC into equivalence classes under weak or strong bisimulation.
+ */
+ BisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, bool weak);
+
+ private:
+ void computeBisimulationEquivalenceClasses(storm::models::Dtmc<ValueType> const& model, bool weak);
+ };
+
+ }
+}
+
+#endif /* STORM_STORAGE_BISIMULATIONDECOMPOSITION_H_ */
\ No newline at end of file
diff --git a/src/storage/Distribution.cpp b/src/storage/Distribution.cpp
new file mode 100644
index 000000000..84bda0abf
--- /dev/null
+++ b/src/storage/Distribution.cpp
@@ -0,0 +1,35 @@
+#include "src/storage/Distribution.h"
+
+#include <algorithm>
+
+namespace storm {
+ namespace storage {
+ template<typename ValueType>
+ void Distribution<ValueType>::addProbability(storm::storage::sparse::state_type const& state, ValueType const& probability) {
+ this->distribution[state] += probability;
+ this->hash += static_cast<std::size_t>(state);
+ }
+
+ template<typename ValueType>
+ typename Distribution<ValueType>::iterator Distribution<ValueType>::begin() {
+ return this->distribution.begin();
+ }
+
+ template<typename ValueType>
+ typename Distribution<ValueType>::const_iterator Distribution<ValueType>::begin() const {
+ return this->distribution.begin();
+ }
+
+ template<typename ValueType>
+ typename Distribution<ValueType>::iterator Distribution<ValueType>::end() {
+ return this->distribution.end();
+ }
+
+ template<typename ValueType>
+ typename Distribution<ValueType>::const_iterator Distribution<ValueType>::end() const {
+ return this->distribution.end();
+ }
+
+ template class Distribution<double>;
+ }
+}
\ No newline at end of file
diff --git a/src/storage/Distribution.h b/src/storage/Distribution.h
new file mode 100644
index 000000000..97639501c
--- /dev/null
+++ b/src/storage/Distribution.h
@@ -0,0 +1,71 @@
+#ifndef STORM_STORAGE_DISTRIBUTION_H_
+#define STORM_STORAGE_DISTRIBUTION_H_
+
+#include <vector>
+#include <boost/container/flat_map.hpp>
+
+#include "src/storage/sparse/StateType.h"
+
+namespace storm {
+ namespace storage {
+
+ template<typename ValueType>
+ class Distribution {
+ public:
+ typedef boost::container::flat_map<storm::storage::sparse::state_type, ValueType> container_type;
+ typedef typename container_type::iterator iterator;
+ typedef typename container_type::const_iterator const_iterator;
+
+ /*!
+ * Creates an empty distribution.
+ */
+ Distribution() = default;
+
+ /*!
+ * Assigns the given state the given probability under this distribution.
+ *
+ * @param state The state to which to assign the probability.
+ * @param probability The probability to assign.
+ */
+ void addProbability(storm::storage::sparse::state_type const& state, ValueType const& probability);
+
+ /*!
+ * Retrieves an iterator to the elements in this distribution.
+ *
+ * @return The iterator to the elements in this distribution.
+ */
+ iterator begin();
+
+ /*!
+ * Retrieves an iterator to the elements in this distribution.
+ *
+ * @return The iterator to the elements in this distribution.
+ */
+ const_iterator begin() const;
+
+ /*!
+ * Retrieves an iterator past the elements in this distribution.
+ *
+ * @return The iterator past the elements in this distribution.
+ */
+ iterator end();
+
+ /*!
+ * Retrieves an iterator past the elements in this distribution.
+ *
+ * @return The iterator past the elements in this distribution.
+ */
+ const_iterator end() const;
+
+ private:
+ // A list of states and the probabilities that are assigned to them.
+ container_type distribution;
+
+ // A hash value that is maintained to allow for quicker equality comparison between distribution.s
+ std::size_t hash;
+ };
+
+ }
+}
+
+#endif /* STORM_STORAGE_DISTRIBUTION_H_ */
\ No newline at end of file
From ca9dddb11052691f28d3db8bf692829be7bd71c1 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Wed, 8 Oct 2014 18:10:14 +0200
Subject: [PATCH 02/14] Sparse Bisimulation is still ongoing work.
Former-commit-id: 0b82c628a9b3f2dcf9fa5d2c0281b144bd174c5b
---
src/settings/modules/GeneralSettings.cpp | 4 +-
src/storage/BisimulationDecomposition.cpp | 183 +++++++++++++++++++---
src/storage/BisimulationDecomposition.h | 11 +-
src/storage/Decomposition.cpp | 5 +-
src/storage/Distribution.cpp | 56 ++++++-
src/storage/Distribution.h | 32 +++-
src/storage/StateBlock.cpp | 5 +
src/storage/StateBlock.h | 7 +
src/utility/cli.h | 10 ++
9 files changed, 284 insertions(+), 29 deletions(-)
diff --git a/src/settings/modules/GeneralSettings.cpp b/src/settings/modules/GeneralSettings.cpp
index b10204e29..f251aad38 100644
--- a/src/settings/modules/GeneralSettings.cpp
+++ b/src/settings/modules/GeneralSettings.cpp
@@ -74,7 +74,7 @@ namespace storm {
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the LTL formulas.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, counterexampleOptionName, false, "Generates a counterexample for the given PRCTL formulas if not satisfied by the model")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to which the counterexample is to be written.").setDefaultValueString("-").setIsOptional(true).build()).setShortName(counterexampleOptionShortName).build());
- this->addOption(storm::settings::OptionBuilder(moduleName, bisimulationOptionName, true, "Sets whether to perform bisimulation minimization.").setShortName(bisimulationOptionShortName).build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, bisimulationOptionName, false, "Sets whether to perform bisimulation minimization.").setShortName(bisimulationOptionShortName).build());
this->addOption(storm::settings::OptionBuilder(moduleName, transitionRewardsOptionName, "", "If given, the transition rewards are read from this file and added to the explicit model. Note that this requires the model to be given as an explicit model (i.e., via --" + explicitOptionName + ").")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the transition rewards.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, stateRewardsOptionName, false, "If given, the state rewards are read from this file and added to the explicit model. Note that this requires the model to be given as an explicit model (i.e., via --" + explicitOptionName + ").")
@@ -92,7 +92,7 @@ namespace storm {
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of an LP solver. Available are: gurobi and glpk.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(lpSolvers)).setDefaultValueString("glpk").build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, constantsOptionName, false, "Specifies the constant replacements to use in symbolic models. Note that Note that this requires the model to be given as an symbolic model (i.e., via --" + symbolicOptionName + ").").setShortName(constantsOptionShortName)
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("values", "A comma separated list of constants and their value, e.g. a=1,b=2,c=3.").setDefaultValueString("").build()).build());
- this->addOption(storm::settings::OptionBuilder(moduleName, statisticsOptionName, true, "Sets whether to display statistics if available.").setShortName(statisticsOptionShortName).build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, statisticsOptionName, false, "Sets whether to display statistics if available.").setShortName(statisticsOptionShortName).build());
}
bool GeneralSettings::isHelpSet() const {
diff --git a/src/storage/BisimulationDecomposition.cpp b/src/storage/BisimulationDecomposition.cpp
index ba2e4111b..53459fb38 100644
--- a/src/storage/BisimulationDecomposition.cpp
+++ b/src/storage/BisimulationDecomposition.cpp
@@ -1,48 +1,189 @@
#include "src/storage/BisimulationDecomposition.h"
-#include <queue>
+#include <unordered_map>
+#include <chrono>
namespace storm {
namespace storage {
template<typename ValueType>
- BisimulationDecomposition<ValueType>::BisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, bool weak) {
- computeBisimulationEquivalenceClasses(model, weak);
+ BisimulationDecomposition<ValueType>::BisimulationDecomposition(storm::models::Dtmc<ValueType> const& dtmc, bool weak) {
+ computeBisimulationEquivalenceClasses(dtmc, weak);
}
template<typename ValueType>
- void BisimulationDecomposition<ValueType>::computeBisimulationEquivalenceClasses(storm::models::Dtmc<ValueType> const& model, bool weak) {
+ void BisimulationDecomposition<ValueType>::computeBisimulationEquivalenceClasses(storm::models::Dtmc<ValueType> const& dtmc, bool weak) {
+ std::chrono::high_resolution_clock::time_point totalStart = std::chrono::high_resolution_clock::now();
// We start by computing the initial partition. In particular, we also keep a mapping of states to their blocks.
- std::vector<std::size_t> stateToBlockMapping(model.getNumberOfStates());
- storm::storage::BitVector labeledStates = model.getLabeledStates("one");
+ std::vector<std::size_t> stateToBlockMapping(dtmc.getNumberOfStates());
+ storm::storage::BitVector labeledStates = dtmc.getLabeledStates("observe0Greater1");
this->blocks.emplace_back(labeledStates.begin(), labeledStates.end());
std::for_each(labeledStates.begin(), labeledStates.end(), [&] (storm::storage::sparse::state_type const& state) { stateToBlockMapping[state] = 0; } );
labeledStates.complement();
this->blocks.emplace_back(labeledStates.begin(), labeledStates.end());
std::for_each(labeledStates.begin(), labeledStates.end(), [&] (storm::storage::sparse::state_type const& state) { stateToBlockMapping[state] = 1; } );
+ // Create empty distributions for the two initial blocks.
+ std::vector<storm::storage::Distribution<ValueType>> distributions(2);
+
// Retrieve the backward transitions to allow for better checking of states that need to be re-examined.
- storm::storage::SparseMatrix<ValueType> const& backwardTransitions = model.getBackwardTransitions();
+ storm::storage::SparseMatrix<ValueType> const& backwardTransitions = dtmc.getBackwardTransitions();
- // Initially, both blocks are potential splitters.
- std::queue<std::size_t> splitterQueue;
- splitterQueue.push(0);
- splitterQueue.push(1);
-
- // As long as there is a splitter, we keep refining the current partition.
- while (!splitterQueue.empty()) {
+ // Initially, both blocks are potential splitters. A splitter is marked as a pair in which the first entry
+ // is the ID of the parent block of the splitter and the second entry is the block ID of the splitter itself.
+ std::deque<std::size_t> refinementQueue;
+ storm::storage::BitVector blocksInRefinementQueue(this->size());
+ refinementQueue.push_back(0);
+ refinementQueue.push_back(1);
+
+ // As long as there are blocks to refine, well, refine them.
+ uint_fast64_t iteration = 0;
+ while (!refinementQueue.empty()) {
+ ++iteration;
+
+ // Optionally sort the queue to potentially speed up the convergence.
+ // std::sort(refinementQueue.begin(), refinementQueue.end(), [=] (std::size_t const& a, std::size_t const& b) { return this->blocks[a].size() > this->blocks[b].size(); });
+ std::size_t currentBlock = refinementQueue.front();
+ refinementQueue.pop_front();
+ blocksInRefinementQueue.set(currentBlock, false);
+
+ splitBlock(dtmc, backwardTransitions, currentBlock, stateToBlockMapping, distributions, blocksInRefinementQueue, refinementQueue);
}
- // While there is a splitter...
- //
- // check the predecessors of the splitter:
- // * if they still have the same signature as before, then they remain unsplit
- // * otherwise, split off the states that now behave differently
- // and mark the smaller block as a splitter
+ std::chrono::high_resolution_clock::duration totalTime = std::chrono::high_resolution_clock::now() - totalStart;
- //
+ std::cout << "Bisimulation quotient has " << this->blocks.size() << " blocks and took " << iteration << " iterations and " << std::chrono::duration_cast<std::chrono::milliseconds>(totalTime).count() << "ms." << std::endl;
+ }
+
+ template<typename ValueType>
+ std::size_t BisimulationDecomposition<ValueType>::splitPredecessorsGraphBased(storm::models::Dtmc<ValueType> const& dtmc, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::size_t const& blockId, std::vector<std::size_t>& stateToBlockMapping, std::vector<storm::storage::Distribution<ValueType>>& distributions, storm::storage::BitVector& blocksInRefinementQueue, std::deque<std::size_t>& graphRefinementQueue) {
+
+ // This method tries to split the blocks of predecessors of the provided block by checking whether there is
+ // a transition into the current block or not.
+ std::unordered_map<std::size_t, typename BisimulationDecomposition<ValueType>::block_type> predecessorBlockToNewBlock;
+
+ // Now for each predecessor block which state could actually reach the current block.
+ for (auto const& state : this->blocks[blockId]) {
+ for (auto const& predecessorEntry : backwardTransitions.getRow(state)) {
+ storm::storage::sparse::state_type predecessor = predecessorEntry.getColumn();
+ predecessorBlockToNewBlock[stateToBlockMapping[predecessor]].insert(predecessor);
+ }
+ }
+
+ // Now, we can check for each predecessor block whether it needs to be split.
+ for (auto const& blockNewBlockPair : predecessorBlockToNewBlock) {
+ if (this->blocks[blockNewBlockPair.first].size() > blockNewBlockPair.second.size()) {
+ // Add the states which have a successor in the current block to a totally new block.
+ this->blocks.emplace_back(std::move(blockNewBlockPair.second));
+
+ // Compute the set of states that remains in the old block;
+ typename BisimulationDecomposition<ValueType>::block_type newBlock;
+ std::set_difference(this->blocks[blockId].begin(), this->blocks[blockId].end(), this->blocks.back().begin(), this->blocks.back().end(), std::inserter(newBlock, newBlock.begin()));
+ this->blocks[blockNewBlockPair.first] = std::move(newBlock);
+
+ blocksInRefinementQueue.resize(this->blocks.size());
+
+ // Add the smaller part of the old block to the queue.
+ std::size_t blockToAddToQueue = this->blocks.back().size() < this->blocks[blockNewBlockPair.first].size() ? this->blocks.size() - 1 : blockNewBlockPair.first;
+ if (!blocksInRefinementQueue.get(blockToAddToQueue)) {
+ graphRefinementQueue.push_back(blockToAddToQueue);
+ blocksInRefinementQueue.set(blockToAddToQueue, true);
+ }
+ }
+ }
+
+ // FIXME
+ return 0;
+ }
+
+ template<typename ValueType>
+ std::size_t BisimulationDecomposition<ValueType>::splitBlock(storm::models::Dtmc<ValueType> const& dtmc, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::size_t const& blockId, std::vector<std::size_t>& stateToBlockMapping, std::vector<storm::storage::Distribution<ValueType>>& distributions, storm::storage::BitVector& blocksInRefinementQueue, std::deque<std::size_t>& refinementQueue) {
+ std::chrono::high_resolution_clock::time_point totalStart = std::chrono::high_resolution_clock::now();
+ std::unordered_map<storm::storage::Distribution<ValueType>, typename BisimulationDecomposition<ValueType>::block_type> distributionToNewBlocks;
+
+ // Traverse all states of the block and check whether they have different distributions.
+ for (auto const& state : this->blocks[blockId]) {
+ // Now construct the distribution of this state wrt. to the current partitioning.
+ storm::storage::Distribution<ValueType> distribution;
+ for (auto const& successorEntry : dtmc.getTransitionMatrix().getRow(state)) {
+ distribution.addProbability(static_cast<storm::storage::sparse::state_type>(stateToBlockMapping[successorEntry.getColumn()]), successorEntry.getValue());
+ }
+
+ // If the distribution already exists, we simply add the state. Otherwise, we open a new block.
+ auto distributionIterator = distributionToNewBlocks.find(distribution);
+ if (distributionIterator != distributionToNewBlocks.end()) {
+ distributionIterator->second.insert(state);
+ } else {
+ distributionToNewBlocks[distribution].insert(state);
+ }
+ }
+
+ // Now we are ready to split the block.
+ if (distributionToNewBlocks.size() == 1) {
+ // If there is just one behavior, we just set the distribution as the new one for this block.
+ distributions[blockId] = std::move(distributionToNewBlocks.begin()->first);
+ } else {
+ // In this case, we need to split the block.
+ typename BisimulationDecomposition<ValueType>::block_type tmpBlock;
+
+ auto distributionIterator = distributionToNewBlocks.begin();
+ distributions[blockId] = std::move(distributionIterator->first);
+ tmpBlock = std::move(distributionIterator->second);
+ std::swap(this->blocks[blockId], tmpBlock);
+ ++distributionIterator;
+
+ // Remember the number of blocks prior to splitting for later use.
+ std::size_t beforeNumberOfBlocks = this->blocks.size();
+
+ for (; distributionIterator != distributionToNewBlocks.end(); ++distributionIterator) {
+ // In this case, we need to move the newly created block to the end of the list of actual blocks.
+ this->blocks.emplace_back(std::move(distributionIterator->second));
+ distributions.emplace_back(std::move(distributionIterator->first));
+
+ // Update the mapping of states to their blocks.
+ std::size_t newBlockId = this->blocks.size() - 1;
+ for (auto const& state : this->blocks.back()) {
+ stateToBlockMapping[state] = newBlockId;
+ }
+ }
+
+ // Now that we have split the block, we try to trigger a chain of graph-based splittings. That is, we
+ // try to split the predecessors of the current block by checking whether they have some transition
+ // to one given sub-block of the current block.
+ std::deque<std::size_t> localRefinementQueue;
+ storm::storage::BitVector blocksInLocalRefinementQueue(this->size());
+ localRefinementQueue.push_back(blockId);
+ for (std::size_t i = beforeNumberOfBlocks; i < this->blocks.size(); ++i) {
+ localRefinementQueue.push_back(i);
+ }
+
+ while (!localRefinementQueue.empty()) {
+ std::size_t currentBlock = localRefinementQueue.front();
+ localRefinementQueue.pop_front();
+ blocksInLocalRefinementQueue.set(currentBlock, false);
+
+ splitPredecessorsGraphBased(dtmc, backwardTransitions, blockId, stateToBlockMapping, distributions, blocksInLocalRefinementQueue, localRefinementQueue);
+ }
+
+ // Since we created some new blocks, we need to extend the bit vector storing the blocks in the
+ // refinement queue.
+ blocksInRefinementQueue.resize(blocksInRefinementQueue.size() + (distributionToNewBlocks.size() - 1));
+
+ // Insert blocks that possibly need a refinement into the queue.
+ for (auto const& state : tmpBlock) {
+ for (auto const& predecessor : backwardTransitions.getRow(state)) {
+ if (!blocksInRefinementQueue.get(stateToBlockMapping[predecessor.getColumn()])) {
+ blocksInRefinementQueue.set(stateToBlockMapping[predecessor.getColumn()]);
+ refinementQueue.push_back(stateToBlockMapping[predecessor.getColumn()]);
+ }
+ }
+ }
+ }
+ std::chrono::high_resolution_clock::duration totalTime = std::chrono::high_resolution_clock::now() - totalStart;
+ std::cout << "refinement of block " << blockId << " took " << std::chrono::duration_cast<std::chrono::milliseconds>(totalTime).count() << "ms." << std::endl;
+ return distributionToNewBlocks.size();
}
template class BisimulationDecomposition<double>;
diff --git a/src/storage/BisimulationDecomposition.h b/src/storage/BisimulationDecomposition.h
index 1d2535b2e..d02d02bc1 100644
--- a/src/storage/BisimulationDecomposition.h
+++ b/src/storage/BisimulationDecomposition.h
@@ -1,8 +1,12 @@
#ifndef STORM_STORAGE_BISIMULATIONDECOMPOSITION_H_
#define STORM_STORAGE_BISIMULATIONDECOMPOSITION_H_
+#include <queue>
+#include <deque>
+
#include "src/storage/Decomposition.h"
#include "src/models/Dtmc.h"
+#include "src/storage/Distribution.h"
namespace storm {
namespace storage {
@@ -13,15 +17,18 @@ namespace storm {
template <typename ValueType>
class BisimulationDecomposition : public Decomposition<StateBlock> {
public:
+ BisimulationDecomposition() = default;
+
/*!
* Decomposes the given DTMC into equivalence classes under weak or strong bisimulation.
*/
- BisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, bool weak);
+ BisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, bool weak = false);
private:
void computeBisimulationEquivalenceClasses(storm::models::Dtmc<ValueType> const& model, bool weak);
+ std::size_t splitPredecessorsGraphBased(storm::models::Dtmc<ValueType> const& dtmc, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::size_t const& block, std::vector<std::size_t>& stateToBlockMapping, std::vector<storm::storage::Distribution<ValueType>>& distributions, storm::storage::BitVector& blocksInRefinementQueue, std::deque<std::size_t>& refinementQueue);
+ std::size_t splitBlock(storm::models::Dtmc<ValueType> const& dtmc, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::size_t const& block, std::vector<std::size_t>& stateToBlockMapping, std::vector<storm::storage::Distribution<ValueType>>& distributions, storm::storage::BitVector& blocksInRefinementQueue, std::deque<std::size_t>& refinementQueue);
};
-
}
}
diff --git a/src/storage/Decomposition.cpp b/src/storage/Decomposition.cpp
index 06656b483..39c49bf4f 100644
--- a/src/storage/Decomposition.cpp
+++ b/src/storage/Decomposition.cpp
@@ -89,7 +89,10 @@ namespace storm {
out << "]";
return out;
}
-
+
+ template class Decomposition<StateBlock>;
+ template std::ostream& operator<<(std::ostream& out, Decomposition<StateBlock> const& decomposition);
+
template class Decomposition<StronglyConnectedComponent>;
template std::ostream& operator<<(std::ostream& out, Decomposition<StronglyConnectedComponent> const& decomposition);
diff --git a/src/storage/Distribution.cpp b/src/storage/Distribution.cpp
index 84bda0abf..55de31d51 100644
--- a/src/storage/Distribution.cpp
+++ b/src/storage/Distribution.cpp
@@ -1,13 +1,48 @@
#include "src/storage/Distribution.h"
#include <algorithm>
+#include <iostream>
+
+#include "src/settings/SettingsManager.h"
namespace storm {
namespace storage {
+
+ template<typename ValueType>
+ Distribution<ValueType>::Distribution() : hash(0) {
+ // Intentionally left empty.
+ }
+
+ template<typename ValueType>
+ bool Distribution<ValueType>::operator==(Distribution<ValueType> const& other) const {
+ // We need to check equality by ourselves, because we need to account for epsilon differences.
+ if (this->distribution.size() != other.distribution.size() || this->getHash() != other.getHash()) {
+ return false;
+ }
+
+ auto first1 = this->distribution.begin();
+ auto last1 = this->distribution.end();
+ auto first2 = other.distribution.begin();
+ auto last2 = other.distribution.end();
+
+ for (; first1 != last1; ++first1, ++first2) {
+ if (first1->first != first2->first) {
+ return false;
+ }
+ if (std::abs(first1->second - first2->second) > 1e-6) {
+ return false;
+ }
+ }
+
+ return true;
+ }
+
template<typename ValueType>
void Distribution<ValueType>::addProbability(storm::storage::sparse::state_type const& state, ValueType const& probability) {
+ if (this->distribution.find(state) == this->distribution.end()) {
+ this->hash += static_cast<std::size_t>(state);
+ }
this->distribution[state] += probability;
- this->hash += static_cast<std::size_t>(state);
}
template<typename ValueType>
@@ -30,6 +65,23 @@ namespace storm {
return this->distribution.end();
}
+ template<typename ValueType>
+ std::size_t Distribution<ValueType>::getHash() const {
+ return this->hash ^ (this->distribution.size() << 8);
+ }
+
+ template<typename ValueType>
+ std::ostream& operator<<(std::ostream& out, Distribution<ValueType> const& distribution) {
+ out << "{";
+ for (auto const& entry : distribution) {
+ out << "[" << entry.second << ": " << entry.first << "], ";
+ }
+ out << "}";
+
+ return out;
+ }
+
template class Distribution<double>;
+ template std::ostream& operator<<(std::ostream& out, Distribution<double> const& distribution);
}
-}
\ No newline at end of file
+}
diff --git a/src/storage/Distribution.h b/src/storage/Distribution.h
index 97639501c..a888a88ed 100644
--- a/src/storage/Distribution.h
+++ b/src/storage/Distribution.h
@@ -2,6 +2,7 @@
#define STORM_STORAGE_DISTRIBUTION_H_
#include <vector>
+#include <ostream>
#include <boost/container/flat_map.hpp>
#include "src/storage/sparse/StateType.h"
@@ -19,7 +20,15 @@ namespace storm {
/*!
* Creates an empty distribution.
*/
- Distribution() = default;
+ Distribution();
+
+ /*!
+ * Checks whether the two distributions specify the same probabilities to go to the same states.
+ *
+ * @param other The distribution with which the current distribution is to be compared.
+ * @return True iff the two distributions are equal.
+ */
+ bool operator==(Distribution const& other) const;
/*!
* Assigns the given state the given probability under this distribution.
@@ -57,6 +66,13 @@ namespace storm {
*/
const_iterator end() const;
+ /*!
+ * Retrieves the hash value of the distribution.
+ *
+ * @return The hash value of the distribution.
+ */
+ std::size_t getHash() const;
+
private:
// A list of states and the probabilities that are assigned to them.
container_type distribution;
@@ -65,7 +81,21 @@ namespace storm {
std::size_t hash;
};
+ template<typename ValueType>
+ std::ostream& operator<<(std::ostream& out, Distribution<ValueType> const& distribution);
}
}
+namespace std {
+
+ template <typename ValueType>
+ struct hash<storm::storage::Distribution<ValueType>> {
+ std::size_t operator()(storm::storage::Distribution<ValueType> const& distribution) const {
+ return (distribution.getHash());
+ }
+ };
+
+}
+
+
#endif /* STORM_STORAGE_DISTRIBUTION_H_ */
\ No newline at end of file
diff --git a/src/storage/StateBlock.cpp b/src/storage/StateBlock.cpp
index fb4f21133..bc270872d 100644
--- a/src/storage/StateBlock.cpp
+++ b/src/storage/StateBlock.cpp
@@ -30,6 +30,10 @@ namespace storm {
states.insert(state);
}
+ StateBlock::iterator StateBlock::insert(container_type::const_iterator iterator, value_type const& state) {
+ return states.insert(iterator, state);
+ }
+
void StateBlock::erase(value_type const& state) {
states.erase(state);
}
@@ -55,5 +59,6 @@ namespace storm {
out << block.getStates();
return out;
}
+
}
}
\ No newline at end of file
diff --git a/src/storage/StateBlock.h b/src/storage/StateBlock.h
index dcd516277..8497f3a2f 100644
--- a/src/storage/StateBlock.h
+++ b/src/storage/StateBlock.h
@@ -101,6 +101,13 @@ namespace storm {
* @param state The state to add to this SCC.
*/
void insert(value_type const& state);
+
+ /*!
+ * Inserts the given element into this SCC.
+ *
+ * @param state The state to add to this SCC.
+ */
+ iterator insert(container_type::const_iterator iterator, value_type const& state);
/*!
* Removes the given element from this SCC.
diff --git a/src/utility/cli.h b/src/utility/cli.h
index 4ceb64a95..0a416e5c3 100644
--- a/src/utility/cli.h
+++ b/src/utility/cli.h
@@ -43,6 +43,9 @@ log4cplus::Logger logger;
// Headers of adapters.
#include "src/adapters/ExplicitModelAdapter.h"
+// Headers for model processing.
+#include "src/storage/BisimulationDecomposition.h"
+
// Headers for counterexample generation.
#include "src/counterexamples/MILPMinimalLabelSetGenerator.h"
#include "src/counterexamples/SMTMinimalCommandSetGenerator.h"
@@ -254,6 +257,12 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model.");
}
+ 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<storm::models::Dtmc<double>> dtmc = result->template as<storm::models::Dtmc<double>>();
+ storm::storage::BisimulationDecomposition<double> bisimulationDecomposition(*dtmc);
+ }
+
return result;
}
@@ -298,6 +307,7 @@ namespace storm {
std::shared_ptr<storm::properties::prctl::PrctlFilter<double>> filterFormula = storm::parser::PrctlParser::parsePrctlFormula(settings.getPctlProperty());
generateCounterexample(model, filterFormula->getChild());
}
+
}
}
From 7a5131ad6d8b8851a47e593b67183715e68dc8ad Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@rwth-aachen.de>
Date: Wed, 8 Oct 2014 18:12:34 +0200
Subject: [PATCH 03/14] added a header which was missing and caused trouble now
it was removed elsewhere
Former-commit-id: 9df50068daf0821ab6edcbca224fda8b3d7308f4
---
src/utility/cli.h | 1 +
1 file changed, 1 insertion(+)
diff --git a/src/utility/cli.h b/src/utility/cli.h
index ebd8a9bc7..1cb0e597d 100644
--- a/src/utility/cli.h
+++ b/src/utility/cli.h
@@ -30,6 +30,7 @@ log4cplus::Logger logger;
// Headers that provide auxiliary functionality.
#include "src/utility/storm-version.h"
+#include "storm-config.h"
#include "src/utility/OsDetection.h"
#include "src/settings/SettingsManager.h"
From b67ac0619f2cd9825744d70536dfbb5001dccb6f Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Wed, 8 Oct 2014 23:18:10 +0200
Subject: [PATCH 04/14] Weak bisimulation now supported. Still need to improve
the performance of the quotienting, however.
Former-commit-id: d0f76808bb9269df3a39e3fde9b05cd11af1916e
---
src/storage/BisimulationDecomposition.cpp | 114 +++++++++++++++++-----
src/storage/BisimulationDecomposition.h | 4 +-
src/storage/Distribution.cpp | 13 +++
src/storage/Distribution.h | 9 ++
4 files changed, 113 insertions(+), 27 deletions(-)
diff --git a/src/storage/BisimulationDecomposition.cpp b/src/storage/BisimulationDecomposition.cpp
index 53459fb38..1c107d1a8 100644
--- a/src/storage/BisimulationDecomposition.cpp
+++ b/src/storage/BisimulationDecomposition.cpp
@@ -48,7 +48,7 @@ namespace storm {
refinementQueue.pop_front();
blocksInRefinementQueue.set(currentBlock, false);
- splitBlock(dtmc, backwardTransitions, currentBlock, stateToBlockMapping, distributions, blocksInRefinementQueue, refinementQueue);
+ splitBlock(dtmc, backwardTransitions, currentBlock, stateToBlockMapping, distributions, blocksInRefinementQueue, refinementQueue, weak);
}
std::chrono::high_resolution_clock::duration totalTime = std::chrono::high_resolution_clock::now() - totalStart;
@@ -57,52 +57,96 @@ namespace storm {
}
template<typename ValueType>
- std::size_t BisimulationDecomposition<ValueType>::splitPredecessorsGraphBased(storm::models::Dtmc<ValueType> const& dtmc, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::size_t const& blockId, std::vector<std::size_t>& stateToBlockMapping, std::vector<storm::storage::Distribution<ValueType>>& distributions, storm::storage::BitVector& blocksInRefinementQueue, std::deque<std::size_t>& graphRefinementQueue) {
+ std::size_t BisimulationDecomposition<ValueType>::splitPredecessorsGraphBased(storm::models::Dtmc<ValueType> const& dtmc, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::size_t const& blockId, std::vector<std::size_t>& stateToBlockMapping, std::vector<storm::storage::Distribution<ValueType>>& distributions, storm::storage::BitVector& blocksInRefinementQueue, std::deque<std::size_t>& graphRefinementQueue, storm::storage::BitVector& splitBlocks) {
+ std::cout << "entering " << std::endl;
+ std::chrono::high_resolution_clock::time_point totalStart = std::chrono::high_resolution_clock::now();
+
+// std::cout << "refining predecessors of " << blockId << std::endl;
// This method tries to split the blocks of predecessors of the provided block by checking whether there is
// a transition into the current block or not.
std::unordered_map<std::size_t, typename BisimulationDecomposition<ValueType>::block_type> predecessorBlockToNewBlock;
// Now for each predecessor block which state could actually reach the current block.
+ std::chrono::high_resolution_clock::time_point predIterStart = std::chrono::high_resolution_clock::now();
+ int predCounter = 0;
+ storm::storage::BitVector preds(dtmc.getNumberOfStates());
for (auto const& state : this->blocks[blockId]) {
for (auto const& predecessorEntry : backwardTransitions.getRow(state)) {
+ ++predCounter;
storm::storage::sparse::state_type predecessor = predecessorEntry.getColumn();
- predecessorBlockToNewBlock[stateToBlockMapping[predecessor]].insert(predecessor);
+ if (!preds.get(predecessor)) {
+// std::cout << "having pred " << predecessor << " with block " << stateToBlockMapping[predecessor] << std::endl;
+ predecessorBlockToNewBlock[stateToBlockMapping[predecessor]].insert(predecessor);
+ preds.set(predecessor);
+ }
}
}
-
+ std::chrono::high_resolution_clock::duration predIterTime = std::chrono::high_resolution_clock::now() - predIterStart;
+ std::cout << "took " << std::chrono::duration_cast<std::chrono::milliseconds>(predIterTime).count() << "ms. for " << predCounter << " predecessors" << std::endl;
+
// Now, we can check for each predecessor block whether it needs to be split.
for (auto const& blockNewBlockPair : predecessorBlockToNewBlock) {
if (this->blocks[blockNewBlockPair.first].size() > blockNewBlockPair.second.size()) {
- // Add the states which have a successor in the current block to a totally new block.
- this->blocks.emplace_back(std::move(blockNewBlockPair.second));
+ std::cout << "splitting!" << std::endl;
+// std::cout << "found that not all " << this->blocks[blockNewBlockPair.first].size() << " states of block " << blockNewBlockPair.first << " have a successor in " << blockId << " but only " << blockNewBlockPair.second.size() << std::endl;
+// std::cout << "original: " << this->blocks[blockNewBlockPair.first] << std::endl;
+// std::cout << "states with pred: " << blockNewBlockPair.second << std::endl;
+ // Now update the block mapping for the smaller of the two blocks.
+ typename BisimulationDecomposition<ValueType>::block_type smallerBlock;
+ typename BisimulationDecomposition<ValueType>::block_type largerBlock;
+ if (blockNewBlockPair.second.size() < this->blocks[blockNewBlockPair.first].size()/2) {
+ smallerBlock = std::move(blockNewBlockPair.second);
+ std::set_difference(this->blocks[blockNewBlockPair.first].begin(), this->blocks[blockNewBlockPair.first].end(), smallerBlock.begin(), smallerBlock.end(), std::inserter(largerBlock, largerBlock.begin()));
+ } else {
+ largerBlock = std::move(blockNewBlockPair.second);
+ std::set_difference(this->blocks[blockNewBlockPair.first].begin(), this->blocks[blockNewBlockPair.first].end(), largerBlock.begin(), largerBlock.end(), std::inserter(smallerBlock, smallerBlock.begin()));
+ }
- // Compute the set of states that remains in the old block;
- typename BisimulationDecomposition<ValueType>::block_type newBlock;
- std::set_difference(this->blocks[blockId].begin(), this->blocks[blockId].end(), this->blocks.back().begin(), this->blocks.back().end(), std::inserter(newBlock, newBlock.begin()));
- this->blocks[blockNewBlockPair.first] = std::move(newBlock);
+// std::cout << "created a smaller block with " << smallerBlock.size() << " states and a larger one with " << largerBlock.size() << "states" << std::endl;
+// std::cout << "smaller: " << smallerBlock << std::endl;
+// std::cout << "larger: " << largerBlock << std::endl;
+
+ this->blocks.emplace_back(std::move(smallerBlock));
+ this->blocks[blockNewBlockPair.first] = std::move(largerBlock);
+
+ // Update the block mapping of all moved states.
+ std::size_t newBlockId = this->blocks.size() - 1;
+ for (auto const& state : this->blocks.back()) {
+ stateToBlockMapping[state] = newBlockId;
+// std::cout << "updating " << state << " to block " << newBlockId << std::endl;
+ }
blocksInRefinementQueue.resize(this->blocks.size());
- // Add the smaller part of the old block to the queue.
- std::size_t blockToAddToQueue = this->blocks.back().size() < this->blocks[blockNewBlockPair.first].size() ? this->blocks.size() - 1 : blockNewBlockPair.first;
- if (!blocksInRefinementQueue.get(blockToAddToQueue)) {
- graphRefinementQueue.push_back(blockToAddToQueue);
- blocksInRefinementQueue.set(blockToAddToQueue, true);
+ // Add both parts of the old block to the queue.
+ if (!blocksInRefinementQueue.get(blockNewBlockPair.first)) {
+ graphRefinementQueue.push_back(blockNewBlockPair.first);
+ blocksInRefinementQueue.set(blockNewBlockPair.first, true);
+// std::cout << "adding " << blockNewBlockPair.first << " to refine further using graph-based analysis " << std::endl;
}
+
+ graphRefinementQueue.push_back(this->blocks.size() - 1);
+ blocksInRefinementQueue.set(this->blocks.size() - 1);
+// std::cout << "adding " << this->blocks.size() - 1 << " to refine further using graph-based analysis " << std::endl;
}
}
+ std::chrono::high_resolution_clock::duration totalTime = std::chrono::high_resolution_clock::now() - totalStart;
+ std::cout << "refinement of predecessors of block " << blockId << " took " << std::chrono::duration_cast<std::chrono::milliseconds>(totalTime).count() << "ms." << std::endl;
+
+// std::cout << "done. "<< std::endl;
// FIXME
return 0;
}
template<typename ValueType>
- std::size_t BisimulationDecomposition<ValueType>::splitBlock(storm::models::Dtmc<ValueType> const& dtmc, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::size_t const& blockId, std::vector<std::size_t>& stateToBlockMapping, std::vector<storm::storage::Distribution<ValueType>>& distributions, storm::storage::BitVector& blocksInRefinementQueue, std::deque<std::size_t>& refinementQueue) {
+ std::size_t BisimulationDecomposition<ValueType>::splitBlock(storm::models::Dtmc<ValueType> const& dtmc, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::size_t const& blockId, std::vector<std::size_t>& stateToBlockMapping, std::vector<storm::storage::Distribution<ValueType>>& distributions, storm::storage::BitVector& blocksInRefinementQueue, std::deque<std::size_t>& refinementQueue, bool weakBisimulation) {
std::chrono::high_resolution_clock::time_point totalStart = std::chrono::high_resolution_clock::now();
std::unordered_map<storm::storage::Distribution<ValueType>, typename BisimulationDecomposition<ValueType>::block_type> distributionToNewBlocks;
// Traverse all states of the block and check whether they have different distributions.
+ std::chrono::high_resolution_clock::time_point gatherStart = std::chrono::high_resolution_clock::now();
for (auto const& state : this->blocks[blockId]) {
// Now construct the distribution of this state wrt. to the current partitioning.
storm::storage::Distribution<ValueType> distribution;
@@ -110,6 +154,12 @@ namespace storm {
distribution.addProbability(static_cast<storm::storage::sparse::state_type>(stateToBlockMapping[successorEntry.getColumn()]), successorEntry.getValue());
}
+ // If we are requested to compute a weak bisimulation, we need to scale the distribution with the
+ // self-loop probability.
+ if (weakBisimulation) {
+ distribution.scale(blockId);
+ }
+
// If the distribution already exists, we simply add the state. Otherwise, we open a new block.
auto distributionIterator = distributionToNewBlocks.find(distribution);
if (distributionIterator != distributionToNewBlocks.end()) {
@@ -119,10 +169,13 @@ namespace storm {
}
}
+ std::chrono::high_resolution_clock::duration gatherTime = std::chrono::high_resolution_clock::now() - gatherStart;
+ std::cout << "time to iterate over all states was " << std::chrono::duration_cast<std::chrono::milliseconds>(gatherTime).count() << "ms." << std::endl;
+
// Now we are ready to split the block.
if (distributionToNewBlocks.size() == 1) {
// If there is just one behavior, we just set the distribution as the new one for this block.
- distributions[blockId] = std::move(distributionToNewBlocks.begin()->first);
+ // distributions[blockId] = std::move(distributionToNewBlocks.begin()->first);
} else {
// In this case, we need to split the block.
typename BisimulationDecomposition<ValueType>::block_type tmpBlock;
@@ -154,21 +207,32 @@ namespace storm {
std::deque<std::size_t> localRefinementQueue;
storm::storage::BitVector blocksInLocalRefinementQueue(this->size());
localRefinementQueue.push_back(blockId);
+// std::cout << "adding " << blockId << " to local ref queue " << std::endl;
+ blocksInLocalRefinementQueue.set(blockId);
for (std::size_t i = beforeNumberOfBlocks; i < this->blocks.size(); ++i) {
localRefinementQueue.push_back(i);
+ blocksInLocalRefinementQueue.set(i);
+// std::cout << "adding " << i << " to local refinement queue " << std::endl;
}
+
+ // We need to keep track of which blocks were split so we can later add all their predecessors as
+ // candidates for furter splitting.
+ storm::storage::BitVector splitBlocks(this->size());
- while (!localRefinementQueue.empty()) {
- std::size_t currentBlock = localRefinementQueue.front();
- localRefinementQueue.pop_front();
- blocksInLocalRefinementQueue.set(currentBlock, false);
-
- splitPredecessorsGraphBased(dtmc, backwardTransitions, blockId, stateToBlockMapping, distributions, blocksInLocalRefinementQueue, localRefinementQueue);
- }
+// while (!localRefinementQueue.empty()) {
+// std::size_t currentBlock = localRefinementQueue.front();
+// localRefinementQueue.pop_front();
+// blocksInLocalRefinementQueue.set(currentBlock, false);
+//
+// splitPredecessorsGraphBased(dtmc, backwardTransitions, currentBlock, stateToBlockMapping, distributions, blocksInLocalRefinementQueue, localRefinementQueue, splitBlocks);
+// }
+
+// std::cout << "split blocks: " << std::endl;
+// std::cout << splitBlocks << std::endl;
// Since we created some new blocks, we need to extend the bit vector storing the blocks in the
// refinement queue.
- blocksInRefinementQueue.resize(blocksInRefinementQueue.size() + (distributionToNewBlocks.size() - 1));
+ blocksInRefinementQueue.resize(this->blocks.size());
// Insert blocks that possibly need a refinement into the queue.
for (auto const& state : tmpBlock) {
diff --git a/src/storage/BisimulationDecomposition.h b/src/storage/BisimulationDecomposition.h
index d02d02bc1..55ed556d8 100644
--- a/src/storage/BisimulationDecomposition.h
+++ b/src/storage/BisimulationDecomposition.h
@@ -26,8 +26,8 @@ namespace storm {
private:
void computeBisimulationEquivalenceClasses(storm::models::Dtmc<ValueType> const& model, bool weak);
- std::size_t splitPredecessorsGraphBased(storm::models::Dtmc<ValueType> const& dtmc, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::size_t const& block, std::vector<std::size_t>& stateToBlockMapping, std::vector<storm::storage::Distribution<ValueType>>& distributions, storm::storage::BitVector& blocksInRefinementQueue, std::deque<std::size_t>& refinementQueue);
- std::size_t splitBlock(storm::models::Dtmc<ValueType> const& dtmc, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::size_t const& block, std::vector<std::size_t>& stateToBlockMapping, std::vector<storm::storage::Distribution<ValueType>>& distributions, storm::storage::BitVector& blocksInRefinementQueue, std::deque<std::size_t>& refinementQueue);
+ std::size_t splitPredecessorsGraphBased(storm::models::Dtmc<ValueType> const& dtmc, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::size_t const& block, std::vector<std::size_t>& stateToBlockMapping, std::vector<storm::storage::Distribution<ValueType>>& distributions, storm::storage::BitVector& blocksInRefinementQueue, std::deque<std::size_t>& refinementQueue, storm::storage::BitVector& splitBlocks);
+ std::size_t splitBlock(storm::models::Dtmc<ValueType> const& dtmc, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::size_t const& block, std::vector<std::size_t>& stateToBlockMapping, std::vector<storm::storage::Distribution<ValueType>>& distributions, storm::storage::BitVector& blocksInRefinementQueue, std::deque<std::size_t>& refinementQueue, bool weakBisimulation);
};
}
}
diff --git a/src/storage/Distribution.cpp b/src/storage/Distribution.cpp
index 55de31d51..50e93f567 100644
--- a/src/storage/Distribution.cpp
+++ b/src/storage/Distribution.cpp
@@ -65,6 +65,19 @@ namespace storm {
return this->distribution.end();
}
+ template<typename ValueType>
+ void Distribution<ValueType>::scale(storm::storage::sparse::state_type const& state) {
+ auto probabilityIterator = this->distribution.find(state);
+ if (probabilityIterator != this->distribution.end()) {
+ ValueType scaleValue = 1 / probabilityIterator->second;
+ this->distribution.erase(probabilityIterator);
+
+ for (auto& entry : this->distribution) {
+ entry.second *= scaleValue;
+ }
+ }
+ }
+
template<typename ValueType>
std::size_t Distribution<ValueType>::getHash() const {
return this->hash ^ (this->distribution.size() << 8);
diff --git a/src/storage/Distribution.h b/src/storage/Distribution.h
index a888a88ed..010cf43bc 100644
--- a/src/storage/Distribution.h
+++ b/src/storage/Distribution.h
@@ -66,6 +66,15 @@ namespace storm {
*/
const_iterator end() const;
+ /*!
+ * Scales the distribution by multiplying all the probabilities with 1/p where p is the probability of moving
+ * to the given state and sets the probability of moving to the given state to zero. If the probability is
+ * already zero, this operation has no effect.
+ *
+ * @param state The state whose associated probability is used to scale the distribution.
+ */
+ void scale(storm::storage::sparse::state_type const& state);
+
/*!
* Retrieves the hash value of the distribution.
*
From a18d5e963180e880f74b84592f82231e6789d5b5 Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@rwth-aachen.de>
Date: Wed, 8 Oct 2014 18:12:34 +0200
Subject: [PATCH 05/14] missing headers due to removal of other headers in
another file
Former-commit-id: cca55a7a284bacccfeca1165fd67e8a10b2d521e
---
src/utility/cli.h | 2 ++
1 file changed, 2 insertions(+)
diff --git a/src/utility/cli.h b/src/utility/cli.h
index ebd8a9bc7..ac962d873 100644
--- a/src/utility/cli.h
+++ b/src/utility/cli.h
@@ -8,6 +8,7 @@
#include <sstream>
#include <memory>
+#include "storm-config.h"
// Includes for the linked libraries and versions header.
#ifdef STORM_HAVE_INTELTBB
# include "tbb/tbb_stddef.h"
@@ -30,6 +31,7 @@ log4cplus::Logger logger;
// Headers that provide auxiliary functionality.
#include "src/utility/storm-version.h"
+
#include "src/utility/OsDetection.h"
#include "src/settings/SettingsManager.h"
From 828e46ce8770198e543993af4523cdbf3567a722 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Thu, 9 Oct 2014 16:54:59 +0200
Subject: [PATCH 06/14] Started working on a more clever way to do bisimulation
minimization.
Former-commit-id: a2939ececb4df0a09f901d7b3478289d1e648ef4
---
src/models/AtomicPropositionsLabeling.h | 13 ++
src/storage/BisimulationDecomposition.cpp | 2 +-
src/storage/BisimulationDecomposition2.cpp | 242 +++++++++++++++++++++
src/storage/BisimulationDecomposition2.h | 93 ++++++++
src/utility/cli.h | 2 +
5 files changed, 351 insertions(+), 1 deletion(-)
create mode 100644 src/storage/BisimulationDecomposition2.cpp
create mode 100644 src/storage/BisimulationDecomposition2.h
diff --git a/src/models/AtomicPropositionsLabeling.h b/src/models/AtomicPropositionsLabeling.h
index b7b067090..6281c5d6b 100644
--- a/src/models/AtomicPropositionsLabeling.h
+++ b/src/models/AtomicPropositionsLabeling.h
@@ -217,6 +217,19 @@ public:
return this->singleLabelings[apIndexPair->second].get(state);
}
+ /*!
+ * Retrieves the set of atomic propositions of the model.
+ *
+ * @return The set of atomic propositions of the model.
+ */
+ std::set<std::string> getAtomicPropositions() const {
+ std::set<std::string> result;
+ for (auto const& labeling : this->nameToLabelingMap) {
+ result.insert(labeling.first);
+ }
+ return result;
+ }
+
/*!
* Returns the number of atomic propositions managed by this object (set in the initialization).
*
diff --git a/src/storage/BisimulationDecomposition.cpp b/src/storage/BisimulationDecomposition.cpp
index 1c107d1a8..d55bd2f0d 100644
--- a/src/storage/BisimulationDecomposition.cpp
+++ b/src/storage/BisimulationDecomposition.cpp
@@ -16,7 +16,7 @@ namespace storm {
std::chrono::high_resolution_clock::time_point totalStart = std::chrono::high_resolution_clock::now();
// We start by computing the initial partition. In particular, we also keep a mapping of states to their blocks.
std::vector<std::size_t> stateToBlockMapping(dtmc.getNumberOfStates());
- storm::storage::BitVector labeledStates = dtmc.getLabeledStates("observe0Greater1");
+ storm::storage::BitVector labeledStates = dtmc.getLabeledStates("one");
this->blocks.emplace_back(labeledStates.begin(), labeledStates.end());
std::for_each(labeledStates.begin(), labeledStates.end(), [&] (storm::storage::sparse::state_type const& state) { stateToBlockMapping[state] = 0; } );
labeledStates.complement();
diff --git a/src/storage/BisimulationDecomposition2.cpp b/src/storage/BisimulationDecomposition2.cpp
new file mode 100644
index 000000000..2722d0f9d
--- /dev/null
+++ b/src/storage/BisimulationDecomposition2.cpp
@@ -0,0 +1,242 @@
+#include "src/storage/BisimulationDecomposition2.h"
+
+#include <algorithm>
+#include <unordered_map>
+#include <chrono>
+
+namespace storm {
+ namespace storage {
+
+ template<typename ValueType>
+ BisimulationDecomposition2<ValueType>::Block::Block(storm::storage::sparse::state_type begin, storm::storage::sparse::state_type end, Block* prev, Block* next) : begin(begin), end(end), prev(prev), next(next), numberOfStates(end - begin) {
+ // Intentionally left empty.
+ }
+
+ template<typename ValueType>
+ BisimulationDecomposition2<ValueType>::Partition::Partition(std::size_t numberOfStates) : stateToBlockMapping(numberOfStates), states(numberOfStates), positions(numberOfStates), values(numberOfStates) {
+ this->blocks.back().itToSelf = blocks.emplace(this->blocks.end(), 0, numberOfStates, nullptr);
+ for (storm::storage::sparse::state_type state = 0; state < numberOfStates; ++state) {
+ states[state] = state;
+ positions[state] = state;
+ stateToBlockMapping[state] = &blocks.back();
+ }
+ }
+
+ template<typename ValueType>
+ void BisimulationDecomposition2<ValueType>::Partition::splitLabel(storm::storage::BitVector const& statesWithLabel) {
+ for (auto blockIterator = this->blocks.begin(), ite = this->blocks.end(); blockIterator != ite; ) { // The update of the loop was intentionally moved to the bottom of the loop.
+ Block& block = *blockIterator;
+
+ // Sort the range of the block such that all states that have the label are moved to the front.
+ std::sort(this->states.begin() + block.begin, this->states.begin() + block.end, [&statesWithLabel] (storm::storage::sparse::state_type const& a, storm::storage::sparse::state_type const& b) { return statesWithLabel.get(a) && !statesWithLabel.get(b); } );
+
+ // Update the positions vector.
+ storm::storage::sparse::state_type position = block.begin;
+ for (auto stateIt = this->states.begin() + block.begin, stateIte = this->states.begin() + block.end; stateIt != stateIte; ++stateIt, ++position) {
+ this->positions[*stateIt] = position;
+ }
+
+ // Now we can find the first position in the block that does not have the label and create new blocks.
+ std::vector<storm::storage::sparse::state_type>::iterator it = std::find_if(this->states.begin() + block.begin, this->states.begin() + block.end, [&] (storm::storage::sparse::state_type const& a) { return !statesWithLabel.get(a); });
+
+ // If not all the states agreed on the validity of the label, we need to split the block.
+ if (it != this->states.begin() + block.begin && it != this->states.begin() + block.end) {
+ auto cutPoint = std::distance(this->states.begin(), it);
+
+ ++blockIterator;
+ auto newBlockIterator = this->blocks.emplace(blockIterator, cutPoint, block.end, &(*blockIterator), block.next);
+
+ // Make the old block end at the cut position and insert a new block after it.
+ block.end = cutPoint;
+ block.next = &(*newBlockIterator);
+ block.numberOfStates = block.end - block.begin;
+ } else {
+ // Otherwise, we simply proceed to the next block.
+ ++blockIterator;
+ }
+ }
+ }
+
+ template<typename ValueType>
+ void BisimulationDecomposition2<ValueType>::Partition::print() const {
+ for (auto const& block : this->blocks) {
+ std::cout << "begin: " << block.begin << " and end: " << block.end << " (number of states: " << block.numberOfStates << ")" << std::endl;
+ std::cout << "states:" << std::endl;
+ for (storm::storage::sparse::state_type index = block.begin; index < block.end; ++index) {
+ std::cout << this->states[index] << " " << std::endl;
+ }
+ }
+ }
+
+ template<typename ValueType>
+ std::size_t BisimulationDecomposition2<ValueType>::Partition::size() const {
+ return this->blocks.size();
+ }
+
+ template<typename ValueType>
+ BisimulationDecomposition2<ValueType>::BisimulationDecomposition2(storm::models::Dtmc<ValueType> const& dtmc, bool weak) {
+ computeBisimulationEquivalenceClasses(dtmc, weak);
+ }
+
+ template<typename ValueType>
+ void BisimulationDecomposition2<ValueType>::computeBisimulationEquivalenceClasses(storm::models::Dtmc<ValueType> const& dtmc, bool weak) {
+ std::chrono::high_resolution_clock::time_point totalStart = std::chrono::high_resolution_clock::now();
+
+ // We start by computing the initial partition.
+ Partition partition(dtmc.getNumberOfStates());
+ partition.print();
+ for (auto const& label : dtmc.getStateLabeling().getAtomicPropositions()) {
+ if (label == "init") {
+ continue;
+ }
+ partition.splitLabel(dtmc.getLabeledStates(label));
+ }
+
+ std::cout << "initial partition:" << std::endl;
+ partition.print();
+
+ // Initially, all blocks are potential splitter, so we insert them in the splitterQueue.
+ std::deque<Block*> splitterQueue;
+ std::for_each(partition.blocks.begin(), partition.blocks.end(), [&] (Block& a) { splitterQueue.push_back(&a); });
+
+ storm::storage::SparseMatrix<ValueType> backwardTransitions = dtmc.getBackwardTransitions();
+
+ // Then perform the actual splitting until there are no more splitters.
+ while (!splitterQueue.empty()) {
+ splitPartition(backwardTransitions, *splitterQueue.front(), partition, splitterQueue);
+ splitterQueue.pop_front();
+ }
+
+ std::chrono::high_resolution_clock::duration totalTime = std::chrono::high_resolution_clock::now() - totalStart;
+ std::cout << "Bisimulation took " << std::chrono::duration_cast<std::chrono::milliseconds>(totalTime).count() << "ms." << std::endl;
+ }
+
+ template<typename ValueType>
+ std::size_t BisimulationDecomposition2<ValueType>::splitPartition(storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Block const& splitter, Partition& partition, std::deque<Block*>& splitterQueue) {
+
+ std::list<Block*> predecessorBlocks;
+
+ // Iterate over all states of the splitter and check its predecessors.
+ for (auto stateIterator = partition.states.begin() + splitter.begin, stateIte = partition.states.begin() + splitter.end; stateIterator != stateIte; ++stateIterator) {
+ storm::storage::sparse::state_type& state = *stateIterator;
+
+ for (auto const& predecessorEntry : backwardTransitions.getRow(state)) {
+ storm::storage::sparse::state_type predecessor = predecessorEntry.getColumn();
+ Block* predecessorBlock = partition.stateToBlockMapping[predecessor];
+ storm::storage::sparse::state_type predecessorPosition = partition.positions[predecessor];
+
+ // If we have not seen this predecessor before, we move it to a part near the beginning of the block.
+ if (predecessorPosition < predecessorBlock->begin) {
+ std::swap(partition.states[predecessorPosition], partition.states[predecessorBlock->begin]);
+ std::swap(partition.positions[predecessor], partition.positions[predecessorBlock->begin]);
+ ++predecessorBlock->begin;
+ partition.values[predecessor] = predecessorEntry.getValue();
+ } else {
+ // Otherwise, we just need to update the probability for this predecessor.
+ partition.values[predecessor] += predecessorEntry.getValue();
+ }
+
+ if (!predecessorBlock->isMarked) {
+ predecessorBlocks.emplace_back(predecessorBlock);
+ predecessorBlock->isMarked = true;
+ }
+ }
+ }
+
+ // Now, we can iterate over the predecessor blocks and see whether we have to create a new block for
+ // predecessors of the splitter.
+ for (auto block : predecessorBlocks) {
+ // If we have moved the begin of the block to somewhere in the middle of the block, we need to split it.
+ if (block->begin != block->end) {
+
+
+ storm::storage::sparse::state_type tmpBegin = block->begin;
+ storm::storage::sparse::state_type tmpEnd = block->end;
+
+
+ }
+
+
+ }
+
+ return 0;
+ }
+
+// template<typename ValueType>
+// std::size_t BisimulationDecomposition2<ValueType>::splitPartition(storm::models::Dtmc<ValueType> const& dtmc, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::size_t const& blockId, std::vector<std::size_t>& stateToBlockMapping, storm::storage::BitVector& blocksInSplitterQueue, std::deque<std::size_t>& splitterQueue, bool weakBisimulation) {
+// std::chrono::high_resolution_clock::time_point totalStart = std::chrono::high_resolution_clock::now();
+// std::unordered_map<storm::storage::Distribution<ValueType>, typename BisimulationDecomposition2<ValueType>::block_type> distributionToNewBlocks;
+//
+// // Traverse all states of the block and check whether they have different distributions.
+// std::chrono::high_resolution_clock::time_point gatherStart = std::chrono::high_resolution_clock::now();
+// for (auto const& state : this->blocks[blockId]) {
+// // Now construct the distribution of this state wrt. to the current partitioning.
+// storm::storage::Distribution<ValueType> distribution;
+// for (auto const& successorEntry : dtmc.getTransitionMatrix().getRow(state)) {
+// distribution.addProbability(static_cast<storm::storage::sparse::state_type>(stateToBlockMapping[successorEntry.getColumn()]), successorEntry.getValue());
+// }
+//
+// // If we are requested to compute a weak bisimulation, we need to scale the distribution with the
+// // self-loop probability.
+// if (weakBisimulation) {
+// distribution.scale(blockId);
+// }
+//
+// // If the distribution already exists, we simply add the state. Otherwise, we open a new block.
+// auto distributionIterator = distributionToNewBlocks.find(distribution);
+// if (distributionIterator != distributionToNewBlocks.end()) {
+// distributionIterator->second.insert(state);
+// } else {
+// distributionToNewBlocks[distribution].insert(state);
+// }
+// }
+//
+// std::chrono::high_resolution_clock::duration gatherTime = std::chrono::high_resolution_clock::now() - gatherStart;
+// std::cout << "time to iterate over all states was " << std::chrono::duration_cast<std::chrono::milliseconds>(gatherTime).count() << "ms." << std::endl;
+//
+// // Now we are ready to split the block.
+// if (distributionToNewBlocks.size() == 1) {
+// // If there is just one behavior, we just set the distribution as the new one for this block.
+// // distributions[blockId] = std::move(distributionToNewBlocks.begin()->first);
+// } else {
+// // In this case, we need to split the block.
+// typename BisimulationDecomposition2<ValueType>::block_type tmpBlock;
+//
+// auto distributionIterator = distributionToNewBlocks.begin();
+// tmpBlock = std::move(distributionIterator->second);
+// std::swap(this->blocks[blockId], tmpBlock);
+// ++distributionIterator;
+//
+// // Remember the number of blocks prior to splitting for later use.
+// std::size_t beforeNumberOfBlocks = this->blocks.size();
+//
+// for (; distributionIterator != distributionToNewBlocks.end(); ++distributionIterator) {
+// // In this case, we need to move the newly created block to the end of the list of actual blocks.
+// this->blocks.emplace_back(std::move(distributionIterator->second));
+//
+// // Update the mapping of states to their blocks.
+// std::size_t newBlockId = this->blocks.size() - 1;
+// for (auto const& state : this->blocks.back()) {
+// stateToBlockMapping[state] = newBlockId;
+// }
+// }
+//
+// // Insert blocks that possibly need a refinement into the queue.
+// for (auto const& state : tmpBlock) {
+// for (auto const& predecessor : backwardTransitions.getRow(state)) {
+// if (!blocksInRefinementQueue.get(stateToBlockMapping[predecessor.getColumn()])) {
+// blocksInRefinementQueue.set(stateToBlockMapping[predecessor.getColumn()]);
+// refinementQueue.push_back(stateToBlockMapping[predecessor.getColumn()]);
+// }
+// }
+// }
+// }
+//
+// std::chrono::high_resolution_clock::duration totalTime = std::chrono::high_resolution_clock::now() - totalStart;
+// std::cout << "refinement of block " << blockId << " took " << std::chrono::duration_cast<std::chrono::milliseconds>(totalTime).count() << "ms." << std::endl;
+// return distributionToNewBlocks.size();
+// }
+
+ template class BisimulationDecomposition2<double>;
+ }
+}
\ No newline at end of file
diff --git a/src/storage/BisimulationDecomposition2.h b/src/storage/BisimulationDecomposition2.h
new file mode 100644
index 000000000..bf5fc5990
--- /dev/null
+++ b/src/storage/BisimulationDecomposition2.h
@@ -0,0 +1,93 @@
+#ifndef STORM_STORAGE_BISIMULATIONDECOMPOSITION2_H_
+#define STORM_STORAGE_BISIMULATIONDECOMPOSITION2_H_
+
+#include <queue>
+#include <deque>
+
+#include "src/storage/sparse/StateType.h"
+#include "src/storage/Decomposition.h"
+#include "src/models/Dtmc.h"
+#include "src/storage/Distribution.h"
+
+namespace storm {
+ namespace storage {
+
+ /*!
+ * This class represents the decomposition model into its bisimulation quotient.
+ */
+ template <typename ValueType>
+ class BisimulationDecomposition2 : public Decomposition<StateBlock> {
+ public:
+ BisimulationDecomposition2() = default;
+
+ /*!
+ * Decomposes the given DTMC into equivalence classes under weak or strong bisimulation.
+ */
+ BisimulationDecomposition2(storm::models::Dtmc<ValueType> const& model, bool weak = false);
+
+ private:
+ class Block {
+ public:
+ Block(storm::storage::sparse::state_type begin, storm::storage::sparse::state_type end, Block* prev, Block* next);
+
+ // An iterator to itself. This is needed to conveniently insert elements in the overall list of blocks
+ // kept by the partition.
+ typename std::list<Block>::iterator itToSelf;
+
+ // The begin and end indices of the block in terms of the state vector of the partition.
+ storm::storage::sparse::state_type begin;
+ storm::storage::sparse::state_type end;
+
+ // The block before and after the current one.
+ Block* prev;
+ Block* next;
+
+ // The number of states in the block.
+ std::size_t numberOfStates;
+
+ // A field that can be used for marking the block.
+ bool isMarked;
+ };
+
+ class Partition {
+ public:
+ /*!
+ * Creates a partition with one block consisting of all the states.
+ */
+ Partition(std::size_t numberOfStates);
+
+ /*!
+ * Splits all blocks of the partition such that afterwards all blocks contain only states with the label
+ * or no labeled state at all.
+ */
+ void splitLabel(storm::storage::BitVector const& statesWithLabel);
+
+ // The list of blocks in the partition.
+ std::list<Block> blocks;
+
+ // A mapping of states to their blocks.
+ std::vector<Block*> stateToBlockMapping;
+
+ // A vector containing all the states. It is ordered in a special way such that the blocks only need to
+ // define their start/end indices.
+ std::vector<storm::storage::sparse::state_type> states;
+
+ // This vector keeps track of the position of each state in the state vector.
+ std::vector<storm::storage::sparse::state_type> positions;
+
+ // This vector stores the probabilities of going to the current splitter.
+ std::vector<ValueType> values;
+
+ std::size_t size() const;
+
+ void print() const;
+ };
+
+ void computeBisimulationEquivalenceClasses(storm::models::Dtmc<ValueType> const& model, bool weak);
+
+ std::size_t splitPartition(storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Block const& splitter, Partition& partition, std::deque<Block*>& splitterQueue);
+ };
+ }
+}
+
+#endif /* STORM_STORAGE_BISIMULATIONDECOMPOSITION2_H_ */
\ No newline at end of file
diff --git a/src/utility/cli.h b/src/utility/cli.h
index 0a416e5c3..6996736a4 100644
--- a/src/utility/cli.h
+++ b/src/utility/cli.h
@@ -45,6 +45,7 @@ log4cplus::Logger logger;
// Headers for model processing.
#include "src/storage/BisimulationDecomposition.h"
+#include "src/storage/BisimulationDecomposition2.h"
// Headers for counterexample generation.
#include "src/counterexamples/MILPMinimalLabelSetGenerator.h"
@@ -261,6 +262,7 @@ namespace storm {
STORM_LOG_THROW(result->getType() == storm::models::DTMC, storm::exceptions::InvalidSettingsException, "Bisimulation minimization is currently only compatible with DTMCs.");
std::shared_ptr<storm::models::Dtmc<double>> dtmc = result->template as<storm::models::Dtmc<double>>();
storm::storage::BisimulationDecomposition<double> bisimulationDecomposition(*dtmc);
+ storm::storage::BisimulationDecomposition2<double> bisimulationDecomposition2(*dtmc);
}
return result;
From 43bc81a5fb96bb6a5d34a15f0ab025df16a44982 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Thu, 9 Oct 2014 23:57:21 +0200
Subject: [PATCH 07/14] New bisimulatin minimization works on tiny example.
Former-commit-id: 2d62985977d8c8c7c768c0d21366167c0735436a
---
src/storage/BisimulationDecomposition2.cpp | 172 +++++++++++++++++++--
src/storage/BisimulationDecomposition2.h | 9 +-
2 files changed, 166 insertions(+), 15 deletions(-)
diff --git a/src/storage/BisimulationDecomposition2.cpp b/src/storage/BisimulationDecomposition2.cpp
index 2722d0f9d..ab70ee1c8 100644
--- a/src/storage/BisimulationDecomposition2.cpp
+++ b/src/storage/BisimulationDecomposition2.cpp
@@ -8,13 +8,24 @@ namespace storm {
namespace storage {
template<typename ValueType>
- BisimulationDecomposition2<ValueType>::Block::Block(storm::storage::sparse::state_type begin, storm::storage::sparse::state_type end, Block* prev, Block* next) : begin(begin), end(end), prev(prev), next(next), numberOfStates(end - begin) {
+ BisimulationDecomposition2<ValueType>::Block::Block(storm::storage::sparse::state_type begin, storm::storage::sparse::state_type end, Block* prev, Block* next) : begin(begin), end(end), prev(prev), next(next), numberOfStates(end - begin), isMarked(false) {
// Intentionally left empty.
}
+ template<typename ValueType>
+ void BisimulationDecomposition2<ValueType>::Block::print(Partition const& partition) const {
+ std::cout << "this " << this << std::endl;
+ std::cout << "begin: " << this->begin << " and end: " << this->end << " (number of states: " << this->numberOfStates << ")" << std::endl;
+ std::cout << "next: " << this->next << " and prev " << this->prev << std::endl;
+ std::cout << "states:" << std::endl;
+ for (storm::storage::sparse::state_type index = this->begin; index < this->end; ++index) {
+ std::cout << partition.states[index] << " " << std::endl;
+ }
+ }
+
template<typename ValueType>
BisimulationDecomposition2<ValueType>::Partition::Partition(std::size_t numberOfStates) : stateToBlockMapping(numberOfStates), states(numberOfStates), positions(numberOfStates), values(numberOfStates) {
- this->blocks.back().itToSelf = blocks.emplace(this->blocks.end(), 0, numberOfStates, nullptr);
+ this->blocks.back().itToSelf = blocks.emplace(this->blocks.end(), 0, numberOfStates, nullptr, nullptr);
for (storm::storage::sparse::state_type state = 0; state < numberOfStates; ++state) {
states[state] = state;
positions[state] = state;
@@ -44,12 +55,18 @@ namespace storm {
auto cutPoint = std::distance(this->states.begin(), it);
++blockIterator;
- auto newBlockIterator = this->blocks.emplace(blockIterator, cutPoint, block.end, &(*blockIterator), block.next);
+ auto newBlockIterator = this->blocks.emplace(blockIterator, cutPoint, block.end, &block, block.next);
+ newBlockIterator->itToSelf = newBlockIterator;
// Make the old block end at the cut position and insert a new block after it.
block.end = cutPoint;
block.next = &(*newBlockIterator);
block.numberOfStates = block.end - block.begin;
+
+ // Update the block mapping for all states that we just removed from the block.
+ for (auto it = this->states.begin() + newBlockIterator->begin, ite = this->states.begin() + newBlockIterator->end; it != ite; ++it) {
+ stateToBlockMapping[*it] = &(*newBlockIterator);
+ }
} else {
// Otherwise, we simply proceed to the next block.
++blockIterator;
@@ -60,12 +77,21 @@ namespace storm {
template<typename ValueType>
void BisimulationDecomposition2<ValueType>::Partition::print() const {
for (auto const& block : this->blocks) {
- std::cout << "begin: " << block.begin << " and end: " << block.end << " (number of states: " << block.numberOfStates << ")" << std::endl;
- std::cout << "states:" << std::endl;
- for (storm::storage::sparse::state_type index = block.begin; index < block.end; ++index) {
- std::cout << this->states[index] << " " << std::endl;
- }
+ block.print(*this);
}
+ std::cout << "states" << std::endl;
+ for (auto const& state : states) {
+ std::cout << state << " ";
+ }
+ std::cout << std::endl << "positions: " << std::endl;
+ for (auto const& index : positions) {
+ std::cout << index << " ";
+ }
+ std::cout << std::endl << "state to block mapping: " << std::endl;
+ for (auto const& block : stateToBlockMapping) {
+ std::cout << block << " ";
+ }
+ std::cout << std::endl;
}
template<typename ValueType>
@@ -105,6 +131,10 @@ namespace storm {
while (!splitterQueue.empty()) {
splitPartition(backwardTransitions, *splitterQueue.front(), partition, splitterQueue);
splitterQueue.pop_front();
+
+ std::cout << "####### updated partition ##############" << std::endl;
+ partition.print();
+ std::cout << "####### end of updated partition #######" << std::endl;
}
std::chrono::high_resolution_clock::duration totalTime = std::chrono::high_resolution_clock::now() - totalStart;
@@ -112,8 +142,63 @@ namespace storm {
}
template<typename ValueType>
- std::size_t BisimulationDecomposition2<ValueType>::splitPartition(storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Block const& splitter, Partition& partition, std::deque<Block*>& splitterQueue) {
+ std::size_t BisimulationDecomposition2<ValueType>::splitBlockProbabilities(Block* block, Partition& partition, std::deque<Block*>& splitterQueue) {
+ Block& currentBlock = *block;
+
+ // Sort the states in the block based on their probabilities.
+ std::sort(partition.states.begin() + currentBlock.begin, partition.states.begin() + currentBlock.end, [&partition] (storm::storage::sparse::state_type const& a, storm::storage::sparse::state_type const& b) { return partition.values[a] < partition.values[b]; } );
+
+ // FIXME: This can probably be done more efficiently.
+ std::sort(partition.values.begin() + currentBlock.begin, partition.values.begin() + currentBlock.end);
+
+ // Update the positions vector.
+ storm::storage::sparse::state_type position = currentBlock.begin;
+ for (auto stateIt = partition.states.begin() + currentBlock.begin, stateIte = partition.states.begin() + currentBlock.end; stateIt != stateIte; ++stateIt, ++position) {
+ partition.positions[*stateIt] = position;
+ }
+
+ // Finally, we need to scan the ranges of states that agree on the probability.
+ storm::storage::sparse::state_type beginIndex = currentBlock.begin;
+ storm::storage::sparse::state_type currentIndex = beginIndex;
+ storm::storage::sparse::state_type endIndex = currentBlock.end;
+
+ Block* prevBlock = block->prev;
+
+ std::list<Block*> createdBlocks;
+ std::cout << currentIndex << " < " << endIndex << std::endl;
+ while (currentIndex < endIndex) {
+ ValueType& currentValue = *(partition.values.begin() + currentIndex);
+
+ ++currentIndex;
+ ValueType* nextValuePtr = ¤tValue;
+ while (currentIndex < endIndex && std::abs(currentValue - *nextValuePtr) < 1e-6) {
+ ++currentIndex;
+ ++nextValuePtr;
+ }
+
+ // Create a new block from the states that agree on the values.
+ typename std::list<Block>::iterator newBlockIterator = partition.blocks.emplace(currentBlock.itToSelf, beginIndex, endIndex, prevBlock, currentBlock.next);
+ newBlockIterator->itToSelf = newBlockIterator;
+ if (prevBlock != nullptr) {
+ prevBlock->next = &(*newBlockIterator);
+ }
+ prevBlock = &(*newBlockIterator);
+ if (prevBlock->numberOfStates > 1) {
+ createdBlocks.emplace_back(prevBlock);
+ }
+ }
+
+ for (auto block : createdBlocks) {
+ splitterQueue.push_back(block);
+ }
+ return createdBlocks.size();
+ }
+
+ template<typename ValueType>
+ std::size_t BisimulationDecomposition2<ValueType>::splitPartition(storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Block const& splitter, Partition& partition, std::deque<Block*>& splitterQueue) {
+ std::cout << "getting block " << &splitter << " as splitter" << std::endl;
+ splitter.print(partition);
std::list<Block*> predecessorBlocks;
// Iterate over all states of the splitter and check its predecessors.
@@ -122,17 +207,36 @@ namespace storm {
for (auto const& predecessorEntry : backwardTransitions.getRow(state)) {
storm::storage::sparse::state_type predecessor = predecessorEntry.getColumn();
+ std::cout << "found pred " << predecessor << std::endl;
Block* predecessorBlock = partition.stateToBlockMapping[predecessor];
+ std::cout << "predecessor block " << std::endl;
+ predecessorBlock->print(partition);
+
+ // If the predecessor block has just one state, there is no point in splitting it.
+ if (predecessorBlock->numberOfStates <= 1) {
+ std::cout << "continuing" << std::endl;
+ continue;
+ }
+
storm::storage::sparse::state_type predecessorPosition = partition.positions[predecessor];
// If we have not seen this predecessor before, we move it to a part near the beginning of the block.
- if (predecessorPosition < predecessorBlock->begin) {
+ std::cout << "predecessor position: " << predecessorPosition << " and begin " << predecessorBlock->begin << std::endl;
+ if (predecessorPosition >= predecessorBlock->begin) {
std::swap(partition.states[predecessorPosition], partition.states[predecessorBlock->begin]);
- std::swap(partition.positions[predecessor], partition.positions[predecessorBlock->begin]);
+ std::cout << "swapping positions of " << predecessor << " and " << partition.states[predecessorPosition] << std::endl;
+ storm::storage::sparse::state_type tmp = partition.positions[partition.states[predecessorPosition]];
+ partition.positions[partition.states[predecessorPosition]] = partition.positions[predecessor];
+ partition.positions[predecessor] = tmp;
+
+// std::swap(partition.positions[predecessor], partition.positions[predecessorBlock->begin]);
+
++predecessorBlock->begin;
+ std::cout << "incrementing begin... " << std::endl;
partition.values[predecessor] = predecessorEntry.getValue();
} else {
// Otherwise, we just need to update the probability for this predecessor.
+ std::cout << "updating probability" << std::endl;
partition.values[predecessor] += predecessorEntry.getValue();
}
@@ -143,20 +247,60 @@ namespace storm {
}
}
+ std::list<Block*> blocksToSplit;
+
// Now, we can iterate over the predecessor blocks and see whether we have to create a new block for
// predecessors of the splitter.
for (auto block : predecessorBlocks) {
+ block->isMarked = false;
+
// If we have moved the begin of the block to somewhere in the middle of the block, we need to split it.
if (block->begin != block->end) {
-
-
+ std::cout << "moved begin to " << block->begin << " and end to " << block->end << std::endl;
storm::storage::sparse::state_type tmpBegin = block->begin;
storm::storage::sparse::state_type tmpEnd = block->end;
+ block->begin = block->prev != nullptr ? block->prev->end : 0;
+ std::cout << "begin: " << block->begin << " and not-null? " << (block->prev != nullptr) << ": " << block->prev << std::endl;
+ block->end = tmpBegin;
+ block->numberOfStates = block->end - block->begin;
+ // Create a new block that holds all states that do not have a successor in the current splitter.
+ typename std::list<Block>::iterator it = partition.blocks.emplace(block->next != nullptr ? block->next->itToSelf : partition.blocks.end(), tmpBegin, tmpEnd, block, block->next);
+ Block* newBlock = &(*it);
+ newBlock->itToSelf = it;
+ if (block->next != nullptr) {
+ block->next->prev = newBlock;
+ }
+ block->next = newBlock;
+
+ std::cout << "created new block " << std::endl;
+ newBlock->print(partition);
+
+ // Update the block mapping in the partition.
+ for (auto it = partition.states.begin() + newBlock->begin, ite = partition.states.begin() + newBlock->end; it != ite; ++it) {
+ partition.stateToBlockMapping[*it] = newBlock;
+ }
+
+ // Mark the half of the block that can be further refined using the probability information.
+ blocksToSplit.emplace_back(block);
+ block->print(partition);
+
+ splitterQueue.push_back(newBlock);
+ } else {
+ std::cout << "found block to split" << std::endl;
+ blocksToSplit.emplace_back(block);
+ }
+ }
+
+ // Finally, we walk through the blocks that have a transition to the splitter and split them using
+ // probabilistic information.
+ for (auto block : blocksToSplit) {
+ if (block->numberOfStates <= 1) {
+ continue;
}
-
+ splitBlockProbabilities(block, partition, splitterQueue);
}
return 0;
diff --git a/src/storage/BisimulationDecomposition2.h b/src/storage/BisimulationDecomposition2.h
index bf5fc5990..121f5487d 100644
--- a/src/storage/BisimulationDecomposition2.h
+++ b/src/storage/BisimulationDecomposition2.h
@@ -26,13 +26,18 @@ namespace storm {
BisimulationDecomposition2(storm::models::Dtmc<ValueType> const& model, bool weak = false);
private:
+ class Partition;
+
class Block {
public:
Block(storm::storage::sparse::state_type begin, storm::storage::sparse::state_type end, Block* prev, Block* next);
+ // Prints the block.
+ void print(Partition const& partition) const;
+
// An iterator to itself. This is needed to conveniently insert elements in the overall list of blocks
// kept by the partition.
- typename std::list<Block>::iterator itToSelf;
+ typename std::list<Block>::const_iterator itToSelf;
// The begin and end indices of the block in terms of the state vector of the partition.
storm::storage::sparse::state_type begin;
@@ -86,6 +91,8 @@ namespace storm {
void computeBisimulationEquivalenceClasses(storm::models::Dtmc<ValueType> const& model, bool weak);
std::size_t splitPartition(storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Block const& splitter, Partition& partition, std::deque<Block*>& splitterQueue);
+
+ std::size_t splitBlockProbabilities(Block* block, Partition& partition, std::deque<Block*>& splitterQueue);
};
}
}
From 8c64a1911cf67f53ae80a1a62a0933e701c6b149 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Fri, 10 Oct 2014 14:24:46 +0200
Subject: [PATCH 08/14] Still bugs in bisimulation minimization.
Former-commit-id: b0a340f26026a20807f13c373ea3957a52386474
---
src/storage/BisimulationDecomposition.cpp | 4 +-
src/storage/BisimulationDecomposition2.cpp | 155 +++++++++++++++++----
src/storage/BisimulationDecomposition2.h | 6 +
src/utility/cli.h | 2 +-
4 files changed, 136 insertions(+), 31 deletions(-)
diff --git a/src/storage/BisimulationDecomposition.cpp b/src/storage/BisimulationDecomposition.cpp
index d55bd2f0d..342914601 100644
--- a/src/storage/BisimulationDecomposition.cpp
+++ b/src/storage/BisimulationDecomposition.cpp
@@ -16,7 +16,7 @@ namespace storm {
std::chrono::high_resolution_clock::time_point totalStart = std::chrono::high_resolution_clock::now();
// We start by computing the initial partition. In particular, we also keep a mapping of states to their blocks.
std::vector<std::size_t> stateToBlockMapping(dtmc.getNumberOfStates());
- storm::storage::BitVector labeledStates = dtmc.getLabeledStates("one");
+ storm::storage::BitVector labeledStates = dtmc.getLabeledStates("observe0Greater1");
this->blocks.emplace_back(labeledStates.begin(), labeledStates.end());
std::for_each(labeledStates.begin(), labeledStates.end(), [&] (storm::storage::sparse::state_type const& state) { stateToBlockMapping[state] = 0; } );
labeledStates.complement();
@@ -51,6 +51,8 @@ namespace storm {
splitBlock(dtmc, backwardTransitions, currentBlock, stateToBlockMapping, distributions, blocksInRefinementQueue, refinementQueue, weak);
}
+ std::cout << *this << std::endl;
+
std::chrono::high_resolution_clock::duration totalTime = std::chrono::high_resolution_clock::now() - totalStart;
std::cout << "Bisimulation quotient has " << this->blocks.size() << " blocks and took " << iteration << " iterations and " << std::chrono::duration_cast<std::chrono::milliseconds>(totalTime).count() << "ms." << std::endl;
diff --git a/src/storage/BisimulationDecomposition2.cpp b/src/storage/BisimulationDecomposition2.cpp
index ab70ee1c8..35bd1c703 100644
--- a/src/storage/BisimulationDecomposition2.cpp
+++ b/src/storage/BisimulationDecomposition2.cpp
@@ -3,29 +3,45 @@
#include <algorithm>
#include <unordered_map>
#include <chrono>
+#include <iomanip>
namespace storm {
namespace storage {
+ static int globalId = 0;
+
template<typename ValueType>
- BisimulationDecomposition2<ValueType>::Block::Block(storm::storage::sparse::state_type begin, storm::storage::sparse::state_type end, Block* prev, Block* next) : begin(begin), end(end), prev(prev), next(next), numberOfStates(end - begin), isMarked(false) {
+ BisimulationDecomposition2<ValueType>::Block::Block(storm::storage::sparse::state_type begin, storm::storage::sparse::state_type end, Block* prev, Block* next) : originalBegin(begin), begin(begin), end(end), prev(prev), next(next), numberOfStates(end - begin), isMarked(false), myId(globalId++) {
// Intentionally left empty.
+ std::cout << "created new block from " << begin << " to " << end << std::endl;
}
template<typename ValueType>
void BisimulationDecomposition2<ValueType>::Block::print(Partition const& partition) const {
- std::cout << "this " << this << std::endl;
+ std::cout << "block " << this->myId << " and ptr " << this << std::endl;
std::cout << "begin: " << this->begin << " and end: " << this->end << " (number of states: " << this->numberOfStates << ")" << std::endl;
std::cout << "next: " << this->next << " and prev " << this->prev << std::endl;
std::cout << "states:" << std::endl;
for (storm::storage::sparse::state_type index = this->begin; index < this->end; ++index) {
- std::cout << partition.states[index] << " " << std::endl;
+ std::cout << partition.states[index] << " ";
+ }
+ std::cout << std::endl << "values:" << std::endl;
+ for (storm::storage::sparse::state_type index = this->begin; index < this->end; ++index) {
+ std::cout << std::setprecision(3) << partition.values[index] << " ";
}
+ std::cout << std::endl;
+ }
+
+ template<typename ValueType>
+ void BisimulationDecomposition2<ValueType>::Block::setBegin(storm::storage::sparse::state_type begin) {
+ this->begin = begin;
+ this->originalBegin = begin;
}
template<typename ValueType>
BisimulationDecomposition2<ValueType>::Partition::Partition(std::size_t numberOfStates) : stateToBlockMapping(numberOfStates), states(numberOfStates), positions(numberOfStates), values(numberOfStates) {
- this->blocks.back().itToSelf = blocks.emplace(this->blocks.end(), 0, numberOfStates, nullptr, nullptr);
+ typename std::list<Block>::iterator it = blocks.emplace(this->blocks.end(), 0, numberOfStates, nullptr, nullptr);
+ it->itToSelf = it;
for (storm::storage::sparse::state_type state = 0; state < numberOfStates; ++state) {
states[state] = state;
positions[state] = state;
@@ -79,7 +95,7 @@ namespace storm {
for (auto const& block : this->blocks) {
block.print(*this);
}
- std::cout << "states" << std::endl;
+ std::cout << "states in partition" << std::endl;
for (auto const& state : states) {
std::cout << state << " ";
}
@@ -92,10 +108,16 @@ namespace storm {
std::cout << block << " ";
}
std::cout << std::endl;
+ std::cout << "size: " << this->blocks.size() << std::endl;
}
template<typename ValueType>
std::size_t BisimulationDecomposition2<ValueType>::Partition::size() const {
+ int counter = 0;
+ for (auto const& element : blocks) {
+ ++counter;
+ }
+ std::cout << "found " << counter << " elements" << std::endl;
return this->blocks.size();
}
@@ -137,12 +159,17 @@ namespace storm {
std::cout << "####### end of updated partition #######" << std::endl;
}
+ std::cout << "computed a quotient of size " << partition.size() << std::endl;
+
std::chrono::high_resolution_clock::duration totalTime = std::chrono::high_resolution_clock::now() - totalStart;
std::cout << "Bisimulation took " << std::chrono::duration_cast<std::chrono::milliseconds>(totalTime).count() << "ms." << std::endl;
}
template<typename ValueType>
std::size_t BisimulationDecomposition2<ValueType>::splitBlockProbabilities(Block* block, Partition& partition, std::deque<Block*>& splitterQueue) {
+ std::cout << "part before split prob" << std::endl;
+ partition.print();
+
Block& currentBlock = *block;
// Sort the states in the block based on their probabilities.
@@ -162,12 +189,48 @@ namespace storm {
storm::storage::sparse::state_type currentIndex = beginIndex;
storm::storage::sparse::state_type endIndex = currentBlock.end;
- Block* prevBlock = block->prev;
+ // Now we can check whether the block needs to be split, which is the case iff the probabilities for the
+ // first and the last state are different.
+ // Note that this check requires the block to be non-empty.
+ if (std::abs(partition.values[beginIndex] - partition.values[endIndex - 1]) < 1e-6) {
+ return 1;
+ }
+
+ // Now we scan for the first state in the block that disagrees on the probability value.
+ // Note that we do not have to check currentIndex for staying within bounds, because we know the matching
+ // state is within bounds.
+ ValueType currentValue = partition.values[beginIndex];
+ ValueType* valueIterator = &(partition.values[beginIndex]) + 1;
+ ++currentIndex;
+ while (std::abs(*valueIterator - currentValue) < 1e-6) {
+ std::cout << "prob: " << *valueIterator << std::endl;
+ ++currentIndex;
+ ++valueIterator;
+ }
+
+ // Now resize the block.
+ std::cout << "resizing block from " << std::endl;
+ currentBlock.print(partition);
+ currentBlock.end = currentIndex;
+ currentBlock.numberOfStates = currentBlock.end - currentBlock.begin;
+ std::cout << " to " << std::endl;
+ currentBlock.print(partition);
+ beginIndex = currentIndex;
+ // If it is not already a splitter, we mark it as such.
+ if (!currentBlock.isMarked) {
+ currentBlock.isMarked = true;
+ }
+
+ Block* prevBlock = ¤tBlock;
+
+ // Now scan for new blocks.
std::list<Block*> createdBlocks;
std::cout << currentIndex << " < " << endIndex << std::endl;
+ typename std::list<Block>::const_iterator insertPosition = currentBlock.itToSelf;
+ ++insertPosition;
while (currentIndex < endIndex) {
- ValueType& currentValue = *(partition.values.begin() + currentIndex);
+ ValueType currentValue = *(partition.values.begin() + currentIndex);
++currentIndex;
ValueType* nextValuePtr = ¤tValue;
@@ -177,28 +240,36 @@ namespace storm {
}
// Create a new block from the states that agree on the values.
- typename std::list<Block>::iterator newBlockIterator = partition.blocks.emplace(currentBlock.itToSelf, beginIndex, endIndex, prevBlock, currentBlock.next);
+ ++insertPosition;
+ typename std::list<Block>::iterator newBlockIterator = partition.blocks.emplace(insertPosition, beginIndex, currentIndex, prevBlock, prevBlock->next);
newBlockIterator->itToSelf = newBlockIterator;
- if (prevBlock != nullptr) {
- prevBlock->next = &(*newBlockIterator);
- }
- prevBlock = &(*newBlockIterator);
+ Block* newBlock = &(*newBlockIterator);
+ prevBlock->next = newBlock;
+ prevBlock = newBlock;
if (prevBlock->numberOfStates > 1) {
createdBlocks.emplace_back(prevBlock);
}
+ beginIndex = currentIndex;
+
+ // Update the block mapping for the moved states.
+ for (auto it = partition.states.begin() + newBlock->begin, ite = partition.states.begin() + newBlock->end; it != ite; ++it) {
+ partition.stateToBlockMapping[*it] = newBlock;
+ }
}
for (auto block : createdBlocks) {
splitterQueue.push_back(block);
+ block->isMarked = true;
}
+ std::cout << "created " << createdBlocks.size() << " blocks" << std::endl;
+
return createdBlocks.size();
}
template<typename ValueType>
std::size_t BisimulationDecomposition2<ValueType>::splitPartition(storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Block const& splitter, Partition& partition, std::deque<Block*>& splitterQueue) {
- std::cout << "getting block " << &splitter << " as splitter" << std::endl;
- splitter.print(partition);
+ std::cout << "getting block " << splitter.myId << " as splitter" << std::endl;
std::list<Block*> predecessorBlocks;
// Iterate over all states of the splitter and check its predecessors.
@@ -207,14 +278,12 @@ namespace storm {
for (auto const& predecessorEntry : backwardTransitions.getRow(state)) {
storm::storage::sparse::state_type predecessor = predecessorEntry.getColumn();
- std::cout << "found pred " << predecessor << std::endl;
+ std::cout << "found predecessor " << predecessor << " of state " << *stateIterator << std::endl;
Block* predecessorBlock = partition.stateToBlockMapping[predecessor];
- std::cout << "predecessor block " << std::endl;
- predecessorBlock->print(partition);
+ std::cout << "predecessor block " << predecessorBlock->myId << std::endl;
// If the predecessor block has just one state, there is no point in splitting it.
if (predecessorBlock->numberOfStates <= 1) {
- std::cout << "continuing" << std::endl;
continue;
}
@@ -223,21 +292,34 @@ namespace storm {
// If we have not seen this predecessor before, we move it to a part near the beginning of the block.
std::cout << "predecessor position: " << predecessorPosition << " and begin " << predecessorBlock->begin << std::endl;
if (predecessorPosition >= predecessorBlock->begin) {
- std::swap(partition.states[predecessorPosition], partition.states[predecessorBlock->begin]);
- std::cout << "swapping positions of " << predecessor << " and " << partition.states[predecessorPosition] << std::endl;
- storm::storage::sparse::state_type tmp = partition.positions[partition.states[predecessorPosition]];
- partition.positions[partition.states[predecessorPosition]] = partition.positions[predecessor];
- partition.positions[predecessor] = tmp;
+
+// We cannot directly move the states at this point, otherwise we would consider states multiple
+// times while others are skipped.
+// std::swap(partition.states[predecessorPosition], partition.states[predecessorBlock->begin]);
+// std::cout << "swapping positions of " << predecessor << " and " << partition.states[predecessorPosition] << std::endl;
+
+ // Instead, we only virtually move the states by setting their positions and move them in place
+ // later.
+ storm::storage::sparse::state_type tmp = partition.positions[predecessor];
+ partition.positions[predecessor] = predecessorBlock->begin;
+ std::cout << "moved " << predecessor << " to pos " << predecessorBlock->begin << std::endl;
+ partition.positions[partition.states[predecessorBlock->begin]] = tmp;
+
+// storm::storage::sparse::state_type tmp = partition.positions[partition.states[predecessorPosition]];
+// partition.positions[partition.states[predecessorPosition]] = partition.positions[predecessor];
+// partition.positions[predecessor] = tmp;
// std::swap(partition.positions[predecessor], partition.positions[predecessorBlock->begin]);
++predecessorBlock->begin;
- std::cout << "incrementing begin... " << std::endl;
- partition.values[predecessor] = predecessorEntry.getValue();
+ std::cout << "incrementing begin, setting probability at " << partition.positions[predecessor] << " to " << predecessorEntry.getValue() << " ... " << std::endl;
+ partition.values[partition.positions[predecessor]] = predecessorEntry.getValue();
+ assert(partition.values[partition.positions[predecessor]] <= 1);
} else {
// Otherwise, we just need to update the probability for this predecessor.
- std::cout << "updating probability" << std::endl;
- partition.values[predecessor] += predecessorEntry.getValue();
+ partition.values[predecessorPosition] += predecessorEntry.getValue();
+ std::cout << "updating probability " << predecessorPosition << " to " << std::setprecision(10) << partition.values[predecessorPosition] << std::endl;
+ assert(partition.values[predecessorPosition] <= 1 + 1e-6);
}
if (!predecessorBlock->isMarked) {
@@ -246,6 +328,17 @@ namespace storm {
}
}
}
+
+ // Now that we have computed the new positions of the states we want to move, we need to actually move them.
+ for (auto block : predecessorBlocks) {
+ std::cout << "moving block " << block->myId << std::endl;
+ for (auto stateIterator = partition.states.begin() + block->originalBegin, stateIte = partition.states.begin() + block->end; stateIterator != stateIte; ++stateIterator) {
+ std::cout << "swapping " << *stateIterator << " to " << partition.positions[*stateIterator] << std::endl;
+ std::swap(partition.states[partition.positions[*stateIterator]], *stateIterator);
+ }
+ // Set the original begin and begin to the same value.
+ block->setBegin(block->begin);
+ }
std::list<Block*> blocksToSplit;
@@ -260,8 +353,7 @@ namespace storm {
storm::storage::sparse::state_type tmpBegin = block->begin;
storm::storage::sparse::state_type tmpEnd = block->end;
- block->begin = block->prev != nullptr ? block->prev->end : 0;
- std::cout << "begin: " << block->begin << " and not-null? " << (block->prev != nullptr) << ": " << block->prev << std::endl;
+ block->setBegin(block->prev != nullptr ? block->prev->end : 0);
block->end = tmpBegin;
block->numberOfStates = block->end - block->begin;
@@ -289,8 +381,13 @@ namespace storm {
splitterQueue.push_back(newBlock);
} else {
std::cout << "found block to split" << std::endl;
+
+ // In this case, we can keep the block by setting its begin to the old value.
+ block->setBegin((block->prev != nullptr) ? block->prev->end : 0);
blocksToSplit.emplace_back(block);
}
+
+ block->setBegin(block->begin);
}
// Finally, we walk through the blocks that have a transition to the splitter and split them using
diff --git a/src/storage/BisimulationDecomposition2.h b/src/storage/BisimulationDecomposition2.h
index 121f5487d..2cc4a98d8 100644
--- a/src/storage/BisimulationDecomposition2.h
+++ b/src/storage/BisimulationDecomposition2.h
@@ -34,12 +34,16 @@ namespace storm {
// Prints the block.
void print(Partition const& partition) const;
+
+ // Sets the beginning index of the block.
+ void setBegin(storm::storage::sparse::state_type begin);
// An iterator to itself. This is needed to conveniently insert elements in the overall list of blocks
// kept by the partition.
typename std::list<Block>::const_iterator itToSelf;
// The begin and end indices of the block in terms of the state vector of the partition.
+ storm::storage::sparse::state_type originalBegin;
storm::storage::sparse::state_type begin;
storm::storage::sparse::state_type end;
@@ -52,6 +56,8 @@ namespace storm {
// A field that can be used for marking the block.
bool isMarked;
+
+ int myId;
};
class Partition {
diff --git a/src/utility/cli.h b/src/utility/cli.h
index 6996736a4..70d4e75af 100644
--- a/src/utility/cli.h
+++ b/src/utility/cli.h
@@ -261,7 +261,7 @@ namespace storm {
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<storm::models::Dtmc<double>> dtmc = result->template as<storm::models::Dtmc<double>>();
- storm::storage::BisimulationDecomposition<double> bisimulationDecomposition(*dtmc);
+// storm::storage::BisimulationDecomposition<double> bisimulationDecomposition(*dtmc);
storm::storage::BisimulationDecomposition2<double> bisimulationDecomposition2(*dtmc);
}
From 404b12848eb9f7d7bfcb6181dd1332bbb8d79892 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Sun, 12 Oct 2014 21:03:36 +0200
Subject: [PATCH 09/14] More (and more) work on bisimulation minimization.
Former-commit-id: 946085c71b2aea86044b4b13f6fe85ba004ccacd
---
src/storage/BisimulationDecomposition2.cpp | 804 ++++++++++++++-------
src/storage/BisimulationDecomposition2.h | 210 +++++-
2 files changed, 728 insertions(+), 286 deletions(-)
diff --git a/src/storage/BisimulationDecomposition2.cpp b/src/storage/BisimulationDecomposition2.cpp
index 35bd1c703..abda69f66 100644
--- a/src/storage/BisimulationDecomposition2.cpp
+++ b/src/storage/BisimulationDecomposition2.cpp
@@ -8,23 +8,30 @@
namespace storm {
namespace storage {
- static int globalId = 0;
+ static std::size_t globalId = 0;
template<typename ValueType>
- BisimulationDecomposition2<ValueType>::Block::Block(storm::storage::sparse::state_type begin, storm::storage::sparse::state_type end, Block* prev, Block* next) : originalBegin(begin), begin(begin), end(end), prev(prev), next(next), numberOfStates(end - begin), isMarked(false), myId(globalId++) {
- // Intentionally left empty.
- std::cout << "created new block from " << begin << " to " << end << std::endl;
+ BisimulationDecomposition2<ValueType>::Block::Block(storm::storage::sparse::state_type begin, storm::storage::sparse::state_type end, Block* prev, Block* next) : next(next), prev(prev), begin(begin), end(end), markedAsSplitter(false), markedPosition(begin), id(globalId++) {
+ if (next != nullptr) {
+ next->prev = this;
+ }
+ if (prev != nullptr) {
+ prev->next = this;
+ }
}
template<typename ValueType>
void BisimulationDecomposition2<ValueType>::Block::print(Partition const& partition) const {
- std::cout << "block " << this->myId << " and ptr " << this << std::endl;
- std::cout << "begin: " << this->begin << " and end: " << this->end << " (number of states: " << this->numberOfStates << ")" << std::endl;
- std::cout << "next: " << this->next << " and prev " << this->prev << std::endl;
+ std::cout << "block " << this->getId() << " with marked position " << this->getMarkedPosition() << std::endl;
+ std::cout << "begin: " << this->begin << " and end: " << this->end << " (number of states: " << this->getNumberOfStates() << ")" << std::endl;
std::cout << "states:" << std::endl;
for (storm::storage::sparse::state_type index = this->begin; index < this->end; ++index) {
std::cout << partition.states[index] << " ";
}
+ std::cout << std::endl << "original: " << std::endl;
+ for (storm::storage::sparse::state_type index = this->getOriginalBegin(); index < this->end; ++index) {
+ std::cout << partition.states[index] << " ";
+ }
std::cout << std::endl << "values:" << std::endl;
for (storm::storage::sparse::state_type index = this->begin; index < this->end; ++index) {
std::cout << std::setprecision(3) << partition.values[index] << " ";
@@ -35,13 +42,187 @@ namespace storm {
template<typename ValueType>
void BisimulationDecomposition2<ValueType>::Block::setBegin(storm::storage::sparse::state_type begin) {
this->begin = begin;
- this->originalBegin = begin;
+ this->markedPosition = begin;
+ }
+
+ template<typename ValueType>
+ void BisimulationDecomposition2<ValueType>::Block::setEnd(storm::storage::sparse::state_type end) {
+ this->end = end;
+ }
+
+ template<typename ValueType>
+ void BisimulationDecomposition2<ValueType>::Block::incrementBegin() {
+ ++this->begin;
+ std::cout << "incremented begin to " << this->begin << std::endl;
+ }
+
+ template<typename ValueType>
+ void BisimulationDecomposition2<ValueType>::Block::decrementEnd() {
+ ++this->begin;
+ }
+
+ template<typename ValueType>
+ storm::storage::sparse::state_type BisimulationDecomposition2<ValueType>::Block::getBegin() const {
+ return this->begin;
+ }
+
+ template<typename ValueType>
+ storm::storage::sparse::state_type BisimulationDecomposition2<ValueType>::Block::getOriginalBegin() const {
+ if (this->hasPreviousBlock()) {
+ return this->getPreviousBlock().getEnd();
+ } else {
+ return 0;
+ }
+ }
+
+ template<typename ValueType>
+ storm::storage::sparse::state_type BisimulationDecomposition2<ValueType>::Block::getEnd() const {
+ return this->end;
+ }
+
+ template<typename ValueType>
+ void BisimulationDecomposition2<ValueType>::Block::setIterator(const_iterator it) {
+ this->selfIt = it;
+ }
+
+ template<typename ValueType>
+ typename BisimulationDecomposition2<ValueType>::Block::const_iterator BisimulationDecomposition2<ValueType>::Block::getIterator() const {
+ return this->selfIt;
+ }
+
+ template<typename ValueType>
+ typename BisimulationDecomposition2<ValueType>::Block::const_iterator BisimulationDecomposition2<ValueType>::Block::getNextIterator() const {
+ return this->getNextBlock().getIterator();
+ }
+
+ template<typename ValueType>
+ typename BisimulationDecomposition2<ValueType>::Block::const_iterator BisimulationDecomposition2<ValueType>::Block::getPreviousIterator() const {
+ return this->getPreviousBlock().getIterator();
+ }
+
+ template<typename ValueType>
+ typename BisimulationDecomposition2<ValueType>::Block& BisimulationDecomposition2<ValueType>::Block::getNextBlock() {
+ return *this->next;
+ }
+
+ template<typename ValueType>
+ typename BisimulationDecomposition2<ValueType>::Block const& BisimulationDecomposition2<ValueType>::Block::getNextBlock() const {
+ return *this->next;
+ }
+
+ template<typename ValueType>
+ bool BisimulationDecomposition2<ValueType>::Block::hasNextBlock() const {
+ return this->next != nullptr;
+ }
+
+ template<typename ValueType>
+ typename BisimulationDecomposition2<ValueType>::Block& BisimulationDecomposition2<ValueType>::Block::getPreviousBlock() {
+ return *this->prev;
+ }
+
+ template<typename ValueType>
+ typename BisimulationDecomposition2<ValueType>::Block* BisimulationDecomposition2<ValueType>::Block::getPreviousBlockPointer() {
+ return this->prev;
+ }
+
+ template<typename ValueType>
+ typename BisimulationDecomposition2<ValueType>::Block* BisimulationDecomposition2<ValueType>::Block::getNextBlockPointer() {
+ return this->next;
+ }
+
+ template<typename ValueType>
+ typename BisimulationDecomposition2<ValueType>::Block const& BisimulationDecomposition2<ValueType>::Block::getPreviousBlock() const {
+ return *this->prev;
+ }
+
+ template<typename ValueType>
+ bool BisimulationDecomposition2<ValueType>::Block::hasPreviousBlock() const {
+ return this->prev != nullptr;
+ }
+
+ template<typename ValueType>
+ bool BisimulationDecomposition2<ValueType>::Block::check() const {
+ if (this->begin >= this->end) {
+ std::cout << "beg: " << this->begin << " and end " << this->end << std::endl;
+ assert(false);
+ }
+ if (this->prev != nullptr) {
+ assert (this->prev->next == this);
+ }
+ if (this->next != nullptr) {
+ assert (this->next->prev == this);
+ }
+ return true;
+ }
+
+ template<typename ValueType>
+ std::size_t BisimulationDecomposition2<ValueType>::Block::getNumberOfStates() const {
+ // We need to take the original begin here, because the begin is temporarily moved.
+ return (this->end - this->getOriginalBegin());
+ }
+
+ template<typename ValueType>
+ bool BisimulationDecomposition2<ValueType>::Block::isMarkedAsSplitter() const {
+ return this->markedAsSplitter;
+ }
+
+ template<typename ValueType>
+ void BisimulationDecomposition2<ValueType>::Block::markAsSplitter() {
+ this->markedAsSplitter = true;
+ }
+
+ template<typename ValueType>
+ void BisimulationDecomposition2<ValueType>::Block::unmarkAsSplitter() {
+ this->markedAsSplitter = false;
+ }
+
+ template<typename ValueType>
+ std::size_t BisimulationDecomposition2<ValueType>::Block::getId() const {
+ return this->id;
+ }
+
+ template<typename ValueType>
+ storm::storage::sparse::state_type BisimulationDecomposition2<ValueType>::Block::getMarkedPosition() const {
+ return this->markedPosition;
+ }
+
+ template<typename ValueType>
+ void BisimulationDecomposition2<ValueType>::Block::setMarkedPosition(storm::storage::sparse::state_type position) {
+ this->markedPosition = position;
+ }
+
+ template<typename ValueType>
+ void BisimulationDecomposition2<ValueType>::Block::resetMarkedPosition() {
+ this->markedPosition = this->begin;
+ }
+
+ template<typename ValueType>
+ void BisimulationDecomposition2<ValueType>::Block::incrementMarkedPosition() {
+ ++this->markedPosition;
+ }
+
+ template<typename ValueType>
+ void BisimulationDecomposition2<ValueType>::Block::markAsPredecessorBlock() {
+ this->markedAsPredecessorBlock = true;
+ }
+
+ template<typename ValueType>
+ void BisimulationDecomposition2<ValueType>::Block::unmarkAsPredecessorBlock() {
+ this->markedAsPredecessorBlock = false;
+ }
+
+ template<typename ValueType>
+ bool BisimulationDecomposition2<ValueType>::Block::isMarkedAsPredecessor() const {
+ return markedAsPredecessorBlock;
}
template<typename ValueType>
BisimulationDecomposition2<ValueType>::Partition::Partition(std::size_t numberOfStates) : stateToBlockMapping(numberOfStates), states(numberOfStates), positions(numberOfStates), values(numberOfStates) {
+ // Create the block and give it an iterator to itself.
typename std::list<Block>::iterator it = blocks.emplace(this->blocks.end(), 0, numberOfStates, nullptr, nullptr);
- it->itToSelf = it;
+ it->setIterator(it);
+
+ // Set up the different parts of the internal structure.
for (storm::storage::sparse::state_type state = 0; state < numberOfStates; ++state) {
states[state] = state;
positions[state] = state;
@@ -49,40 +230,192 @@ namespace storm {
}
}
+ template<typename ValueType>
+ void BisimulationDecomposition2<ValueType>::Partition::swapStates(storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2) {
+ std::cout << "swapping states " << state1 << " and " << state2 << std::endl;
+ std::swap(this->states[this->positions[state1]], this->states[this->positions[state2]]);
+ std::swap(this->values[this->positions[state1]], this->values[this->positions[state2]]);
+ std::swap(this->positions[state1], this->positions[state2]);
+ assert(this->check());
+ }
+
+ template<typename ValueType>
+ void BisimulationDecomposition2<ValueType>::Partition::swapStatesAtPositions(storm::storage::sparse::state_type position1, storm::storage::sparse::state_type position2) {
+ storm::storage::sparse::state_type state1 = this->states[position1];
+ storm::storage::sparse::state_type state2 = this->states[position2];
+ std::cout << "swapping states " << state1 << " and " << state2 << " at positions " << position1 << " and " << position2 << std::endl;
+
+ std::swap(this->states[position1], this->states[position2]);
+ std::swap(this->values[position1], this->values[position2]);
+
+ this->positions[state1] = position2;
+ this->positions[state2] = position1;
+ std::cout << "pos of " << state1 << " is now " << position2 << " and pos of " << state2 << " is now " << position1 << std::endl;
+ std::cout << this->states[position1] << " vs " << state2 << " and " << this->states[position2] << " vs " << state1 << std::endl;
+ assert(this->check());
+ }
+
+ template<typename ValueType>
+ storm::storage::sparse::state_type const& BisimulationDecomposition2<ValueType>::Partition::getPosition(storm::storage::sparse::state_type state) const {
+ return this->positions[state];
+ }
+
+ template<typename ValueType>
+ void BisimulationDecomposition2<ValueType>::Partition::setPosition(storm::storage::sparse::state_type state, storm::storage::sparse::state_type position) {
+ this->positions[state] = position;
+ }
+
+ template<typename ValueType>
+ storm::storage::sparse::state_type const& BisimulationDecomposition2<ValueType>::Partition::getState(storm::storage::sparse::state_type position) const {
+ return this->states[position];
+ }
+
+ template<typename ValueType>
+ ValueType const& BisimulationDecomposition2<ValueType>::Partition::getValue(storm::storage::sparse::state_type state) const {
+ return this->values[this->positions[state]];
+ }
+
+ template<typename ValueType>
+ ValueType const& BisimulationDecomposition2<ValueType>::Partition::getValueAtPosition(storm::storage::sparse::state_type position) const {
+ return this->values[position];
+ }
+
+ template<typename ValueType>
+ void BisimulationDecomposition2<ValueType>::Partition::setValue(storm::storage::sparse::state_type state, ValueType value) {
+ this->values[this->positions[state]] = value;
+ }
+
+ template<typename ValueType>
+ std::vector<ValueType>& BisimulationDecomposition2<ValueType>::Partition::getValues() {
+ return this->values;
+ }
+
+ template<typename ValueType>
+ void BisimulationDecomposition2<ValueType>::Partition::increaseValue(storm::storage::sparse::state_type state, ValueType value) {
+ this->values[this->positions[state]] += value;
+ }
+
+ template<typename ValueType>
+ void BisimulationDecomposition2<ValueType>::Partition::updateBlockMapping(Block& block, std::vector<storm::storage::sparse::state_type>::iterator first, std::vector<storm::storage::sparse::state_type>::iterator last) {
+ for (; first != last; ++first) {
+ this->stateToBlockMapping[*first] = █
+ }
+ }
+
+ template<typename ValueType>
+ typename BisimulationDecomposition2<ValueType>::Block& BisimulationDecomposition2<ValueType>::Partition::getBlock(storm::storage::sparse::state_type state) {
+ return *this->stateToBlockMapping[state];
+ }
+
+ template<typename ValueType>
+ std::vector<storm::storage::sparse::state_type>::iterator BisimulationDecomposition2<ValueType>::Partition::getBeginOfStates(Block const& block) {
+ return this->states.begin() + block.getBegin();
+ }
+
+ template<typename ValueType>
+ std::vector<storm::storage::sparse::state_type>::iterator BisimulationDecomposition2<ValueType>::Partition::getEndOfStates(Block const& block) {
+ return this->states.begin() + block.getEnd();
+ }
+
+ template<typename ValueType>
+ std::vector<storm::storage::sparse::state_type>::const_iterator BisimulationDecomposition2<ValueType>::Partition::getBeginOfStates(Block const& block) const {
+ return this->states.begin() + block.getBegin();
+ }
+
+ template<typename ValueType>
+ std::vector<storm::storage::sparse::state_type>::const_iterator BisimulationDecomposition2<ValueType>::Partition::getEndOfStates(Block const& block) const {
+ return this->states.begin() + block.getEnd();
+ }
+
+ template<typename ValueType>
+ typename std::vector<ValueType>::iterator BisimulationDecomposition2<ValueType>::Partition::getBeginOfValues(Block const& block) {
+ return this->values.begin() + block.getBegin();
+ }
+
+ template<typename ValueType>
+ typename std::vector<ValueType>::iterator BisimulationDecomposition2<ValueType>::Partition::getEndOfValues(Block const& block) {
+ return this->values.begin() + block.getEnd();
+ }
+
+ template<typename ValueType>
+ typename BisimulationDecomposition2<ValueType>::Block& BisimulationDecomposition2<ValueType>::Partition::splitBlock(Block& block, storm::storage::sparse::state_type position) {
+ // FIXME: this could be improved by splitting off the smaller of the two resulting blocks.
+
+ std::cout << "splitting block (" << block.getBegin() << "," << block.getEnd() << ") at position " << position << std::endl;
+ block.print(*this);
+
+ // In case one of the resulting blocks would be empty, we simply return the current block and do not create
+ // a new one.
+ if (position == block.getBegin() || position == block.getEnd()) {
+ return block;
+ }
+
+ // Actually create the new block and insert it at the correct position.
+ typename std::list<Block>::iterator selfIt = this->blocks.emplace(block.getIterator(), block.getBegin(), position, block.getPreviousBlockPointer(), &block);
+ std::cout << "created new block from " << block.getBegin() << " to " << position << std::endl;
+ selfIt->setIterator(selfIt);
+ Block& newBlock = *selfIt;
+
+ // Make the current block end at the given position.
+ block.setBegin(position);
+
+ std::cout << "old block: " << std::endl;
+ block.print(*this);
+
+ // Update the mapping of the states in the newly created block.
+ for (auto it = this->getBeginOfStates(newBlock), ite = this->getEndOfStates(newBlock); it != ite; ++it) {
+ stateToBlockMapping[*it] = &newBlock;
+ }
+
+ return newBlock;
+ }
+
+ template<typename ValueType>
+ typename BisimulationDecomposition2<ValueType>::Block& BisimulationDecomposition2<ValueType>::Partition::insertBlock(Block& block) {
+ // Find the beginning of the new block.
+ storm::storage::sparse::state_type begin;
+ if (block.hasPreviousBlock()) {
+ begin = block.getPreviousBlock().getEnd();
+ std::cout << "previous block ended at " << begin << std::endl;
+ block.getPreviousBlock().print(*this);
+ } else {
+ begin = 0;
+ }
+
+ // Actually insert the new block.
+ typename std::list<Block>::iterator it = this->blocks.emplace(block.getIterator(), begin, block.getBegin(), block.getPreviousBlockPointer(), &block);
+ Block& newBlock = *it;
+ newBlock.setIterator(it);
+
+ // Update the mapping of the states in the newly created block.
+ for (auto it = this->getBeginOfStates(newBlock), ite = this->getEndOfStates(newBlock); it != ite; ++it) {
+ stateToBlockMapping[*it] = &newBlock;
+ }
+
+ return *it;
+ }
+
template<typename ValueType>
void BisimulationDecomposition2<ValueType>::Partition::splitLabel(storm::storage::BitVector const& statesWithLabel) {
for (auto blockIterator = this->blocks.begin(), ite = this->blocks.end(); blockIterator != ite; ) { // The update of the loop was intentionally moved to the bottom of the loop.
Block& block = *blockIterator;
// Sort the range of the block such that all states that have the label are moved to the front.
- std::sort(this->states.begin() + block.begin, this->states.begin() + block.end, [&statesWithLabel] (storm::storage::sparse::state_type const& a, storm::storage::sparse::state_type const& b) { return statesWithLabel.get(a) && !statesWithLabel.get(b); } );
+ std::sort(this->getBeginOfStates(block), this->getEndOfStates(block), [&statesWithLabel] (storm::storage::sparse::state_type const& a, storm::storage::sparse::state_type const& b) { return statesWithLabel.get(a) && !statesWithLabel.get(b); } );
// Update the positions vector.
- storm::storage::sparse::state_type position = block.begin;
- for (auto stateIt = this->states.begin() + block.begin, stateIte = this->states.begin() + block.end; stateIt != stateIte; ++stateIt, ++position) {
+ storm::storage::sparse::state_type position = block.getBegin();
+ for (auto stateIt = this->getBeginOfStates(block), stateIte = this->getEndOfStates(block); stateIt != stateIte; ++stateIt, ++position) {
this->positions[*stateIt] = position;
}
// Now we can find the first position in the block that does not have the label and create new blocks.
- std::vector<storm::storage::sparse::state_type>::iterator it = std::find_if(this->states.begin() + block.begin, this->states.begin() + block.end, [&] (storm::storage::sparse::state_type const& a) { return !statesWithLabel.get(a); });
+ std::vector<storm::storage::sparse::state_type>::iterator it = std::find_if(this->getBeginOfStates(block), this->getEndOfStates(block), [&] (storm::storage::sparse::state_type const& a) { return !statesWithLabel.get(a); });
// If not all the states agreed on the validity of the label, we need to split the block.
- if (it != this->states.begin() + block.begin && it != this->states.begin() + block.end) {
+ if (it != this->getBeginOfStates(block) && it != this->getEndOfStates(block)) {
auto cutPoint = std::distance(this->states.begin(), it);
-
- ++blockIterator;
- auto newBlockIterator = this->blocks.emplace(blockIterator, cutPoint, block.end, &block, block.next);
- newBlockIterator->itToSelf = newBlockIterator;
-
- // Make the old block end at the cut position and insert a new block after it.
- block.end = cutPoint;
- block.next = &(*newBlockIterator);
- block.numberOfStates = block.end - block.begin;
-
- // Update the block mapping for all states that we just removed from the block.
- for (auto it = this->states.begin() + newBlockIterator->begin, ite = this->states.begin() + newBlockIterator->end; it != ite; ++it) {
- stateToBlockMapping[*it] = &(*newBlockIterator);
- }
+ this->splitBlock(block, cutPoint);
} else {
// Otherwise, we simply proceed to the next block.
++blockIterator;
@@ -90,6 +423,40 @@ namespace storm {
}
}
+ template<typename ValueType>
+ std::list<typename BisimulationDecomposition2<ValueType>::Block> const& BisimulationDecomposition2<ValueType>::Partition::getBlocks() const {
+ return this->blocks;
+ }
+
+ template<typename ValueType>
+ std::vector<storm::storage::sparse::state_type>& BisimulationDecomposition2<ValueType>::Partition::getStates() {
+ return this->states;
+ }
+
+ template<typename ValueType>
+ std::list<typename BisimulationDecomposition2<ValueType>::Block>& BisimulationDecomposition2<ValueType>::Partition::getBlocks() {
+ return this->blocks;
+ }
+
+ template<typename ValueType>
+ bool BisimulationDecomposition2<ValueType>::Partition::check() const {
+ for (uint_fast64_t state = 0; state < this->positions.size(); ++state) {
+ if (this->states[this->positions[state]] != state) {
+ assert(false);
+ }
+ }
+ for (auto const& block : this->blocks) {
+ assert(block.check());
+ for (auto stateIt = this->getBeginOfStates(block), stateIte = this->getEndOfStates(block); stateIt != stateIte; ++stateIt) {
+ if (this->stateToBlockMapping[*stateIt] != &block) {
+ std::cout << "state " << *stateIt << " has wrong block mapping " << this->stateToBlockMapping[*stateIt] << " (should have " << &block << ")" << std::endl;
+ assert(false);
+ }
+ }
+ }
+ return true;
+ }
+
template<typename ValueType>
void BisimulationDecomposition2<ValueType>::Partition::print() const {
for (auto const& block : this->blocks) {
@@ -109,6 +476,7 @@ namespace storm {
}
std::cout << std::endl;
std::cout << "size: " << this->blocks.size() << std::endl;
+ assert(this->check());
}
template<typename ValueType>
@@ -129,7 +497,7 @@ namespace storm {
template<typename ValueType>
void BisimulationDecomposition2<ValueType>::computeBisimulationEquivalenceClasses(storm::models::Dtmc<ValueType> const& dtmc, bool weak) {
std::chrono::high_resolution_clock::time_point totalStart = std::chrono::high_resolution_clock::now();
-
+
// We start by computing the initial partition.
Partition partition(dtmc.getNumberOfStates());
partition.print();
@@ -142,10 +510,11 @@ namespace storm {
std::cout << "initial partition:" << std::endl;
partition.print();
+ assert(partition.check());
// Initially, all blocks are potential splitter, so we insert them in the splitterQueue.
std::deque<Block*> splitterQueue;
- std::for_each(partition.blocks.begin(), partition.blocks.end(), [&] (Block& a) { splitterQueue.push_back(&a); });
+ std::for_each(partition.getBlocks().begin(), partition.getBlocks().end(), [&] (Block& a) { splitterQueue.push_back(&a); });
storm::storage::SparseMatrix<ValueType> backwardTransitions = dtmc.getBackwardTransitions();
@@ -166,318 +535,213 @@ namespace storm {
}
template<typename ValueType>
- std::size_t BisimulationDecomposition2<ValueType>::splitBlockProbabilities(Block* block, Partition& partition, std::deque<Block*>& splitterQueue) {
+ std::size_t BisimulationDecomposition2<ValueType>::splitBlockProbabilities(Block& block, Partition& partition, std::deque<Block*>& splitterQueue) {
std::cout << "part before split prob" << std::endl;
partition.print();
- Block& currentBlock = *block;
-
// Sort the states in the block based on their probabilities.
- std::sort(partition.states.begin() + currentBlock.begin, partition.states.begin() + currentBlock.end, [&partition] (storm::storage::sparse::state_type const& a, storm::storage::sparse::state_type const& b) { return partition.values[a] < partition.values[b]; } );
+ std::sort(partition.getBeginOfStates(block), partition.getEndOfStates(block), [&partition] (storm::storage::sparse::state_type const& a, storm::storage::sparse::state_type const& b) { return partition.getValue(a) < partition.getValue(b); } );
// FIXME: This can probably be done more efficiently.
- std::sort(partition.values.begin() + currentBlock.begin, partition.values.begin() + currentBlock.end);
+ std::sort(partition.getBeginOfValues(block), partition.getEndOfValues(block));
// Update the positions vector.
- storm::storage::sparse::state_type position = currentBlock.begin;
- for (auto stateIt = partition.states.begin() + currentBlock.begin, stateIte = partition.states.begin() + currentBlock.end; stateIt != stateIte; ++stateIt, ++position) {
- partition.positions[*stateIt] = position;
+ storm::storage::sparse::state_type position = block.getBegin();
+ for (auto stateIt = partition.getBeginOfStates(block), stateIte = partition.getEndOfStates(block); stateIt != stateIte; ++stateIt, ++position) {
+ partition.setPosition(*stateIt, position);
}
-
+
// Finally, we need to scan the ranges of states that agree on the probability.
- storm::storage::sparse::state_type beginIndex = currentBlock.begin;
+ storm::storage::sparse::state_type beginIndex = block.getBegin();
storm::storage::sparse::state_type currentIndex = beginIndex;
- storm::storage::sparse::state_type endIndex = currentBlock.end;
+ storm::storage::sparse::state_type endIndex = block.getEnd();
// Now we can check whether the block needs to be split, which is the case iff the probabilities for the
// first and the last state are different.
- // Note that this check requires the block to be non-empty.
- if (std::abs(partition.values[beginIndex] - partition.values[endIndex - 1]) < 1e-6) {
- return 1;
- }
-
- // Now we scan for the first state in the block that disagrees on the probability value.
- // Note that we do not have to check currentIndex for staying within bounds, because we know the matching
- // state is within bounds.
- ValueType currentValue = partition.values[beginIndex];
- ValueType* valueIterator = &(partition.values[beginIndex]) + 1;
- ++currentIndex;
- while (std::abs(*valueIterator - currentValue) < 1e-6) {
- std::cout << "prob: " << *valueIterator << std::endl;
- ++currentIndex;
- ++valueIterator;
- }
-
- // Now resize the block.
- std::cout << "resizing block from " << std::endl;
- currentBlock.print(partition);
- currentBlock.end = currentIndex;
- currentBlock.numberOfStates = currentBlock.end - currentBlock.begin;
- std::cout << " to " << std::endl;
- currentBlock.print(partition);
- beginIndex = currentIndex;
-
- // If it is not already a splitter, we mark it as such.
- if (!currentBlock.isMarked) {
- currentBlock.isMarked = true;
- }
-
- Block* prevBlock = ¤tBlock;
-
- // Now scan for new blocks.
- std::list<Block*> createdBlocks;
- std::cout << currentIndex << " < " << endIndex << std::endl;
- typename std::list<Block>::const_iterator insertPosition = currentBlock.itToSelf;
- ++insertPosition;
- while (currentIndex < endIndex) {
- ValueType currentValue = *(partition.values.begin() + currentIndex);
+ std::size_t createdBlocks = 0;
+ while (std::abs(partition.getValueAtPosition(beginIndex) - partition.getValueAtPosition(endIndex)) >= 1e-6) {
+ // Now we scan for the first state in the block that disagrees on the probability value.
+ // Note that we do not have to check currentIndex for staying within bounds, because we know the matching
+ // state is within bounds.
+ ValueType const& currentValue = partition.getValueAtPosition(beginIndex);
+ typename std::vector<ValueType>::const_iterator valueIterator = partition.getValues().begin() + beginIndex + 1;
++currentIndex;
- ValueType* nextValuePtr = ¤tValue;
- while (currentIndex < endIndex && std::abs(currentValue - *nextValuePtr) < 1e-6) {
+ while (currentIndex < endIndex && std::abs(*valueIterator - currentValue) <= 1e-6) {
+ ++valueIterator;
++currentIndex;
- ++nextValuePtr;
}
- // Create a new block from the states that agree on the values.
- ++insertPosition;
- typename std::list<Block>::iterator newBlockIterator = partition.blocks.emplace(insertPosition, beginIndex, currentIndex, prevBlock, prevBlock->next);
- newBlockIterator->itToSelf = newBlockIterator;
- Block* newBlock = &(*newBlockIterator);
- prevBlock->next = newBlock;
- prevBlock = newBlock;
- if (prevBlock->numberOfStates > 1) {
- createdBlocks.emplace_back(prevBlock);
+ // Now we split the block and mark it as a potential splitter.
+ ++createdBlocks;
+ Block& newBlock = partition.splitBlock(block, currentIndex);
+ if (!newBlock.isMarkedAsPredecessor()) {
+ newBlock.markAsSplitter();
+ splitterQueue.push_back(&newBlock);
}
beginIndex = currentIndex;
-
- // Update the block mapping for the moved states.
- for (auto it = partition.states.begin() + newBlock->begin, ite = partition.states.begin() + newBlock->end; it != ite; ++it) {
- partition.stateToBlockMapping[*it] = newBlock;
- }
- }
-
- for (auto block : createdBlocks) {
- splitterQueue.push_back(block);
- block->isMarked = true;
}
- std::cout << "created " << createdBlocks.size() << " blocks" << std::endl;
+ assert(partition.check());
- return createdBlocks.size();
+ return createdBlocks;
}
template<typename ValueType>
- std::size_t BisimulationDecomposition2<ValueType>::splitPartition(storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Block const& splitter, Partition& partition, std::deque<Block*>& splitterQueue) {
- std::cout << "getting block " << splitter.myId << " as splitter" << std::endl;
+ std::size_t BisimulationDecomposition2<ValueType>::splitPartition(storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Block& splitter, Partition& partition, std::deque<Block*>& splitterQueue) {
+ std::cout << "treating block " << splitter.getId() << " as splitter" << std::endl;
+ splitter.print(partition);
+
std::list<Block*> predecessorBlocks;
// Iterate over all states of the splitter and check its predecessors.
- for (auto stateIterator = partition.states.begin() + splitter.begin, stateIte = partition.states.begin() + splitter.end; stateIterator != stateIte; ++stateIterator) {
- storm::storage::sparse::state_type& state = *stateIterator;
+ storm::storage::sparse::state_type currentPosition = splitter.getBegin();
+ for (auto stateIterator = partition.getBeginOfStates(splitter), stateIte = partition.getEndOfStates(splitter); stateIterator != stateIte; ++stateIterator, ++currentPosition) {
+ std::cout << "states -----" << std::endl;
+ for (auto stateIterator = partition.getStates().begin() + splitter.getOriginalBegin(), stateIte = partition.getStates().begin() + splitter.getEnd(); stateIterator != stateIte; ++stateIterator) {
+ std::cout << *stateIterator << " ";
+ }
+ std::cout << std::endl;
+
+ storm::storage::sparse::state_type currentState = *stateIterator;
+ std::cout << "current state " << currentState << " at pos " << currentPosition << std::endl;
- for (auto const& predecessorEntry : backwardTransitions.getRow(state)) {
+ uint_fast64_t elementsToSkip = 0;
+ for (auto const& predecessorEntry : backwardTransitions.getRow(currentState)) {
storm::storage::sparse::state_type predecessor = predecessorEntry.getColumn();
- std::cout << "found predecessor " << predecessor << " of state " << *stateIterator << std::endl;
- Block* predecessorBlock = partition.stateToBlockMapping[predecessor];
- std::cout << "predecessor block " << predecessorBlock->myId << std::endl;
+ std::cout << "found predecessor " << predecessor << " of state " << currentState << std::endl;
+
+ Block& predecessorBlock = partition.getBlock(predecessor);
+ std::cout << "predecessor block " << predecessorBlock.getId() << std::endl;
// If the predecessor block has just one state, there is no point in splitting it.
- if (predecessorBlock->numberOfStates <= 1) {
+ if (predecessorBlock.getNumberOfStates() <= 1) {
continue;
}
- storm::storage::sparse::state_type predecessorPosition = partition.positions[predecessor];
+ storm::storage::sparse::state_type predecessorPosition = partition.getPosition(predecessor);
// If we have not seen this predecessor before, we move it to a part near the beginning of the block.
- std::cout << "predecessor position: " << predecessorPosition << " and begin " << predecessorBlock->begin << std::endl;
- if (predecessorPosition >= predecessorBlock->begin) {
-
-// We cannot directly move the states at this point, otherwise we would consider states multiple
-// times while others are skipped.
-// std::swap(partition.states[predecessorPosition], partition.states[predecessorBlock->begin]);
-// std::cout << "swapping positions of " << predecessor << " and " << partition.states[predecessorPosition] << std::endl;
-
- // Instead, we only virtually move the states by setting their positions and move them in place
- // later.
- storm::storage::sparse::state_type tmp = partition.positions[predecessor];
- partition.positions[predecessor] = predecessorBlock->begin;
- std::cout << "moved " << predecessor << " to pos " << predecessorBlock->begin << std::endl;
- partition.positions[partition.states[predecessorBlock->begin]] = tmp;
-
-// storm::storage::sparse::state_type tmp = partition.positions[partition.states[predecessorPosition]];
-// partition.positions[partition.states[predecessorPosition]] = partition.positions[predecessor];
-// partition.positions[predecessor] = tmp;
-
-// std::swap(partition.positions[predecessor], partition.positions[predecessorBlock->begin]);
-
- ++predecessorBlock->begin;
- std::cout << "incrementing begin, setting probability at " << partition.positions[predecessor] << " to " << predecessorEntry.getValue() << " ... " << std::endl;
- partition.values[partition.positions[predecessor]] = predecessorEntry.getValue();
- assert(partition.values[partition.positions[predecessor]] <= 1);
+ if (predecessorPosition >= predecessorBlock.getBegin()) {
+ if (&predecessorBlock == &splitter) {
+ // If the predecessor we just found was already processed (in terms of visiting its predecessors),
+ // we swap it with the state that is currently at the beginning of the block and move the start
+ // of the block one step further.
+ if (predecessorPosition <= currentPosition) {
+ partition.swapStates(predecessor, partition.getState(predecessorBlock.getBegin()));
+ predecessorBlock.incrementBegin();
+ } else {
+ std::cout << "current position is " << currentPosition << std::endl;
+ // Otherwise, we need to move the predecessor, but we need to make sure that we explore its
+ // predecessors later.
+ if (predecessorBlock.getMarkedPosition() == predecessorBlock.getBegin()) {
+ partition.swapStatesAtPositions(predecessorBlock.getMarkedPosition(), predecessorPosition);
+ partition.swapStatesAtPositions(predecessorPosition, currentPosition + elementsToSkip + 1);
+ } else {
+ partition.swapStatesAtPositions(predecessorBlock.getMarkedPosition(), predecessorPosition);
+ partition.swapStatesAtPositions(predecessorPosition, predecessorBlock.getBegin());
+ partition.swapStatesAtPositions(predecessorPosition, currentPosition + elementsToSkip + 1);
+ }
+
+ ++elementsToSkip;
+ predecessorBlock.incrementMarkedPosition();
+ predecessorBlock.incrementBegin();
+ }
+ } else {
+ partition.swapStates(predecessor, partition.getState(predecessorBlock.getBegin()));
+ predecessorBlock.incrementBegin();
+ }
+ partition.setValue(predecessor, predecessorEntry.getValue());
} else {
// Otherwise, we just need to update the probability for this predecessor.
- partition.values[predecessorPosition] += predecessorEntry.getValue();
- std::cout << "updating probability " << predecessorPosition << " to " << std::setprecision(10) << partition.values[predecessorPosition] << std::endl;
- assert(partition.values[predecessorPosition] <= 1 + 1e-6);
+ partition.increaseValue(predecessor, predecessorEntry.getValue());
}
- if (!predecessorBlock->isMarked) {
- predecessorBlocks.emplace_back(predecessorBlock);
- predecessorBlock->isMarked = true;
+ if (!predecessorBlock.isMarkedAsPredecessor()) {
+ predecessorBlocks.emplace_back(&predecessorBlock);
+ predecessorBlock.markAsPredecessorBlock();
}
}
+
+ // If we had to move some elements beyond the current element, we may have to skip them.
+ if (elementsToSkip > 0) {
+ std::cout << "skipping " << elementsToSkip << " elements" << std::endl;
+ stateIterator += elementsToSkip;
+ currentPosition += elementsToSkip;
+ }
}
-
- // Now that we have computed the new positions of the states we want to move, we need to actually move them.
- for (auto block : predecessorBlocks) {
- std::cout << "moving block " << block->myId << std::endl;
- for (auto stateIterator = partition.states.begin() + block->originalBegin, stateIte = partition.states.begin() + block->end; stateIterator != stateIte; ++stateIterator) {
- std::cout << "swapping " << *stateIterator << " to " << partition.positions[*stateIterator] << std::endl;
- std::swap(partition.states[partition.positions[*stateIterator]], *stateIterator);
+
+ // Now we can traverse the list of states of the splitter whose predecessors we have not yet explored.
+ for (auto stateIterator = partition.getStates().begin() + splitter.getOriginalBegin(), stateIte = partition.getStates().begin() + splitter.getMarkedPosition(); stateIterator != stateIte; ++stateIterator) {
+ storm::storage::sparse::state_type currentState = *stateIterator;
+
+ for (auto const& predecessorEntry : backwardTransitions.getRow(currentState)) {
+ storm::storage::sparse::state_type predecessor = predecessorEntry.getColumn();
+ Block& predecessorBlock = partition.getBlock(predecessor);
+ storm::storage::sparse::state_type predecessorPosition = partition.getPosition(predecessor);
+
+ if (predecessorPosition >= predecessorBlock.getBegin()) {
+ partition.swapStatesAtPositions(predecessorPosition, predecessorBlock.getBegin());
+ predecessorBlock.incrementBegin();
+ partition.setValue(predecessor, predecessorEntry.getValue());
+ } else {
+ partition.increaseValue(predecessor, predecessorEntry.getValue());
+ }
+
+ if (!predecessorBlock.isMarkedAsPredecessor()) {
+ predecessorBlocks.emplace_back(&predecessorBlock);
+ predecessorBlock.markAsPredecessorBlock();
+ }
}
- // Set the original begin and begin to the same value.
- block->setBegin(block->begin);
}
+ splitter.setMarkedPosition(splitter.getBegin());
+
std::list<Block*> blocksToSplit;
+ std::cout << "having " << predecessorBlocks.size() << " pred blocks " << std::endl;
+
// Now, we can iterate over the predecessor blocks and see whether we have to create a new block for
// predecessors of the splitter.
- for (auto block : predecessorBlocks) {
- block->isMarked = false;
+ for (auto blockPtr : predecessorBlocks) {
+ Block& block = *blockPtr;
+
+ block.unmarkAsPredecessorBlock();
+ block.resetMarkedPosition();
// If we have moved the begin of the block to somewhere in the middle of the block, we need to split it.
- if (block->begin != block->end) {
- std::cout << "moved begin to " << block->begin << " and end to " << block->end << std::endl;
- storm::storage::sparse::state_type tmpBegin = block->begin;
- storm::storage::sparse::state_type tmpEnd = block->end;
-
- block->setBegin(block->prev != nullptr ? block->prev->end : 0);
- block->end = tmpBegin;
- block->numberOfStates = block->end - block->begin;
-
- // Create a new block that holds all states that do not have a successor in the current splitter.
- typename std::list<Block>::iterator it = partition.blocks.emplace(block->next != nullptr ? block->next->itToSelf : partition.blocks.end(), tmpBegin, tmpEnd, block, block->next);
- Block* newBlock = &(*it);
- newBlock->itToSelf = it;
- if (block->next != nullptr) {
- block->next->prev = newBlock;
- }
- block->next = newBlock;
+ if (block.getBegin() != block.getEnd()) {
+ std::cout << "moved begin of block " << block.getId() << " to " << block.getBegin() << " and end to " << block.getEnd() << std::endl;
+ Block& newBlock = partition.insertBlock(block);
std::cout << "created new block " << std::endl;
- newBlock->print(partition);
-
- // Update the block mapping in the partition.
- for (auto it = partition.states.begin() + newBlock->begin, ite = partition.states.begin() + newBlock->end; it != ite; ++it) {
- partition.stateToBlockMapping[*it] = newBlock;
- }
-
- // Mark the half of the block that can be further refined using the probability information.
- blocksToSplit.emplace_back(block);
- block->print(partition);
-
- splitterQueue.push_back(newBlock);
+ newBlock.print(partition);
+ splitterQueue.push_back(&newBlock);
} else {
- std::cout << "found block to split" << std::endl;
-
+ std::cout << "all states are predecessors" << std::endl;
+
// In this case, we can keep the block by setting its begin to the old value.
- block->setBegin((block->prev != nullptr) ? block->prev->end : 0);
- blocksToSplit.emplace_back(block);
+ block.setBegin(block.getOriginalBegin());
+ blocksToSplit.emplace_back(&block);
}
-
- block->setBegin(block->begin);
}
+ assert(partition.check());
+
// Finally, we walk through the blocks that have a transition to the splitter and split them using
// probabilistic information.
- for (auto block : blocksToSplit) {
- if (block->numberOfStates <= 1) {
+ for (auto blockPtr : blocksToSplit) {
+ std::cout << "block to split: " << blockPtr->getId() << std::endl;
+ if (blockPtr->getNumberOfStates() <= 1) {
continue;
}
- splitBlockProbabilities(block, partition, splitterQueue);
+ splitBlockProbabilities(*blockPtr, partition, splitterQueue);
}
return 0;
}
-// template<typename ValueType>
-// std::size_t BisimulationDecomposition2<ValueType>::splitPartition(storm::models::Dtmc<ValueType> const& dtmc, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::size_t const& blockId, std::vector<std::size_t>& stateToBlockMapping, storm::storage::BitVector& blocksInSplitterQueue, std::deque<std::size_t>& splitterQueue, bool weakBisimulation) {
-// std::chrono::high_resolution_clock::time_point totalStart = std::chrono::high_resolution_clock::now();
-// std::unordered_map<storm::storage::Distribution<ValueType>, typename BisimulationDecomposition2<ValueType>::block_type> distributionToNewBlocks;
-//
-// // Traverse all states of the block and check whether they have different distributions.
-// std::chrono::high_resolution_clock::time_point gatherStart = std::chrono::high_resolution_clock::now();
-// for (auto const& state : this->blocks[blockId]) {
-// // Now construct the distribution of this state wrt. to the current partitioning.
-// storm::storage::Distribution<ValueType> distribution;
-// for (auto const& successorEntry : dtmc.getTransitionMatrix().getRow(state)) {
-// distribution.addProbability(static_cast<storm::storage::sparse::state_type>(stateToBlockMapping[successorEntry.getColumn()]), successorEntry.getValue());
-// }
-//
-// // If we are requested to compute a weak bisimulation, we need to scale the distribution with the
-// // self-loop probability.
-// if (weakBisimulation) {
-// distribution.scale(blockId);
-// }
-//
-// // If the distribution already exists, we simply add the state. Otherwise, we open a new block.
-// auto distributionIterator = distributionToNewBlocks.find(distribution);
-// if (distributionIterator != distributionToNewBlocks.end()) {
-// distributionIterator->second.insert(state);
-// } else {
-// distributionToNewBlocks[distribution].insert(state);
-// }
-// }
-//
-// std::chrono::high_resolution_clock::duration gatherTime = std::chrono::high_resolution_clock::now() - gatherStart;
-// std::cout << "time to iterate over all states was " << std::chrono::duration_cast<std::chrono::milliseconds>(gatherTime).count() << "ms." << std::endl;
-//
-// // Now we are ready to split the block.
-// if (distributionToNewBlocks.size() == 1) {
-// // If there is just one behavior, we just set the distribution as the new one for this block.
-// // distributions[blockId] = std::move(distributionToNewBlocks.begin()->first);
-// } else {
-// // In this case, we need to split the block.
-// typename BisimulationDecomposition2<ValueType>::block_type tmpBlock;
-//
-// auto distributionIterator = distributionToNewBlocks.begin();
-// tmpBlock = std::move(distributionIterator->second);
-// std::swap(this->blocks[blockId], tmpBlock);
-// ++distributionIterator;
-//
-// // Remember the number of blocks prior to splitting for later use.
-// std::size_t beforeNumberOfBlocks = this->blocks.size();
-//
-// for (; distributionIterator != distributionToNewBlocks.end(); ++distributionIterator) {
-// // In this case, we need to move the newly created block to the end of the list of actual blocks.
-// this->blocks.emplace_back(std::move(distributionIterator->second));
-//
-// // Update the mapping of states to their blocks.
-// std::size_t newBlockId = this->blocks.size() - 1;
-// for (auto const& state : this->blocks.back()) {
-// stateToBlockMapping[state] = newBlockId;
-// }
-// }
-//
-// // Insert blocks that possibly need a refinement into the queue.
-// for (auto const& state : tmpBlock) {
-// for (auto const& predecessor : backwardTransitions.getRow(state)) {
-// if (!blocksInRefinementQueue.get(stateToBlockMapping[predecessor.getColumn()])) {
-// blocksInRefinementQueue.set(stateToBlockMapping[predecessor.getColumn()]);
-// refinementQueue.push_back(stateToBlockMapping[predecessor.getColumn()]);
-// }
-// }
-// }
-// }
-//
-// std::chrono::high_resolution_clock::duration totalTime = std::chrono::high_resolution_clock::now() - totalStart;
-// std::cout << "refinement of block " << blockId << " took " << std::chrono::duration_cast<std::chrono::milliseconds>(totalTime).count() << "ms." << std::endl;
-// return distributionToNewBlocks.size();
-// }
-
template class BisimulationDecomposition2<double>;
}
}
\ No newline at end of file
diff --git a/src/storage/BisimulationDecomposition2.h b/src/storage/BisimulationDecomposition2.h
index 2cc4a98d8..50153d4b5 100644
--- a/src/storage/BisimulationDecomposition2.h
+++ b/src/storage/BisimulationDecomposition2.h
@@ -30,6 +30,8 @@ namespace storm {
class Block {
public:
+ typedef typename std::list<Block>::const_iterator const_iterator;
+
Block(storm::storage::sparse::state_type begin, storm::storage::sparse::state_type end, Block* prev, Block* next);
// Prints the block.
@@ -37,31 +39,130 @@ namespace storm {
// Sets the beginning index of the block.
void setBegin(storm::storage::sparse::state_type begin);
+
+ // Moves the beginning index of the block one step further.
+ void incrementBegin();
+
+ // Sets the end index of the block.
+ void setEnd(storm::storage::sparse::state_type end);
+
+ // Moves the end index of the block one step to the front.
+ void decrementEnd();
+
+ // Returns the beginning index of the block.
+ storm::storage::sparse::state_type getBegin() const;
+
+ // Returns the beginning index of the block.
+ storm::storage::sparse::state_type getEnd() const;
+
+ // Retrieves the original beginning index of the block in case the begin index has been moved.
+ storm::storage::sparse::state_type getOriginalBegin() const;
+
+ // Returns the iterator the block in the list of overall blocks.
+ const_iterator getIterator() const;
+
+ // Returns the iterator the block in the list of overall blocks.
+ void setIterator(const_iterator it);
+
+ // Returns the iterator the next block in the list of overall blocks if it exists.
+ const_iterator getNextIterator() const;
+
+ // Returns the iterator the next block in the list of overall blocks if it exists.
+ const_iterator getPreviousIterator() const;
+
+ // Gets the next block (if there is one).
+ Block& getNextBlock();
+
+ // Gets the next block (if there is one).
+ Block const& getNextBlock() const;
+
+ // Gets a pointer to the next block (if there is one).
+ Block* getNextBlockPointer();
+
+ // Retrieves whether the block as a successor block.
+ bool hasNextBlock() const;
+
+ // Gets the previous block (if there is one).
+ Block& getPreviousBlock();
+
+ // Gets a pointer to the previous block (if there is one).
+ Block* getPreviousBlockPointer();
+
+ // Gets the next block (if there is one).
+ Block const& getPreviousBlock() const;
+
+ // Retrieves whether the block as a successor block.
+ bool hasPreviousBlock() const;
+
+ // Checks consistency of the information in the block.
+ bool check() const;
+
+ // Retrieves the number of states in this block.
+ std::size_t getNumberOfStates() const;
+
+ // Checks whether the block is marked as a splitter.
+ bool isMarkedAsSplitter() const;
+
+ // Marks the block as being a splitter.
+ void markAsSplitter();
+
+ // Removes the mark.
+ void unmarkAsSplitter();
+
+ // Retrieves the ID of the block.
+ std::size_t getId() const;
+
+ // Retrieves the marked position in the block.
+ storm::storage::sparse::state_type getMarkedPosition() const;
+
+ // Sets the marked position to the given value..
+ void setMarkedPosition(storm::storage::sparse::state_type position);
+
+ // Increases the marked position by one.
+ void incrementMarkedPosition();
+
+ // Resets the marked position to the begin of the block.
+ void resetMarkedPosition();
+
+ // Retrieves whether the block is marked as a predecessor.
+ bool isMarkedAsPredecessor() const;
+
+ // Marks the block as being a predecessor block.
+ void markAsPredecessorBlock();
+
+ // Removes the marking.
+ void unmarkAsPredecessorBlock();
+ private:
// An iterator to itself. This is needed to conveniently insert elements in the overall list of blocks
// kept by the partition.
- typename std::list<Block>::const_iterator itToSelf;
+ const_iterator selfIt;
+
+ // Pointers to the next and previous block.
+ Block* next;
+ Block* prev;
// The begin and end indices of the block in terms of the state vector of the partition.
- storm::storage::sparse::state_type originalBegin;
storm::storage::sparse::state_type begin;
storm::storage::sparse::state_type end;
- // The block before and after the current one.
- Block* prev;
- Block* next;
+ // A field that can be used for marking the block.
+ bool markedAsSplitter;
- // The number of states in the block.
- std::size_t numberOfStates;
+ // A field that can be used for marking the block as a predecessor block.
+ bool markedAsPredecessorBlock;
- // A field that can be used for marking the block.
- bool isMarked;
+ // A position that can be used to store a certain position within the block.
+ storm::storage::sparse::state_type markedPosition;
- int myId;
+ // The ID of the block. This is only used for debugging purposes.
+ std::size_t id;
};
class Partition {
public:
+ friend class Block;
+
/*!
* Creates a partition with one block consisting of all the states.
*/
@@ -73,6 +174,87 @@ namespace storm {
*/
void splitLabel(storm::storage::BitVector const& statesWithLabel);
+ // Retrieves the size of the partition, i.e. the number of blocks.
+ std::size_t size() const;
+
+ // Prints the partition to the standard output.
+ void print() const;
+
+ // Splits the block at the given position and inserts a new block after the current one holding the rest
+ // of the states.
+ Block& splitBlock(Block& block, storm::storage::sparse::state_type position);
+
+ // Inserts a block before the given block. The new block will cover all states between the beginning
+ // of the given block and the end of the previous block.
+ Block& insertBlock(Block& block);
+
+ // Retrieves the blocks of the partition.
+ std::list<Block> const& getBlocks() const;
+
+ // Retrieves the blocks of the partition.
+ std::list<Block>& getBlocks();
+
+ // Retrieves the vector of all the states.
+ std::vector<storm::storage::sparse::state_type>& getStates();
+
+ // Checks the partition for internal consistency.
+ bool check() const;
+
+ // Returns an iterator to the beginning of the states of the given block.
+ std::vector<storm::storage::sparse::state_type>::iterator getBeginOfStates(Block const& block);
+
+ // Returns an iterator to the beginning of the states of the given block.
+ std::vector<storm::storage::sparse::state_type>::iterator getEndOfStates(Block const& block);
+
+ // Returns an iterator to the beginning of the states of the given block.
+ std::vector<storm::storage::sparse::state_type>::const_iterator getBeginOfStates(Block const& block) const;
+
+ // Returns an iterator to the beginning of the states of the given block.
+ std::vector<storm::storage::sparse::state_type>::const_iterator getEndOfStates(Block const& block) const;
+
+ // Returns an iterator to the beginning of the states of the given block.
+ typename std::vector<ValueType>::iterator getBeginOfValues(Block const& block);
+
+ // Returns an iterator to the beginning of the states of the given block.
+ typename std::vector<ValueType>::iterator getEndOfValues(Block const& block);
+
+ // Swaps the positions of the two given states.
+ void swapStates(storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2);
+
+ // Swaps the positions of the two states given by their positions.
+ void swapStatesAtPositions(storm::storage::sparse::state_type position1, storm::storage::sparse::state_type position2);
+
+ // Retrieves the block of the given state.
+ Block& getBlock(storm::storage::sparse::state_type state);
+
+ // Retrieves the position of the given state.
+ storm::storage::sparse::state_type const& getPosition(storm::storage::sparse::state_type state) const;
+
+ // Retrieves the position of the given state.
+ void setPosition(storm::storage::sparse::state_type state, storm::storage::sparse::state_type position);
+
+ // Sets the position of the state to the given position.
+ storm::storage::sparse::state_type const& getState(storm::storage::sparse::state_type position) const;
+
+ // Retrieves the value for the given state.
+ ValueType const& getValue(storm::storage::sparse::state_type state) const;
+
+ // Retrieves the value at the given position.
+ ValueType const& getValueAtPosition(storm::storage::sparse::state_type position) const;
+
+ // Sets the given value for the given state.
+ void setValue(storm::storage::sparse::state_type state, ValueType value);
+
+ // Retrieves the vector with the probabilities going into the current splitter.
+ std::vector<ValueType>& getValues();
+
+ // Increases the value for the given state by the specified amount.
+ void increaseValue(storm::storage::sparse::state_type state, ValueType value);
+
+ // Updates the block mapping for the given range of states to the specified block.
+ void updateBlockMapping(Block& block, std::vector<storm::storage::sparse::state_type>::iterator first, std::vector<storm::storage::sparse::state_type>::iterator end);
+
+ private:
// The list of blocks in the partition.
std::list<Block> blocks;
@@ -88,17 +270,13 @@ namespace storm {
// This vector stores the probabilities of going to the current splitter.
std::vector<ValueType> values;
-
- std::size_t size() const;
-
- void print() const;
};
void computeBisimulationEquivalenceClasses(storm::models::Dtmc<ValueType> const& model, bool weak);
- std::size_t splitPartition(storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Block const& splitter, Partition& partition, std::deque<Block*>& splitterQueue);
+ std::size_t splitPartition(storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Block& splitter, Partition& partition, std::deque<Block*>& splitterQueue);
- std::size_t splitBlockProbabilities(Block* block, Partition& partition, std::deque<Block*>& splitterQueue);
+ std::size_t splitBlockProbabilities(Block& block, Partition& partition, std::deque<Block*>& splitterQueue);
};
}
}
From bc43ce52ab25c5548d77fe1dfc14532d0a88baec Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Sun, 12 Oct 2014 22:51:33 +0200
Subject: [PATCH 10/14] Eliminated two bugs, more to come.
Former-commit-id: 3ea21c66b946aae54cf62990d8f3e9687d2c0c15
---
src/storage/BisimulationDecomposition.cpp | 2 +-
src/storage/BisimulationDecomposition2.cpp | 26 +++++++++++++---------
src/utility/cli.h | 2 +-
3 files changed, 18 insertions(+), 12 deletions(-)
diff --git a/src/storage/BisimulationDecomposition.cpp b/src/storage/BisimulationDecomposition.cpp
index 342914601..0d7abc44a 100644
--- a/src/storage/BisimulationDecomposition.cpp
+++ b/src/storage/BisimulationDecomposition.cpp
@@ -16,7 +16,7 @@ namespace storm {
std::chrono::high_resolution_clock::time_point totalStart = std::chrono::high_resolution_clock::now();
// We start by computing the initial partition. In particular, we also keep a mapping of states to their blocks.
std::vector<std::size_t> stateToBlockMapping(dtmc.getNumberOfStates());
- storm::storage::BitVector labeledStates = dtmc.getLabeledStates("observe0Greater1");
+ storm::storage::BitVector labeledStates = dtmc.getLabeledStates("elected");
this->blocks.emplace_back(labeledStates.begin(), labeledStates.end());
std::for_each(labeledStates.begin(), labeledStates.end(), [&] (storm::storage::sparse::state_type const& state) { stateToBlockMapping[state] = 0; } );
labeledStates.complement();
diff --git a/src/storage/BisimulationDecomposition2.cpp b/src/storage/BisimulationDecomposition2.cpp
index abda69f66..38d02ae90 100644
--- a/src/storage/BisimulationDecomposition2.cpp
+++ b/src/storage/BisimulationDecomposition2.cpp
@@ -11,7 +11,7 @@ namespace storm {
static std::size_t globalId = 0;
template<typename ValueType>
- BisimulationDecomposition2<ValueType>::Block::Block(storm::storage::sparse::state_type begin, storm::storage::sparse::state_type end, Block* prev, Block* next) : next(next), prev(prev), begin(begin), end(end), markedAsSplitter(false), markedPosition(begin), id(globalId++) {
+ BisimulationDecomposition2<ValueType>::Block::Block(storm::storage::sparse::state_type begin, storm::storage::sparse::state_type end, Block* prev, Block* next) : next(next), prev(prev), begin(begin), end(end), markedAsSplitter(false), markedAsPredecessorBlock(false), markedPosition(begin), id(globalId++) {
if (next != nullptr) {
next->prev = this;
}
@@ -232,11 +232,10 @@ namespace storm {
template<typename ValueType>
void BisimulationDecomposition2<ValueType>::Partition::swapStates(storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2) {
- std::cout << "swapping states " << state1 << " and " << state2 << std::endl;
+ std::cout << "swapping states " << state1 << " and " << state2 << " at positions " << this->positions[state1] << " and " << this->positions[state2] << std::endl;
std::swap(this->states[this->positions[state1]], this->states[this->positions[state2]]);
std::swap(this->values[this->positions[state1]], this->values[this->positions[state2]]);
std::swap(this->positions[state1], this->positions[state2]);
- assert(this->check());
}
template<typename ValueType>
@@ -252,7 +251,6 @@ namespace storm {
this->positions[state2] = position1;
std::cout << "pos of " << state1 << " is now " << position2 << " and pos of " << state2 << " is now " << position1 << std::endl;
std::cout << this->states[position1] << " vs " << state2 << " and " << this->states[position2] << " vs " << state1 << std::endl;
- assert(this->check());
}
template<typename ValueType>
@@ -559,7 +557,7 @@ namespace storm {
// Now we can check whether the block needs to be split, which is the case iff the probabilities for the
// first and the last state are different.
std::size_t createdBlocks = 0;
- while (std::abs(partition.getValueAtPosition(beginIndex) - partition.getValueAtPosition(endIndex)) >= 1e-6) {
+ while (std::abs(partition.getValueAtPosition(beginIndex) - partition.getValueAtPosition(endIndex - 1)) >= 1e-6) {
// Now we scan for the first state in the block that disagrees on the probability value.
// Note that we do not have to check currentIndex for staying within bounds, because we know the matching
// state is within bounds.
@@ -575,9 +573,9 @@ namespace storm {
// Now we split the block and mark it as a potential splitter.
++createdBlocks;
Block& newBlock = partition.splitBlock(block, currentIndex);
- if (!newBlock.isMarkedAsPredecessor()) {
- newBlock.markAsSplitter();
+ if (!newBlock.isMarkedAsSplitter()) {
splitterQueue.push_back(&newBlock);
+ newBlock.markAsSplitter();
}
beginIndex = currentIndex;
}
@@ -658,8 +656,11 @@ namespace storm {
}
if (!predecessorBlock.isMarkedAsPredecessor()) {
+ std::cout << "not already in there" << std::endl;
predecessorBlocks.emplace_back(&predecessorBlock);
predecessorBlock.markAsPredecessorBlock();
+ } else {
+ std::cout << "already in there" << std::endl;
}
}
@@ -671,6 +672,8 @@ namespace storm {
}
}
+ std::cout << "(1)having " << predecessorBlocks.size() << " pred blocks " << std::endl;
+
// Now we can traverse the list of states of the splitter whose predecessors we have not yet explored.
for (auto stateIterator = partition.getStates().begin() + splitter.getOriginalBegin(), stateIte = partition.getStates().begin() + splitter.getMarkedPosition(); stateIterator != stateIte; ++stateIterator) {
storm::storage::sparse::state_type currentState = *stateIterator;
@@ -699,7 +702,7 @@ namespace storm {
std::list<Block*> blocksToSplit;
- std::cout << "having " << predecessorBlocks.size() << " pred blocks " << std::endl;
+ std::cout << "(2)having " << predecessorBlocks.size() << " pred blocks " << std::endl;
// Now, we can iterate over the predecessor blocks and see whether we have to create a new block for
// predecessors of the splitter.
@@ -714,9 +717,12 @@ namespace storm {
std::cout << "moved begin of block " << block.getId() << " to " << block.getBegin() << " and end to " << block.getEnd() << std::endl;
Block& newBlock = partition.insertBlock(block);
- std::cout << "created new block " << std::endl;
+ std::cout << "created new block " << newBlock.getId() << " from block " << block.getId() << std::endl;
newBlock.print(partition);
- splitterQueue.push_back(&newBlock);
+ if (!newBlock.isMarkedAsSplitter()) {
+ splitterQueue.push_back(&newBlock);
+ newBlock.markAsSplitter();
+ }
} else {
std::cout << "all states are predecessors" << std::endl;
diff --git a/src/utility/cli.h b/src/utility/cli.h
index 70d4e75af..6996736a4 100644
--- a/src/utility/cli.h
+++ b/src/utility/cli.h
@@ -261,7 +261,7 @@ namespace storm {
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<storm::models::Dtmc<double>> dtmc = result->template as<storm::models::Dtmc<double>>();
-// storm::storage::BisimulationDecomposition<double> bisimulationDecomposition(*dtmc);
+ storm::storage::BisimulationDecomposition<double> bisimulationDecomposition(*dtmc);
storm::storage::BisimulationDecomposition2<double> bisimulationDecomposition2(*dtmc);
}
From 0e0027aa8e51ee9034681b4b5dacb8a66028d90b Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Mon, 13 Oct 2014 11:59:57 +0200
Subject: [PATCH 11/14] Further work on sparse bisimulation.
Former-commit-id: ba256b8b0a9c5e3f1a9a5870f4ef32af7fa18396
---
...inisticModelBisimulationDecomposition.cpp} | 273 +++++++++---------
...rministicModelBisimulationDecomposition.h} | 25 +-
...inisticModelBisimulationDecomposition.cpp} | 43 +--
...rministicModelBisimulationDecomposition.h} | 12 +-
src/utility/cli.h | 8 +-
5 files changed, 188 insertions(+), 173 deletions(-)
rename src/storage/{BisimulationDecomposition2.cpp => DeterministicModelBisimulationDecomposition.cpp} (66%)
rename src/storage/{BisimulationDecomposition2.h => DeterministicModelBisimulationDecomposition.h} (92%)
rename src/storage/{BisimulationDecomposition.cpp => NaiveDeterministicModelBisimulationDecomposition.cpp} (84%)
rename src/storage/{BisimulationDecomposition.h => NaiveDeterministicModelBisimulationDecomposition.h} (74%)
diff --git a/src/storage/BisimulationDecomposition2.cpp b/src/storage/DeterministicModelBisimulationDecomposition.cpp
similarity index 66%
rename from src/storage/BisimulationDecomposition2.cpp
rename to src/storage/DeterministicModelBisimulationDecomposition.cpp
index 38d02ae90..144560557 100644
--- a/src/storage/BisimulationDecomposition2.cpp
+++ b/src/storage/DeterministicModelBisimulationDecomposition.cpp
@@ -1,4 +1,4 @@
-#include "src/storage/BisimulationDecomposition2.h"
+#include "src/storage/DeterministicModelBisimulationDecomposition.h"
#include <algorithm>
#include <unordered_map>
@@ -11,7 +11,7 @@ namespace storm {
static std::size_t globalId = 0;
template<typename ValueType>
- BisimulationDecomposition2<ValueType>::Block::Block(storm::storage::sparse::state_type begin, storm::storage::sparse::state_type end, Block* prev, Block* next) : next(next), prev(prev), begin(begin), end(end), markedAsSplitter(false), markedAsPredecessorBlock(false), markedPosition(begin), id(globalId++) {
+ DeterministicModelBisimulationDecomposition<ValueType>::Block::Block(storm::storage::sparse::state_type begin, storm::storage::sparse::state_type end, Block* prev, Block* next) : next(next), prev(prev), begin(begin), end(end), markedAsSplitter(false), markedAsPredecessorBlock(false), markedPosition(begin), id(globalId++) {
if (next != nullptr) {
next->prev = this;
}
@@ -21,8 +21,8 @@ namespace storm {
}
template<typename ValueType>
- void BisimulationDecomposition2<ValueType>::Block::print(Partition const& partition) const {
- std::cout << "block " << this->getId() << " with marked position " << this->getMarkedPosition() << std::endl;
+ void DeterministicModelBisimulationDecomposition<ValueType>::Block::print(Partition const& partition) const {
+ std::cout << "block " << this->getId() << " with marked position " << this->getMarkedPosition() << " and original begin " << this->getOriginalBegin() << std::endl;
std::cout << "begin: " << this->begin << " and end: " << this->end << " (number of states: " << this->getNumberOfStates() << ")" << std::endl;
std::cout << "states:" << std::endl;
for (storm::storage::sparse::state_type index = this->begin; index < this->end; ++index) {
@@ -40,34 +40,33 @@ namespace storm {
}
template<typename ValueType>
- void BisimulationDecomposition2<ValueType>::Block::setBegin(storm::storage::sparse::state_type begin) {
+ void DeterministicModelBisimulationDecomposition<ValueType>::Block::setBegin(storm::storage::sparse::state_type begin) {
this->begin = begin;
this->markedPosition = begin;
}
template<typename ValueType>
- void BisimulationDecomposition2<ValueType>::Block::setEnd(storm::storage::sparse::state_type end) {
+ void DeterministicModelBisimulationDecomposition<ValueType>::Block::setEnd(storm::storage::sparse::state_type end) {
this->end = end;
}
template<typename ValueType>
- void BisimulationDecomposition2<ValueType>::Block::incrementBegin() {
+ void DeterministicModelBisimulationDecomposition<ValueType>::Block::incrementBegin() {
++this->begin;
- std::cout << "incremented begin to " << this->begin << std::endl;
}
template<typename ValueType>
- void BisimulationDecomposition2<ValueType>::Block::decrementEnd() {
+ void DeterministicModelBisimulationDecomposition<ValueType>::Block::decrementEnd() {
++this->begin;
}
template<typename ValueType>
- storm::storage::sparse::state_type BisimulationDecomposition2<ValueType>::Block::getBegin() const {
+ storm::storage::sparse::state_type DeterministicModelBisimulationDecomposition<ValueType>::Block::getBegin() const {
return this->begin;
}
template<typename ValueType>
- storm::storage::sparse::state_type BisimulationDecomposition2<ValueType>::Block::getOriginalBegin() const {
+ storm::storage::sparse::state_type DeterministicModelBisimulationDecomposition<ValueType>::Block::getOriginalBegin() const {
if (this->hasPreviousBlock()) {
return this->getPreviousBlock().getEnd();
} else {
@@ -76,74 +75,73 @@ namespace storm {
}
template<typename ValueType>
- storm::storage::sparse::state_type BisimulationDecomposition2<ValueType>::Block::getEnd() const {
+ storm::storage::sparse::state_type DeterministicModelBisimulationDecomposition<ValueType>::Block::getEnd() const {
return this->end;
}
template<typename ValueType>
- void BisimulationDecomposition2<ValueType>::Block::setIterator(const_iterator it) {
+ void DeterministicModelBisimulationDecomposition<ValueType>::Block::setIterator(const_iterator it) {
this->selfIt = it;
}
template<typename ValueType>
- typename BisimulationDecomposition2<ValueType>::Block::const_iterator BisimulationDecomposition2<ValueType>::Block::getIterator() const {
+ typename DeterministicModelBisimulationDecomposition<ValueType>::Block::const_iterator DeterministicModelBisimulationDecomposition<ValueType>::Block::getIterator() const {
return this->selfIt;
}
template<typename ValueType>
- typename BisimulationDecomposition2<ValueType>::Block::const_iterator BisimulationDecomposition2<ValueType>::Block::getNextIterator() const {
+ typename DeterministicModelBisimulationDecomposition<ValueType>::Block::const_iterator DeterministicModelBisimulationDecomposition<ValueType>::Block::getNextIterator() const {
return this->getNextBlock().getIterator();
}
template<typename ValueType>
- typename BisimulationDecomposition2<ValueType>::Block::const_iterator BisimulationDecomposition2<ValueType>::Block::getPreviousIterator() const {
+ typename DeterministicModelBisimulationDecomposition<ValueType>::Block::const_iterator DeterministicModelBisimulationDecomposition<ValueType>::Block::getPreviousIterator() const {
return this->getPreviousBlock().getIterator();
}
template<typename ValueType>
- typename BisimulationDecomposition2<ValueType>::Block& BisimulationDecomposition2<ValueType>::Block::getNextBlock() {
+ typename DeterministicModelBisimulationDecomposition<ValueType>::Block& DeterministicModelBisimulationDecomposition<ValueType>::Block::getNextBlock() {
return *this->next;
}
template<typename ValueType>
- typename BisimulationDecomposition2<ValueType>::Block const& BisimulationDecomposition2<ValueType>::Block::getNextBlock() const {
+ typename DeterministicModelBisimulationDecomposition<ValueType>::Block const& DeterministicModelBisimulationDecomposition<ValueType>::Block::getNextBlock() const {
return *this->next;
}
template<typename ValueType>
- bool BisimulationDecomposition2<ValueType>::Block::hasNextBlock() const {
+ bool DeterministicModelBisimulationDecomposition<ValueType>::Block::hasNextBlock() const {
return this->next != nullptr;
}
template<typename ValueType>
- typename BisimulationDecomposition2<ValueType>::Block& BisimulationDecomposition2<ValueType>::Block::getPreviousBlock() {
+ typename DeterministicModelBisimulationDecomposition<ValueType>::Block& DeterministicModelBisimulationDecomposition<ValueType>::Block::getPreviousBlock() {
return *this->prev;
}
template<typename ValueType>
- typename BisimulationDecomposition2<ValueType>::Block* BisimulationDecomposition2<ValueType>::Block::getPreviousBlockPointer() {
+ typename DeterministicModelBisimulationDecomposition<ValueType>::Block* DeterministicModelBisimulationDecomposition<ValueType>::Block::getPreviousBlockPointer() {
return this->prev;
}
template<typename ValueType>
- typename BisimulationDecomposition2<ValueType>::Block* BisimulationDecomposition2<ValueType>::Block::getNextBlockPointer() {
+ typename DeterministicModelBisimulationDecomposition<ValueType>::Block* DeterministicModelBisimulationDecomposition<ValueType>::Block::getNextBlockPointer() {
return this->next;
}
template<typename ValueType>
- typename BisimulationDecomposition2<ValueType>::Block const& BisimulationDecomposition2<ValueType>::Block::getPreviousBlock() const {
+ typename DeterministicModelBisimulationDecomposition<ValueType>::Block const& DeterministicModelBisimulationDecomposition<ValueType>::Block::getPreviousBlock() const {
return *this->prev;
}
template<typename ValueType>
- bool BisimulationDecomposition2<ValueType>::Block::hasPreviousBlock() const {
+ bool DeterministicModelBisimulationDecomposition<ValueType>::Block::hasPreviousBlock() const {
return this->prev != nullptr;
}
template<typename ValueType>
- bool BisimulationDecomposition2<ValueType>::Block::check() const {
+ bool DeterministicModelBisimulationDecomposition<ValueType>::Block::check() const {
if (this->begin >= this->end) {
- std::cout << "beg: " << this->begin << " and end " << this->end << std::endl;
assert(false);
}
if (this->prev != nullptr) {
@@ -156,68 +154,68 @@ namespace storm {
}
template<typename ValueType>
- std::size_t BisimulationDecomposition2<ValueType>::Block::getNumberOfStates() const {
+ std::size_t DeterministicModelBisimulationDecomposition<ValueType>::Block::getNumberOfStates() const {
// We need to take the original begin here, because the begin is temporarily moved.
return (this->end - this->getOriginalBegin());
}
template<typename ValueType>
- bool BisimulationDecomposition2<ValueType>::Block::isMarkedAsSplitter() const {
+ bool DeterministicModelBisimulationDecomposition<ValueType>::Block::isMarkedAsSplitter() const {
return this->markedAsSplitter;
}
template<typename ValueType>
- void BisimulationDecomposition2<ValueType>::Block::markAsSplitter() {
+ void DeterministicModelBisimulationDecomposition<ValueType>::Block::markAsSplitter() {
this->markedAsSplitter = true;
}
template<typename ValueType>
- void BisimulationDecomposition2<ValueType>::Block::unmarkAsSplitter() {
+ void DeterministicModelBisimulationDecomposition<ValueType>::Block::unmarkAsSplitter() {
this->markedAsSplitter = false;
}
template<typename ValueType>
- std::size_t BisimulationDecomposition2<ValueType>::Block::getId() const {
+ std::size_t DeterministicModelBisimulationDecomposition<ValueType>::Block::getId() const {
return this->id;
}
template<typename ValueType>
- storm::storage::sparse::state_type BisimulationDecomposition2<ValueType>::Block::getMarkedPosition() const {
+ storm::storage::sparse::state_type DeterministicModelBisimulationDecomposition<ValueType>::Block::getMarkedPosition() const {
return this->markedPosition;
}
template<typename ValueType>
- void BisimulationDecomposition2<ValueType>::Block::setMarkedPosition(storm::storage::sparse::state_type position) {
+ void DeterministicModelBisimulationDecomposition<ValueType>::Block::setMarkedPosition(storm::storage::sparse::state_type position) {
this->markedPosition = position;
}
template<typename ValueType>
- void BisimulationDecomposition2<ValueType>::Block::resetMarkedPosition() {
+ void DeterministicModelBisimulationDecomposition<ValueType>::Block::resetMarkedPosition() {
this->markedPosition = this->begin;
}
template<typename ValueType>
- void BisimulationDecomposition2<ValueType>::Block::incrementMarkedPosition() {
+ void DeterministicModelBisimulationDecomposition<ValueType>::Block::incrementMarkedPosition() {
++this->markedPosition;
}
template<typename ValueType>
- void BisimulationDecomposition2<ValueType>::Block::markAsPredecessorBlock() {
+ void DeterministicModelBisimulationDecomposition<ValueType>::Block::markAsPredecessorBlock() {
this->markedAsPredecessorBlock = true;
}
template<typename ValueType>
- void BisimulationDecomposition2<ValueType>::Block::unmarkAsPredecessorBlock() {
+ void DeterministicModelBisimulationDecomposition<ValueType>::Block::unmarkAsPredecessorBlock() {
this->markedAsPredecessorBlock = false;
}
template<typename ValueType>
- bool BisimulationDecomposition2<ValueType>::Block::isMarkedAsPredecessor() const {
+ bool DeterministicModelBisimulationDecomposition<ValueType>::Block::isMarkedAsPredecessor() const {
return markedAsPredecessorBlock;
}
template<typename ValueType>
- BisimulationDecomposition2<ValueType>::Partition::Partition(std::size_t numberOfStates) : stateToBlockMapping(numberOfStates), states(numberOfStates), positions(numberOfStates), values(numberOfStates) {
+ DeterministicModelBisimulationDecomposition<ValueType>::Partition::Partition(std::size_t numberOfStates) : stateToBlockMapping(numberOfStates), states(numberOfStates), positions(numberOfStates), values(numberOfStates) {
// Create the block and give it an iterator to itself.
typename std::list<Block>::iterator it = blocks.emplace(this->blocks.end(), 0, numberOfStates, nullptr, nullptr);
it->setIterator(it);
@@ -231,117 +229,110 @@ namespace storm {
}
template<typename ValueType>
- void BisimulationDecomposition2<ValueType>::Partition::swapStates(storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2) {
- std::cout << "swapping states " << state1 << " and " << state2 << " at positions " << this->positions[state1] << " and " << this->positions[state2] << std::endl;
+ void DeterministicModelBisimulationDecomposition<ValueType>::Partition::swapStates(storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2) {
std::swap(this->states[this->positions[state1]], this->states[this->positions[state2]]);
std::swap(this->values[this->positions[state1]], this->values[this->positions[state2]]);
std::swap(this->positions[state1], this->positions[state2]);
}
template<typename ValueType>
- void BisimulationDecomposition2<ValueType>::Partition::swapStatesAtPositions(storm::storage::sparse::state_type position1, storm::storage::sparse::state_type position2) {
+ void DeterministicModelBisimulationDecomposition<ValueType>::Partition::swapStatesAtPositions(storm::storage::sparse::state_type position1, storm::storage::sparse::state_type position2) {
storm::storage::sparse::state_type state1 = this->states[position1];
storm::storage::sparse::state_type state2 = this->states[position2];
- std::cout << "swapping states " << state1 << " and " << state2 << " at positions " << position1 << " and " << position2 << std::endl;
std::swap(this->states[position1], this->states[position2]);
std::swap(this->values[position1], this->values[position2]);
this->positions[state1] = position2;
this->positions[state2] = position1;
- std::cout << "pos of " << state1 << " is now " << position2 << " and pos of " << state2 << " is now " << position1 << std::endl;
- std::cout << this->states[position1] << " vs " << state2 << " and " << this->states[position2] << " vs " << state1 << std::endl;
}
template<typename ValueType>
- storm::storage::sparse::state_type const& BisimulationDecomposition2<ValueType>::Partition::getPosition(storm::storage::sparse::state_type state) const {
+ storm::storage::sparse::state_type const& DeterministicModelBisimulationDecomposition<ValueType>::Partition::getPosition(storm::storage::sparse::state_type state) const {
return this->positions[state];
}
template<typename ValueType>
- void BisimulationDecomposition2<ValueType>::Partition::setPosition(storm::storage::sparse::state_type state, storm::storage::sparse::state_type position) {
+ void DeterministicModelBisimulationDecomposition<ValueType>::Partition::setPosition(storm::storage::sparse::state_type state, storm::storage::sparse::state_type position) {
this->positions[state] = position;
}
template<typename ValueType>
- storm::storage::sparse::state_type const& BisimulationDecomposition2<ValueType>::Partition::getState(storm::storage::sparse::state_type position) const {
+ storm::storage::sparse::state_type const& DeterministicModelBisimulationDecomposition<ValueType>::Partition::getState(storm::storage::sparse::state_type position) const {
return this->states[position];
}
template<typename ValueType>
- ValueType const& BisimulationDecomposition2<ValueType>::Partition::getValue(storm::storage::sparse::state_type state) const {
+ ValueType const& DeterministicModelBisimulationDecomposition<ValueType>::Partition::getValue(storm::storage::sparse::state_type state) const {
return this->values[this->positions[state]];
}
template<typename ValueType>
- ValueType const& BisimulationDecomposition2<ValueType>::Partition::getValueAtPosition(storm::storage::sparse::state_type position) const {
+ ValueType const& DeterministicModelBisimulationDecomposition<ValueType>::Partition::getValueAtPosition(storm::storage::sparse::state_type position) const {
return this->values[position];
}
template<typename ValueType>
- void BisimulationDecomposition2<ValueType>::Partition::setValue(storm::storage::sparse::state_type state, ValueType value) {
+ void DeterministicModelBisimulationDecomposition<ValueType>::Partition::setValue(storm::storage::sparse::state_type state, ValueType value) {
this->values[this->positions[state]] = value;
}
template<typename ValueType>
- std::vector<ValueType>& BisimulationDecomposition2<ValueType>::Partition::getValues() {
+ std::vector<ValueType>& DeterministicModelBisimulationDecomposition<ValueType>::Partition::getValues() {
return this->values;
}
template<typename ValueType>
- void BisimulationDecomposition2<ValueType>::Partition::increaseValue(storm::storage::sparse::state_type state, ValueType value) {
+ void DeterministicModelBisimulationDecomposition<ValueType>::Partition::increaseValue(storm::storage::sparse::state_type state, ValueType value) {
this->values[this->positions[state]] += value;
}
template<typename ValueType>
- void BisimulationDecomposition2<ValueType>::Partition::updateBlockMapping(Block& block, std::vector<storm::storage::sparse::state_type>::iterator first, std::vector<storm::storage::sparse::state_type>::iterator last) {
+ void DeterministicModelBisimulationDecomposition<ValueType>::Partition::updateBlockMapping(Block& block, std::vector<storm::storage::sparse::state_type>::iterator first, std::vector<storm::storage::sparse::state_type>::iterator last) {
for (; first != last; ++first) {
this->stateToBlockMapping[*first] = █
}
}
template<typename ValueType>
- typename BisimulationDecomposition2<ValueType>::Block& BisimulationDecomposition2<ValueType>::Partition::getBlock(storm::storage::sparse::state_type state) {
+ typename DeterministicModelBisimulationDecomposition<ValueType>::Block& DeterministicModelBisimulationDecomposition<ValueType>::Partition::getBlock(storm::storage::sparse::state_type state) {
return *this->stateToBlockMapping[state];
}
template<typename ValueType>
- std::vector<storm::storage::sparse::state_type>::iterator BisimulationDecomposition2<ValueType>::Partition::getBeginOfStates(Block const& block) {
+ std::vector<storm::storage::sparse::state_type>::iterator DeterministicModelBisimulationDecomposition<ValueType>::Partition::getBeginOfStates(Block const& block) {
return this->states.begin() + block.getBegin();
}
template<typename ValueType>
- std::vector<storm::storage::sparse::state_type>::iterator BisimulationDecomposition2<ValueType>::Partition::getEndOfStates(Block const& block) {
+ std::vector<storm::storage::sparse::state_type>::iterator DeterministicModelBisimulationDecomposition<ValueType>::Partition::getEndOfStates(Block const& block) {
return this->states.begin() + block.getEnd();
}
template<typename ValueType>
- std::vector<storm::storage::sparse::state_type>::const_iterator BisimulationDecomposition2<ValueType>::Partition::getBeginOfStates(Block const& block) const {
+ std::vector<storm::storage::sparse::state_type>::const_iterator DeterministicModelBisimulationDecomposition<ValueType>::Partition::getBeginOfStates(Block const& block) const {
return this->states.begin() + block.getBegin();
}
template<typename ValueType>
- std::vector<storm::storage::sparse::state_type>::const_iterator BisimulationDecomposition2<ValueType>::Partition::getEndOfStates(Block const& block) const {
+ std::vector<storm::storage::sparse::state_type>::const_iterator DeterministicModelBisimulationDecomposition<ValueType>::Partition::getEndOfStates(Block const& block) const {
return this->states.begin() + block.getEnd();
}
template<typename ValueType>
- typename std::vector<ValueType>::iterator BisimulationDecomposition2<ValueType>::Partition::getBeginOfValues(Block const& block) {
+ typename std::vector<ValueType>::iterator DeterministicModelBisimulationDecomposition<ValueType>::Partition::getBeginOfValues(Block const& block) {
return this->values.begin() + block.getBegin();
}
template<typename ValueType>
- typename std::vector<ValueType>::iterator BisimulationDecomposition2<ValueType>::Partition::getEndOfValues(Block const& block) {
+ typename std::vector<ValueType>::iterator DeterministicModelBisimulationDecomposition<ValueType>::Partition::getEndOfValues(Block const& block) {
return this->values.begin() + block.getEnd();
}
template<typename ValueType>
- typename BisimulationDecomposition2<ValueType>::Block& BisimulationDecomposition2<ValueType>::Partition::splitBlock(Block& block, storm::storage::sparse::state_type position) {
+ typename DeterministicModelBisimulationDecomposition<ValueType>::Block& DeterministicModelBisimulationDecomposition<ValueType>::Partition::splitBlock(Block& block, storm::storage::sparse::state_type position) {
// FIXME: this could be improved by splitting off the smaller of the two resulting blocks.
- std::cout << "splitting block (" << block.getBegin() << "," << block.getEnd() << ") at position " << position << std::endl;
- block.print(*this);
-
// In case one of the resulting blocks would be empty, we simply return the current block and do not create
// a new one.
if (position == block.getBegin() || position == block.getEnd()) {
@@ -350,16 +341,12 @@ namespace storm {
// Actually create the new block and insert it at the correct position.
typename std::list<Block>::iterator selfIt = this->blocks.emplace(block.getIterator(), block.getBegin(), position, block.getPreviousBlockPointer(), &block);
- std::cout << "created new block from " << block.getBegin() << " to " << position << std::endl;
selfIt->setIterator(selfIt);
Block& newBlock = *selfIt;
// Make the current block end at the given position.
block.setBegin(position);
- std::cout << "old block: " << std::endl;
- block.print(*this);
-
// Update the mapping of the states in the newly created block.
for (auto it = this->getBeginOfStates(newBlock), ite = this->getEndOfStates(newBlock); it != ite; ++it) {
stateToBlockMapping[*it] = &newBlock;
@@ -369,13 +356,11 @@ namespace storm {
}
template<typename ValueType>
- typename BisimulationDecomposition2<ValueType>::Block& BisimulationDecomposition2<ValueType>::Partition::insertBlock(Block& block) {
+ typename DeterministicModelBisimulationDecomposition<ValueType>::Block& DeterministicModelBisimulationDecomposition<ValueType>::Partition::insertBlock(Block& block) {
// Find the beginning of the new block.
storm::storage::sparse::state_type begin;
if (block.hasPreviousBlock()) {
begin = block.getPreviousBlock().getEnd();
- std::cout << "previous block ended at " << begin << std::endl;
- block.getPreviousBlock().print(*this);
} else {
begin = 0;
}
@@ -394,7 +379,7 @@ namespace storm {
}
template<typename ValueType>
- void BisimulationDecomposition2<ValueType>::Partition::splitLabel(storm::storage::BitVector const& statesWithLabel) {
+ void DeterministicModelBisimulationDecomposition<ValueType>::Partition::splitLabel(storm::storage::BitVector const& statesWithLabel) {
for (auto blockIterator = this->blocks.begin(), ite = this->blocks.end(); blockIterator != ite; ) { // The update of the loop was intentionally moved to the bottom of the loop.
Block& block = *blockIterator;
@@ -422,22 +407,22 @@ namespace storm {
}
template<typename ValueType>
- std::list<typename BisimulationDecomposition2<ValueType>::Block> const& BisimulationDecomposition2<ValueType>::Partition::getBlocks() const {
+ std::list<typename DeterministicModelBisimulationDecomposition<ValueType>::Block> const& DeterministicModelBisimulationDecomposition<ValueType>::Partition::getBlocks() const {
return this->blocks;
}
template<typename ValueType>
- std::vector<storm::storage::sparse::state_type>& BisimulationDecomposition2<ValueType>::Partition::getStates() {
+ std::vector<storm::storage::sparse::state_type>& DeterministicModelBisimulationDecomposition<ValueType>::Partition::getStates() {
return this->states;
}
template<typename ValueType>
- std::list<typename BisimulationDecomposition2<ValueType>::Block>& BisimulationDecomposition2<ValueType>::Partition::getBlocks() {
+ std::list<typename DeterministicModelBisimulationDecomposition<ValueType>::Block>& DeterministicModelBisimulationDecomposition<ValueType>::Partition::getBlocks() {
return this->blocks;
}
template<typename ValueType>
- bool BisimulationDecomposition2<ValueType>::Partition::check() const {
+ bool DeterministicModelBisimulationDecomposition<ValueType>::Partition::check() const {
for (uint_fast64_t state = 0; state < this->positions.size(); ++state) {
if (this->states[this->positions[state]] != state) {
assert(false);
@@ -447,7 +432,6 @@ namespace storm {
assert(block.check());
for (auto stateIt = this->getBeginOfStates(block), stateIte = this->getEndOfStates(block); stateIt != stateIte; ++stateIt) {
if (this->stateToBlockMapping[*stateIt] != &block) {
- std::cout << "state " << *stateIt << " has wrong block mapping " << this->stateToBlockMapping[*stateIt] << " (should have " << &block << ")" << std::endl;
assert(false);
}
}
@@ -456,7 +440,7 @@ namespace storm {
}
template<typename ValueType>
- void BisimulationDecomposition2<ValueType>::Partition::print() const {
+ void DeterministicModelBisimulationDecomposition<ValueType>::Partition::print() const {
for (auto const& block : this->blocks) {
block.print(*this);
}
@@ -478,27 +462,60 @@ namespace storm {
}
template<typename ValueType>
- std::size_t BisimulationDecomposition2<ValueType>::Partition::size() const {
- int counter = 0;
- for (auto const& element : blocks) {
- ++counter;
- }
- std::cout << "found " << counter << " elements" << std::endl;
+ std::size_t DeterministicModelBisimulationDecomposition<ValueType>::Partition::size() const {
return this->blocks.size();
}
template<typename ValueType>
- BisimulationDecomposition2<ValueType>::BisimulationDecomposition2(storm::models::Dtmc<ValueType> const& dtmc, bool weak) {
+ DeterministicModelBisimulationDecomposition<ValueType>::DeterministicModelBisimulationDecomposition(storm::models::Dtmc<ValueType> const& dtmc, bool weak) : model(dtmc), initialBlocks() {
computeBisimulationEquivalenceClasses(dtmc, weak);
}
template<typename ValueType>
- void BisimulationDecomposition2<ValueType>::computeBisimulationEquivalenceClasses(storm::models::Dtmc<ValueType> const& dtmc, bool weak) {
+ std::shared_ptr<storm::models::AbstractDeterministicModel<ValueType>> DeterministicModelBisimulationDecomposition<ValueType>::getQuotient() const {
+ // In order to create the quotient model, we need to construct
+ // (a) the new transition matrix,
+ // (b) the new labeling,
+ // (c) the new reward structures.
+
+ // Prepare a matrix builder for (a).
+ storm::storage::SparseMatrixBuilder<ValueType> builder;
+
+ // Prepare the new state labeling for (b).
+ storm::models::AtomicPropositionsLabeling newLabeling(this->size(), model.getStateLabeling().getNumberOfAtomicPropositions());
+ std::set<std::string> atomicPropositionsSet = model.getStateLabeling().getAtomicPropositions();
+ std::vector<std::string> atomicPropositions = std::vector<std::string>(atomicPropositionsSet.begin(), atomicPropositionsSet.end());
+ for (auto const& ap : atomicPropositions) {
+ newLabeling.addAtomicProposition(ap);
+ }
+
+ // Now build (a) and (b) by traversing all blocks.
+ for (uint_fast64_t blockIndex = 0; blockIndex < this->blocks.size(); ++blockIndex) {
+ auto const& block = this->blocks[blockIndex];
+
+ // 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
+
+ // Add all atomic propositions to the equivalence class that the representative state satisfies.
+ for (auto const& ap : atomicPropositions) {
+ if (model.getStateLabeling().getStateHasAtomicProposition(ap, representativeState)) {
+ newLabeling.addAtomicPropositionToState(ap, blockIndex);
+ }
+ }
+ }
+
+
+ return nullptr;
+ }
+
+ template<typename ValueType>
+ void DeterministicModelBisimulationDecomposition<ValueType>::computeBisimulationEquivalenceClasses(storm::models::Dtmc<ValueType> const& dtmc, bool weak) {
std::chrono::high_resolution_clock::time_point totalStart = std::chrono::high_resolution_clock::now();
// We start by computing the initial partition.
Partition partition(dtmc.getNumberOfStates());
- partition.print();
for (auto const& label : dtmc.getStateLabeling().getAtomicPropositions()) {
if (label == "init") {
continue;
@@ -506,37 +523,47 @@ namespace storm {
partition.splitLabel(dtmc.getLabeledStates(label));
}
- std::cout << "initial partition:" << std::endl;
- partition.print();
- assert(partition.check());
-
// Initially, all blocks are potential splitter, so we insert them in the splitterQueue.
std::deque<Block*> splitterQueue;
std::for_each(partition.getBlocks().begin(), partition.getBlocks().end(), [&] (Block& a) { splitterQueue.push_back(&a); });
+ // FIXME: if weak is set, we want to eliminate the self-loops before doing bisimulation.
+
storm::storage::SparseMatrix<ValueType> backwardTransitions = dtmc.getBackwardTransitions();
// Then perform the actual splitting until there are no more splitters.
while (!splitterQueue.empty()) {
splitPartition(backwardTransitions, *splitterQueue.front(), partition, splitterQueue);
splitterQueue.pop_front();
-
- std::cout << "####### updated partition ##############" << std::endl;
- partition.print();
- std::cout << "####### end of updated partition #######" << std::endl;
}
- std::cout << "computed a quotient of size " << partition.size() << std::endl;
+ // 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));
+ }
+
+ // FIXME: as we will drop the state-to-block-mapping, we need to create the distribution of each block now.
+
+ // Now check which of the blocks of the partition contain at least one initial state.
+ for (auto initialState : model.getInitialStates()) {
+ Block& initialBlock = partition.getBlock(initialState);
+ if (std::find(this->initialBlocks.begin(), this->initialBlocks.end(), initialBlock.getId()) == this->initialBlocks.end()) {
+ this->initialBlocks.emplace_back(initialBlock.getId());
+ }
+ }
+ std::sort(this->initialBlocks.begin(), this->initialBlocks.end());
std::chrono::high_resolution_clock::duration totalTime = std::chrono::high_resolution_clock::now() - totalStart;
- std::cout << "Bisimulation took " << std::chrono::duration_cast<std::chrono::milliseconds>(totalTime).count() << "ms." << std::endl;
+
+ if (storm::settings::generalSettings().isShowStatisticsSet()) {
+ std::cout << "Computed bisimulation quotient in " << std::chrono::duration_cast<std::chrono::milliseconds>(totalTime).count() << "ms." << std::endl;
+ }
}
template<typename ValueType>
- std::size_t BisimulationDecomposition2<ValueType>::splitBlockProbabilities(Block& block, Partition& partition, std::deque<Block*>& splitterQueue) {
- std::cout << "part before split prob" << std::endl;
- partition.print();
-
+ std::size_t DeterministicModelBisimulationDecomposition<ValueType>::splitBlockProbabilities(Block& block, Partition& partition, std::deque<Block*>& splitterQueue) {
// Sort the states in the block based on their probabilities.
std::sort(partition.getBeginOfStates(block), partition.getEndOfStates(block), [&partition] (storm::storage::sparse::state_type const& a, storm::storage::sparse::state_type const& b) { return partition.getValue(a) < partition.getValue(b); } );
@@ -580,37 +607,23 @@ namespace storm {
beginIndex = currentIndex;
}
- assert(partition.check());
-
return createdBlocks;
}
template<typename ValueType>
- std::size_t BisimulationDecomposition2<ValueType>::splitPartition(storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Block& splitter, Partition& partition, std::deque<Block*>& splitterQueue) {
- std::cout << "treating block " << splitter.getId() << " as splitter" << std::endl;
- splitter.print(partition);
-
+ std::size_t DeterministicModelBisimulationDecomposition<ValueType>::splitPartition(storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Block& splitter, Partition& partition, std::deque<Block*>& splitterQueue) {
std::list<Block*> predecessorBlocks;
// Iterate over all states of the splitter and check its predecessors.
storm::storage::sparse::state_type currentPosition = splitter.getBegin();
for (auto stateIterator = partition.getBeginOfStates(splitter), stateIte = partition.getEndOfStates(splitter); stateIterator != stateIte; ++stateIterator, ++currentPosition) {
- std::cout << "states -----" << std::endl;
- for (auto stateIterator = partition.getStates().begin() + splitter.getOriginalBegin(), stateIte = partition.getStates().begin() + splitter.getEnd(); stateIterator != stateIte; ++stateIterator) {
- std::cout << *stateIterator << " ";
- }
- std::cout << std::endl;
-
storm::storage::sparse::state_type currentState = *stateIterator;
- std::cout << "current state " << currentState << " at pos " << currentPosition << std::endl;
uint_fast64_t elementsToSkip = 0;
for (auto const& predecessorEntry : backwardTransitions.getRow(currentState)) {
storm::storage::sparse::state_type predecessor = predecessorEntry.getColumn();
- std::cout << "found predecessor " << predecessor << " of state " << currentState << std::endl;
Block& predecessorBlock = partition.getBlock(predecessor);
- std::cout << "predecessor block " << predecessorBlock.getId() << std::endl;
// If the predecessor block has just one state, there is no point in splitting it.
if (predecessorBlock.getNumberOfStates() <= 1) {
@@ -625,11 +638,10 @@ namespace storm {
// If the predecessor we just found was already processed (in terms of visiting its predecessors),
// we swap it with the state that is currently at the beginning of the block and move the start
// of the block one step further.
- if (predecessorPosition <= currentPosition) {
+ if (predecessorPosition <= currentPosition + elementsToSkip) {
partition.swapStates(predecessor, partition.getState(predecessorBlock.getBegin()));
predecessorBlock.incrementBegin();
} else {
- std::cout << "current position is " << currentPosition << std::endl;
// Otherwise, we need to move the predecessor, but we need to make sure that we explore its
// predecessors later.
if (predecessorBlock.getMarkedPosition() == predecessorBlock.getBegin()) {
@@ -656,24 +668,18 @@ namespace storm {
}
if (!predecessorBlock.isMarkedAsPredecessor()) {
- std::cout << "not already in there" << std::endl;
predecessorBlocks.emplace_back(&predecessorBlock);
predecessorBlock.markAsPredecessorBlock();
- } else {
- std::cout << "already in there" << std::endl;
}
}
// If we had to move some elements beyond the current element, we may have to skip them.
if (elementsToSkip > 0) {
- std::cout << "skipping " << elementsToSkip << " elements" << std::endl;
stateIterator += elementsToSkip;
currentPosition += elementsToSkip;
}
}
- std::cout << "(1)having " << predecessorBlocks.size() << " pred blocks " << std::endl;
-
// Now we can traverse the list of states of the splitter whose predecessors we have not yet explored.
for (auto stateIterator = partition.getStates().begin() + splitter.getOriginalBegin(), stateIte = partition.getStates().begin() + splitter.getMarkedPosition(); stateIterator != stateIte; ++stateIterator) {
storm::storage::sparse::state_type currentState = *stateIterator;
@@ -698,12 +704,11 @@ namespace storm {
}
}
+ // Reset the marked position of the splitter to the begin.
splitter.setMarkedPosition(splitter.getBegin());
std::list<Block*> blocksToSplit;
- std::cout << "(2)having " << predecessorBlocks.size() << " pred blocks " << std::endl;
-
// Now, we can iterate over the predecessor blocks and see whether we have to create a new block for
// predecessors of the splitter.
for (auto blockPtr : predecessorBlocks) {
@@ -714,30 +719,24 @@ namespace storm {
// If we have moved the begin of the block to somewhere in the middle of the block, we need to split it.
if (block.getBegin() != block.getEnd()) {
- std::cout << "moved begin of block " << block.getId() << " to " << block.getBegin() << " and end to " << block.getEnd() << std::endl;
-
Block& newBlock = partition.insertBlock(block);
- std::cout << "created new block " << newBlock.getId() << " from block " << block.getId() << std::endl;
- newBlock.print(partition);
if (!newBlock.isMarkedAsSplitter()) {
splitterQueue.push_back(&newBlock);
newBlock.markAsSplitter();
}
- } else {
- std::cout << "all states are predecessors" << std::endl;
+ // Schedule the block of predecessors for refinement based on probabilities.
+ blocksToSplit.emplace_back(&newBlock);
+ } else {
// In this case, we can keep the block by setting its begin to the old value.
block.setBegin(block.getOriginalBegin());
blocksToSplit.emplace_back(&block);
}
}
- assert(partition.check());
-
// Finally, we walk through the blocks that have a transition to the splitter and split them using
// probabilistic information.
for (auto blockPtr : blocksToSplit) {
- std::cout << "block to split: " << blockPtr->getId() << std::endl;
if (blockPtr->getNumberOfStates() <= 1) {
continue;
}
@@ -748,6 +747,6 @@ namespace storm {
return 0;
}
- template class BisimulationDecomposition2<double>;
+ template class DeterministicModelBisimulationDecomposition<double>;
}
}
\ No newline at end of file
diff --git a/src/storage/BisimulationDecomposition2.h b/src/storage/DeterministicModelBisimulationDecomposition.h
similarity index 92%
rename from src/storage/BisimulationDecomposition2.h
rename to src/storage/DeterministicModelBisimulationDecomposition.h
index 50153d4b5..a595d7c28 100644
--- a/src/storage/BisimulationDecomposition2.h
+++ b/src/storage/DeterministicModelBisimulationDecomposition.h
@@ -1,5 +1,5 @@
-#ifndef STORM_STORAGE_BISIMULATIONDECOMPOSITION2_H_
-#define STORM_STORAGE_BISIMULATIONDECOMPOSITION2_H_
+#ifndef STORM_STORAGE_DETERMINISTICMODELBISIMULATIONDECOMPOSITION_H_
+#define STORM_STORAGE_DETERMINISTICMODELBISIMULATIONDECOMPOSITION_H_
#include <queue>
#include <deque>
@@ -16,14 +16,19 @@ namespace storm {
* This class represents the decomposition model into its bisimulation quotient.
*/
template <typename ValueType>
- class BisimulationDecomposition2 : public Decomposition<StateBlock> {
+ class DeterministicModelBisimulationDecomposition : public Decomposition<StateBlock> {
public:
- BisimulationDecomposition2() = default;
-
/*!
* Decomposes the given DTMC into equivalence classes under weak or strong bisimulation.
*/
- BisimulationDecomposition2(storm::models::Dtmc<ValueType> const& model, bool weak = false);
+ DeterministicModelBisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, bool weak = false);
+
+ /*!
+ * Retrieves the quotient of the model under the previously computed bisimulation.
+ *
+ * @return The quotient model.
+ */
+ std::shared_ptr<storm::models::AbstractDeterministicModel<ValueType>> getQuotient() const;
private:
class Partition;
@@ -277,8 +282,14 @@ namespace storm {
std::size_t splitPartition(storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Block& splitter, Partition& partition, std::deque<Block*>& splitterQueue);
std::size_t splitBlockProbabilities(Block& block, Partition& partition, std::deque<Block*>& splitterQueue);
+
+ // The model for which the bisimulation is computed.
+ storm::models::Dtmc<ValueType> const& model;
+
+ // The indices of all blocks that hold one or more initial states.
+ std::vector<storm::storage::sparse::state_type> initialBlocks;
};
}
}
-#endif /* STORM_STORAGE_BISIMULATIONDECOMPOSITION2_H_ */
\ No newline at end of file
+#endif /* STORM_STORAGE_DETERMINISTICMODELBISIMULATIONDECOMPOSITION_H_ */
\ No newline at end of file
diff --git a/src/storage/BisimulationDecomposition.cpp b/src/storage/NaiveDeterministicModelBisimulationDecomposition.cpp
similarity index 84%
rename from src/storage/BisimulationDecomposition.cpp
rename to src/storage/NaiveDeterministicModelBisimulationDecomposition.cpp
index 0d7abc44a..bf41414de 100644
--- a/src/storage/BisimulationDecomposition.cpp
+++ b/src/storage/NaiveDeterministicModelBisimulationDecomposition.cpp
@@ -1,4 +1,4 @@
-#include "src/storage/BisimulationDecomposition.h"
+#include "src/storage/NaiveDeterministicModelBisimulationDecomposition.h"
#include <unordered_map>
#include <chrono>
@@ -7,22 +7,26 @@ namespace storm {
namespace storage {
template<typename ValueType>
- BisimulationDecomposition<ValueType>::BisimulationDecomposition(storm::models::Dtmc<ValueType> const& dtmc, bool weak) {
+ NaiveDeterministicModelBisimulationDecomposition<ValueType>::NaiveDeterministicModelBisimulationDecomposition(storm::models::Dtmc<ValueType> const& dtmc, bool weak) {
computeBisimulationEquivalenceClasses(dtmc, weak);
}
template<typename ValueType>
- void BisimulationDecomposition<ValueType>::computeBisimulationEquivalenceClasses(storm::models::Dtmc<ValueType> const& dtmc, bool weak) {
+ void NaiveDeterministicModelBisimulationDecomposition<ValueType>::computeBisimulationEquivalenceClasses(storm::models::Dtmc<ValueType> const& dtmc, bool weak) {
std::chrono::high_resolution_clock::time_point totalStart = std::chrono::high_resolution_clock::now();
// We start by computing the initial partition. In particular, we also keep a mapping of states to their blocks.
std::vector<std::size_t> stateToBlockMapping(dtmc.getNumberOfStates());
- storm::storage::BitVector labeledStates = dtmc.getLabeledStates("elected");
+ storm::storage::BitVector labeledStates = dtmc.getLabeledStates("observe0Greater1");
this->blocks.emplace_back(labeledStates.begin(), labeledStates.end());
std::for_each(labeledStates.begin(), labeledStates.end(), [&] (storm::storage::sparse::state_type const& state) { stateToBlockMapping[state] = 0; } );
labeledStates.complement();
this->blocks.emplace_back(labeledStates.begin(), labeledStates.end());
std::for_each(labeledStates.begin(), labeledStates.end(), [&] (storm::storage::sparse::state_type const& state) { stateToBlockMapping[state] = 1; } );
+ // Check whether any of the blocks is empty and remove it.
+ auto eraseIterator = std::remove_if(this->blocks.begin(), this->blocks.end(), [] (typename NaiveDeterministicModelBisimulationDecomposition<ValueType>::block_type const& a) { return a.empty(); });
+ this->blocks.erase(eraseIterator, this->blocks.end());
+
// Create empty distributions for the two initial blocks.
std::vector<storm::storage::Distribution<ValueType>> distributions(2);
@@ -33,8 +37,9 @@ namespace storm {
// is the ID of the parent block of the splitter and the second entry is the block ID of the splitter itself.
std::deque<std::size_t> refinementQueue;
storm::storage::BitVector blocksInRefinementQueue(this->size());
- refinementQueue.push_back(0);
- refinementQueue.push_back(1);
+ for (uint_fast64_t index = 0; index < this->blocks.size(); ++index) {
+ refinementQueue.push_back(index);
+ }
// As long as there are blocks to refine, well, refine them.
uint_fast64_t iteration = 0;
@@ -50,24 +55,22 @@ namespace storm {
splitBlock(dtmc, backwardTransitions, currentBlock, stateToBlockMapping, distributions, blocksInRefinementQueue, refinementQueue, weak);
}
-
- std::cout << *this << std::endl;
-
+
std::chrono::high_resolution_clock::duration totalTime = std::chrono::high_resolution_clock::now() - totalStart;
std::cout << "Bisimulation quotient has " << this->blocks.size() << " blocks and took " << iteration << " iterations and " << std::chrono::duration_cast<std::chrono::milliseconds>(totalTime).count() << "ms." << std::endl;
}
template<typename ValueType>
- std::size_t BisimulationDecomposition<ValueType>::splitPredecessorsGraphBased(storm::models::Dtmc<ValueType> const& dtmc, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::size_t const& blockId, std::vector<std::size_t>& stateToBlockMapping, std::vector<storm::storage::Distribution<ValueType>>& distributions, storm::storage::BitVector& blocksInRefinementQueue, std::deque<std::size_t>& graphRefinementQueue, storm::storage::BitVector& splitBlocks) {
- std::cout << "entering " << std::endl;
+ std::size_t NaiveDeterministicModelBisimulationDecomposition<ValueType>::splitPredecessorsGraphBased(storm::models::Dtmc<ValueType> const& dtmc, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::size_t const& blockId, std::vector<std::size_t>& stateToBlockMapping, std::vector<storm::storage::Distribution<ValueType>>& distributions, storm::storage::BitVector& blocksInRefinementQueue, std::deque<std::size_t>& graphRefinementQueue, storm::storage::BitVector& splitBlocks) {
+// std::cout << "entering " << std::endl;
std::chrono::high_resolution_clock::time_point totalStart = std::chrono::high_resolution_clock::now();
// std::cout << "refining predecessors of " << blockId << std::endl;
// This method tries to split the blocks of predecessors of the provided block by checking whether there is
// a transition into the current block or not.
- std::unordered_map<std::size_t, typename BisimulationDecomposition<ValueType>::block_type> predecessorBlockToNewBlock;
+ std::unordered_map<std::size_t, typename NaiveDeterministicModelBisimulationDecomposition<ValueType>::block_type> predecessorBlockToNewBlock;
// Now for each predecessor block which state could actually reach the current block.
std::chrono::high_resolution_clock::time_point predIterStart = std::chrono::high_resolution_clock::now();
@@ -95,8 +98,8 @@ namespace storm {
// std::cout << "original: " << this->blocks[blockNewBlockPair.first] << std::endl;
// std::cout << "states with pred: " << blockNewBlockPair.second << std::endl;
// Now update the block mapping for the smaller of the two blocks.
- typename BisimulationDecomposition<ValueType>::block_type smallerBlock;
- typename BisimulationDecomposition<ValueType>::block_type largerBlock;
+ typename NaiveDeterministicModelBisimulationDecomposition<ValueType>::block_type smallerBlock;
+ typename NaiveDeterministicModelBisimulationDecomposition<ValueType>::block_type largerBlock;
if (blockNewBlockPair.second.size() < this->blocks[blockNewBlockPair.first].size()/2) {
smallerBlock = std::move(blockNewBlockPair.second);
std::set_difference(this->blocks[blockNewBlockPair.first].begin(), this->blocks[blockNewBlockPair.first].end(), smallerBlock.begin(), smallerBlock.end(), std::inserter(largerBlock, largerBlock.begin()));
@@ -143,9 +146,9 @@ namespace storm {
}
template<typename ValueType>
- std::size_t BisimulationDecomposition<ValueType>::splitBlock(storm::models::Dtmc<ValueType> const& dtmc, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::size_t const& blockId, std::vector<std::size_t>& stateToBlockMapping, std::vector<storm::storage::Distribution<ValueType>>& distributions, storm::storage::BitVector& blocksInRefinementQueue, std::deque<std::size_t>& refinementQueue, bool weakBisimulation) {
+ std::size_t NaiveDeterministicModelBisimulationDecomposition<ValueType>::splitBlock(storm::models::Dtmc<ValueType> const& dtmc, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::size_t const& blockId, std::vector<std::size_t>& stateToBlockMapping, std::vector<storm::storage::Distribution<ValueType>>& distributions, storm::storage::BitVector& blocksInRefinementQueue, std::deque<std::size_t>& refinementQueue, bool weakBisimulation) {
std::chrono::high_resolution_clock::time_point totalStart = std::chrono::high_resolution_clock::now();
- std::unordered_map<storm::storage::Distribution<ValueType>, typename BisimulationDecomposition<ValueType>::block_type> distributionToNewBlocks;
+ std::unordered_map<storm::storage::Distribution<ValueType>, typename NaiveDeterministicModelBisimulationDecomposition<ValueType>::block_type> distributionToNewBlocks;
// Traverse all states of the block and check whether they have different distributions.
std::chrono::high_resolution_clock::time_point gatherStart = std::chrono::high_resolution_clock::now();
@@ -180,10 +183,12 @@ namespace storm {
// distributions[blockId] = std::move(distributionToNewBlocks.begin()->first);
} else {
// In this case, we need to split the block.
- typename BisimulationDecomposition<ValueType>::block_type tmpBlock;
+ typename NaiveDeterministicModelBisimulationDecomposition<ValueType>::block_type tmpBlock;
auto distributionIterator = distributionToNewBlocks.begin();
- distributions[blockId] = std::move(distributionIterator->first);
+ STORM_LOG_ASSERT(distributionIterator != distributionToNewBlocks.end(), "One block has no distribution...");
+
+ // distributions[blockId] = std::move(distributionIterator->first);
tmpBlock = std::move(distributionIterator->second);
std::swap(this->blocks[blockId], tmpBlock);
++distributionIterator;
@@ -252,6 +257,6 @@ namespace storm {
return distributionToNewBlocks.size();
}
- template class BisimulationDecomposition<double>;
+ template class NaiveDeterministicModelBisimulationDecomposition<double>;
}
}
\ No newline at end of file
diff --git a/src/storage/BisimulationDecomposition.h b/src/storage/NaiveDeterministicModelBisimulationDecomposition.h
similarity index 74%
rename from src/storage/BisimulationDecomposition.h
rename to src/storage/NaiveDeterministicModelBisimulationDecomposition.h
index 55ed556d8..300922cf5 100644
--- a/src/storage/BisimulationDecomposition.h
+++ b/src/storage/NaiveDeterministicModelBisimulationDecomposition.h
@@ -1,5 +1,5 @@
-#ifndef STORM_STORAGE_BISIMULATIONDECOMPOSITION_H_
-#define STORM_STORAGE_BISIMULATIONDECOMPOSITION_H_
+#ifndef STORM_STORAGE_NAIVEDETERMINISTICMODELBISIMULATIONDECOMPOSITION_H_
+#define STORM_STORAGE_NAIVEDETERMINISTICMODELBISIMULATIONDECOMPOSITION_H_
#include <queue>
#include <deque>
@@ -15,14 +15,14 @@ namespace storm {
* This class represents the decomposition model into its bisimulation quotient.
*/
template <typename ValueType>
- class BisimulationDecomposition : public Decomposition<StateBlock> {
+ class NaiveDeterministicModelBisimulationDecomposition : public Decomposition<StateBlock> {
public:
- BisimulationDecomposition() = default;
+ NaiveDeterministicModelBisimulationDecomposition() = default;
/*!
* Decomposes the given DTMC into equivalence classes under weak or strong bisimulation.
*/
- BisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, bool weak = false);
+ NaiveDeterministicModelBisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, bool weak = false);
private:
void computeBisimulationEquivalenceClasses(storm::models::Dtmc<ValueType> const& model, bool weak);
@@ -32,4 +32,4 @@ namespace storm {
}
}
-#endif /* STORM_STORAGE_BISIMULATIONDECOMPOSITION_H_ */
\ No newline at end of file
+#endif /* STORM_STORAGE_NAIVEDETERMINISTICMODELBISIMULATIONDECOMPOSITION_H_ */
\ No newline at end of file
diff --git a/src/utility/cli.h b/src/utility/cli.h
index 6996736a4..ed63f5086 100644
--- a/src/utility/cli.h
+++ b/src/utility/cli.h
@@ -44,8 +44,8 @@ log4cplus::Logger logger;
#include "src/adapters/ExplicitModelAdapter.h"
// Headers for model processing.
-#include "src/storage/BisimulationDecomposition.h"
-#include "src/storage/BisimulationDecomposition2.h"
+#include "src/storage/NaiveDeterministicModelBisimulationDecomposition.h"
+#include "src/storage/DeterministicModelBisimulationDecomposition.h"
// Headers for counterexample generation.
#include "src/counterexamples/MILPMinimalLabelSetGenerator.h"
@@ -261,8 +261,8 @@ namespace storm {
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<storm::models::Dtmc<double>> dtmc = result->template as<storm::models::Dtmc<double>>();
- storm::storage::BisimulationDecomposition<double> bisimulationDecomposition(*dtmc);
- storm::storage::BisimulationDecomposition2<double> bisimulationDecomposition2(*dtmc);
+ storm::storage::DeterministicModelBisimulationDecomposition<double> bisimulationDecomposition(*dtmc);
+ return bisimulationDecomposition.getQuotient();
}
return result;
From 01e4dd336767f2cf081c1f1aa2a0f81b9f40728e Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Mon, 13 Oct 2014 13:29:46 +0200
Subject: [PATCH 12/14] Commit to switch workplace.
Former-commit-id: 7de1f8a1b1be25a609c4e19ae4f869c95f46545d
---
...ministicModelBisimulationDecomposition.cpp | 54 +++++++++++--------
...erministicModelBisimulationDecomposition.h | 16 +++---
2 files changed, 42 insertions(+), 28 deletions(-)
diff --git a/src/storage/DeterministicModelBisimulationDecomposition.cpp b/src/storage/DeterministicModelBisimulationDecomposition.cpp
index 144560557..6a11b3e9a 100644
--- a/src/storage/DeterministicModelBisimulationDecomposition.cpp
+++ b/src/storage/DeterministicModelBisimulationDecomposition.cpp
@@ -5,6 +5,8 @@
#include <chrono>
#include <iomanip>
+#include "src/exceptions/IllegalFunctionCallException.h"
+
namespace storm {
namespace storage {
@@ -298,7 +300,12 @@ namespace storm {
typename DeterministicModelBisimulationDecomposition<ValueType>::Block& DeterministicModelBisimulationDecomposition<ValueType>::Partition::getBlock(storm::storage::sparse::state_type state) {
return *this->stateToBlockMapping[state];
}
-
+
+ template<typename ValueType>
+ typename DeterministicModelBisimulationDecomposition<ValueType>::Block const& DeterministicModelBisimulationDecomposition<ValueType>::Partition::getBlock(storm::storage::sparse::state_type state) const {
+ return *this->stateToBlockMapping[state];
+ }
+
template<typename ValueType>
std::vector<storm::storage::sparse::state_type>::iterator DeterministicModelBisimulationDecomposition<ValueType>::Partition::getBeginOfStates(Block const& block) {
return this->states.begin() + block.getBegin();
@@ -467,23 +474,29 @@ namespace storm {
}
template<typename ValueType>
- DeterministicModelBisimulationDecomposition<ValueType>::DeterministicModelBisimulationDecomposition(storm::models::Dtmc<ValueType> const& dtmc, bool weak) : model(dtmc), initialBlocks() {
- computeBisimulationEquivalenceClasses(dtmc, weak);
+ DeterministicModelBisimulationDecomposition<ValueType>::DeterministicModelBisimulationDecomposition(storm::models::Dtmc<ValueType> const& dtmc, bool weak, bool buildQuotient) {
+ computeBisimulationEquivalenceClasses(dtmc, weak, buildQuotient);
}
template<typename ValueType>
std::shared_ptr<storm::models::AbstractDeterministicModel<ValueType>> DeterministicModelBisimulationDecomposition<ValueType>::getQuotient() const {
+ STORM_LOG_THROW(this->quotient != nullptr, storm::exceptions::IllegalFunctionCallException, "Unable to retrieve quotient model from bisimulation decomposition, because it was not built.");
+ return this->quotient;
+ }
+
+ template<typename ValueType>
+ void DeterministicModelBisimulationDecomposition<ValueType>::buildQuotient(storm::models::Dtmc<ValueType> const& dtmc, Partition const& partition) {
// In order to create the quotient model, we need to construct
// (a) the new transition matrix,
// (b) the new labeling,
// (c) the new reward structures.
-
+
// Prepare a matrix builder for (a).
storm::storage::SparseMatrixBuilder<ValueType> builder;
-
+
// Prepare the new state labeling for (b).
- storm::models::AtomicPropositionsLabeling newLabeling(this->size(), model.getStateLabeling().getNumberOfAtomicPropositions());
- std::set<std::string> atomicPropositionsSet = model.getStateLabeling().getAtomicPropositions();
+ storm::models::AtomicPropositionsLabeling newLabeling(this->size(), dtmc.getStateLabeling().getNumberOfAtomicPropositions());
+ std::set<std::string> atomicPropositionsSet = dtmc.getStateLabeling().getAtomicPropositions();
std::vector<std::string> atomicPropositions = std::vector<std::string>(atomicPropositionsSet.begin(), atomicPropositionsSet.end());
for (auto const& ap : atomicPropositions) {
newLabeling.addAtomicProposition(ap);
@@ -500,18 +513,23 @@ namespace storm {
// Add all atomic propositions to the equivalence class that the representative state satisfies.
for (auto const& ap : atomicPropositions) {
- if (model.getStateLabeling().getStateHasAtomicProposition(ap, representativeState)) {
+ if (dtmc.getStateLabeling().getStateHasAtomicProposition(ap, representativeState)) {
newLabeling.addAtomicPropositionToState(ap, blockIndex);
}
}
}
+ // Now check which of the blocks of the partition contain at least one initial state.
+ for (auto initialState : dtmc.getInitialStates()) {
+ Block const& initialBlock = partition.getBlock(initialState);
+ newLabeling.addAtomicPropositionToState("init", initialBlock.getId());
+ }
- return nullptr;
+ this->quotient = nullptr;
}
template<typename ValueType>
- void DeterministicModelBisimulationDecomposition<ValueType>::computeBisimulationEquivalenceClasses(storm::models::Dtmc<ValueType> const& dtmc, bool weak) {
+ void DeterministicModelBisimulationDecomposition<ValueType>::computeBisimulationEquivalenceClasses(storm::models::Dtmc<ValueType> const& dtmc, bool weak, bool buildQuotient) {
std::chrono::high_resolution_clock::time_point totalStart = std::chrono::high_resolution_clock::now();
// We start by computing the initial partition.
@@ -537,23 +555,17 @@ 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));
}
-
- // FIXME: as we will drop the state-to-block-mapping, we need to create the distribution of each block now.
-
- // Now check which of the blocks of the partition contain at least one initial state.
- for (auto initialState : model.getInitialStates()) {
- Block& initialBlock = partition.getBlock(initialState);
- if (std::find(this->initialBlocks.begin(), this->initialBlocks.end(), initialBlock.getId()) == this->initialBlocks.end()) {
- this->initialBlocks.emplace_back(initialBlock.getId());
- }
- }
- std::sort(this->initialBlocks.begin(), this->initialBlocks.end());
std::chrono::high_resolution_clock::duration totalTime = std::chrono::high_resolution_clock::now() - totalStart;
diff --git a/src/storage/DeterministicModelBisimulationDecomposition.h b/src/storage/DeterministicModelBisimulationDecomposition.h
index a595d7c28..c1ca37c18 100644
--- a/src/storage/DeterministicModelBisimulationDecomposition.h
+++ b/src/storage/DeterministicModelBisimulationDecomposition.h
@@ -21,7 +21,7 @@ namespace storm {
/*!
* Decomposes the given DTMC into equivalence classes under weak or strong bisimulation.
*/
- DeterministicModelBisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, bool weak = false);
+ DeterministicModelBisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, bool weak = false, bool buildQuotient = false);
/*!
* Retrieves the quotient of the model under the previously computed bisimulation.
@@ -231,7 +231,10 @@ namespace storm {
// Retrieves the block of the given state.
Block& getBlock(storm::storage::sparse::state_type state);
-
+
+ // Retrieves the block of the given state.
+ Block const& getBlock(storm::storage::sparse::state_type state) const;
+
// Retrieves the position of the given state.
storm::storage::sparse::state_type const& getPosition(storm::storage::sparse::state_type state) const;
@@ -277,17 +280,16 @@ namespace storm {
std::vector<ValueType> values;
};
- void computeBisimulationEquivalenceClasses(storm::models::Dtmc<ValueType> const& model, bool weak);
+ void computeBisimulationEquivalenceClasses(storm::models::Dtmc<ValueType> const& model, bool weak, bool buildQuotient);
std::size_t splitPartition(storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Block& splitter, Partition& partition, std::deque<Block*>& splitterQueue);
std::size_t splitBlockProbabilities(Block& block, Partition& partition, std::deque<Block*>& splitterQueue);
- // The model for which the bisimulation is computed.
- storm::models::Dtmc<ValueType> const& model;
+ void buildQuotient(storm::models::Dtmc<ValueType> const& dtmc, Partition const& partition);
- // The indices of all blocks that hold one or more initial states.
- std::vector<storm::storage::sparse::state_type> initialBlocks;
+ // If required, a quotient model is built and stored in this member.
+ std::shared_ptr<storm::models::AbstractDeterministicModel<ValueType>> quotient;
};
}
}
From af270dee8aec1f67fe54498ed868dd7641d28282 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Mon, 13 Oct 2014 17:24:52 +0200
Subject: [PATCH 13/14] 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<T> const& probabilityMatrix, storm::models::AtomicPropositionsLabeling const& stateLabeling,
- boost::optional<std::vector<T>> const& optionalStateRewardVector, boost::optional<storm::storage::SparseMatrix<T>> const& optionalTransitionRewardMatrix,
- boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> const& optionalChoiceLabeling)
+ boost::optional<std::vector<T>> const& optionalStateRewardVector = boost::optional<std::vector<T>>(),
+ boost::optional<storm::storage::SparseMatrix<T>> const& optionalTransitionRewardMatrix = boost::optional<storm::storage::SparseMatrix<T>>(),
+ boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> const& optionalChoiceLabeling = boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>())
: AbstractDeterministicModel<T>(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<T>&& probabilityMatrix, storm::models::AtomicPropositionsLabeling&& stateLabeling,
- boost::optional<std::vector<T>>&& optionalStateRewardVector, boost::optional<storm::storage::SparseMatrix<T>>&& optionalTransitionRewardMatrix,
- boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>&& optionalChoiceLabeling)
+ boost::optional<std::vector<T>>&& optionalStateRewardVector = boost::optional<std::vector<T>>(),
+ boost::optional<storm::storage::SparseMatrix<T>>&& optionalTransitionRewardMatrix = boost::optional<storm::storage::SparseMatrix<T>>(),
+ boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>&& optionalChoiceLabeling = boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>())
// The std::move call must be repeated here because otherwise this calls the copy constructor of the Base Class
: AbstractDeterministicModel<T>(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<typename ValueType>
DeterministicModelBisimulationDecomposition<ValueType>::DeterministicModelBisimulationDecomposition(storm::models::Dtmc<ValueType> 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<ValueType> builder;
+ storm::storage::SparseMatrixBuilder<ValueType> 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<storm::storage::sparse::state_type, ValueType> 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<storm::models::AbstractDeterministicModel<ValueType>>(new storm::models::Dtmc<ValueType>(builder.build(), std::move(newLabeling)));
}
template<typename ValueType>
@@ -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 <boost/container/flat_set.hpp>
+#include <boost/container/container_fwd.hpp>
#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 <typename InputIterator>
- 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<storm::models::Dtmc<double>> dtmc = result->template as<storm::models::Dtmc<double>>();
- storm::storage::DeterministicModelBisimulationDecomposition<double> bisimulationDecomposition(*dtmc);
- return bisimulationDecomposition.getQuotient();
+
+ STORM_PRINT(std::endl << "Performing bisimulation minimization..." << std::endl);
+ storm::storage::DeterministicModelBisimulationDecomposition<double> 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<storm::models::AbstractModel<double>> model = buildModel<double>();
- // 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<double> constantInfinity() {
/*! @endcond */
+
} //namespace utility
} //namespace storm
From 1c091d764095f1951ec13829bdef851fc6ea2576 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Tue, 14 Oct 2014 17:46:40 +0200
Subject: [PATCH 14/14] Renamed some classes to indicate that only strong
bisimulation can be computed. Added option to start with an initial partition
that preserves only certain formulas. Added ConstantsComparator concept that
is to be used when constants have to be compared with other constants.
Former-commit-id: feacadfa381d58e69a9f9d8f2f74358f90627b2f
---
src/models/Ctmc.h | 10 +-
...cModelStrongBisimulationDecomposition.cpp} | 368 ++++++++++++------
...ticModelStrongBisimulationDecomposition.h} | 179 ++++++++-
src/utility/ConstantsComparator.h | 84 ++++
src/utility/cli.h | 6 +-
src/utility/graph.h | 19 +
6 files changed, 523 insertions(+), 143 deletions(-)
rename src/storage/{DeterministicModelBisimulationDecomposition.cpp => DeterministicModelStrongBisimulationDecomposition.cpp} (57%)
rename src/storage/{DeterministicModelBisimulationDecomposition.h => DeterministicModelStrongBisimulationDecomposition.h} (56%)
create mode 100644 src/utility/ConstantsComparator.h
diff --git a/src/models/Ctmc.h b/src/models/Ctmc.h
index 229ccfe9e..b3c1f1ef1 100644
--- a/src/models/Ctmc.h
+++ b/src/models/Ctmc.h
@@ -36,8 +36,9 @@ public:
* propositions to each state.
*/
Ctmc(storm::storage::SparseMatrix<T> const& rateMatrix, storm::models::AtomicPropositionsLabeling const& stateLabeling,
- boost::optional<std::vector<T>> const& optionalStateRewardVector, boost::optional<storm::storage::SparseMatrix<T>> const& optionalTransitionRewardMatrix,
- boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> const& optionalChoiceLabeling)
+ boost::optional<std::vector<T>> const& optionalStateRewardVector = boost::optional<std::vector<T>>(),
+ boost::optional<storm::storage::SparseMatrix<T>> const& optionalTransitionRewardMatrix = boost::optional<storm::storage::SparseMatrix<T>>(),
+ boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> const& optionalChoiceLabeling = boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>())
: AbstractDeterministicModel<T>(rateMatrix, stateLabeling, optionalStateRewardVector, optionalTransitionRewardMatrix, optionalChoiceLabeling) {
// Intentionally left empty.
}
@@ -51,8 +52,9 @@ public:
* propositions to each state.
*/
Ctmc(storm::storage::SparseMatrix<T>&& rateMatrix, storm::models::AtomicPropositionsLabeling&& stateLabeling,
- boost::optional<std::vector<T>>&& optionalStateRewardVector, boost::optional<storm::storage::SparseMatrix<T>>&& optionalTransitionRewardMatrix,
- boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>&& optionalChoiceLabeling)
+ boost::optional<std::vector<T>>&& optionalStateRewardVector = boost::optional<std::vector<T>>(),
+ boost::optional<storm::storage::SparseMatrix<T>>&& optionalTransitionRewardMatrix = boost::optional<storm::storage::SparseMatrix<T>>(),
+ boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>&& optionalChoiceLabeling = boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>())
// The std::move call must be repeated here because otherwise this calls the copy constructor of the Base Class
: AbstractDeterministicModel<T>(std::move(rateMatrix), std::move(stateLabeling), std::move(optionalStateRewardVector), std::move(optionalTransitionRewardMatrix),
std::move(optionalChoiceLabeling)) {
diff --git a/src/storage/DeterministicModelBisimulationDecomposition.cpp b/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp
similarity index 57%
rename from src/storage/DeterministicModelBisimulationDecomposition.cpp
rename to src/storage/DeterministicModelStrongBisimulationDecomposition.cpp
index d9023d153..93433d19f 100644
--- a/src/storage/DeterministicModelBisimulationDecomposition.cpp
+++ b/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp
@@ -1,19 +1,21 @@
-#include "src/storage/DeterministicModelBisimulationDecomposition.h"
+#include "src/storage/DeterministicModelStrongBisimulationDecomposition.h"
#include <algorithm>
#include <unordered_map>
#include <chrono>
#include <iomanip>
+#include "src/utility/graph.h"
#include "src/exceptions/IllegalFunctionCallException.h"
namespace storm {
namespace storage {
- static std::size_t globalId = 0;
+ template<typename ValueType>
+ std::size_t DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::blockId = 0;
template<typename ValueType>
- DeterministicModelBisimulationDecomposition<ValueType>::Block::Block(storm::storage::sparse::state_type begin, storm::storage::sparse::state_type end, Block* prev, Block* next) : next(next), prev(prev), begin(begin), end(end), markedAsSplitter(false), markedAsPredecessorBlock(false), markedPosition(begin), id(globalId++) {
+ DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::Block(storm::storage::sparse::state_type begin, storm::storage::sparse::state_type end, Block* prev, Block* next, std::shared_ptr<std::string> const& label) : next(next), prev(prev), begin(begin), end(end), markedAsSplitter(false), markedAsPredecessorBlock(false), markedPosition(begin), absorbing(false), id(blockId++), label(label) {
if (next != nullptr) {
next->prev = this;
}
@@ -23,7 +25,7 @@ namespace storm {
}
template<typename ValueType>
- void DeterministicModelBisimulationDecomposition<ValueType>::Block::print(Partition const& partition) const {
+ void DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::print(Partition const& partition) const {
std::cout << "block " << this->getId() << " with marked position " << this->getMarkedPosition() << " and original begin " << this->getOriginalBegin() << std::endl;
std::cout << "begin: " << this->begin << " and end: " << this->end << " (number of states: " << this->getNumberOfStates() << ")" << std::endl;
std::cout << "states:" << std::endl;
@@ -42,33 +44,33 @@ namespace storm {
}
template<typename ValueType>
- void DeterministicModelBisimulationDecomposition<ValueType>::Block::setBegin(storm::storage::sparse::state_type begin) {
+ void DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::setBegin(storm::storage::sparse::state_type begin) {
this->begin = begin;
this->markedPosition = begin;
}
template<typename ValueType>
- void DeterministicModelBisimulationDecomposition<ValueType>::Block::setEnd(storm::storage::sparse::state_type end) {
+ void DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::setEnd(storm::storage::sparse::state_type end) {
this->end = end;
}
template<typename ValueType>
- void DeterministicModelBisimulationDecomposition<ValueType>::Block::incrementBegin() {
+ void DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::incrementBegin() {
++this->begin;
}
template<typename ValueType>
- void DeterministicModelBisimulationDecomposition<ValueType>::Block::decrementEnd() {
+ void DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::decrementEnd() {
++this->begin;
}
template<typename ValueType>
- storm::storage::sparse::state_type DeterministicModelBisimulationDecomposition<ValueType>::Block::getBegin() const {
+ storm::storage::sparse::state_type DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getBegin() const {
return this->begin;
}
template<typename ValueType>
- storm::storage::sparse::state_type DeterministicModelBisimulationDecomposition<ValueType>::Block::getOriginalBegin() const {
+ storm::storage::sparse::state_type DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getOriginalBegin() const {
if (this->hasPreviousBlock()) {
return this->getPreviousBlock().getEnd();
} else {
@@ -77,72 +79,72 @@ namespace storm {
}
template<typename ValueType>
- storm::storage::sparse::state_type DeterministicModelBisimulationDecomposition<ValueType>::Block::getEnd() const {
+ storm::storage::sparse::state_type DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getEnd() const {
return this->end;
}
template<typename ValueType>
- void DeterministicModelBisimulationDecomposition<ValueType>::Block::setIterator(const_iterator it) {
+ void DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::setIterator(const_iterator it) {
this->selfIt = it;
}
template<typename ValueType>
- typename DeterministicModelBisimulationDecomposition<ValueType>::Block::const_iterator DeterministicModelBisimulationDecomposition<ValueType>::Block::getIterator() const {
+ typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::const_iterator DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getIterator() const {
return this->selfIt;
}
template<typename ValueType>
- typename DeterministicModelBisimulationDecomposition<ValueType>::Block::const_iterator DeterministicModelBisimulationDecomposition<ValueType>::Block::getNextIterator() const {
+ typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::const_iterator DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getNextIterator() const {
return this->getNextBlock().getIterator();
}
template<typename ValueType>
- typename DeterministicModelBisimulationDecomposition<ValueType>::Block::const_iterator DeterministicModelBisimulationDecomposition<ValueType>::Block::getPreviousIterator() const {
+ typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::const_iterator DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getPreviousIterator() const {
return this->getPreviousBlock().getIterator();
}
template<typename ValueType>
- typename DeterministicModelBisimulationDecomposition<ValueType>::Block& DeterministicModelBisimulationDecomposition<ValueType>::Block::getNextBlock() {
+ typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block& DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getNextBlock() {
return *this->next;
}
template<typename ValueType>
- typename DeterministicModelBisimulationDecomposition<ValueType>::Block const& DeterministicModelBisimulationDecomposition<ValueType>::Block::getNextBlock() const {
+ typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block const& DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getNextBlock() const {
return *this->next;
}
template<typename ValueType>
- bool DeterministicModelBisimulationDecomposition<ValueType>::Block::hasNextBlock() const {
+ bool DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::hasNextBlock() const {
return this->next != nullptr;
}
template<typename ValueType>
- typename DeterministicModelBisimulationDecomposition<ValueType>::Block& DeterministicModelBisimulationDecomposition<ValueType>::Block::getPreviousBlock() {
+ typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block& DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getPreviousBlock() {
return *this->prev;
}
template<typename ValueType>
- typename DeterministicModelBisimulationDecomposition<ValueType>::Block* DeterministicModelBisimulationDecomposition<ValueType>::Block::getPreviousBlockPointer() {
+ typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block* DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getPreviousBlockPointer() {
return this->prev;
}
template<typename ValueType>
- typename DeterministicModelBisimulationDecomposition<ValueType>::Block* DeterministicModelBisimulationDecomposition<ValueType>::Block::getNextBlockPointer() {
+ typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block* DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getNextBlockPointer() {
return this->next;
}
template<typename ValueType>
- typename DeterministicModelBisimulationDecomposition<ValueType>::Block const& DeterministicModelBisimulationDecomposition<ValueType>::Block::getPreviousBlock() const {
+ typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block const& DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getPreviousBlock() const {
return *this->prev;
}
template<typename ValueType>
- bool DeterministicModelBisimulationDecomposition<ValueType>::Block::hasPreviousBlock() const {
+ bool DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::hasPreviousBlock() const {
return this->prev != nullptr;
}
template<typename ValueType>
- bool DeterministicModelBisimulationDecomposition<ValueType>::Block::check() const {
+ bool DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::check() const {
if (this->begin >= this->end) {
assert(false);
}
@@ -156,68 +158,94 @@ namespace storm {
}
template<typename ValueType>
- std::size_t DeterministicModelBisimulationDecomposition<ValueType>::Block::getNumberOfStates() const {
+ std::size_t DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getNumberOfStates() const {
// We need to take the original begin here, because the begin is temporarily moved.
return (this->end - this->getOriginalBegin());
}
template<typename ValueType>
- bool DeterministicModelBisimulationDecomposition<ValueType>::Block::isMarkedAsSplitter() const {
+ bool DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::isMarkedAsSplitter() const {
return this->markedAsSplitter;
}
template<typename ValueType>
- void DeterministicModelBisimulationDecomposition<ValueType>::Block::markAsSplitter() {
+ void DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::markAsSplitter() {
this->markedAsSplitter = true;
}
template<typename ValueType>
- void DeterministicModelBisimulationDecomposition<ValueType>::Block::unmarkAsSplitter() {
+ void DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::unmarkAsSplitter() {
this->markedAsSplitter = false;
}
template<typename ValueType>
- std::size_t DeterministicModelBisimulationDecomposition<ValueType>::Block::getId() const {
+ std::size_t DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getId() const {
return this->id;
}
template<typename ValueType>
- storm::storage::sparse::state_type DeterministicModelBisimulationDecomposition<ValueType>::Block::getMarkedPosition() const {
+ void DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::setAbsorbing(bool absorbing) {
+ this->absorbing = absorbing;
+ }
+
+ template<typename ValueType>
+ bool DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::isAbsorbing() const {
+ return this->absorbing;
+ }
+
+ template<typename ValueType>
+ storm::storage::sparse::state_type DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getMarkedPosition() const {
return this->markedPosition;
}
template<typename ValueType>
- void DeterministicModelBisimulationDecomposition<ValueType>::Block::setMarkedPosition(storm::storage::sparse::state_type position) {
+ void DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::setMarkedPosition(storm::storage::sparse::state_type position) {
this->markedPosition = position;
}
template<typename ValueType>
- void DeterministicModelBisimulationDecomposition<ValueType>::Block::resetMarkedPosition() {
+ void DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::resetMarkedPosition() {
this->markedPosition = this->begin;
}
template<typename ValueType>
- void DeterministicModelBisimulationDecomposition<ValueType>::Block::incrementMarkedPosition() {
+ void DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::incrementMarkedPosition() {
++this->markedPosition;
}
template<typename ValueType>
- void DeterministicModelBisimulationDecomposition<ValueType>::Block::markAsPredecessorBlock() {
+ void DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::markAsPredecessorBlock() {
this->markedAsPredecessorBlock = true;
}
template<typename ValueType>
- void DeterministicModelBisimulationDecomposition<ValueType>::Block::unmarkAsPredecessorBlock() {
+ void DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::unmarkAsPredecessorBlock() {
this->markedAsPredecessorBlock = false;
}
template<typename ValueType>
- bool DeterministicModelBisimulationDecomposition<ValueType>::Block::isMarkedAsPredecessor() const {
+ bool DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::isMarkedAsPredecessor() const {
return markedAsPredecessorBlock;
}
template<typename ValueType>
- DeterministicModelBisimulationDecomposition<ValueType>::Partition::Partition(std::size_t numberOfStates) : stateToBlockMapping(numberOfStates), states(numberOfStates), positions(numberOfStates), values(numberOfStates) {
+ bool DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::hasLabel() const {
+ return this->label != nullptr;
+ }
+
+ template<typename ValueType>
+ std::string const& DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getLabel() const {
+ STORM_LOG_THROW(this->label != nullptr, storm::exceptions::IllegalFunctionCallException, "Unable to retrieve label of block that has none.");
+ return *this->label;
+ }
+
+ template<typename ValueType>
+ std::shared_ptr<std::string> const& DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getLabelPtr() const {
+ return this->label;
+ }
+
+ template<typename ValueType>
+ DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::Partition(std::size_t numberOfStates) : stateToBlockMapping(numberOfStates), states(numberOfStates), positions(numberOfStates), values(numberOfStates) {
// Create the block and give it an iterator to itself.
typename std::list<Block>::iterator it = blocks.emplace(this->blocks.end(), 0, numberOfStates, nullptr, nullptr);
it->setIterator(it);
@@ -231,14 +259,54 @@ namespace storm {
}
template<typename ValueType>
- void DeterministicModelBisimulationDecomposition<ValueType>::Partition::swapStates(storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2) {
+ DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::Partition(std::size_t numberOfStates, storm::storage::BitVector const& prob0States, storm::storage::BitVector const& prob1States, std::string const& otherLabel, std::string const& prob1Label) : stateToBlockMapping(numberOfStates), states(numberOfStates), positions(numberOfStates), values(numberOfStates) {
+ typename std::list<Block>::iterator firstIt = blocks.emplace(this->blocks.end(), 0, prob0States.getNumberOfSetBits(), nullptr, nullptr);
+ Block& firstBlock = *firstIt;
+ firstBlock.setIterator(firstIt);
+
+ storm::storage::sparse::state_type position = 0;
+ for (auto state : prob0States) {
+ states[position] = state;
+ positions[state] = position;
+ stateToBlockMapping[state] = &firstBlock;
+ ++position;
+ }
+ firstBlock.setAbsorbing(true);
+
+ typename std::list<Block>::iterator secondIt = blocks.emplace(this->blocks.end(), position, position + prob1States.getNumberOfSetBits(), &firstBlock, nullptr, std::shared_ptr<std::string>(new std::string(prob1Label)));
+ Block& secondBlock = *secondIt;
+ secondBlock.setIterator(secondIt);
+
+ for (auto state : prob1States) {
+ states[position] = state;
+ positions[state] = position;
+ stateToBlockMapping[state] = &secondBlock;
+ ++position;
+ }
+ secondBlock.setAbsorbing(true);
+
+ typename std::list<Block>::iterator thirdIt = blocks.emplace(this->blocks.end(), position, numberOfStates, &secondBlock, nullptr, otherLabel == "true" ? std::shared_ptr<std::string>(nullptr) : std::shared_ptr<std::string>(new std::string(otherLabel)));
+ Block& thirdBlock = *thirdIt;
+ thirdBlock.setIterator(thirdIt);
+
+ storm::storage::BitVector otherStates = ~(prob0States | prob1States);
+ for (auto state : otherStates) {
+ states[position] = state;
+ positions[state] = position;
+ stateToBlockMapping[state] = &thirdBlock;
+ ++position;
+ }
+ }
+
+ template<typename ValueType>
+ void DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::swapStates(storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2) {
std::swap(this->states[this->positions[state1]], this->states[this->positions[state2]]);
std::swap(this->values[this->positions[state1]], this->values[this->positions[state2]]);
std::swap(this->positions[state1], this->positions[state2]);
}
template<typename ValueType>
- void DeterministicModelBisimulationDecomposition<ValueType>::Partition::swapStatesAtPositions(storm::storage::sparse::state_type position1, storm::storage::sparse::state_type position2) {
+ void DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::swapStatesAtPositions(storm::storage::sparse::state_type position1, storm::storage::sparse::state_type position2) {
storm::storage::sparse::state_type state1 = this->states[position1];
storm::storage::sparse::state_type state2 = this->states[position2];
@@ -250,94 +318,99 @@ namespace storm {
}
template<typename ValueType>
- storm::storage::sparse::state_type const& DeterministicModelBisimulationDecomposition<ValueType>::Partition::getPosition(storm::storage::sparse::state_type state) const {
+ storm::storage::sparse::state_type const& DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getPosition(storm::storage::sparse::state_type state) const {
return this->positions[state];
}
template<typename ValueType>
- void DeterministicModelBisimulationDecomposition<ValueType>::Partition::setPosition(storm::storage::sparse::state_type state, storm::storage::sparse::state_type position) {
+ void DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::setPosition(storm::storage::sparse::state_type state, storm::storage::sparse::state_type position) {
this->positions[state] = position;
}
template<typename ValueType>
- storm::storage::sparse::state_type const& DeterministicModelBisimulationDecomposition<ValueType>::Partition::getState(storm::storage::sparse::state_type position) const {
+ storm::storage::sparse::state_type const& DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getState(storm::storage::sparse::state_type position) const {
return this->states[position];
}
template<typename ValueType>
- ValueType const& DeterministicModelBisimulationDecomposition<ValueType>::Partition::getValue(storm::storage::sparse::state_type state) const {
+ ValueType const& DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getValue(storm::storage::sparse::state_type state) const {
return this->values[this->positions[state]];
}
template<typename ValueType>
- ValueType const& DeterministicModelBisimulationDecomposition<ValueType>::Partition::getValueAtPosition(storm::storage::sparse::state_type position) const {
+ ValueType const& DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getValueAtPosition(storm::storage::sparse::state_type position) const {
return this->values[position];
}
template<typename ValueType>
- void DeterministicModelBisimulationDecomposition<ValueType>::Partition::setValue(storm::storage::sparse::state_type state, ValueType value) {
+ void DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::setValue(storm::storage::sparse::state_type state, ValueType value) {
this->values[this->positions[state]] = value;
}
template<typename ValueType>
- std::vector<ValueType>& DeterministicModelBisimulationDecomposition<ValueType>::Partition::getValues() {
+ std::vector<ValueType>& DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getValues() {
return this->values;
}
template<typename ValueType>
- void DeterministicModelBisimulationDecomposition<ValueType>::Partition::increaseValue(storm::storage::sparse::state_type state, ValueType value) {
+ void DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::increaseValue(storm::storage::sparse::state_type state, ValueType value) {
this->values[this->positions[state]] += value;
}
template<typename ValueType>
- void DeterministicModelBisimulationDecomposition<ValueType>::Partition::updateBlockMapping(Block& block, std::vector<storm::storage::sparse::state_type>::iterator first, std::vector<storm::storage::sparse::state_type>::iterator last) {
+ void DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::updateBlockMapping(Block& block, std::vector<storm::storage::sparse::state_type>::iterator first, std::vector<storm::storage::sparse::state_type>::iterator last) {
for (; first != last; ++first) {
this->stateToBlockMapping[*first] = █
}
}
template<typename ValueType>
- typename DeterministicModelBisimulationDecomposition<ValueType>::Block& DeterministicModelBisimulationDecomposition<ValueType>::Partition::getBlock(storm::storage::sparse::state_type state) {
+ typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block& DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getFirstBlock() {
+ return *this->blocks.begin();
+ }
+
+ template<typename ValueType>
+ typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block& DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getBlock(storm::storage::sparse::state_type state) {
return *this->stateToBlockMapping[state];
}
template<typename ValueType>
- typename DeterministicModelBisimulationDecomposition<ValueType>::Block const& DeterministicModelBisimulationDecomposition<ValueType>::Partition::getBlock(storm::storage::sparse::state_type state) const {
+ typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block const& DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getBlock(storm::storage::sparse::state_type state) const {
return *this->stateToBlockMapping[state];
}
template<typename ValueType>
- std::vector<storm::storage::sparse::state_type>::iterator DeterministicModelBisimulationDecomposition<ValueType>::Partition::getBeginOfStates(Block const& block) {
+ std::vector<storm::storage::sparse::state_type>::iterator DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getBeginOfStates(Block const& block) {
return this->states.begin() + block.getBegin();
}
template<typename ValueType>
- std::vector<storm::storage::sparse::state_type>::iterator DeterministicModelBisimulationDecomposition<ValueType>::Partition::getEndOfStates(Block const& block) {
+ std::vector<storm::storage::sparse::state_type>::iterator DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getEndOfStates(Block const& block) {
return this->states.begin() + block.getEnd();
}
template<typename ValueType>
- std::vector<storm::storage::sparse::state_type>::const_iterator DeterministicModelBisimulationDecomposition<ValueType>::Partition::getBeginOfStates(Block const& block) const {
+ std::vector<storm::storage::sparse::state_type>::const_iterator DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getBeginOfStates(Block const& block) const {
return this->states.begin() + block.getBegin();
}
template<typename ValueType>
- std::vector<storm::storage::sparse::state_type>::const_iterator DeterministicModelBisimulationDecomposition<ValueType>::Partition::getEndOfStates(Block const& block) const {
+ std::vector<storm::storage::sparse::state_type>::const_iterator DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getEndOfStates(Block const& block) const {
return this->states.begin() + block.getEnd();
}
template<typename ValueType>
- typename std::vector<ValueType>::iterator DeterministicModelBisimulationDecomposition<ValueType>::Partition::getBeginOfValues(Block const& block) {
+ typename std::vector<ValueType>::iterator DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getBeginOfValues(Block const& block) {
return this->values.begin() + block.getBegin();
}
template<typename ValueType>
- typename std::vector<ValueType>::iterator DeterministicModelBisimulationDecomposition<ValueType>::Partition::getEndOfValues(Block const& block) {
+ typename std::vector<ValueType>::iterator DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getEndOfValues(Block const& block) {
return this->values.begin() + block.getEnd();
}
template<typename ValueType>
- typename DeterministicModelBisimulationDecomposition<ValueType>::Block& DeterministicModelBisimulationDecomposition<ValueType>::Partition::splitBlock(Block& block, storm::storage::sparse::state_type position) {
+ typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block& DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::splitBlock(Block& block, storm::storage::sparse::state_type position) {
// FIXME: this could be improved by splitting off the smaller of the two resulting blocks.
// In case one of the resulting blocks would be empty, we simply return the current block and do not create
@@ -347,7 +420,7 @@ namespace storm {
}
// Actually create the new block and insert it at the correct position.
- typename std::list<Block>::iterator selfIt = this->blocks.emplace(block.getIterator(), block.getBegin(), position, block.getPreviousBlockPointer(), &block);
+ typename std::list<Block>::iterator selfIt = this->blocks.emplace(block.getIterator(), block.getBegin(), position, block.getPreviousBlockPointer(), &block, block.getLabelPtr());
selfIt->setIterator(selfIt);
Block& newBlock = *selfIt;
@@ -363,7 +436,7 @@ namespace storm {
}
template<typename ValueType>
- typename DeterministicModelBisimulationDecomposition<ValueType>::Block& DeterministicModelBisimulationDecomposition<ValueType>::Partition::insertBlock(Block& block) {
+ typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block& DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::insertBlock(Block& block) {
// Find the beginning of the new block.
storm::storage::sparse::state_type begin;
if (block.hasPreviousBlock()) {
@@ -386,7 +459,7 @@ namespace storm {
}
template<typename ValueType>
- void DeterministicModelBisimulationDecomposition<ValueType>::Partition::splitLabel(storm::storage::BitVector const& statesWithLabel) {
+ void DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::splitLabel(storm::storage::BitVector const& statesWithLabel) {
for (auto blockIterator = this->blocks.begin(), ite = this->blocks.end(); blockIterator != ite; ) { // The update of the loop was intentionally moved to the bottom of the loop.
Block& block = *blockIterator;
@@ -414,22 +487,22 @@ namespace storm {
}
template<typename ValueType>
- std::list<typename DeterministicModelBisimulationDecomposition<ValueType>::Block> const& DeterministicModelBisimulationDecomposition<ValueType>::Partition::getBlocks() const {
+ std::list<typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block> const& DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getBlocks() const {
return this->blocks;
}
template<typename ValueType>
- std::vector<storm::storage::sparse::state_type>& DeterministicModelBisimulationDecomposition<ValueType>::Partition::getStates() {
+ std::vector<storm::storage::sparse::state_type>& DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getStates() {
return this->states;
}
template<typename ValueType>
- std::list<typename DeterministicModelBisimulationDecomposition<ValueType>::Block>& DeterministicModelBisimulationDecomposition<ValueType>::Partition::getBlocks() {
+ std::list<typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block>& DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getBlocks() {
return this->blocks;
}
template<typename ValueType>
- bool DeterministicModelBisimulationDecomposition<ValueType>::Partition::check() const {
+ bool DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::check() const {
for (uint_fast64_t state = 0; state < this->positions.size(); ++state) {
if (this->states[this->positions[state]] != state) {
assert(false);
@@ -447,7 +520,7 @@ namespace storm {
}
template<typename ValueType>
- void DeterministicModelBisimulationDecomposition<ValueType>::Partition::print() const {
+ void DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::print() const {
for (auto const& block : this->blocks) {
block.print(*this);
}
@@ -469,24 +542,49 @@ namespace storm {
}
template<typename ValueType>
- std::size_t DeterministicModelBisimulationDecomposition<ValueType>::Partition::size() const {
+ std::size_t DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::size() const {
return this->blocks.size();
}
template<typename ValueType>
- DeterministicModelBisimulationDecomposition<ValueType>::DeterministicModelBisimulationDecomposition(storm::models::Dtmc<ValueType> 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);
+ DeterministicModelStrongBisimulationDecomposition<ValueType>::DeterministicModelStrongBisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, bool buildQuotient) {
+ STORM_LOG_THROW(!model.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures.");
+ Partition initialPartition = getLabelBasedInitialPartition(model);
+ partitionRefinement(model, model.getBackwardTransitions(), initialPartition, buildQuotient);
+ }
+
+ template<typename ValueType>
+ DeterministicModelStrongBisimulationDecomposition<ValueType>::DeterministicModelStrongBisimulationDecomposition(storm::models::Ctmc<ValueType> const& model, bool buildQuotient) {
+ STORM_LOG_THROW(!model.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures.");
+ Partition initialPartition = getLabelBasedInitialPartition(model);
+ partitionRefinement(model, model.getBackwardTransitions(), initialPartition, buildQuotient);
+ }
+
+ template<typename ValueType>
+ DeterministicModelStrongBisimulationDecomposition<ValueType>::DeterministicModelStrongBisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, std::string const& phiLabel, std::string const& psiLabel, bool bounded, bool buildQuotient) {
+ STORM_LOG_THROW(!model.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures.");
+ storm::storage::SparseMatrix<ValueType> backwardTransitions = model.getBackwardTransitions();
+ Partition initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, phiLabel, psiLabel, bounded);
+ partitionRefinement(model, model.getBackwardTransitions(), initialPartition, buildQuotient);
+ }
+
+ template<typename ValueType>
+ DeterministicModelStrongBisimulationDecomposition<ValueType>::DeterministicModelStrongBisimulationDecomposition(storm::models::Ctmc<ValueType> const& model, std::string const& phiLabel, std::string const& psiLabel, bool bounded, bool buildQuotient) {
+ STORM_LOG_THROW(!model.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures.");
+ storm::storage::SparseMatrix<ValueType> backwardTransitions = model.getBackwardTransitions();
+ Partition initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, phiLabel, psiLabel, bounded);
+ partitionRefinement(model, model.getBackwardTransitions(), initialPartition, buildQuotient);
}
template<typename ValueType>
- std::shared_ptr<storm::models::AbstractDeterministicModel<ValueType>> DeterministicModelBisimulationDecomposition<ValueType>::getQuotient() const {
+ std::shared_ptr<storm::models::AbstractDeterministicModel<ValueType>> DeterministicModelStrongBisimulationDecomposition<ValueType>::getQuotient() const {
STORM_LOG_THROW(this->quotient != nullptr, storm::exceptions::IllegalFunctionCallException, "Unable to retrieve quotient model from bisimulation decomposition, because it was not built.");
return this->quotient;
}
template<typename ValueType>
- void DeterministicModelBisimulationDecomposition<ValueType>::buildQuotient(storm::models::Dtmc<ValueType> const& dtmc, Partition const& partition) {
+ template<typename ModelType>
+ void DeterministicModelStrongBisimulationDecomposition<ValueType>::buildQuotient(ModelType const& model, Partition const& partition) {
// In order to create the quotient model, we need to construct
// (a) the new transition matrix,
// (b) the new labeling,
@@ -496,8 +594,8 @@ namespace storm {
storm::storage::SparseMatrixBuilder<ValueType> builder(this->size(), this->size());
// Prepare the new state labeling for (b).
- storm::models::AtomicPropositionsLabeling newLabeling(this->size(), dtmc.getStateLabeling().getNumberOfAtomicPropositions());
- std::set<std::string> atomicPropositionsSet = dtmc.getStateLabeling().getAtomicPropositions();
+ storm::models::AtomicPropositionsLabeling newLabeling(this->size(), model.getStateLabeling().getNumberOfAtomicPropositions());
+ std::set<std::string> atomicPropositionsSet = model.getStateLabeling().getAtomicPropositions();
std::vector<std::string> atomicPropositions = std::vector<std::string>(atomicPropositionsSet.begin(), atomicPropositionsSet.end());
for (auto const& ap : atomicPropositions) {
newLabeling.addAtomicProposition(ap);
@@ -510,33 +608,50 @@ 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();
- // Compute the outgoing transitions of the block.
- std::map<storm::storage::sparse::state_type, ValueType> 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);
- }
+ Block const& oldBlock = partition.getBlock(representativeState);
- // Add all atomic propositions to the equivalence class that the representative state satisfies.
- for (auto const& ap : atomicPropositions) {
- if (dtmc.getStateLabeling().getStateHasAtomicProposition(ap, representativeState)) {
- newLabeling.addAtomicPropositionToState(ap, blockIndex);
+ // If the block is absorbing, we simply add a self-loop.
+ if (oldBlock.isAbsorbing()) {
+ builder.addNextValue(blockIndex, blockIndex, storm::utility::constantOne<ValueType>());
+
+ if (oldBlock.hasLabel()) {
+ newLabeling.addAtomicPropositionToState(oldBlock.getLabel(), blockIndex);
+ }
+ } else {
+ // Compute the outgoing transitions of the block.
+ std::map<storm::storage::sparse::state_type, ValueType> blockProbability;
+ for (auto const& entry : model.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);
+ }
+
+ // If the block has a special label, we only add that to the block.
+ if (oldBlock.hasLabel()) {
+ newLabeling.addAtomicPropositionToState(oldBlock.getLabel(), blockIndex);
+ } else {
+ // Otherwise add all atomic propositions to the equivalence class that the representative state
+ // satisfies.
+ for (auto const& ap : atomicPropositions) {
+ if (model.getStateLabeling().getStateHasAtomicProposition(ap, representativeState)) {
+ newLabeling.addAtomicPropositionToState(ap, blockIndex);
+ }
+ }
}
}
}
// Now check which of the blocks of the partition contain at least one initial state.
- for (auto initialState : dtmc.getInitialStates()) {
+ for (auto initialState : model.getInitialStates()) {
Block const& initialBlock = partition.getBlock(initialState);
newLabeling.addAtomicPropositionToState("init", initialBlock.getId());
}
@@ -545,33 +660,21 @@ namespace storm {
// If reward structures are allowed, the quotient structures need to be built here.
// Finally construct the quotient model.
- this->quotient = std::shared_ptr<storm::models::AbstractDeterministicModel<ValueType>>(new storm::models::Dtmc<ValueType>(builder.build(), std::move(newLabeling)));
+ this->quotient = std::shared_ptr<storm::models::AbstractDeterministicModel<ValueType>>(new ModelType(builder.build(), std::move(newLabeling)));
}
template<typename ValueType>
- void DeterministicModelBisimulationDecomposition<ValueType>::computeBisimulationEquivalenceClasses(storm::models::Dtmc<ValueType> const& dtmc, bool weak, bool buildQuotient) {
+ template<typename ModelType>
+ void DeterministicModelStrongBisimulationDecomposition<ValueType>::partitionRefinement(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Partition& partition, bool buildQuotient) {
std::chrono::high_resolution_clock::time_point totalStart = std::chrono::high_resolution_clock::now();
- // We start by computing the initial partition.
- Partition partition(dtmc.getNumberOfStates());
- for (auto const& label : dtmc.getStateLabeling().getAtomicPropositions()) {
- if (label == "init") {
- continue;
- }
- partition.splitLabel(dtmc.getLabeledStates(label));
- }
-
// Initially, all blocks are potential splitter, so we insert them in the splitterQueue.
std::deque<Block*> splitterQueue;
std::for_each(partition.getBlocks().begin(), partition.getBlocks().end(), [&] (Block& a) { splitterQueue.push_back(&a); });
- // FIXME: if weak is set, we want to eliminate the self-loops before doing bisimulation.
-
- storm::storage::SparseMatrix<ValueType> backwardTransitions = dtmc.getBackwardTransitions();
-
// Then perform the actual splitting until there are no more splitters.
while (!splitterQueue.empty()) {
- splitPartition(backwardTransitions, *splitterQueue.front(), partition, splitterQueue);
+ refinePartition(backwardTransitions, *splitterQueue.front(), partition, splitterQueue);
splitterQueue.pop_front();
}
@@ -579,12 +682,14 @@ namespace storm {
// a way that maintains the block IDs as indices.
this->blocks.resize(partition.size());
for (auto const& block : partition.getBlocks()) {
+ // We need to sort the states to allow for rapid construction of the blocks.
+ std::sort(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);
+ this->buildQuotient(model, partition);
}
std::chrono::high_resolution_clock::duration totalTime = std::chrono::high_resolution_clock::now() - totalStart;
@@ -595,7 +700,7 @@ namespace storm {
}
template<typename ValueType>
- std::size_t DeterministicModelBisimulationDecomposition<ValueType>::splitBlockProbabilities(Block& block, Partition& partition, std::deque<Block*>& splitterQueue) {
+ void DeterministicModelStrongBisimulationDecomposition<ValueType>::refineBlockProbabilities(Block& block, Partition& partition, std::deque<Block*>& splitterQueue) {
// Sort the states in the block based on their probabilities.
std::sort(partition.getBeginOfStates(block), partition.getEndOfStates(block), [&partition] (storm::storage::sparse::state_type const& a, storm::storage::sparse::state_type const& b) { return partition.getValue(a) < partition.getValue(b); } );
@@ -615,8 +720,7 @@ namespace storm {
// Now we can check whether the block needs to be split, which is the case iff the probabilities for the
// first and the last state are different.
- std::size_t createdBlocks = 0;
- while (std::abs(partition.getValueAtPosition(beginIndex) - partition.getValueAtPosition(endIndex - 1)) >= 1e-6) {
+ while (!comparator.isEqual(partition.getValueAtPosition(beginIndex), partition.getValueAtPosition(endIndex - 1))) {
// Now we scan for the first state in the block that disagrees on the probability value.
// Note that we do not have to check currentIndex for staying within bounds, because we know the matching
// state is within bounds.
@@ -624,13 +728,12 @@ namespace storm {
typename std::vector<ValueType>::const_iterator valueIterator = partition.getValues().begin() + beginIndex + 1;
++currentIndex;
- while (currentIndex < endIndex && std::abs(*valueIterator - currentValue) <= 1e-6) {
+ while (currentIndex < endIndex && comparator.isEqual(*valueIterator, currentValue)) {
++valueIterator;
++currentIndex;
}
// Now we split the block and mark it as a potential splitter.
- ++createdBlocks;
Block& newBlock = partition.splitBlock(block, currentIndex);
if (!newBlock.isMarkedAsSplitter()) {
splitterQueue.push_back(&newBlock);
@@ -638,12 +741,10 @@ namespace storm {
}
beginIndex = currentIndex;
}
-
- return createdBlocks;
}
template<typename ValueType>
- std::size_t DeterministicModelBisimulationDecomposition<ValueType>::splitPartition(storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Block& splitter, Partition& partition, std::deque<Block*>& splitterQueue) {
+ void DeterministicModelStrongBisimulationDecomposition<ValueType>::refinePartition(storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Block& splitter, Partition& partition, std::deque<Block*>& splitterQueue) {
std::list<Block*> predecessorBlocks;
// Iterate over all states of the splitter and check its predecessors.
@@ -658,7 +759,7 @@ namespace storm {
Block& predecessorBlock = partition.getBlock(predecessor);
// If the predecessor block has just one state, there is no point in splitting it.
- if (predecessorBlock.getNumberOfStates() <= 1) {
+ if (predecessorBlock.getNumberOfStates() <= 1 || predecessorBlock.isAbsorbing()) {
continue;
}
@@ -773,12 +874,31 @@ namespace storm {
continue;
}
- splitBlockProbabilities(*blockPtr, partition, splitterQueue);
+ refineBlockProbabilities(*blockPtr, partition, splitterQueue);
}
-
- return 0;
}
- template class DeterministicModelBisimulationDecomposition<double>;
+ template<typename ValueType>
+ template<typename ModelType>
+ typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition DeterministicModelStrongBisimulationDecomposition<ValueType>::getMeasureDrivenInitialPartition(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::string const& phiLabel, std::string const& psiLabel, bool bounded) {
+ std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::utility::graph::performProb01(backwardTransitions, phiLabel == "true" ? storm::storage::BitVector(model.getNumberOfStates(), true) : model.getLabeledStates(phiLabel), model.getLabeledStates(psiLabel));
+ Partition partition(model.getNumberOfStates(), statesWithProbability01.first, bounded ? model.getLabeledStates(psiLabel) : statesWithProbability01.second, phiLabel, psiLabel);
+ return partition;
+ }
+
+ template<typename ValueType>
+ template<typename ModelType>
+ typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition DeterministicModelStrongBisimulationDecomposition<ValueType>::getLabelBasedInitialPartition(ModelType const& model) {
+ Partition partition(model.getNumberOfStates());
+ for (auto const& label : model.getStateLabeling().getAtomicPropositions()) {
+ if (label == "init") {
+ continue;
+ }
+ partition.splitLabel(model.getLabeledStates(label));
+ }
+ return partition;
+ }
+
+ template class DeterministicModelStrongBisimulationDecomposition<double>;
}
}
\ No newline at end of file
diff --git a/src/storage/DeterministicModelBisimulationDecomposition.h b/src/storage/DeterministicModelStrongBisimulationDecomposition.h
similarity index 56%
rename from src/storage/DeterministicModelBisimulationDecomposition.h
rename to src/storage/DeterministicModelStrongBisimulationDecomposition.h
index c1ca37c18..e5ac547db 100644
--- a/src/storage/DeterministicModelBisimulationDecomposition.h
+++ b/src/storage/DeterministicModelStrongBisimulationDecomposition.h
@@ -1,5 +1,5 @@
-#ifndef STORM_STORAGE_DETERMINISTICMODELBISIMULATIONDECOMPOSITION_H_
-#define STORM_STORAGE_DETERMINISTICMODELBISIMULATIONDECOMPOSITION_H_
+#ifndef STORM_STORAGE_DETERMINISTICMODELSTRONGBISIMULATIONDECOMPOSITION_H_
+#define STORM_STORAGE_DETERMINISTICMODELSTRONGBISIMULATIONDECOMPOSITION_H_
#include <queue>
#include <deque>
@@ -7,21 +7,59 @@
#include "src/storage/sparse/StateType.h"
#include "src/storage/Decomposition.h"
#include "src/models/Dtmc.h"
+#include "src/models/Ctmc.h"
#include "src/storage/Distribution.h"
+#include "src/utility/ConstantsComparator.h"
+#include "src/utility/OsDetection.h"
namespace storm {
namespace storage {
/*!
- * This class represents the decomposition model into its bisimulation quotient.
+ * This class represents the decomposition model into its (strong) bisimulation quotient.
*/
template <typename ValueType>
- class DeterministicModelBisimulationDecomposition : public Decomposition<StateBlock> {
+ class DeterministicModelStrongBisimulationDecomposition : public Decomposition<StateBlock> {
public:
/*!
- * Decomposes the given DTMC into equivalence classes under weak or strong bisimulation.
+ * Decomposes the given DTMC into equivalence classes under strong bisimulation.
+ *
+ * @param model The model to decompose.
+ * @param buildQuotient Sets whether or not the quotient model is to be built.
+ */
+ DeterministicModelStrongBisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, bool buildQuotient = false);
+
+ /*!
+ * Decomposes the given CTMC into equivalence classes under strong bisimulation.
+ *
+ * @param model The model to decompose.
+ * @param buildQuotient Sets whether or not the quotient model is to be built.
+ */
+ DeterministicModelStrongBisimulationDecomposition(storm::models::Ctmc<ValueType> const& model, bool buildQuotient = false);
+
+ /*!
+ * Decomposes the given DTMC into equivalence classes under strong bisimulation in a way that onle safely
+ * preserves formulas of the form phi until psi.
+ *
+ * @param model The model to decompose.
+ * @param phiLabel The label that all phi states carry in the model.
+ * @param psiLabel The label that all psi states carry in the model.
+ * @param bounded If set to true, also bounded until formulas are preserved.
+ * @param buildQuotient Sets whether or not the quotient model is to be built.
*/
- DeterministicModelBisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, bool weak = false, bool buildQuotient = false);
+ DeterministicModelStrongBisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, std::string const& phiLabel, std::string const& psiLabel, bool bounded, bool buildQuotient = false);
+
+ /*!
+ * Decomposes the given CTMC into equivalence classes under strong bisimulation in a way that onle safely
+ * preserves formulas of the form phi until psi.
+ *
+ * @param model The model to decompose.
+ * @param phiLabel The label that all phi states carry in the model.
+ * @param psiLabel The label that all psi states carry in the model.
+ * @param bounded If set to true, also bounded until formulas are preserved.
+ * @param buildQuotient Sets whether or not the quotient model is to be built.
+ */
+ DeterministicModelStrongBisimulationDecomposition(storm::models::Ctmc<ValueType> const& model, std::string const& phiLabel, std::string const& psiLabel, bool bounded, bool buildQuotient = false);
/*!
* Retrieves the quotient of the model under the previously computed bisimulation.
@@ -37,7 +75,7 @@ namespace storm {
public:
typedef typename std::list<Block>::const_iterator const_iterator;
- Block(storm::storage::sparse::state_type begin, storm::storage::sparse::state_type end, Block* prev, Block* next);
+ Block(storm::storage::sparse::state_type begin, storm::storage::sparse::state_type end, Block* prev, Block* next, std::shared_ptr<std::string> const& label = nullptr);
// Prints the block.
void print(Partition const& partition) const;
@@ -138,6 +176,21 @@ namespace storm {
// Removes the marking.
void unmarkAsPredecessorBlock();
+ // Sets whether or not the block is to be interpreted as absorbing.
+ void setAbsorbing(bool absorbing);
+
+ // Retrieves whether the block is to be interpreted as absorbing.
+ bool isAbsorbing() const;
+
+ // Retrieves whether the block has a special label.
+ bool hasLabel() const;
+
+ // Retrieves the special label of the block if it has one.
+ std::string const& getLabel() const;
+
+ // Retrieves a pointer to the label of the block (which is the nullptr if there is none).
+ std::shared_ptr<std::string> const& getLabelPtr() const;
+
private:
// An iterator to itself. This is needed to conveniently insert elements in the overall list of blocks
// kept by the partition.
@@ -160,8 +213,17 @@ namespace storm {
// A position that can be used to store a certain position within the block.
storm::storage::sparse::state_type markedPosition;
+ // A flag indicating whether the block is to be interpreted as absorbing or not.
+ bool absorbing;
+
// The ID of the block. This is only used for debugging purposes.
std::size_t id;
+
+ // The label of the block or nullptr if it has none.
+ std::shared_ptr<std::string> label;
+
+ // A counter for the IDs of the blocks.
+ static std::size_t blockId;
};
class Partition {
@@ -170,8 +232,31 @@ namespace storm {
/*!
* Creates a partition with one block consisting of all the states.
+ *
+ * @param numberOfStates The number of states the partition holds.
*/
Partition(std::size_t numberOfStates);
+
+ /*!
+ * Creates a partition with three blocks: one with all phi states, one with all psi states and one with
+ * all other states. The former two blocks are marked as being absorbing, because their outgoing
+ * transitions shall not be taken into account for future refinement.
+ *
+ * @param numberOfStates The number of states the partition holds.
+ * @param prob0States The states which have probability 0 of satisfying phi until psi.
+ * @param prob1States The states which have probability 1 of satisfying phi until psi.
+ * @param otherLabel The label that is to be attached to all other states.
+ * @param prob1Label The label that is to be attached to all states with probability 1.
+ */
+ Partition(std::size_t numberOfStates, storm::storage::BitVector const& prob0States, storm::storage::BitVector const& prob1States, std::string const& otherLabel, std::string const& prob1Label);
+
+ Partition() = default;
+ Partition(Partition const& other) = default;
+ Partition& operator=(Partition const& other) = default;
+#ifndef WINDOWS
+ Partition(Partition&& other) = default;
+ Partition& operator=(Partition&& other) = default;
+#endif
/*!
* Splits all blocks of the partition such that afterwards all blocks contain only states with the label
@@ -262,6 +347,8 @@ namespace storm {
// Updates the block mapping for the given range of states to the specified block.
void updateBlockMapping(Block& block, std::vector<storm::storage::sparse::state_type>::iterator first, std::vector<storm::storage::sparse::state_type>::iterator end);
+ // Retrieves the first block of the partition.
+ Block& getFirstBlock();
private:
// The list of blocks in the partition.
std::list<Block> blocks;
@@ -280,18 +367,86 @@ namespace storm {
std::vector<ValueType> values;
};
- void computeBisimulationEquivalenceClasses(storm::models::Dtmc<ValueType> const& model, bool weak, bool buildQuotient);
+ /*!
+ * Performs the partition refinement on the model and thereby computes the equivalence classes under strong
+ * bisimulation equivalence. If required, the quotient model is built and may be retrieved using
+ * getQuotient().
+ *
+ * @param model The model on whose state space to compute the coarses strong bisimulation relation.
+ * @param backwardTransitions The backward transitions of the model.
+ * @param The initial partition.
+ * @param buildQuotient If set, the quotient model is built and may be retrieved using the getQuotient()
+ * method.
+ */
+ template<typename ModelType>
+ void partitionRefinement(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Partition& partition, bool buildQuotient);
- std::size_t splitPartition(storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Block& splitter, Partition& partition, std::deque<Block*>& splitterQueue);
+ /*!
+ * Refines the partition based on the provided splitter. After calling this method all blocks are stable
+ * with respect to the splitter.
+ *
+ * @param backwardTransitions A matrix that can be used to retrieve the predecessors (and their
+ * probabilities).
+ * @param splitter The splitter to use.
+ * @param partition The partition to split.
+ * @param splitterQueue A queue into which all blocks that were split are inserted so they can be treated
+ * as splitters in the future.
+ */
+ void refinePartition(storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Block& splitter, Partition& partition, std::deque<Block*>& splitterQueue);
- std::size_t splitBlockProbabilities(Block& block, Partition& partition, std::deque<Block*>& splitterQueue);
+ /*!
+ * Refines the block based on their probability values (leading into the splitter).
+ *
+ * @param block The block to refine.
+ * @param partition The partition that contains the block.
+ * @param splitterQueue A queue into which all blocks that were split are inserted so they can be treated
+ * as splitters in the future.
+ */
+ void refineBlockProbabilities(Block& block, Partition& partition, std::deque<Block*>& splitterQueue);
- void buildQuotient(storm::models::Dtmc<ValueType> const& dtmc, Partition const& partition);
+ /*!
+ * Builds the quotient model based on the previously computed equivalence classes (stored in the blocks
+ * of the decomposition.
+ *
+ * @param model The model whose state space was used for computing the equivalence classes. This is used for
+ * determining the transitions of each equivalence class.
+ * @param partition The previously computed partition. This is used for quickly retrieving the block of a
+ * state.
+ */
+ template<typename ModelType>
+ void buildQuotient(ModelType const& model, Partition const& partition);
+ /*!
+ * Creates the measure-driven initial partition for reaching psi states from phi states.
+ *
+ * @param model The model whose state space is partitioned based on reachability of psi states from phi
+ * states.
+ * @param backwardTransitions The backward transitions of the model.
+ * @param phiLabel The label that all phi states carry in the model.
+ * @param psiLabel The label that all psi states carry in the model.
+ * @param bounded If set to true, the initial partition will be chosen in such a way that preserves bounded
+ * reachability queries.
+ * @return The resulting partition.
+ */
+ template<typename ModelType>
+ Partition getMeasureDrivenInitialPartition(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::string const& phiLabel, std::string const& psiLabel, bool bounded = false);
+
+ /*!
+ * Creates the initial partition based on all the labels in the given model.
+ *
+ * @param model The model whose state space is partitioned based on its labels.
+ * @return The resulting partition.
+ */
+ template<typename ModelType>
+ Partition getLabelBasedInitialPartition(ModelType const& model);
+
// If required, a quotient model is built and stored in this member.
std::shared_ptr<storm::models::AbstractDeterministicModel<ValueType>> quotient;
+
+ // A comparator that is used for determining whether two probabilities are considered to be equal.
+ storm::utility::ConstantsComparator<ValueType> comparator;
};
}
}
-#endif /* STORM_STORAGE_DETERMINISTICMODELBISIMULATIONDECOMPOSITION_H_ */
\ No newline at end of file
+#endif /* STORM_STORAGE_DETERMINISTICMODELSTRONGBISIMULATIONDECOMPOSITION_H_ */
\ No newline at end of file
diff --git a/src/utility/ConstantsComparator.h b/src/utility/ConstantsComparator.h
new file mode 100644
index 000000000..fc46b251f
--- /dev/null
+++ b/src/utility/ConstantsComparator.h
@@ -0,0 +1,84 @@
+#ifndef STORM_UTILITY_CONSTANTSCOMPARATOR_H_
+#define STORM_UTILITY_CONSTANTSCOMPARATOR_H_
+
+#ifdef max
+# undef max
+#endif
+
+#ifdef min
+# undef min
+#endif
+
+#include <limits>
+#include <cstdint>
+
+#include "src/settings/SettingsManager.h"
+
+namespace storm {
+ namespace utility {
+
+ template<typename ValueType>
+ ValueType one() {
+ return ValueType(1);
+ }
+
+ template<typename ValueType>
+ ValueType zero() {
+ return ValueType(0);
+ }
+
+ template<typename ValueType>
+ ValueType infinity() {
+ return std::numeric_limits<ValueType>::infinity();
+ }
+
+ // A class that can be used for comparing constants.
+ template<typename ValueType>
+ class ConstantsComparator {
+ public:
+ bool isOne(ValueType const& value) {
+ return value == one<ValueType>();
+ }
+
+ bool isZero(ValueType const& value) {
+ return value == zero<ValueType>();
+ }
+
+ bool isEqual(ValueType const& value1, ValueType const& value2) {
+ return value1 == value2;
+ }
+ };
+
+ // For doubles we specialize this class and consider the comparison modulo some predefined precision.
+ template<>
+ class ConstantsComparator<double> {
+ public:
+ ConstantsComparator() : precision(storm::settings::generalSettings().getPrecision()) {
+ // Intentionally left empty.
+ }
+
+ ConstantsComparator(double precision) : precision(precision) {
+ // Intentionally left empty.
+ }
+
+ bool isOne(double const& value) {
+ return std::abs(value - one<double>()) <= precision;
+ }
+
+ bool isZero(double const& value) {
+ return std::abs(value) <= precision;
+ }
+
+ bool isEqual(double const& value1, double const& value2) {
+ return std::abs(value1 - value2) <= precision;
+ }
+
+ private:
+ // The precision used for comparisons.
+ double precision;
+ };
+
+ }
+}
+
+#endif /* STORM_UTILITY_CONSTANTSCOMPARATOR_H_ */
\ No newline at end of file
diff --git a/src/utility/cli.h b/src/utility/cli.h
index 813a6fa74..908d7dc52 100644
--- a/src/utility/cli.h
+++ b/src/utility/cli.h
@@ -47,7 +47,7 @@ log4cplus::Logger logger;
// Headers for model processing.
#include "src/storage/NaiveDeterministicModelBisimulationDecomposition.h"
-#include "src/storage/DeterministicModelBisimulationDecomposition.h"
+#include "src/storage/DeterministicModelStrongBisimulationDecomposition.h"
// Headers for counterexample generation.
#include "src/counterexamples/MILPMinimalLabelSetGenerator.h"
@@ -267,7 +267,7 @@ namespace storm {
std::shared_ptr<storm::models::Dtmc<double>> dtmc = result->template as<storm::models::Dtmc<double>>();
STORM_PRINT(std::endl << "Performing bisimulation minimization..." << std::endl);
- storm::storage::DeterministicModelBisimulationDecomposition<double> bisimulationDecomposition(*dtmc, false, true);
+ storm::storage::DeterministicModelStrongBisimulationDecomposition<double> bisimulationDecomposition(*dtmc, true);
result = bisimulationDecomposition.getQuotient();
@@ -285,7 +285,7 @@ namespace storm {
std::shared_ptr<storm::models::Mdp<double>> mdp = model->as<storm::models::Mdp<double>>();
- // FIXME: re-parse the program.
+ // FIXME: do not re-parse the program.
std::string const programFile = storm::settings::generalSettings().getSymbolicModelFilename();
std::string const constants = storm::settings::generalSettings().getConstantDefinitionString();
storm::prism::Program program = storm::parser::PrismParser::parse(programFile);
diff --git a/src/utility/graph.h b/src/utility/graph.h
index 21972adbc..3af235fe3 100644
--- a/src/utility/graph.h
+++ b/src/utility/graph.h
@@ -204,6 +204,25 @@ namespace storm {
return result;
}
+ /*!
+ * Computes the sets of states that have probability 0 or 1, respectively, of satisfying phi until psi in a
+ * deterministic model.
+ *
+ * @param backwardTransitions The backward transitions of the model whose graph structure to search.
+ * @param phiStates The set of all states satisfying phi.
+ * @param psiStates The set of all states satisfying psi.
+ * @return A pair of bit vectors such that the first bit vector stores the indices of all states
+ * with probability 0 and the second stores all indices of states with probability 1.
+ */
+ template <typename T>
+ static std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01(storm::storage::SparseMatrix<T> backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
+ std::pair<storm::storage::BitVector, storm::storage::BitVector> result;
+ result.first = performProbGreater0(backwardTransitions, phiStates, psiStates);
+ result.second = performProb1(backwardTransitions, phiStates, psiStates, result.first);
+ result.first.complement();
+ return result;
+ }
+
/*!
* Computes the sets of states that have probability greater 0 of satisfying phi until psi under at least
* one possible resolution of non-determinism in a non-deterministic model. Stated differently,