From 370a0ae47642c6316b944a3377f2fa28f919da03 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Thu, 27 Nov 2014 15:22:47 +0100
Subject: [PATCH] Fixed some issues in bisimulation and added some tests.
Former-commit-id: 98801de9db21fc4aeb4eaa50ec328533449a5e19
---
src/exceptions/BaseException.cpp | 2 +-
src/settings/OptionBuilder.h | 2 +-
...ministicModelBisimulationDecomposition.cpp | 76 +++++++++++--------
...erministicModelBisimulationDecomposition.h | 26 ++++---
src/storage/StateBlock.h | 2 +-
src/utility/cli.h | 2 +-
...sticModelBisimulationDecompositionTest.cpp | 67 ++++++++++++++++
7 files changed, 134 insertions(+), 43 deletions(-)
create mode 100644 test/functional/storage/DeterministicModelBisimulationDecompositionTest.cpp
diff --git a/src/exceptions/BaseException.cpp b/src/exceptions/BaseException.cpp
index 0cb03e00f..ed28a918c 100644
--- a/src/exceptions/BaseException.cpp
+++ b/src/exceptions/BaseException.cpp
@@ -18,7 +18,7 @@ namespace storm {
// Intentionally left empty.
}
- const char* BaseException::what() const {
+ const char* BaseException::what() const noexcept {
std::string errorString = this->stream.str();
char* result = new char[errorString.size() + 1];
result[errorString.size()] = '\0';
diff --git a/src/settings/OptionBuilder.h b/src/settings/OptionBuilder.h
index 2d7ad9a19..abcd35862 100644
--- a/src/settings/OptionBuilder.h
+++ b/src/settings/OptionBuilder.h
@@ -68,7 +68,7 @@ namespace storm {
*/
OptionBuilder& addArgument(std::shared_ptr<ArgumentBase> argument) {
STORM_LOG_THROW(!this->isBuild, storm::exceptions::IllegalFunctionCallException, "Cannot add an argument to an option builder that was already used to build the option.");
- STORM_LOG_THROW(this->arguments.empty() || !argument->getIsOptional() || this->arguments.back()->getIsOptional(), storm::exceptions::IllegalArgumentException, "Unable to add non-optional argument after an option that is optional.");
+ STORM_LOG_THROW(this->arguments.empty() || argument->getIsOptional() || !this->arguments.back()->getIsOptional(), storm::exceptions::IllegalArgumentException, "Unable to add non-optional argument after an option that is optional.");
std::string lowerArgumentName = boost::algorithm::to_lower_copy(argument->getName());
STORM_LOG_THROW(argumentNameSet.find(lowerArgumentName) == argumentNameSet.end(), storm::exceptions::IllegalArgumentException, "Unable to add argument to option, because it already has an argument with the same name.");
diff --git a/src/storage/DeterministicModelBisimulationDecomposition.cpp b/src/storage/DeterministicModelBisimulationDecomposition.cpp
index ccb33a153..7d8287dd0 100644
--- a/src/storage/DeterministicModelBisimulationDecomposition.cpp
+++ b/src/storage/DeterministicModelBisimulationDecomposition.cpp
@@ -13,10 +13,7 @@ namespace storm {
namespace storage {
template<typename ValueType>
- std::size_t DeterministicModelBisimulationDecomposition<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, 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) {
+ DeterministicModelBisimulationDecomposition<ValueType>::Block::Block(storm::storage::sparse::state_type begin, storm::storage::sparse::state_type end, Block* prev, Block* next, std::size_t id, std::shared_ptr<std::string> const& label) : next(next), prev(prev), begin(begin), end(end), markedAsSplitter(false), markedAsPredecessorBlock(false), markedPosition(begin), absorbing(false), id(id), label(label) {
if (next != nullptr) {
next->prev = this;
}
@@ -247,7 +244,7 @@ namespace storm {
template<typename ValueType>
DeterministicModelBisimulationDecomposition<ValueType>::Partition::Partition(std::size_t numberOfStates, bool keepSilentProbabilities) : stateToBlockMapping(numberOfStates), statesAndValues(numberOfStates), positions(numberOfStates), keepSilentProbabilities(keepSilentProbabilities), silentProbabilities() {
// 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);
+ typename std::list<Block>::iterator it = blocks.emplace(this->blocks.end(), 0, numberOfStates, nullptr, nullptr, this->blocks.size());
it->setIterator(it);
// Set up the different parts of the internal structure.
@@ -265,7 +262,7 @@ namespace storm {
template<typename ValueType>
DeterministicModelBisimulationDecomposition<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, bool keepSilentProbabilities) : stateToBlockMapping(numberOfStates), statesAndValues(numberOfStates), positions(numberOfStates), keepSilentProbabilities(keepSilentProbabilities), silentProbabilities() {
- typename std::list<Block>::iterator firstIt = blocks.emplace(this->blocks.end(), 0, prob0States.getNumberOfSetBits(), nullptr, nullptr);
+ typename std::list<Block>::iterator firstIt = blocks.emplace(this->blocks.end(), 0, prob0States.getNumberOfSetBits(), nullptr, nullptr, this->blocks.size());
Block& firstBlock = *firstIt;
firstBlock.setIterator(firstIt);
@@ -278,7 +275,7 @@ namespace storm {
}
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)));
+ typename std::list<Block>::iterator secondIt = blocks.emplace(this->blocks.end(), position, position + prob1States.getNumberOfSetBits(), &firstBlock, nullptr, this->blocks.size(), std::shared_ptr<std::string>(new std::string(prob1Label)));
Block& secondBlock = *secondIt;
secondBlock.setIterator(secondIt);
@@ -290,7 +287,7 @@ namespace storm {
}
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)));
+ typename std::list<Block>::iterator thirdIt = blocks.emplace(this->blocks.end(), position, numberOfStates, &secondBlock, nullptr, this->blocks.size(), otherLabel == "true" ? std::shared_ptr<std::string>(nullptr) : std::shared_ptr<std::string>(new std::string(otherLabel)));
Block& thirdBlock = *thirdIt;
thirdBlock.setIterator(thirdIt);
@@ -411,7 +408,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, block.getLabelPtr());
+ typename std::list<Block>::iterator selfIt = this->blocks.emplace(block.getIterator(), block.getBegin(), position, block.getPreviousBlockPointer(), &block, this->blocks.size(), block.getLabelPtr());
selfIt->setIterator(selfIt);
Block& newBlock = *selfIt;
@@ -435,7 +432,7 @@ namespace storm {
}
// Actually insert the new block.
- typename std::list<Block>::iterator it = this->blocks.emplace(block.getIterator(), begin, block.getBegin(), block.getPreviousBlockPointer(), &block);
+ typename std::list<Block>::iterator it = this->blocks.emplace(block.getIterator(), begin, block.getBegin(), block.getPreviousBlockPointer(), &block, this->blocks.size());
Block& newBlock = *it;
newBlock.setIterator(it);
@@ -563,9 +560,16 @@ namespace storm {
}
std::cout << std::endl << "state to block mapping: " << std::endl;
for (auto const& block : stateToBlockMapping) {
- std::cout << block << " ";
+ std::cout << block << "[" << block->getId() <<"] ";
}
std::cout << std::endl;
+ if (this->keepSilentProbabilities) {
+ std::cout << "silent probabilities" << std::endl;
+ for (auto const& prob : silentProbabilities) {
+ std::cout << prob << " ";
+ }
+ std::cout << std::endl;
+ }
std::cout << "size: " << this->blocks.size() << std::endl;
assert(this->check());
}
@@ -576,21 +580,21 @@ namespace storm {
}
template<typename ValueType>
- DeterministicModelBisimulationDecomposition<ValueType>::DeterministicModelBisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, bool weak, bool buildQuotient) : comparator() {
- STORM_LOG_THROW(!model.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures.");
+ DeterministicModelBisimulationDecomposition<ValueType>::DeterministicModelBisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, boost::optional<std::set<std::string>> const& atomicPropositions, bool weak, bool buildQuotient) : comparator() {
+ STORM_LOG_THROW(!model.hasStateRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures.");
storm::storage::SparseMatrix<ValueType> backwardTransitions = model.getBackwardTransitions();
BisimulationType bisimulationType = weak ? BisimulationType::WeakDtmc : BisimulationType::Strong;
- Partition initialPartition = getLabelBasedInitialPartition(model, backwardTransitions, bisimulationType);
- partitionRefinement(model, backwardTransitions, initialPartition, bisimulationType, buildQuotient);
+ Partition initialPartition = getLabelBasedInitialPartition(model, backwardTransitions, bisimulationType, atomicPropositions);
+ partitionRefinement(model, atomicPropositions, backwardTransitions, initialPartition, bisimulationType, buildQuotient);
}
template<typename ValueType>
- DeterministicModelBisimulationDecomposition<ValueType>::DeterministicModelBisimulationDecomposition(storm::models::Ctmc<ValueType> const& model, bool weak, bool buildQuotient) {
+ DeterministicModelBisimulationDecomposition<ValueType>::DeterministicModelBisimulationDecomposition(storm::models::Ctmc<ValueType> const& model, boost::optional<std::set<std::string>> const& atomicPropositions, bool weak, 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();
BisimulationType bisimulationType = weak ? BisimulationType::WeakCtmc : BisimulationType::Strong;
- Partition initialPartition = getLabelBasedInitialPartition(model, backwardTransitions, bisimulationType);
- partitionRefinement(model, backwardTransitions, initialPartition, bisimulationType, buildQuotient);
+ Partition initialPartition = getLabelBasedInitialPartition(model, backwardTransitions, bisimulationType, atomicPropositions);
+ partitionRefinement(model, atomicPropositions, backwardTransitions, initialPartition, bisimulationType, buildQuotient);
}
template<typename ValueType>
@@ -600,7 +604,7 @@ namespace storm {
storm::storage::SparseMatrix<ValueType> backwardTransitions = model.getBackwardTransitions();
BisimulationType bisimulationType = weak ? BisimulationType::WeakDtmc : BisimulationType::Strong;
Partition initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, phiLabel, psiLabel, bisimulationType, bounded);
- partitionRefinement(model, model.getBackwardTransitions(), initialPartition, bisimulationType, buildQuotient);
+ partitionRefinement(model, std::set<std::string>({phiLabel, psiLabel}), model.getBackwardTransitions(), initialPartition, bisimulationType, buildQuotient);
}
template<typename ValueType>
@@ -610,7 +614,7 @@ namespace storm {
storm::storage::SparseMatrix<ValueType> backwardTransitions = model.getBackwardTransitions();
BisimulationType bisimulationType = weak ? BisimulationType::WeakCtmc : BisimulationType::Strong;
Partition initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, phiLabel, psiLabel, bisimulationType, bounded);
- partitionRefinement(model, model.getBackwardTransitions(), initialPartition, bisimulationType, buildQuotient);
+ partitionRefinement(model, std::set<std::string>({phiLabel, psiLabel}), model.getBackwardTransitions(), initialPartition, bisimulationType, buildQuotient);
}
template<typename ValueType>
@@ -621,7 +625,7 @@ namespace storm {
template<typename ValueType>
template<typename ModelType>
- void DeterministicModelBisimulationDecomposition<ValueType>::buildQuotient(ModelType const& model, Partition const& partition, BisimulationType bisimulationType) {
+ void DeterministicModelBisimulationDecomposition<ValueType>::buildQuotient(ModelType const& model, boost::optional<std::set<std::string>> const& selectedAtomicPropositions, Partition const& partition, BisimulationType bisimulationType) {
// In order to create the quotient model, we need to construct
// (a) the new transition matrix,
// (b) the new labeling,
@@ -632,7 +636,8 @@ namespace storm {
// 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::set<std::string> atomicPropositionsSet = selectedAtomicPropositions ? selectedAtomicPropositions.get() : model.getStateLabeling().getAtomicPropositions();
+ atomicPropositionsSet.insert("init");
std::vector<std::string> atomicPropositions = std::vector<std::string>(atomicPropositionsSet.begin(), atomicPropositionsSet.end());
for (auto const& ap : atomicPropositions) {
newLabeling.addAtomicProposition(ap);
@@ -646,7 +651,8 @@ namespace storm {
// they all behave equally.
storm::storage::sparse::state_type representativeState = *block.begin();
- // However, for weak bisimulation, we need to make sure the representative state is a non-silent one.
+ // However, for weak bisimulation, we need to make sure the representative state is a non-silent one (if
+ // there is any such state).
if (bisimulationType == BisimulationType::WeakDtmc) {
for (auto const& state : block) {
if (!partition.isSilent(state, comparator)) {
@@ -731,7 +737,7 @@ namespace storm {
template<typename ValueType>
template<typename ModelType>
- void DeterministicModelBisimulationDecomposition<ValueType>::partitionRefinement(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Partition& partition, BisimulationType bisimulationType, bool buildQuotient) {
+ void DeterministicModelBisimulationDecomposition<ValueType>::partitionRefinement(ModelType const& model, boost::optional<std::set<std::string>> const& atomicPropositions, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Partition& partition, BisimulationType bisimulationType, bool buildQuotient) {
std::chrono::high_resolution_clock::time_point totalStart = std::chrono::high_resolution_clock::now();
// Initially, all blocks are potential splitter, so we insert them in the splitterQueue.
@@ -769,7 +775,7 @@ namespace storm {
// If we are required to build the quotient model, do so now.
if (buildQuotient) {
- this->buildQuotient(model, partition, bisimulationType);
+ this->buildQuotient(model, atomicPropositions, partition, bisimulationType);
}
std::chrono::high_resolution_clock::duration extractionTime = std::chrono::high_resolution_clock::now() - extractionStart;
@@ -1265,13 +1271,23 @@ namespace storm {
template<typename ValueType>
template<typename ModelType>
- typename DeterministicModelBisimulationDecomposition<ValueType>::Partition DeterministicModelBisimulationDecomposition<ValueType>::getLabelBasedInitialPartition(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, BisimulationType bisimulationType) {
+ typename DeterministicModelBisimulationDecomposition<ValueType>::Partition DeterministicModelBisimulationDecomposition<ValueType>::getLabelBasedInitialPartition(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, BisimulationType bisimulationType, boost::optional<std::set<std::string>> const& atomicPropositions) {
Partition partition(model.getNumberOfStates(), bisimulationType == BisimulationType::WeakDtmc);
- for (auto const& label : model.getStateLabeling().getAtomicPropositions()) {
- if (label == "init") {
- continue;
+
+ if (atomicPropositions) {
+ for (auto const& label : atomicPropositions.get()) {
+ if (label == "init") {
+ continue;
+ }
+ partition.splitLabel(model.getLabeledStates(label));
+ }
+ } else {
+ for (auto const& label : model.getStateLabeling().getAtomicPropositions()) {
+ if (label == "init") {
+ continue;
+ }
+ partition.splitLabel(model.getLabeledStates(label));
}
- partition.splitLabel(model.getLabeledStates(label));
}
// If we are creating the initial partition for weak bisimulation, we need to (a) split off all divergent
diff --git a/src/storage/DeterministicModelBisimulationDecomposition.h b/src/storage/DeterministicModelBisimulationDecomposition.h
index 47d605b99..1a25815c9 100644
--- a/src/storage/DeterministicModelBisimulationDecomposition.h
+++ b/src/storage/DeterministicModelBisimulationDecomposition.h
@@ -25,19 +25,23 @@ namespace storm {
* Decomposes the given DTMC into equivalence classes under weak or strong bisimulation.
*
* @param model The model to decompose.
+ * @param A set of atomic propositions that is to be respected. If not given, all atomic propositions of the
+ * model will be respected. If built, the quotient model will only contain the respected atomic propositions.
* @param weak A flag indication whether a weak bisimulation is to be computed.
* @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);
+ DeterministicModelBisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, boost::optional<std::set<std::string>> const& atomicPropositions = boost::optional<std::set<std::string>>(), bool weak = false, bool buildQuotient = false);
/*!
* Decomposes the given CTMC into equivalence classes under weak or strong bisimulation.
*
* @param model The model to decompose.
+ * @param A set of atomic propositions that is to be respected. If not given, all atomic propositions of the
+ * model will be respected. If built, the quotient model will only contain the respected atomic propositions.
* @param weak A flag indication whether a weak bisimulation is to be computed.
* @param buildQuotient Sets whether or not the quotient model is to be built.
*/
- DeterministicModelBisimulationDecomposition(storm::models::Ctmc<ValueType> const& model, bool weak = false, bool buildQuotient = false);
+ DeterministicModelBisimulationDecomposition(storm::models::Ctmc<ValueType> const& model, boost::optional<std::set<std::string>> const& atomicPropositions = boost::optional<std::set<std::string>>(), bool weak = false, bool buildQuotient = false);
/*!
* Decomposes the given DTMC into equivalence classes under strong bisimulation in a way that onle safely
@@ -83,7 +87,7 @@ namespace storm {
typedef typename std::list<Block>::const_iterator const_iterator;
// Creates a new block with the given begin and end.
- 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);
+ Block(storm::storage::sparse::state_type begin, storm::storage::sparse::state_type end, Block* prev, Block* next, std::size_t id, std::shared_ptr<std::string> const& label = nullptr);
// Prints the block.
void print(Partition const& partition) const;
@@ -226,9 +230,6 @@ namespace storm {
// 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 {
@@ -394,6 +395,8 @@ namespace storm {
* getQuotient().
*
* @param model The model on whose state space to compute the coarses strong bisimulation relation.
+ * @param atomicPropositions The set of atomic propositions that the bisimulation considers. If not given,
+ * all atomic propositions are considered.
* @param backwardTransitions The backward transitions of the model.
* @param The initial partition.
* @param bisimulationType The kind of bisimulation that is to be computed.
@@ -401,7 +404,7 @@ namespace storm {
* method.
*/
template<typename ModelType>
- void partitionRefinement(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Partition& partition, BisimulationType bisimulationType, bool buildQuotient);
+ void partitionRefinement(ModelType const& model, boost::optional<std::set<std::string>> const& atomicPropositions, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Partition& partition, BisimulationType bisimulationType, bool buildQuotient);
/*!
* Refines the partition based on the provided splitter. After calling this method all blocks are stable
@@ -445,12 +448,15 @@ namespace storm {
*
* @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 selectedAtomicPropositions The set of atomic propositions that was considered by the bisimulation. The
+ * quotient will only have these atomic propositions. If not given, all atomic propositions will be
+ * considered.
* @param partition The previously computed partition. This is used for quickly retrieving the block of a
* state.
* @param bisimulationType The kind of bisimulation that is to be computed.
*/
template<typename ModelType>
- void buildQuotient(ModelType const& model, Partition const& partition, BisimulationType bisimulationType);
+ void buildQuotient(ModelType const& model, boost::optional<std::set<std::string>> const& selectedAtomicPropositions, Partition const& partition, BisimulationType bisimulationType);
/*!
* Creates the measure-driven initial partition for reaching psi states from phi states.
@@ -474,10 +480,12 @@ namespace storm {
* @param model The model whose state space is partitioned based on its labels.
* @param backwardTransitions The backward transitions of the model.
* @param bisimulationType The kind of bisimulation that is to be computed.
+ * @param atomicPropositions The set of atomic propositions to respect. If not given, then all atomic
+ * propositions of the model are respected.
* @return The resulting partition.
*/
template<typename ModelType>
- Partition getLabelBasedInitialPartition(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, BisimulationType bisimulationType);
+ Partition getLabelBasedInitialPartition(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, BisimulationType bisimulationType, boost::optional<std::set<std::string>> const& atomicPropositions = boost::optional<std::set<std::string>>());
/*!
* Splits all blocks of the given partition into a block that contains all divergent states and another block
diff --git a/src/storage/StateBlock.h b/src/storage/StateBlock.h
index e9a8d5ebe..32d21c98c 100644
--- a/src/storage/StateBlock.h
+++ b/src/storage/StateBlock.h
@@ -10,7 +10,7 @@
namespace storm {
namespace storage {
- // Typedef the most common state container
+ // Typedef the most common state container.
typedef boost::container::flat_set<sparse::state_type> FlatSetStateContainer;
std::ostream& operator<<(std::ostream& out, FlatSetStateContainer const& block);
diff --git a/src/utility/cli.h b/src/utility/cli.h
index a185a56a2..1051d22b6 100644
--- a/src/utility/cli.h
+++ b/src/utility/cli.h
@@ -271,7 +271,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, storm::settings::bisimulationSettings().isWeakBisimulationSet(), true);
+ storm::storage::DeterministicModelBisimulationDecomposition<double> bisimulationDecomposition(*dtmc, boost::optional<std::set<std::string>>(), storm::settings::bisimulationSettings().isWeakBisimulationSet(), true);
result = bisimulationDecomposition.getQuotient();
diff --git a/test/functional/storage/DeterministicModelBisimulationDecompositionTest.cpp b/test/functional/storage/DeterministicModelBisimulationDecompositionTest.cpp
new file mode 100644
index 000000000..f984b0fe9
--- /dev/null
+++ b/test/functional/storage/DeterministicModelBisimulationDecompositionTest.cpp
@@ -0,0 +1,67 @@
+#include "gtest/gtest.h"
+#include "storm-config.h"
+#include "src/parser/AutoParser.h"
+#include "storage/DeterministicModelBisimulationDecomposition.h"
+
+TEST(DeterministicModelBisimulationDecomposition, Die) {
+ std::shared_ptr<storm::models::AbstractModel<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/die/die.tra", STORM_CPP_BASE_PATH "/examples/dtmc/die/die.lab", "", "");
+
+ ASSERT_EQ(abstractModel->getType(), storm::models::DTMC);
+ std::shared_ptr<storm::models::Dtmc<double>> dtmc = abstractModel->as<storm::models::Dtmc<double>>();
+
+ storm::storage::DeterministicModelBisimulationDecomposition<double> bisim(*dtmc, boost::optional<std::set<std::string>>(), false, true);
+ std::shared_ptr<storm::models::AbstractModel<double>> result;
+ ASSERT_NO_THROW(result = bisim.getQuotient());
+
+ EXPECT_EQ(storm::models::DTMC, result->getType());
+ EXPECT_EQ(13, result->getNumberOfStates());
+ EXPECT_EQ(20, result->getNumberOfTransitions());
+
+ storm::storage::DeterministicModelBisimulationDecomposition<double> bisim2(*dtmc, std::set<std::string>({"one"}), false, true);
+ ASSERT_NO_THROW(result = bisim2.getQuotient());
+
+ EXPECT_EQ(storm::models::DTMC, result->getType());
+ EXPECT_EQ(5, result->getNumberOfStates());
+ EXPECT_EQ(8, result->getNumberOfTransitions());
+
+ storm::storage::DeterministicModelBisimulationDecomposition<double> bisim3(*dtmc, std::set<std::string>({"one"}), true, true);
+ ASSERT_NO_THROW(result = bisim3.getQuotient());
+
+ EXPECT_EQ(storm::models::DTMC, result->getType());
+ EXPECT_EQ(5, result->getNumberOfStates());
+ EXPECT_EQ(8, result->getNumberOfTransitions());
+
+// std::shared_ptr<storm::models::AbstractModel<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/die/die.tra", STORM_CPP_BASE_PATH "/examples/dtmc/die/die.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/die/die.coin_flips.trans.rew");
+//
+// ASSERT_EQ(abstractModel->getType(), storm::models::DTMC);
+// std::shared_ptr<storm::models::Dtmc<double>> dtmc = abstractModel->as<storm::models::Dtmc<double>>();
+}
+
+TEST(DeterministicModelBisimulationDecomposition, Crowds) {
+ std::shared_ptr<storm::models::AbstractModel<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds5_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds5_5.lab", "", "");
+
+ ASSERT_EQ(abstractModel->getType(), storm::models::DTMC);
+ std::shared_ptr<storm::models::Dtmc<double>> dtmc = abstractModel->as<storm::models::Dtmc<double>>();
+
+ storm::storage::DeterministicModelBisimulationDecomposition<double> bisim(*dtmc, boost::optional<std::set<std::string>>(), false, true);
+ std::shared_ptr<storm::models::AbstractModel<double>> result;
+ ASSERT_NO_THROW(result = bisim.getQuotient());
+
+ EXPECT_EQ(storm::models::DTMC, result->getType());
+ EXPECT_EQ(334, result->getNumberOfStates());
+ EXPECT_EQ(546, result->getNumberOfTransitions());
+
+ storm::storage::DeterministicModelBisimulationDecomposition<double> bisim2(*dtmc, std::set<std::string>({"observe0Greater1"}), false, true);
+ ASSERT_NO_THROW(result = bisim2.getQuotient());
+
+ EXPECT_EQ(storm::models::DTMC, result->getType());
+ EXPECT_EQ(65, result->getNumberOfStates());
+ EXPECT_EQ(105, result->getNumberOfTransitions());
+
+ storm::storage::DeterministicModelBisimulationDecomposition<double> bisim3(*dtmc, std::set<std::string>({"observe0Greater1"}), true, true);
+ ASSERT_NO_THROW(result = bisim3.getQuotient());
+
+ EXPECT_EQ(storm::models::DTMC, result->getType());
+ EXPECT_EQ(43, result->getNumberOfStates());
+ EXPECT_EQ(83, result->getNumberOfTransitions());
+}