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 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 - std::size_t DeterministicModelBisimulationDecomposition::Block::blockId = 0; - - template - DeterministicModelBisimulationDecomposition::Block::Block(storm::storage::sparse::state_type begin, storm::storage::sparse::state_type end, Block* prev, Block* next, std::shared_ptr const& label) : next(next), prev(prev), begin(begin), end(end), markedAsSplitter(false), markedAsPredecessorBlock(false), markedPosition(begin), absorbing(false), id(blockId++), label(label) { + DeterministicModelBisimulationDecomposition::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 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 DeterministicModelBisimulationDecomposition::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::iterator it = blocks.emplace(this->blocks.end(), 0, numberOfStates, nullptr, nullptr); + typename std::list::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 DeterministicModelBisimulationDecomposition::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::iterator firstIt = blocks.emplace(this->blocks.end(), 0, prob0States.getNumberOfSetBits(), nullptr, nullptr); + typename std::list::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::iterator secondIt = blocks.emplace(this->blocks.end(), position, position + prob1States.getNumberOfSetBits(), &firstBlock, nullptr, std::shared_ptr(new std::string(prob1Label))); + typename std::list::iterator secondIt = blocks.emplace(this->blocks.end(), position, position + prob1States.getNumberOfSetBits(), &firstBlock, nullptr, this->blocks.size(), std::shared_ptr(new std::string(prob1Label))); Block& secondBlock = *secondIt; secondBlock.setIterator(secondIt); @@ -290,7 +287,7 @@ namespace storm { } secondBlock.setAbsorbing(true); - typename std::list::iterator thirdIt = blocks.emplace(this->blocks.end(), position, numberOfStates, &secondBlock, nullptr, otherLabel == "true" ? std::shared_ptr(nullptr) : std::shared_ptr(new std::string(otherLabel))); + typename std::list::iterator thirdIt = blocks.emplace(this->blocks.end(), position, numberOfStates, &secondBlock, nullptr, this->blocks.size(), otherLabel == "true" ? std::shared_ptr(nullptr) : std::shared_ptr(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::iterator selfIt = this->blocks.emplace(block.getIterator(), block.getBegin(), position, block.getPreviousBlockPointer(), &block, block.getLabelPtr()); + typename std::list::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::iterator it = this->blocks.emplace(block.getIterator(), begin, block.getBegin(), block.getPreviousBlockPointer(), &block); + typename std::list::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 - DeterministicModelBisimulationDecomposition::DeterministicModelBisimulationDecomposition(storm::models::Dtmc 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::DeterministicModelBisimulationDecomposition(storm::models::Dtmc const& model, boost::optional> 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 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 - DeterministicModelBisimulationDecomposition::DeterministicModelBisimulationDecomposition(storm::models::Ctmc const& model, bool weak, bool buildQuotient) { + DeterministicModelBisimulationDecomposition::DeterministicModelBisimulationDecomposition(storm::models::Ctmc const& model, boost::optional> 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 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 @@ -600,7 +604,7 @@ namespace storm { storm::storage::SparseMatrix 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({phiLabel, psiLabel}), model.getBackwardTransitions(), initialPartition, bisimulationType, buildQuotient); } template @@ -610,7 +614,7 @@ namespace storm { storm::storage::SparseMatrix 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({phiLabel, psiLabel}), model.getBackwardTransitions(), initialPartition, bisimulationType, buildQuotient); } template @@ -621,7 +625,7 @@ namespace storm { template template - void DeterministicModelBisimulationDecomposition::buildQuotient(ModelType const& model, Partition const& partition, BisimulationType bisimulationType) { + void DeterministicModelBisimulationDecomposition::buildQuotient(ModelType const& model, boost::optional> 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 atomicPropositionsSet = model.getStateLabeling().getAtomicPropositions(); + std::set atomicPropositionsSet = selectedAtomicPropositions ? selectedAtomicPropositions.get() : model.getStateLabeling().getAtomicPropositions(); + atomicPropositionsSet.insert("init"); std::vector atomicPropositions = std::vector(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 template - void DeterministicModelBisimulationDecomposition::partitionRefinement(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, Partition& partition, BisimulationType bisimulationType, bool buildQuotient) { + void DeterministicModelBisimulationDecomposition::partitionRefinement(ModelType const& model, boost::optional> const& atomicPropositions, storm::storage::SparseMatrix 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 template - typename DeterministicModelBisimulationDecomposition::Partition DeterministicModelBisimulationDecomposition::getLabelBasedInitialPartition(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, BisimulationType bisimulationType) { + typename DeterministicModelBisimulationDecomposition::Partition DeterministicModelBisimulationDecomposition::getLabelBasedInitialPartition(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, BisimulationType bisimulationType, boost::optional> 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 const& model, bool weak = false, bool buildQuotient = false); + DeterministicModelBisimulationDecomposition(storm::models::Dtmc const& model, boost::optional> const& atomicPropositions = boost::optional>(), 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 const& model, bool weak = false, bool buildQuotient = false); + DeterministicModelBisimulationDecomposition(storm::models::Ctmc const& model, boost::optional> const& atomicPropositions = boost::optional>(), 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::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 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 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 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 - void partitionRefinement(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, Partition& partition, BisimulationType bisimulationType, bool buildQuotient); + void partitionRefinement(ModelType const& model, boost::optional> const& atomicPropositions, storm::storage::SparseMatrix 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 - void buildQuotient(ModelType const& model, Partition const& partition, BisimulationType bisimulationType); + void buildQuotient(ModelType const& model, boost::optional> 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 - Partition getLabelBasedInitialPartition(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, BisimulationType bisimulationType); + Partition getLabelBasedInitialPartition(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, BisimulationType bisimulationType, boost::optional> const& atomicPropositions = boost::optional>()); /*! * 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 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> dtmc = result->template as>(); STORM_PRINT(std::endl << "Performing bisimulation minimization..." << std::endl); - storm::storage::DeterministicModelBisimulationDecomposition bisimulationDecomposition(*dtmc, storm::settings::bisimulationSettings().isWeakBisimulationSet(), true); + storm::storage::DeterministicModelBisimulationDecomposition bisimulationDecomposition(*dtmc, boost::optional>(), 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> 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> dtmc = abstractModel->as>(); + + storm::storage::DeterministicModelBisimulationDecomposition bisim(*dtmc, boost::optional>(), false, true); + std::shared_ptr> 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 bisim2(*dtmc, std::set({"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 bisim3(*dtmc, std::set({"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> 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> dtmc = abstractModel->as>(); +} + +TEST(DeterministicModelBisimulationDecomposition, Crowds) { + std::shared_ptr> 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> dtmc = abstractModel->as>(); + + storm::storage::DeterministicModelBisimulationDecomposition bisim(*dtmc, boost::optional>(), false, true); + std::shared_ptr> 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 bisim2(*dtmc, std::set({"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 bisim3(*dtmc, std::set({"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()); +}