Worked on making bisimulation decomposition a bit easier to use.

Former-commit-id: 0fe6b2af6a

src/exceptions/InvalidOptionException.h

@@ -0,0 +1,15 @@
+#ifndef STORM_EXCEPTIONS_INVALIDOPTIONEXCEPTION_H_
+#define STORM_EXCEPTIONS_INVALIDOPTIONEXCEPTION_H_
+
+#include "src/exceptions/BaseException.h"
+#include "src/exceptions/ExceptionMacros.h"
+
+namespace storm {
+    namespace exceptions {
+        
+        STORM_NEW_EXCEPTION(InvalidOptionException)
+        
+    } // namespace exceptions
+} // namespace storm
+
+#endif /* STORM_EXCEPTIONS_INVALIDOPTIONEXCEPTION_H_ */

src/logic/BinaryPathFormula.cpp

@@ -18,6 +18,14 @@ namespace storm {
             return this->getLeftSubformula().isLtlFormula() && this->getRightSubformula().isLtlFormula();
         }
         
+        bool BinaryPathFormula::containsBoundedUntilFormula() const {
+            return this->getLeftSubformula().containsBoundedUntilFormula() || this->getRightSubformula().containsBoundedUntilFormula();
+        }
+        
+        bool BinaryPathFormula::containsNextFormula() const {
+            return this->getLeftSubformula().containsNextFormula() || this->getRightSubformula().containsNextFormula();
+        }
+        
         bool BinaryPathFormula::containsProbabilityOperator() const {
             return this->getLeftSubformula().containsProbabilityOperator() || this->getRightSubformula().containsProbabilityOperator();
         }

src/logic/BinaryPathFormula.h

@@ -19,6 +19,8 @@ namespace storm {
             
             virtual bool isPctlPathFormula() const override;
             virtual bool isLtlFormula() const override;
+            virtual bool containsBoundedUntilFormula() const override;
+            virtual bool containsNextFormula() const override;
             virtual bool containsProbabilityOperator() const override;
             virtual bool containsNestedProbabilityOperators() const override;
             virtual bool containsRewardOperator() const override;

src/logic/BinaryStateFormula.cpp

@@ -18,6 +18,14 @@ namespace storm {
             return this->getLeftSubformula().isLtlFormula() && this->getRightSubformula().isLtlFormula();
         }
         
+        bool BinaryStateFormula::containsBoundedUntilFormula() const {
+            return this->getLeftSubformula().containsBoundedUntilFormula() || this->getRightSubformula().containsBoundedUntilFormula();
+        }
+        
+        bool BinaryStateFormula::containsNextFormula() const {
+            return this->getLeftSubformula().containsNextFormula() || this->getRightSubformula().containsNextFormula();
+        }
+        
         bool BinaryStateFormula::containsProbabilityOperator() const {
             return this->getLeftSubformula().containsProbabilityOperator() || this->getRightSubformula().containsProbabilityOperator();
         }

src/logic/BinaryStateFormula.h

@@ -17,6 +17,8 @@ namespace storm {
 
             virtual bool isPctlStateFormula() const override;
             virtual bool isLtlFormula() const override;
+            virtual bool containsBoundedUntilFormula() const override;
+            virtual bool containsNextFormula() const override;
             virtual bool containsProbabilityOperator() const override;
             virtual bool containsNestedProbabilityOperators() const override;
             virtual bool containsRewardOperator() const override;

src/logic/BoundedUntilFormula.cpp

@@ -18,6 +18,10 @@ namespace storm {
             return true;
         }
         
+        bool BoundedUntilFormula::containsBoundedUntilFormula() const {
+            return true;
+        }
+        
         bool BoundedUntilFormula::isIntervalBounded() const {
             return bounds.which() == 1;
         }

src/logic/BoundedUntilFormula.h

@@ -14,6 +14,8 @@ namespace storm {
             
             virtual bool isBoundedUntilFormula() const override;
 
+            virtual bool containsBoundedUntilFormula() const override;
+            
             bool isIntervalBounded() const;
             bool isIntegerUpperBounded() const;
             

src/logic/Formula.cpp

@@ -138,6 +138,14 @@ namespace storm {
             return false;
         }
         
+        bool Formula::containsBoundedUntilFormula() const {
+            return false;
+        }
+        
+        bool Formula::containsNextFormula() const {
+            return false;
+        }
+        
         bool Formula::containsProbabilityOperator() const {
             return false;
         }

src/logic/Formula.h

@@ -83,6 +83,8 @@ namespace storm {
             virtual bool isPltlFormula() const;
             virtual bool isLtlFormula() const;
             virtual bool isPropositionalFormula() const;
+            virtual bool containsBoundedUntilFormula() const;
+            virtual bool containsNextFormula() const;
             virtual bool containsProbabilityOperator() const;
             virtual bool containsNestedProbabilityOperators() const;
             virtual bool containsRewardOperator() const;

src/logic/NextFormula.cpp

@@ -10,6 +10,10 @@ namespace storm {
             return true;
         }
         
+        bool NextFormula::containsNextFormula() const {
+            return true;
+        }
+        
         std::ostream& NextFormula::writeToStream(std::ostream& out) const {
             out << "X ";
             this->getSubformula().writeToStream(out);

src/logic/NextFormula.h

@@ -15,6 +15,8 @@ namespace storm {
             
             virtual bool isNextFormula() const override;
             
+            virtual bool containsNextFormula() const override;
+            
             virtual std::ostream& writeToStream(std::ostream& out) const override;
         };
     }

src/logic/UnaryPathFormula.cpp

@@ -18,6 +18,14 @@ namespace storm {
             return this->getSubformula().isLtlFormula();
         }
         
+        bool UnaryPathFormula::containsBoundedUntilFormula() const {
+            return this->getSubformula().containsBoundedUntilFormula();
+        }
+        
+        bool UnaryPathFormula::containsNextFormula() const {
+            return this->getSubformula().containsNextFormula();
+        }
+        
         bool UnaryPathFormula::containsProbabilityOperator() const {
             return this->getSubformula().containsProbabilityOperator();
         }

src/logic/UnaryPathFormula.h

@@ -19,6 +19,8 @@ namespace storm {
             
             virtual bool isPctlPathFormula() const override;
             virtual bool isLtlFormula() const override;
+            virtual bool containsBoundedUntilFormula() const override;
+            virtual bool containsNextFormula() const override;
             virtual bool containsProbabilityOperator() const override;
             virtual bool containsNestedProbabilityOperators() const override;
             virtual bool containsRewardOperator() const override;

src/logic/UnaryStateFormula.cpp

@@ -22,6 +22,14 @@ namespace storm {
             return this->getSubformula().isLtlFormula();
         }
         
+        bool UnaryStateFormula::containsBoundedUntilFormula() const {
+            return this->getSubformula().containsBoundedUntilFormula();
+        }
+        
+        bool UnaryStateFormula::containsNextFormula() const {
+            return this->getSubformula().containsNextFormula();
+        }
+        
         bool UnaryStateFormula::containsProbabilityOperator() const {
             return getSubformula().containsProbabilityOperator();
         }

src/logic/UnaryStateFormula.h

@@ -18,6 +18,8 @@ namespace storm {
             virtual bool isPropositionalFormula() const override;
             virtual bool isPctlStateFormula() const override;
             virtual bool isLtlFormula() const override;
+            virtual bool containsBoundedUntilFormula() const override;
+            virtual bool containsNextFormula() const override;
             virtual bool containsProbabilityOperator() const override;
             virtual bool containsNestedProbabilityOperators() const override;
             virtual bool containsRewardOperator() const override;

src/models/AbstractModel.h

@@ -340,7 +340,7 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
         } else {
             this->stateRewardVector = transitionMatrix.getPointwiseProductRowSumVector(transitionRewardMatrix.get());
         }
-        this->transitionRewardMatrix.reset();
+        this->transitionRewardMatrix = boost::optional<storm::storage::SparseMatrix<T>>();
     }
     
 		/*!

src/storage/DeterministicModelBisimulationDecomposition.cpp

@@ -6,14 +6,18 @@
 #include <iomanip>
 #include <boost/iterator/transform_iterator.hpp>
 
+#include "src/modelchecker/propositional/SparsePropositionalModelChecker.h"
+#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h"
+
 #include "src/utility/graph.h"
 #include "src/exceptions/IllegalFunctionCallException.h"
+#include "src/exceptions/InvalidOptionException.h"
 
 namespace storm {
     namespace storage {
         
         template<typename ValueType>
-        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) {
+        DeterministicModelBisimulationDecomposition<ValueType>::Block::Block(storm::storage::sparse::state_type begin, storm::storage::sparse::state_type end, Block* prev, Block* next, std::size_t id) : next(next), prev(prev), begin(begin), end(end), markedAsSplitter(false), markedAsPredecessorBlock(false), markedPosition(begin), absorbing(false), id(id) {
             if (next != nullptr) {
                 next->prev = this;
             }
@@ -225,22 +229,6 @@ namespace storm {
             return markedAsPredecessorBlock;
         }
         
-        template<typename ValueType>
-        bool DeterministicModelBisimulationDecomposition<ValueType>::Block::hasLabel() const {
-            return this->label != nullptr;
-        }
-        
-        template<typename ValueType>
-        std::string const& DeterministicModelBisimulationDecomposition<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& DeterministicModelBisimulationDecomposition<ValueType>::Block::getLabelPtr() const {
-            return this->label;
-        }
-        
         template<typename ValueType>
         DeterministicModelBisimulationDecomposition<ValueType>::Partition::Partition(std::size_t numberOfStates, bool keepSilentProbabilities) : numberOfBlocks(0), stateToBlockMapping(numberOfStates), statesAndValues(numberOfStates), positions(numberOfStates), keepSilentProbabilities(keepSilentProbabilities), silentProbabilities() {
             // Create the block and give it an iterator to itself.
@@ -261,7 +249,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) : numberOfBlocks(0), stateToBlockMapping(numberOfStates), statesAndValues(numberOfStates), positions(numberOfStates), keepSilentProbabilities(keepSilentProbabilities), silentProbabilities() {
+        DeterministicModelBisimulationDecomposition<ValueType>::Partition::Partition(std::size_t numberOfStates, storm::storage::BitVector const& prob0States, storm::storage::BitVector const& prob1States, bool keepSilentProbabilities) : numberOfBlocks(0), stateToBlockMapping(numberOfStates), statesAndValues(numberOfStates), positions(numberOfStates), keepSilentProbabilities(keepSilentProbabilities), silentProbabilities() {
             storm::storage::sparse::state_type position = 0;
             Block* firstBlock = nullptr;
             Block* secondBlock = nullptr;
@@ -281,7 +269,7 @@ namespace storm {
             }
             
             if (!prob1States.empty()) {
-                typename std::list<Block>::iterator secondIt = blocks.emplace(this->blocks.end(), position, position + prob1States.getNumberOfSetBits(), firstBlock, nullptr, numberOfBlocks++, 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, numberOfBlocks++);
                 secondBlock = &(*secondIt);
                 secondBlock->setIterator(secondIt);
                 
@@ -296,7 +284,7 @@ namespace storm {
             
             storm::storage::BitVector otherStates = ~(prob0States | prob1States);
             if (!otherStates.empty()) {
-                typename std::list<Block>::iterator thirdIt = blocks.emplace(this->blocks.end(), position, numberOfStates, secondBlock, nullptr, numberOfBlocks++, 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, numberOfBlocks++);
                 thirdBlock = &(*thirdIt);
                 thirdBlock->setIterator(thirdIt);
                 
@@ -417,7 +405,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, numberOfBlocks++, block.getLabelPtr());
+            typename std::list<Block>::iterator selfIt = this->blocks.emplace(block.getIterator(), block.getBegin(), position, block.getPreviousBlockPointer(), &block, numberOfBlocks++);
             selfIt->setIterator(selfIt);
             Block& newBlock = *selfIt;
             
@@ -589,41 +577,121 @@ namespace storm {
         }
         
         template<typename ValueType>
-        DeterministicModelBisimulationDecomposition<ValueType>::DeterministicModelBisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, boost::optional<std::set<std::string>> const& atomicPropositions, bool keepRewards, bool weak, bool buildQuotient) : comparator() {
-            STORM_LOG_THROW(!model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without transition rewards.");
-            storm::storage::SparseMatrix<ValueType> backwardTransitions = model.getBackwardTransitions();
-            BisimulationType bisimulationType = weak ? BisimulationType::WeakDtmc : BisimulationType::Strong;
-            Partition initialPartition = getLabelBasedInitialPartition(model, backwardTransitions, bisimulationType, atomicPropositions, keepRewards);
-            partitionRefinement(model, atomicPropositions, backwardTransitions, initialPartition, bisimulationType, keepRewards, buildQuotient);
+        DeterministicModelBisimulationDecomposition<ValueType>::Options::Options(storm::logic::Formula const& formula) : Options() {
+            if (!formula.containsRewardOperator()) {
+                this->keepRewards = false;
+            }
+            
+            // As a tradeoff, we compute a strong bisimulation, because that is typically much faster. If the number of
+            // states is to be minimized, this should be set to weak by the calling site.
+            weak = false;
+            
+            // We need to preserve bounded properties iff the formula contains a bounded until or a next subformula.
+            bounded = formula.containsBoundedUntilFormula() || formula.containsNextFormula();
+            
+            std::vector<std::shared_ptr<storm::logic::AtomicExpressionFormula const>> atomicExpressionFormulas = formula.getAtomicExpressionFormulas();
+            std::vector<std::shared_ptr<storm::logic::AtomicLabelFormula const>> atomicLabelFormulas = formula.getAtomicLabelFormulas();
+            
+            std::set<std::string> labelsToRespect;
+            for (auto const& labelFormula : atomicLabelFormulas) {
+                labelsToRespect.insert(labelFormula->getLabel());
+            }
+            for (auto const& expressionFormula : atomicExpressionFormulas) {
+                std::stringstream stream;
+                stream << expressionFormula;
+                labelsToRespect.insert(stream.str());
+            }
+            respectedAtomicPropositions = labelsToRespect;
+            
+            std::shared_ptr<storm::logic::Formula const> newFormula = formula.asSharedPointer();
+            
+            if (formula.isProbabilityOperatorFormula()) {
+                newFormula = formula.asProbabilityOperatorFormula().getSubformula().asSharedPointer();
+            } else if (formula.isRewardOperatorFormula()) {
+                newFormula = formula.asRewardOperatorFormula().getSubformula().asSharedPointer();
+            }
+            
+            std::shared_ptr<storm::logic::Formula const> leftSubformula = std::make_shared<storm::logic::BooleanLiteralFormula>(true);
+            std::shared_ptr<storm::logic::Formula const> rightSubformula;
+            if (newFormula->isUntilFormula()) {
+                leftSubformula = newFormula->asUntilFormula().getLeftSubformula().asSharedPointer();
+                rightSubformula = newFormula->asUntilFormula().getRightSubformula().asSharedPointer();
+                if (leftSubformula->isPropositionalFormula() && rightSubformula->isPropositionalFormula()) {
+                    measureDrivenInitialPartition = true;
+                }
+            } else if (newFormula->isEventuallyFormula()) {
+                rightSubformula = newFormula->asEventuallyFormula().getSubformula().asSharedPointer();
+                if (rightSubformula->isPropositionalFormula()) {
+                    measureDrivenInitialPartition = true;
+                }
+            } else if (newFormula->isReachabilityRewardFormula()) {
+                rightSubformula = newFormula->asEventuallyFormula().getSubformula().asSharedPointer();
+                if (rightSubformula->isPropositionalFormula()) {
+                    measureDrivenInitialPartition = true;
+                }
+            }
+            
+            if (measureDrivenInitialPartition) {
+                phiStateFormula = leftSubformula;
+                psiStateFormula = rightSubformula;
+            }
         }
         
         template<typename ValueType>
-        DeterministicModelBisimulationDecomposition<ValueType>::DeterministicModelBisimulationDecomposition(storm::models::Ctmc<ValueType> const& model, boost::optional<std::set<std::string>> const& atomicPropositions, bool keepRewards, bool weak, bool buildQuotient) {
-            STORM_LOG_THROW(!keepRewards || !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without transition rewards.");
-            storm::storage::SparseMatrix<ValueType> backwardTransitions = model.getBackwardTransitions();
-            BisimulationType bisimulationType = weak ? BisimulationType::WeakCtmc : BisimulationType::Strong;
-            Partition initialPartition = getLabelBasedInitialPartition(model, backwardTransitions, bisimulationType, atomicPropositions, keepRewards);
-            partitionRefinement(model, atomicPropositions, backwardTransitions, initialPartition, bisimulationType, keepRewards,buildQuotient);
+        DeterministicModelBisimulationDecomposition<ValueType>::Options::Options() : measureDrivenInitialPartition(false), phiStateFormula(), psiStateFormula(), respectedAtomicPropositions(), keepRewards(true), weak(false), bounded(true), buildQuotient(true) {
+            // Intentionally left empty.
         }
         
         template<typename ValueType>
-        DeterministicModelBisimulationDecomposition<ValueType>::DeterministicModelBisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, std::string const& phiLabel, std::string const& psiLabel, bool keepRewards, bool weak, bool bounded, bool buildQuotient) {
-            STORM_LOG_THROW(!keepRewards || !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without transition rewards.");
-            STORM_LOG_THROW(!weak || !bounded, storm::exceptions::IllegalFunctionCallException, "Weak bisimulation does not preserve bounded properties.");
+        DeterministicModelBisimulationDecomposition<ValueType>::DeterministicModelBisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, Options const& options) {
+            STORM_LOG_THROW(!model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without transition rewards. Consider converting the transition rewards to state rewards (via suitable function calls).");
+            STORM_LOG_THROW(!options.weak || !options.bounded, storm::exceptions::IllegalFunctionCallException, "Weak bisimulation cannot preserve bounded properties.");
             storm::storage::SparseMatrix<ValueType> backwardTransitions = model.getBackwardTransitions();
-            BisimulationType bisimulationType = weak ? BisimulationType::WeakDtmc : BisimulationType::Strong;
-            Partition initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, phiLabel, psiLabel, bisimulationType, keepRewards, bounded);
-            partitionRefinement(model, std::set<std::string>({phiLabel, psiLabel}), model.getBackwardTransitions(), initialPartition, bisimulationType, keepRewards, buildQuotient);
+            BisimulationType bisimulationType = options.weak ? BisimulationType::WeakDtmc : BisimulationType::Strong;
+            
+            std::set<std::string> atomicPropositions;
+            if (options.respectedAtomicPropositions) {
+                atomicPropositions = options.respectedAtomicPropositions.get();
+            } else {
+                atomicPropositions = model.getStateLabeling().getAtomicPropositions();
+            }
+            
+            Partition initialPartition;
+            if (options.measureDrivenInitialPartition) {
+                STORM_LOG_THROW(options.phiStateFormula, storm::exceptions::InvalidOptionException, "Unable to compute measure-driven initial partition without phi and psi states.");
+                STORM_LOG_THROW(options.psiStateFormula, storm::exceptions::InvalidOptionException, "Unable to compute measure-driven initial partition without phi and psi states.");
+                initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, options.phiStateFormula.get(), options.psiStateFormula.get(), bisimulationType, options.keepRewards, options.bounded);
+            } else {
+                initialPartition = getLabelBasedInitialPartition(model, backwardTransitions, bisimulationType, atomicPropositions, options.keepRewards);
+            }
+            
+            partitionRefinement(model, atomicPropositions, backwardTransitions, initialPartition, bisimulationType, options.keepRewards, options.buildQuotient);
         }
         
         template<typename ValueType>
-        DeterministicModelBisimulationDecomposition<ValueType>::DeterministicModelBisimulationDecomposition(storm::models::Ctmc<ValueType> const& model, std::string const& phiLabel, std::string const& psiLabel, bool keepRewards, bool weak, bool bounded, bool buildQuotient) {
-            STORM_LOG_THROW(!keepRewards || !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without transition rewards.");
-            STORM_LOG_THROW(!weak || !bounded, storm::exceptions::IllegalFunctionCallException, "Weak bisimulation does not preserve bounded properties.");
+        DeterministicModelBisimulationDecomposition<ValueType>::DeterministicModelBisimulationDecomposition(storm::models::Ctmc<ValueType> const& model, Options const& options) {
+            STORM_LOG_THROW(!model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without transition rewards. Consider converting the transition rewards to state rewards (via suitable function calls).");
+            STORM_LOG_THROW(!options.weak || !options.bounded, storm::exceptions::IllegalFunctionCallException, "Weak bisimulation cannot preserve bounded properties.");
             storm::storage::SparseMatrix<ValueType> backwardTransitions = model.getBackwardTransitions();
-            BisimulationType bisimulationType = weak ? BisimulationType::WeakCtmc : BisimulationType::Strong;
-            Partition initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, phiLabel, psiLabel, bisimulationType, keepRewards, bounded);
-            partitionRefinement(model, std::set<std::string>({phiLabel, psiLabel}), model.getBackwardTransitions(), initialPartition, bisimulationType, keepRewards, buildQuotient);
+            BisimulationType bisimulationType = options.weak ? BisimulationType::WeakCtmc : BisimulationType::Strong;
+            
+            std::set<std::string> atomicPropositions;
+            if (options.respectedAtomicPropositions) {
+                atomicPropositions = options.respectedAtomicPropositions.get();
+            } else {
+                atomicPropositions = model.getStateLabeling().getAtomicPropositions();
+            }
+            
+            Partition initialPartition;
+            if (options.measureDrivenInitialPartition) {
+                STORM_LOG_THROW(options.phiStateFormula, storm::exceptions::InvalidOptionException, "Unable to compute measure-driven initial partition without phi and psi states.");
+                STORM_LOG_THROW(options.psiStateFormula, storm::exceptions::InvalidOptionException, "Unable to compute measure-driven initial partition without phi and psi states.");
+                initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, options.phiStateFormula.get(), options.psiStateFormula.get(), bisimulationType, options.keepRewards, options.bounded);
+            } else {
+                initialPartition = getLabelBasedInitialPartition(model, backwardTransitions, bisimulationType, atomicPropositions, options.keepRewards);
+            }
+            
+            partitionRefinement(model, atomicPropositions, backwardTransitions, initialPartition, bisimulationType, options.keepRewards, options.buildQuotient);
         }
         
         template<typename ValueType>
@@ -683,15 +751,11 @@ namespace storm {
                 if (oldBlock.isAbsorbing()) {
                     builder.addNextValue(blockIndex, blockIndex, storm::utility::constantOne<ValueType>());
                     
-                    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);
-                            }
+                    // 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);
                         }
                     }
                 } else {
@@ -722,16 +786,11 @@ namespace storm {
                         }
                     }
                     
-                    // 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);
-                            }
+                    // 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);
                         }
                     }
                 }
@@ -1205,9 +1264,13 @@ namespace storm {
         
         template<typename ValueType>
         template<typename ModelType>
-        typename DeterministicModelBisimulationDecomposition<ValueType>::Partition DeterministicModelBisimulationDecomposition<ValueType>::getMeasureDrivenInitialPartition(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::string const& phiLabel, std::string const& psiLabel, BisimulationType bisimulationType, bool keepRewards, 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 || keepRewards ? model.getLabeledStates(psiLabel) : statesWithProbability01.second, phiLabel, psiLabel, bisimulationType == BisimulationType::WeakDtmc);
+        typename DeterministicModelBisimulationDecomposition<ValueType>::Partition DeterministicModelBisimulationDecomposition<ValueType>::getMeasureDrivenInitialPartition(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::shared_ptr<storm::logic::Formula const> const& phiStateFormula, std::shared_ptr<storm::logic::Formula const> const& psiStateFormula, BisimulationType bisimulationType, bool keepRewards, bool bounded) {
+            storm::modelchecker::SparsePropositionalModelChecker<ValueType> checker(model);
+            std::unique_ptr<storm::modelchecker::CheckResult> phiStates = checker.check(*phiStateFormula);
+            std::unique_ptr<storm::modelchecker::CheckResult> psiStates = checker.check(*psiStateFormula);
+            
+            std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::utility::graph::performProb01(backwardTransitions, phiStates->asExplicitQualitativeCheckResult().getTruthValuesVector(), psiStates->asExplicitQualitativeCheckResult().getTruthValuesVector());
+            Partition partition(model.getNumberOfStates(), statesWithProbability01.first, bounded || keepRewards ? psiStates->asExplicitQualitativeCheckResult().getTruthValuesVector() : statesWithProbability01.second, bisimulationType == BisimulationType::WeakDtmc);
             
             // If the model has state rewards, we need to consider them, because otherwise reward properties are not
             // preserved.

src/storage/DeterministicModelBisimulationDecomposition.h

@@ -6,6 +6,7 @@
 
 #include "src/storage/sparse/StateType.h"
 #include "src/storage/Decomposition.h"
+#include "src/logic/Formulas.h"
 #include "src/models/Dtmc.h"
 #include "src/models/Ctmc.h"
 #include "src/storage/Distribution.h"
@@ -21,53 +22,62 @@ namespace storm {
         template <typename ValueType>
         class DeterministicModelBisimulationDecomposition : public Decomposition<StateBlock> {
         public:
-            /*!
-             * 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, boost::optional<std::set<std::string>> const& atomicPropositions = boost::optional<std::set<std::string>>(), bool keepRewards = true, bool weak = false, bool buildQuotient = false);
+            // A class that offers the possibility to customize the bisimulation.
+            struct Options {
+                // Creates an object representing the default values for all options.
+                Options();
 
-            /*!
-             * 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, boost::optional<std::set<std::string>> const& atomicPropositions = boost::optional<std::set<std::string>>(), bool keepRewards = true, bool weak = false, bool buildQuotient = false);
+                /*!
+                 * Creates an object representing the options necessary to obtain the smallest quotient while still
+                 * preserving the given formula.
+                 *
+                 * @param formula The formula that is to be preserved.
+                 */
+                Options(storm::logic::Formula const& formula);
+                
+                // A flag that indicates whether a measure driven initial partition is to be used. If this flag is set
+                // to true, the two optional pairs phiStatesAndLabel and psiStatesAndLabel must be set. Then, the
+                // measure driven initial partition wrt. to the states phi and psi is taken.
+                bool measureDrivenInitialPartition;
+                boost::optional<std::shared_ptr<storm::logic::Formula const>> phiStateFormula;
+                boost::optional<std::shared_ptr<storm::logic::Formula const>> psiStateFormula;
+                
+                // An optional set of strings that indicate which of the atomic propositions of the model are to be
+                // respected and which may be ignored. If not given, all atomic propositions of the model are respected.
+                boost::optional<std::set<std::string>> respectedAtomicPropositions;
+                
+                // A flag that indicates whether or not the state-rewards of the model are to be respected (and should
+                // be kept in the quotient model, if one is built).
+                bool keepRewards;
+                
+                // A flag that indicates whether a strong or a weak bisimulation is to be computed.
+                bool weak;
+                
+                // A flag that indicates whether step-bounded properties are to be preserved. This may only be set to tru
+                // when computing strong bisimulation equivalence.
+                bool bounded;
+                
+                // A flag that governs whether the quotient model is actually built or only the decomposition is computed.
+                bool buildQuotient;
+            };
             
             /*!
-             * Decomposes the given DTMC into equivalence classes under strong bisimulation in a way that onle safely
-             * preserves formulas of the form phi until psi.
+             * Decomposes the given DTMC into equivalance classes of a bisimulation. Which kind of bisimulation is
+             * computed, is customizable via the given options.
              *
              * @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 weak A flag indication whether a weak bisimulation is to be computed.
-             * @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.
+             * @param options The options that customize the computed bisimulation.
              */
-            DeterministicModelBisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, std::string const& phiLabel, std::string const& psiLabel, bool keepRewards, bool weak, bool bounded, bool buildQuotient = false);
+            DeterministicModelBisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, Options const& options = Options());
             
             /*!
-             * Decomposes the given CTMC into equivalence classes under strong bisimulation in a way that onle safely
-             * preserves formulas of the form phi until psi.
+             * Decomposes the given CTMC into equivalance classes of a bisimulation. Which kind of bisimulation is
+             * computed, is customizable via the given options.
              *
              * @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 weak A flag indication whether a weak bisimulation is to be computed.
-             * @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.
+             * @param options The options that customize the computed bisimulation.
              */
-            DeterministicModelBisimulationDecomposition(storm::models::Ctmc<ValueType> const& model, std::string const& phiLabel, std::string const& psiLabel, bool keepRewards, bool weak, bool bounded, bool buildQuotient = false);
+            DeterministicModelBisimulationDecomposition(storm::models::Ctmc<ValueType> const& model, Options const& options = Options());
             
             /*!
              * Retrieves the quotient of the model under the previously computed bisimulation.
@@ -87,7 +97,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::size_t id, 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);
                 
                 // Prints the block.
                 void print(Partition const& partition) const;
@@ -191,15 +201,6 @@ namespace storm {
                 // 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.
@@ -227,9 +228,6 @@ namespace storm {
                 
                 // 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;
             };
             
             class Partition {
@@ -252,11 +250,9 @@ namespace storm {
                  * @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.
                  * @param keepSilentProbabilities A flag indicating whether or not silent probabilities are to be tracked.
                  */
-                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 = false);
+                Partition(std::size_t numberOfStates, storm::storage::BitVector const& prob0States, storm::storage::BitVector const& prob1States, bool keepSilentProbabilities = false);
                 
                 Partition() = default;
                 Partition(Partition const& other) = default;
@@ -468,15 +464,15 @@ namespace storm {
              * @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 phiStateFormula The formula that defines the phi states in the model.
+             * @param psiStateFormula The formula that defines the psi states in the model.
              * @param bisimulationType The kind of bisimulation that is to be computed.
              * @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, BisimulationType bisimulationType, bool keepRewards = true, bool bounded = false);
+            Partition getMeasureDrivenInitialPartition(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::shared_ptr<storm::logic::Formula const> const& phiStateFormula, std::shared_ptr<storm::logic::Formula const> const& psiStateFormula, BisimulationType bisimulationType, bool keepRewards = true, bool bounded = false);
             
             /*!
              * Creates the initial partition based on all the labels in the given model.

src/utility/cli.h

@@ -293,7 +293,10 @@ namespace storm {
                     }
                     
                     std::cout << "Performing bisimulation minimization... ";
-                    storm::storage::DeterministicModelBisimulationDecomposition<double> bisimulationDecomposition(*dtmc, boost::optional<std::set<std::string>>(), true, storm::settings::bisimulationSettings().isWeakBisimulationSet(), true);
+                    typename storm::storage::DeterministicModelBisimulationDecomposition<double>::Options options;
+                    options.weak = storm::settings::bisimulationSettings().isWeakBisimulationSet();
+                    
+                    storm::storage::DeterministicModelBisimulationDecomposition<double> bisimulationDecomposition(*dtmc, options);
                     model = bisimulationDecomposition.getQuotient();
                     std::cout << "done." << std::endl << std::endl;
                 }

test/functional/storage/DeterministicModelBisimulationDecompositionTest.cpp

@@ -9,7 +9,7 @@ TEST(DeterministicModelBisimulationDecomposition, Die) {
     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>>(), true, false, true);
+    storm::storage::DeterministicModelBisimulationDecomposition<double> bisim(*dtmc);
     std::shared_ptr<storm::models::AbstractModel<double>> result;
     ASSERT_NO_THROW(result = bisim.getQuotient());
 
@@ -17,14 +17,20 @@ TEST(DeterministicModelBisimulationDecomposition, Die) {
     EXPECT_EQ(13, result->getNumberOfStates());
     EXPECT_EQ(20, result->getNumberOfTransitions());
 
-    storm::storage::DeterministicModelBisimulationDecomposition<double> bisim2(*dtmc, std::set<std::string>({"one"}), true, false, true);
+    typename storm::storage::DeterministicModelBisimulationDecomposition<double>::Options options;
+    options.respectedAtomicPropositions = std::set<std::string>({"one"});
+    
+    storm::storage::DeterministicModelBisimulationDecomposition<double> bisim2(*dtmc, options);
     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, true);
+    options.bounded = false;
+    options.weak = true;
+    
+    storm::storage::DeterministicModelBisimulationDecomposition<double> bisim3(*dtmc, options);
     ASSERT_NO_THROW(result = bisim3.getQuotient());
     
     EXPECT_EQ(storm::models::DTMC, result->getType());
@@ -38,7 +44,7 @@ TEST(DeterministicModelBisimulationDecomposition, Crowds) {
     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>>(), true, false, true);
+    storm::storage::DeterministicModelBisimulationDecomposition<double> bisim(*dtmc);
     std::shared_ptr<storm::models::AbstractModel<double>> result;
     ASSERT_NO_THROW(result = bisim.getQuotient());
     
@@ -46,14 +52,20 @@ TEST(DeterministicModelBisimulationDecomposition, Crowds) {
     EXPECT_EQ(334, result->getNumberOfStates());
     EXPECT_EQ(546, result->getNumberOfTransitions());
     
-    storm::storage::DeterministicModelBisimulationDecomposition<double> bisim2(*dtmc, std::set<std::string>({"observe0Greater1"}), true, false, true);
+    typename storm::storage::DeterministicModelBisimulationDecomposition<double>::Options options;
+    options.respectedAtomicPropositions = std::set<std::string>({"observe0Greater1"});
+    
+    storm::storage::DeterministicModelBisimulationDecomposition<double> bisim2(*dtmc, options);
     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, true);
+    options.bounded = false;
+    options.weak = true;
+    
+    storm::storage::DeterministicModelBisimulationDecomposition<double> bisim3(*dtmc, options);
     ASSERT_NO_THROW(result = bisim3.getQuotient());
     
     EXPECT_EQ(storm::models::DTMC, result->getType());