Merge branch 'parametricSystems' of https://sselab.de/lab9/private/git/storm into parametricSystems

Former-commit-id: b42d733ef9

src/builder/ExplicitPrismModelBuilder.cpp

@@ -13,7 +13,7 @@
 namespace storm {
     namespace builder {
         template <typename ValueType, typename IndexType>
-        ExplicitPrismModelBuilder<ValueType, IndexType>::StateInformation::StateInformation(uint64_t bitsPerState) : stateStorage(bitsPerState, 1000000), bitsPerState(bitsPerState), reachableStates() {
+        ExplicitPrismModelBuilder<ValueType, IndexType>::StateInformation::StateInformation(uint64_t bitsPerState) : stateStorage(bitsPerState, 10000000), bitsPerState(bitsPerState), reachableStates() {
             // Intentionally left empty.
         }
         
@@ -97,7 +97,7 @@ namespace storm {
             // Start by defining the undefined constants in the model.
             storm::prism::Program preparedProgram;
             if (options.constantDefinitions) {
-                 preparedProgram = program.defineUndefinedConstants(options.constantDefinitions.get());
+                preparedProgram = program.defineUndefinedConstants(options.constantDefinitions.get());
             } else {
                 preparedProgram = program;
             }
@@ -220,6 +220,7 @@ namespace storm {
                 int_fast64_t assignedValue = evaluator.asInt(assignmentIt->getExpression());
                 STORM_LOG_THROW(assignedValue <= integerIt->upperBound, storm::exceptions::WrongFormatException, "The update " << update << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getVariableName() << "'.");
                 newState.setFromInt(integerIt->bitOffset, integerIt->bitWidth, assignedValue - integerIt->lowerBound);
+                STORM_LOG_ASSERT(newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth) + integerIt->lowerBound == assignedValue, "Writing to the bit vector bucket failed (read " << newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth) << " but wrote " << assignedValue << ").");
             }
             
             // Check that we processed all assignments.
@@ -328,7 +329,7 @@ namespace storm {
                         choice.addProbability(stateIndex, probability);
                         probabilitySum += probability;
                     }
-                    
+
                     // Check that the resulting distribution is in fact a distribution.
                     STORM_LOG_THROW(!discreteTimeModel || comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Probabilities do not sum to one for command '" << command << "' (actually sum to " << probabilitySum << ").");
                 }

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/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp

@@ -203,7 +203,7 @@ namespace storm {
             storm::storage::BitVector trueStates(model.getNumberOfStates(), true);
             
             // Do some sanity checks to establish some required properties.
-            STORM_LOG_THROW(storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationMethod() != storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationMethod::State, storm::exceptions::InvalidArgumentException, "Unsupported elimination method for conditional probabilities.");
+            STORM_LOG_THROW(storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationMethod() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationMethod::State, storm::exceptions::InvalidArgumentException, "Unsupported elimination method for conditional probabilities.");
             STORM_LOG_THROW(model.getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::IllegalArgumentException, "Input model is required to have exactly one initial state.");
             storm::storage::sparse::state_type initialState = *model.getInitialStates().begin();
             

src/models/AbstractModel.h

@@ -356,7 +356,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/BitVector.cpp

@@ -459,7 +459,7 @@ namespace storm {
                 bucketVector[bucket] = (bucketVector[bucket] & ~mask) | (value << (64 - (bitIndexInBucket + numberOfBits)));
             } else if (bitIndexInBucket + numberOfBits > 64) {
                 // Write the part of the value that falls into the first bucket.
-                bucketVector[bucket] = (bucketVector[bucket] & ~mask) | (value >> (64 - bitIndexInBucket));
+                bucketVector[bucket] = (bucketVector[bucket] & ~mask) | (value >> (numberOfBits + (bitIndexInBucket - 64)));
                 ++bucket;
                 
                 // Compute the remaining number of bits.

src/storage/DeterministicModelBisimulationDecomposition.cpp

@@ -7,14 +7,18 @@
 #include <boost/iterator/transform_iterator.hpp>
 
 #include "src/storage/parameters.h"
+#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;
             }
@@ -131,12 +135,12 @@ namespace storm {
         typename DeterministicModelBisimulationDecomposition<ValueType>::Block* DeterministicModelBisimulationDecomposition<ValueType>::Block::getPreviousBlockPointer() {
             return this->prev;
         }
-
+        
         template<typename ValueType>
         typename DeterministicModelBisimulationDecomposition<ValueType>::Block* DeterministicModelBisimulationDecomposition<ValueType>::Block::getNextBlockPointer() {
             return this->next;
         }
-
+        
         template<typename ValueType>
         typename DeterministicModelBisimulationDecomposition<ValueType>::Block const& DeterministicModelBisimulationDecomposition<ValueType>::Block::getPreviousBlock() const {
             return *this->prev;
@@ -170,12 +174,12 @@ namespace storm {
         void DeterministicModelBisimulationDecomposition<ValueType>::Block::markAsSplitter() {
             this->markedAsSplitter = true;
         }
-
+        
         template<typename ValueType>
         void DeterministicModelBisimulationDecomposition<ValueType>::Block::unmarkAsSplitter() {
             this->markedAsSplitter = false;
         }
-
+        
         template<typename ValueType>
         std::size_t DeterministicModelBisimulationDecomposition<ValueType>::Block::getId() const {
             return this->id;
@@ -191,6 +195,22 @@ namespace storm {
             return this->absorbing;
         }
         
+        template<typename ValueType>
+        void DeterministicModelBisimulationDecomposition<ValueType>::Block::setRepresentativeState(storm::storage::sparse::state_type representativeState) {
+            this->representativeState = representativeState;
+        }
+        
+        template<typename ValueType>
+        bool DeterministicModelBisimulationDecomposition<ValueType>::Block::hasRepresentativeState() const {
+            return static_cast<bool>(representativeState);
+        }
+        
+        template<typename ValueType>
+        storm::storage::sparse::state_type DeterministicModelBisimulationDecomposition<ValueType>::Block::getRepresentativeState() const {
+            STORM_LOG_THROW(representativeState, storm::exceptions::InvalidOperationException, "Unable to retrieve representative state for block.");
+            return representativeState.get();
+        }
+        
         template<typename ValueType>
         storm::storage::sparse::state_type DeterministicModelBisimulationDecomposition<ValueType>::Block::getMarkedPosition() const {
             return this->markedPosition;
@@ -226,22 +246,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.
@@ -262,7 +266,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, boost::optional<storm::storage::sparse::state_type> representativeProb1State, 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;
@@ -271,7 +275,7 @@ namespace storm {
                 typename std::list<Block>::iterator firstIt = blocks.emplace(this->blocks.end(), 0, prob0States.getNumberOfSetBits(), nullptr, nullptr, numberOfBlocks++);
                 firstBlock = &(*firstIt);
                 firstBlock->setIterator(firstIt);
-
+                
                 for (auto state : prob0States) {
                     statesAndValues[position] = std::make_pair(state, storm::utility::zero<ValueType>());
                     positions[state] = position;
@@ -280,9 +284,9 @@ namespace storm {
                 }
                 firstBlock->setAbsorbing(true);
             }
-
+            
             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);
                 
@@ -293,11 +297,12 @@ namespace storm {
                     ++position;
                 }
                 secondBlock->setAbsorbing(true);
+                secondBlock->setRepresentativeState(representativeProb1State.get());
             }
             
             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);
                 
@@ -320,7 +325,7 @@ namespace storm {
             std::swap(this->statesAndValues[this->positions[state1]], this->statesAndValues[this->positions[state2]]);
             std::swap(this->positions[state1], this->positions[state2]);
         }
-
+        
         template<typename ValueType>
         void DeterministicModelBisimulationDecomposition<ValueType>::Partition::swapStatesAtPositions(storm::storage::sparse::state_type position1, storm::storage::sparse::state_type position2) {
             storm::storage::sparse::state_type state1 = this->statesAndValues[position1].first;
@@ -366,7 +371,7 @@ namespace storm {
         void DeterministicModelBisimulationDecomposition<ValueType>::Partition::increaseValue(storm::storage::sparse::state_type state, ValueType value) {
             this->statesAndValues[this->positions[state]].second += value;
         }
-
+        
         template<typename ValueType>
         void DeterministicModelBisimulationDecomposition<ValueType>::Partition::updateBlockMapping(Block& block, typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator first, typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator last) {
             for (; first != last; ++first) {
@@ -383,12 +388,12 @@ namespace storm {
         typename DeterministicModelBisimulationDecomposition<ValueType>::Block& DeterministicModelBisimulationDecomposition<ValueType>::Partition::getBlock(storm::storage::sparse::state_type state) {
             return *this->stateToBlockMapping[state];
         }
-
+        
         template<typename ValueType>
         typename DeterministicModelBisimulationDecomposition<ValueType>::Block const& DeterministicModelBisimulationDecomposition<ValueType>::Partition::getBlock(storm::storage::sparse::state_type state) const {
             return *this->stateToBlockMapping[state];
         }
-
+        
         template<typename ValueType>
         typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator DeterministicModelBisimulationDecomposition<ValueType>::Partition::getBegin(Block const& block) {
             return this->statesAndValues.begin() + block.getBegin();
@@ -398,7 +403,7 @@ namespace storm {
         typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator DeterministicModelBisimulationDecomposition<ValueType>::Partition::getEnd(Block const& block) {
             return this->statesAndValues.begin() + block.getEnd();
         }
-
+        
         template<typename ValueType>
         typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator DeterministicModelBisimulationDecomposition<ValueType>::Partition::getBegin(Block const& block) const {
             return this->statesAndValues.begin() + block.getBegin();
@@ -418,7 +423,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;
             
@@ -590,48 +595,124 @@ 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::models::AbstractModel<ValueType> const& model, 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->asReachabilityRewardFormula().getSubformula().asSharedPointer();
+                if (rightSubformula->isPropositionalFormula()) {
+                    measureDrivenInitialPartition = true;
+                }
+            }
+            
+            if (measureDrivenInitialPartition) {
+                storm::modelchecker::SparsePropositionalModelChecker<ValueType> checker(model);
+                std::unique_ptr<storm::modelchecker::CheckResult> phiStatesCheckResult = checker.check(*leftSubformula);
+                std::unique_ptr<storm::modelchecker::CheckResult> psiStatesCheckResult = checker.check(*rightSubformula);
+                phiStates = phiStatesCheckResult->asExplicitQualitativeCheckResult().getTruthValuesVector();
+                psiStates = psiStatesCheckResult->asExplicitQualitativeCheckResult().getTruthValuesVector();
+            }
         }
-
+        
         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), phiStates(), psiStates(), 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);
+            BisimulationType bisimulationType = options.weak ? BisimulationType::WeakDtmc : BisimulationType::Strong;
+            
             std::set<std::string> atomicPropositions;
-            if (phiLabel != "true" && phiLabel != "false") {
-                atomicPropositions.insert(phiLabel);
+            if (options.respectedAtomicPropositions) {
+                atomicPropositions = options.respectedAtomicPropositions.get();
+            } else {
+                atomicPropositions = model.getStateLabeling().getAtomicPropositions();
             }
-            if (psiLabel != "true" && phiLabel != "false") {
-                atomicPropositions.insert(psiLabel);
+            
+            Partition initialPartition;
+            if (options.measureDrivenInitialPartition) {
+                STORM_LOG_THROW(options.phiStates, storm::exceptions::InvalidOptionException, "Unable to compute measure-driven initial partition without phi and psi states.");
+                STORM_LOG_THROW(options.psiStates, storm::exceptions::InvalidOptionException, "Unable to compute measure-driven initial partition without phi and psi states.");
+                initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, options.phiStates.get(), options.psiStates.get(), bisimulationType, options.keepRewards, options.bounded);
+            } else {
+                initialPartition = getLabelBasedInitialPartition(model, backwardTransitions, bisimulationType, atomicPropositions, options.keepRewards);
             }
-            partitionRefinement(model, std::set<std::string>({phiLabel, psiLabel}), model.getBackwardTransitions(), initialPartition, bisimulationType, keepRewards, buildQuotient);
+            
+            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.phiStates, storm::exceptions::InvalidOptionException, "Unable to compute measure-driven initial partition without phi and psi states.");
+                STORM_LOG_THROW(options.psiStates, storm::exceptions::InvalidOptionException, "Unable to compute measure-driven initial partition without phi and psi states.");
+                initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, options.phiStates.get(), options.psiStates.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>
@@ -642,7 +723,7 @@ namespace storm {
         
         template<typename ValueType>
         template<typename ModelType>
-        void DeterministicModelBisimulationDecomposition<ValueType>::buildQuotient(ModelType const& model, boost::optional<std::set<std::string>> const& selectedAtomicPropositions, Partition const& partition, BisimulationType bisimulationType, bool keepRewards) {
+        void DeterministicModelBisimulationDecomposition<ValueType>::buildQuotient(ModelType const& model, std::set<std::string> const& selectedAtomicPropositions, Partition const& partition, BisimulationType bisimulationType, bool keepRewards) {
             // In order to create the quotient model, we need to construct
             // (a) the new transition matrix,
             // (b) the new labeling,
@@ -653,7 +734,7 @@ namespace storm {
             
             // Prepare the new state labeling for (b).
             storm::models::AtomicPropositionsLabeling newLabeling(this->size(), model.getStateLabeling().getNumberOfAtomicPropositions());
-            std::set<std::string> atomicPropositionsSet = selectedAtomicPropositions ? selectedAtomicPropositions.get() : model.getStateLabeling().getAtomicPropositions();
+            std::set<std::string> atomicPropositionsSet = selectedAtomicPropositions;
             atomicPropositionsSet.insert("init");
             std::vector<std::string> atomicPropositions = std::vector<std::string>(atomicPropositionsSet.begin(), atomicPropositionsSet.end());
             for (auto const& ap : atomicPropositions) {
@@ -691,15 +772,16 @@ 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);
-                            }
+                    // If the block has a special representative state, we retrieve it now.
+                    if (oldBlock.hasRepresentativeState()) {
+                        representativeState = oldBlock.getRepresentativeState();
+                    }
+
+                    // Add all of the selected atomic propositions that hold in the representative state to the state
+                    // representing the block.
+                    for (auto const& ap : atomicPropositions) {
+                        if (model.getStateLabeling().getStateHasAtomicProposition(ap, representativeState)) {
+                            newLabeling.addAtomicPropositionToState(ap, blockIndex);
                         }
                     }
                 } else {
@@ -730,16 +812,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);
                         }
                     }
                 }
@@ -763,9 +840,9 @@ namespace storm {
         
         template<typename ValueType>
         template<typename ModelType>
-        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 keepRewards, bool buildQuotient) {
+        void DeterministicModelBisimulationDecomposition<ValueType>::partitionRefinement(ModelType const& model, std::set<std::string> const& atomicPropositions, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Partition& partition, BisimulationType bisimulationType, bool keepRewards, 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.
             std::chrono::high_resolution_clock::time_point refinementStart = std::chrono::high_resolution_clock::now();
             std::deque<Block*> splitterQueue;
@@ -775,6 +852,7 @@ namespace storm {
             while (!splitterQueue.empty()) {
                 // Optionally: sort the splitter queue according to some criterion (here: prefer small splitters).
                 std::sort(splitterQueue.begin(), splitterQueue.end(), [] (Block const* b1, Block const* b2) { return b1->getNumberOfStates() < b2->getNumberOfStates() || (b1->getNumberOfStates() == b2->getNumberOfStates() && b1->getId() < b2->getId()); } );
+                std::sort(splitterQueue.begin(), splitterQueue.end(), [] (Block const* b1, Block const* b2) { return b1->getNumberOfStates() < b2->getNumberOfStates(); } );
 
                 // Get and prepare the next splitter.
                 Block* splitter = splitterQueue.front();
@@ -785,7 +863,7 @@ namespace storm {
                 refinePartition(model.getTransitionMatrix(), backwardTransitions, *splitter, partition, bisimulationType, splitterQueue);
             }
             std::chrono::high_resolution_clock::duration refinementTime = std::chrono::high_resolution_clock::now() - refinementStart;
-
+            
             // Now move the states from the internal partition into their final place in the decomposition. We do so in
             // a way that maintains the block IDs as indices.
             std::chrono::high_resolution_clock::time_point extractionStart = std::chrono::high_resolution_clock::now();
@@ -798,12 +876,12 @@ namespace storm {
 				std::function<storm::storage::sparse::state_type (std::pair<storm::storage::sparse::state_type, ValueType> const&)> projection = [] (std::pair<storm::storage::sparse::state_type, ValueType> const& a) -> storm::storage::sparse::state_type { return a.first; };
 				this->blocks[block.getId()] = block_type(boost::make_transform_iterator(partition.getBegin(block), projection), boost::make_transform_iterator(partition.getEnd(block), projection), true);
             }
-
+            
             // If we are required to build the quotient model, do so now.
             if (buildQuotient) {
                 this->buildQuotient(model, atomicPropositions, partition, bisimulationType, keepRewards);
             }
-
+            
             std::chrono::high_resolution_clock::duration extractionTime = std::chrono::high_resolution_clock::now() - extractionStart;
             std::chrono::high_resolution_clock::duration totalTime = std::chrono::high_resolution_clock::now() - totalStart;
             
@@ -1018,7 +1096,7 @@ namespace storm {
             typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator end = partition.getStatesAndValues().begin() + block.getBegin() - 1;
             storm::storage::sparse::state_type currentIndex = block.getOriginalBegin();
             result.push_back(currentIndex);
-
+            
             // Now we can check whether the block needs to be split, which is the case iff the probabilities for the
             // first and the last state are different.
             while (!comparator.isEqual(begin->second, end->second)) {
@@ -1033,7 +1111,7 @@ namespace storm {
                     ++begin;
                     ++currentIndex;
                 }
-
+                
                 // Remember the index at which the probabilities were different.
                 result.push_back(currentIndex);
             }
@@ -1126,7 +1204,7 @@ namespace storm {
                     storm::storage::sparse::state_type predecessor = predecessorEntry.getColumn();
                     Block& predecessorBlock = partition.getBlock(predecessor);
                     storm::storage::sparse::state_type predecessorPosition = partition.getPosition(predecessor);
-
+                    
                     if (predecessorPosition >= predecessorBlock.getBegin()) {
                         partition.swapStatesAtPositions(predecessorPosition, predecessorBlock.getBegin());
                         predecessorBlock.incrementBegin();
@@ -1141,7 +1219,7 @@ namespace storm {
                     }
                 }
             }
-
+            
             if (bisimulationType == BisimulationType::Strong || bisimulationType == BisimulationType::WeakCtmc) {
                 std::vector<Block*> blocksToSplit;
                 
@@ -1192,7 +1270,7 @@ namespace storm {
                     partition.setSilentProbabilities(partition.getStatesAndValues().begin() + splitter.getOriginalBegin(), partition.getStatesAndValues().begin() + splitter.getBegin());
                     partition.setSilentProbabilitiesToZero(partition.getStatesAndValues().begin() + splitter.getBegin(), partition.getStatesAndValues().begin() + splitter.getEnd());
                 }
-
+                
                 // Now refine all predecessor blocks in a weak manner. That is, we split according to the criterion of
                 // weak bisimulation.
                 for (auto blockPtr : predecessorBlocks) {
@@ -1205,7 +1283,7 @@ namespace storm {
                         // Restore the begin of the block.
                         block.setBegin(block.getOriginalBegin());
                     }
-
+                    
                     block.unmarkAsPredecessorBlock();
                     block.resetMarkedPosition();
                 }
@@ -1216,9 +1294,15 @@ 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, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, BisimulationType bisimulationType, bool keepRewards, bool bounded) {
+            std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::utility::graph::performProb01(backwardTransitions, phiStates, psiStates);
+            
+            boost::optional<storm::storage::sparse::state_type> representativePsiState;
+            if (!psiStates.empty()) {
+                representativePsiState = *psiStates.begin();
+            }
+            
+            Partition partition(model.getNumberOfStates(), statesWithProbability01.first, bounded || keepRewards ? psiStates : statesWithProbability01.second, representativePsiState, 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,64 @@ 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 The model for which the quotient model shall be computed. This needs to be given in order to
+                 * derive a suitable initial partition.
+                 * @param formula The formula that is to be preserved.
+                 */
+                Options(storm::models::AbstractModel<ValueType> const& model, 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<storm::storage::BitVector> phiStates;
+                boost::optional<storm::storage::BitVector> psiStates;
+                
+                // 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 +99,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,14 +203,14 @@ 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;
+                // Sets the representative state of this block
+                void setRepresentativeState(storm::storage::sparse::state_type representativeState);
                 
-                // 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;
+                // Retrieves the representative state for this block.
+                bool hasRepresentativeState() const;
+
+                // Retrieves the representative state for this block.
+                storm::storage::sparse::state_type getRepresentativeState() const;
                 
             private:
                 // An iterator to itself. This is needed to conveniently insert elements in the overall list of blocks
@@ -228,8 +240,9 @@ 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;
+                // An optional representative state for the block. If this is set, this state is used to derive the
+                // atomic propositions of the meta state in the quotient model.
+                boost::optional<storm::storage::sparse::state_type> representativeState;
             };
             
             class Partition {
@@ -252,11 +265,12 @@ 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 representativeProb1State If the set of prob1States is non-empty, this needs to be a state
+                 * that is representative for this block in the sense that the state representing this block in the quotient
+                 * model will receive exactly the atomic propositions of the representative state.
                  * @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, boost::optional<storm::storage::sparse::state_type> representativeProb1State, bool keepSilentProbabilities = false);
                 
                 Partition() = default;
                 Partition(Partition const& other) = default;
@@ -399,8 +413,7 @@ 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 atomicPropositions The set of atomic propositions that the bisimulation considers.
              * @param backwardTransitions The backward transitions of the model.
              * @param The initial partition.
              * @param bisimulationType The kind of bisimulation that is to be computed.
@@ -408,7 +421,7 @@ namespace storm {
              * method.
              */
             template<typename ModelType>
-            void partitionRefinement(ModelType const& model, boost::optional<std::set<std::string>> const& atomicPropositions, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Partition& partition, BisimulationType bisimulationType, bool keepRewards, bool buildQuotient);
+            void partitionRefinement(ModelType const& model, std::set<std::string> const& atomicPropositions, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Partition& partition, BisimulationType bisimulationType, bool keepRewards, bool buildQuotient);
             
             /*!
              * Refines the partition based on the provided splitter. After calling this method all blocks are stable
@@ -452,15 +465,14 @@ 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 selectedAtomicPropositions The set of atomic propositions that was considered by the bisimulation.
+             * The quotient will only have these atomic propositions.
              * @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, boost::optional<std::set<std::string>> const& selectedAtomicPropositions, Partition const& partition, BisimulationType bisimulationType, bool keepRewards);
+            void buildQuotient(ModelType const& model, std::set<std::string> const& selectedAtomicPropositions, Partition const& partition, BisimulationType bisimulationType, bool keepRewards);
 
             /*!
              * Creates the measure-driven initial partition for reaching psi states from phi states.
@@ -468,15 +480,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 phiStates The phi states in the model.
+             * @param psiStates 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, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, BisimulationType bisimulationType, bool keepRewards = true, bool bounded = false);
             
             /*!
              * Creates the initial partition based on all the labels in the given model.

src/storage/prism/BooleanVariable.cpp

@@ -11,7 +11,7 @@ namespace storm {
         }
         
         std::ostream& operator<<(std::ostream& stream, BooleanVariable const& variable) {
-            stream << variable.getName() << ": bool " << variable.getInitialValueExpression() << ";";
+            stream << variable.getName() << ": bool init" << variable.getInitialValueExpression() << ";";
             return stream;
         }
         

src/stormParametric.cpp

@@ -154,6 +154,11 @@ void check() {
     
     std::shared_ptr<storm::models::AbstractModel<ValueType>> model = storm::builder::ExplicitPrismModelBuilder<ValueType>::translateProgram(program, options);
     
+    // Convert the transition rewards to state rewards if necessary.
+    if (model->hasTransitionRewards()) {
+        model->convertTransitionRewardsToStateRewards();
+    }
+    
     model->printModelInformationToStream(std::cout);
     
     // Program Translation Time Measurement, End
@@ -173,51 +178,14 @@ void check() {
     
     bool checkRewards = formula->isRewardOperatorFormula();
     
-    std::string phiLabel;
-    std::string psiLabel;
-    
-    bool measureDrivenBisimulation = false;
-    if (formula->isProbabilityOperatorFormula()) {
-        storm::logic::Formula const& subformula = formula->asProbabilityOperatorFormula().getSubformula();
-        
-        if (subformula.isEventuallyFormula()) {
-            phiLabel = "true";
-            std::stringstream stream;
-            stream << subformula.asEventuallyFormula().getSubformula();
-            psiLabel = stream.str();
-            measureDrivenBisimulation = true;
-        } else if (subformula.isUntilFormula()) {
-            std::stringstream stream;
-            stream << subformula.asUntilFormula().getLeftSubformula();
-            phiLabel = stream.str();
-
-            std::stringstream stream2;
-            stream2 << subformula.asUntilFormula().getRightSubformula();
-            psiLabel = stream2.str();
-            measureDrivenBisimulation = true;
-        }
-    } else if (formula->isRewardOperatorFormula()) {
-        storm::logic::Formula const& subformula = formula->asRewardOperatorFormula().getSubformula();
-        
-        if (subformula.isReachabilityRewardFormula()) {
-            phiLabel = "true";
-            std::stringstream stream;
-            stream << subformula.asReachabilityRewardFormula().getSubformula();
-            psiLabel = stream.str();
-            measureDrivenBisimulation = true;
-        }
-    }
-    
     // Perform bisimulation minimization if requested.
     if (storm::settings::generalSettings().isBisimulationSet()) {
-        if (measureDrivenBisimulation) {
-            storm::storage::DeterministicModelBisimulationDecomposition<ValueType> bisimulationDecomposition(*dtmc, phiLabel, psiLabel, checkRewards, storm::settings::bisimulationSettings().isWeakBisimulationSet(), false, true);
-            *dtmc = std::move(*bisimulationDecomposition.getQuotient()->template as<storm::models::Dtmc<ValueType>>());
-        } else {
-            storm::storage::DeterministicModelBisimulationDecomposition<ValueType> bisimulationDecomposition(*dtmc, boost::optional<std::set<std::string>>(), checkRewards, storm::settings::bisimulationSettings().isWeakBisimulationSet(), true);
-            *dtmc = std::move(*bisimulationDecomposition.getQuotient()->template as<storm::models::Dtmc<ValueType>>());
-        }
+        typename storm::storage::DeterministicModelBisimulationDecomposition<ValueType>::Options options(*dtmc, *formula);
+        options.weak = storm::settings::bisimulationSettings().isWeakBisimulationSet();
         
+        storm::storage::DeterministicModelBisimulationDecomposition<ValueType> bisimulationDecomposition(*dtmc, options);
+        *dtmc = std::move(*bisimulationDecomposition.getQuotient()->template as<storm::models::Dtmc<ValueType>>());
+
         dtmc->printModelInformationToStream(std::cout);
     }
     

src/utility/cli.h

@@ -297,7 +297,16 @@ 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;
+                    if (formula) {
+                        options = storm::storage::DeterministicModelBisimulationDecomposition<double>::Options(*model, *formula.get());
+                    }
+                    if (storm::settings::bisimulationSettings().isWeakBisimulationSet()) {
+                        options.weak = true;
+                        options.bounded = false;
+                    }
+                    
+                    storm::storage::DeterministicModelBisimulationDecomposition<double> bisimulationDecomposition(*dtmc, options);
                     model = bisimulationDecomposition.getQuotient();
                     std::cout << "done." << std::endl << std::endl;
                 }
@@ -378,8 +387,8 @@ namespace storm {
                     std::unique_ptr<storm::modelchecker::CheckResult> result;
                     if (model->getType() == storm::models::DTMC) {
                         std::shared_ptr<storm::models::Dtmc<double>> dtmc = model->as<storm::models::Dtmc<double>>();
-//                        storm::modelchecker::SparseDtmcPrctlModelChecker<double> modelchecker(*dtmc);
-                        storm::modelchecker::SparseDtmcEliminationModelChecker<double> modelchecker(*dtmc);
+                        storm::modelchecker::SparseDtmcPrctlModelChecker<double> modelchecker(*dtmc);
+//                        storm::modelchecker::SparseDtmcEliminationModelChecker<double> modelchecker(*dtmc);
                         result = modelchecker.check(*formula.get());
                     } else if (model->getType() == storm::models::MDP) {
                         std::shared_ptr<storm::models::Mdp<double>> mdp = model->as<storm::models::Mdp<double>>();

test/functional/storage/BitVectorTest.cpp

@@ -98,6 +98,7 @@ TEST(BitVectorTest, SetFromInt) {
     EXPECT_FALSE(vector.get(62));
     EXPECT_TRUE(vector.get(63));
     
+    vector = storm::storage::BitVector(77);
     vector.setFromInt(62, 4, 15);
 
     EXPECT_TRUE(vector.get(62));
@@ -108,6 +109,14 @@ TEST(BitVectorTest, SetFromInt) {
     vector.setFromInt(62, 5, 17);
 }
 
+TEST(BitVectorTest, GetSetInt) {
+    storm::storage::BitVector vector(77);
+
+    vector.setFromInt(63, 3, 2);
+    EXPECT_EQ(2, vector.getAsInt(63, 3));
+}
+
+
 TEST(BitVectorDeathTest, GetSetAssertion) {
 	storm::storage::BitVector vector(32);
     

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,19 +17,35 @@ 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());
+
+    options.bounded = false;
+    options.weak = true;
     
-    storm::storage::DeterministicModelBisimulationDecomposition<double> bisim3(*dtmc, std::set<std::string>({"one"}), true, true, true);
+    storm::storage::DeterministicModelBisimulationDecomposition<double> bisim3(*dtmc, options);
     ASSERT_NO_THROW(result = bisim3.getQuotient());
     
     EXPECT_EQ(storm::models::DTMC, result->getType());
     EXPECT_EQ(5, result->getNumberOfStates());
     EXPECT_EQ(8, result->getNumberOfTransitions());
+    
+    auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("one");
+    auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
+    
+    typename storm::storage::DeterministicModelBisimulationDecomposition<double>::Options options2(*dtmc, *eventuallyFormula);
+    storm::storage::DeterministicModelBisimulationDecomposition<double> bisim4(*dtmc, options2);
+    ASSERT_NO_THROW(result = bisim4.getQuotient());
+    EXPECT_EQ(storm::models::DTMC, result->getType());
+    EXPECT_EQ(5, result->getNumberOfStates());
+    EXPECT_EQ(8, result->getNumberOfTransitions());
 }
 
 TEST(DeterministicModelBisimulationDecomposition, Crowds) {
@@ -38,7 +54,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,17 +62,54 @@ 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());
     EXPECT_EQ(43, result->getNumberOfStates());
     EXPECT_EQ(83, result->getNumberOfTransitions());
+    
+    auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("observe0Greater1");
+    auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
+    
+    typename storm::storage::DeterministicModelBisimulationDecomposition<double>::Options options2(*dtmc, *eventuallyFormula);
+    storm::storage::DeterministicModelBisimulationDecomposition<double> bisim4(*dtmc, options2);
+    ASSERT_NO_THROW(result = bisim4.getQuotient());
+
+    EXPECT_EQ(storm::models::DTMC, result->getType());
+    EXPECT_EQ(64, result->getNumberOfStates());
+    EXPECT_EQ(104, result->getNumberOfTransitions());
+    
+    auto probabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(eventuallyFormula);
+    
+    typename storm::storage::DeterministicModelBisimulationDecomposition<double>::Options options3(*dtmc, *probabilityOperatorFormula);
+    storm::storage::DeterministicModelBisimulationDecomposition<double> bisim5(*dtmc, options3);
+    ASSERT_NO_THROW(result = bisim5.getQuotient());
+
+    EXPECT_EQ(storm::models::DTMC, result->getType());
+    EXPECT_EQ(64, result->getNumberOfStates());
+    EXPECT_EQ(104, result->getNumberOfTransitions());
+    
+    auto boundedUntilFormula = std::make_shared<storm::logic::BoundedUntilFormula>(std::make_shared<storm::logic::BooleanLiteralFormula>(true), labelFormula, 50);
+    
+    typename storm::storage::DeterministicModelBisimulationDecomposition<double>::Options options4(*dtmc, *boundedUntilFormula);
+    storm::storage::DeterministicModelBisimulationDecomposition<double> bisim6(*dtmc, options4);
+    ASSERT_NO_THROW(result = bisim6.getQuotient());
+    
+    EXPECT_EQ(storm::models::DTMC, result->getType());
+    EXPECT_EQ(65, result->getNumberOfStates());
+    EXPECT_EQ(105, result->getNumberOfTransitions());
 }