Merge branch 'master' into parametricSystems

Conflicts:
	src/adapters/ExplicitModelAdapter.h
	src/storage/DeterministicModelBisimulationDecomposition.cpp
	src/utility/cli.h

Former-commit-id: c48cffb28e

.gitignore

@@ -43,3 +43,5 @@ build//CMakeLists.txt
 #Temp texteditor files
 *.orig
 *.*~
+# CMake generated/configured files
+src/utility/storm-version.cpp

src/adapters/ExplicitModelAdapter.h

@@ -97,12 +97,10 @@ namespace storm {
              * @param program The program to translate.
              * @param constantDefinitionString A string that contains a comma-separated definition of all undefined
              * constants in the model.
-             * @param rewardModelName The name of reward model to be added to the model. This must be either a reward
-             * model of the program or the empty string. In the latter case, the constructed model will contain no 
-             * rewards.
+             * @param rewardModel The reward model that is to be built.
              * @return The explicit model that was given by the probabilistic program.
              */
-            static std::unique_ptr<storm::models::AbstractModel<ValueType>> translateProgram(storm::prism::Program program, std::string const& constantDefinitionString = "", std::string const& rewardModelName = "") {
+            static std::unique_ptr<storm::models::AbstractModel<ValueType>> translateProgram(storm::prism::Program program, storm::prism::RewardModel const& rewardModel = storm::prism::RewardModel(), std::string const& constantDefinitionString = "") {
                 // Start by defining the undefined constants in the model.
                 // First, we need to parse the constant definition string.
                 std::map<std::string, storm::expressions::Expression> constantDefinitions = storm::utility::prism::parseConstantDefinitionString(program, constantDefinitionString);
@@ -118,21 +116,21 @@ namespace storm {
                 // all expressions in the program so we can then evaluate them without having to store the values of the
                 // constants in the state (i.e., valuation).
                 preparedProgram = preparedProgram.substituteConstants();
-                ModelComponents modelComponents = buildModelComponents(preparedProgram, rewardModelName);
+                ModelComponents modelComponents = buildModelComponents(preparedProgram, rewardModel);
                 
                 std::unique_ptr<storm::models::AbstractModel<ValueType>> result;
                 switch (program.getModelType()) {
                     case storm::prism::Program::ModelType::DTMC:
-                        result = std::unique_ptr<storm::models::AbstractModel<ValueType>>(new storm::models::Dtmc<ValueType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModelName != "" ? std::move(modelComponents.stateRewards) : boost::optional<std::vector<ValueType>>(), rewardModelName != "" ? std::move(modelComponents.transitionRewardMatrix) : boost::optional<storm::storage::SparseMatrix<ValueType>>(), std::move(modelComponents.choiceLabeling)));
+                        result = std::unique_ptr<storm::models::AbstractModel<ValueType>>(new storm::models::Dtmc<ValueType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModel.hasStateRewards() ? std::move(modelComponents.stateRewards) : boost::optional<std::vector<ValueType>>(), rewardModel.hasTransitionRewards() ? std::move(modelComponents.transitionRewardMatrix) : boost::optional<storm::storage::SparseMatrix<ValueType>>(), std::move(modelComponents.choiceLabeling)));
                         break;
                     case storm::prism::Program::ModelType::CTMC:
-                        result = std::unique_ptr<storm::models::AbstractModel<ValueType>>(new storm::models::Ctmc<ValueType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModelName != "" ? std::move(modelComponents.stateRewards) : boost::optional<std::vector<ValueType>>(), rewardModelName != "" ? std::move(modelComponents.transitionRewardMatrix) : boost::optional<storm::storage::SparseMatrix<ValueType>>(), std::move(modelComponents.choiceLabeling)));
+                        result = std::unique_ptr<storm::models::AbstractModel<ValueType>>(new storm::models::Ctmc<ValueType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModel.hasStateRewards() ? std::move(modelComponents.stateRewards) : boost::optional<std::vector<ValueType>>(), rewardModel.hasTransitionRewards() ? std::move(modelComponents.transitionRewardMatrix) : boost::optional<storm::storage::SparseMatrix<ValueType>>(), std::move(modelComponents.choiceLabeling)));
                         break;
                     case storm::prism::Program::ModelType::MDP:
-                        result = std::unique_ptr<storm::models::AbstractModel<ValueType>>(new storm::models::Mdp<ValueType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModelName != "" ? std::move(modelComponents.stateRewards) : boost::optional<std::vector<ValueType>>(), rewardModelName != "" ? std::move(modelComponents.transitionRewardMatrix) : boost::optional<storm::storage::SparseMatrix<ValueType>>(), std::move(modelComponents.choiceLabeling)));
+                        result = std::unique_ptr<storm::models::AbstractModel<ValueType>>(new storm::models::Mdp<ValueType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModel.hasStateRewards() ? std::move(modelComponents.stateRewards) : boost::optional<std::vector<ValueType>>(), rewardModel.hasTransitionRewards() ? std::move(modelComponents.transitionRewardMatrix) : boost::optional<storm::storage::SparseMatrix<ValueType>>(), std::move(modelComponents.choiceLabeling)));
                         break;
                     case storm::prism::Program::ModelType::CTMDP:
-                        result = std::unique_ptr<storm::models::AbstractModel<ValueType>>(new storm::models::Ctmdp<ValueType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModelName != "" ? std::move(modelComponents.stateRewards) : boost::optional<std::vector<ValueType>>(), rewardModelName != "" ? std::move(modelComponents.transitionRewardMatrix) : boost::optional<storm::storage::SparseMatrix<ValueType>>(), std::move(modelComponents.choiceLabeling)));
+                        result = std::unique_ptr<storm::models::AbstractModel<ValueType>>(new storm::models::Ctmdp<ValueType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModel.hasStateRewards() ? std::move(modelComponents.stateRewards) : boost::optional<std::vector<ValueType>>(), rewardModel.hasTransitionRewards() ? std::move(modelComponents.transitionRewardMatrix) : boost::optional<storm::storage::SparseMatrix<ValueType>>(), std::move(modelComponents.choiceLabeling)));
                         break;
                     default:
                         LOG4CPLUS_ERROR(logger, "Error while creating model from probabilistic program: cannot handle this model type.");
@@ -636,11 +634,10 @@ namespace storm {
              * Explores the state space of the given program and returns the components of the model as a result.
              *
              * @param program The program whose state space to explore.
-             * @param rewardModelName The name of the reward model that is to be considered. If empty, no reward model
-             * is considered.
+             * @param rewardModel The reward model that is to be considered.
              * @return A structure containing the components of the resulting model.
              */
-            static ModelComponents buildModelComponents(storm::prism::Program const& program, std::string const& rewardModelName) {
+            static ModelComponents buildModelComponents(storm::prism::Program const& program, storm::prism::RewardModel const& rewardModel) {
                 ModelComponents modelComponents;
 				expressions::ExpressionEvaluation<ValueType> eval;
 				
@@ -657,9 +654,6 @@ namespace storm {
                 // Create the structure for storing the reachable state space.
                 StateInformation stateInformation;
                 
-                // Get the selected reward model or create an empty one if none is selected.
-                storm::prism::RewardModel const& rewardModel = rewardModelName != "" ? program.getRewardModel(rewardModelName) : storm::prism::RewardModel();
-                
                 // Determine whether we have to combine different choices to one or whether this model can have more than
                 // one choice per state.
                 bool deterministicModel = program.getModelType() == storm::prism::Program::ModelType::DTMC || program.getModelType() == storm::prism::Program::ModelType::CTMC;

src/exceptions/BaseException.cpp

@@ -14,7 +14,11 @@ namespace storm {
             stream << cstr;
         }
 
-        const char* BaseException::what() const throw() {
+		BaseException::~BaseException() {
+			// Intentionally left empty.
+		}
+        
+        const char* BaseException::what() const noexcept {
             std::string errorString = this->stream.str();
             char* result = new char[errorString.size() + 1];
             result[errorString.size()] = '\0';

src/exceptions/BaseException.h

@@ -29,12 +29,17 @@ namespace storm {
              */
             BaseException(char const* cstr);
             
+			/*!
+			 * Declare a destructor to counter the "looser throw specificator" error
+			 */
+			virtual ~BaseException();
+
             /*!
              * Retrieves the message associated with this exception.
              *
              * @return The message associated with this exception.
              */
-            virtual const char* what() const throw();
+            virtual const char* what() const noexcept;
             
         protected:
             // This stream stores the message of this exception.

src/exceptions/ExceptionMacros.h

@@ -14,6 +14,8 @@ exception_name(char const* cstr) : BaseException(cstr) { \
 } \
 exception_name(exception_name const& cp) : BaseException(cp) { \
 } \
+~exception_name() throw() { \
+} \
 template<typename T> \
 exception_name& operator<<(T const& var) { \
     this->stream << var; \

src/settings/OptionBuilder.h

@@ -68,7 +68,7 @@ namespace storm {
              */
 			OptionBuilder& addArgument(std::shared_ptr<ArgumentBase> argument) {
                 STORM_LOG_THROW(!this->isBuild, storm::exceptions::IllegalFunctionCallException, "Cannot add an argument to an option builder that was already used to build the option.");
-                STORM_LOG_THROW(this->arguments.empty() || !argument->getIsOptional() || this->arguments.back()->getIsOptional(), storm::exceptions::IllegalArgumentException, "Unable to add non-optional argument after an option that is optional.");
+                STORM_LOG_THROW(this->arguments.empty() || argument->getIsOptional() || !this->arguments.back()->getIsOptional(), storm::exceptions::IllegalArgumentException, "Unable to add non-optional argument after an option that is optional.");
 
 				std::string lowerArgumentName = boost::algorithm::to_lower_copy(argument->getName());
                 STORM_LOG_THROW(argumentNameSet.find(lowerArgumentName) == argumentNameSet.end(), storm::exceptions::IllegalArgumentException, "Unable to add argument to option, because it already has an argument with the same name.");

src/settings/modules/GeneralSettings.cpp

@@ -61,7 +61,8 @@ namespace storm {
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("transition filename", "The name of the file from which to read the transitions.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build())
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("labeling filename", "The name of the file from which to read the state labeling.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, symbolicOptionName, false, "Parses the model given in a symbolic representation.").setShortName(symbolicOptionShortName)
-                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the symbolic model.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the symbolic model.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build())
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("rewardmodel", "The name of the reward model to use.").setDefaultValueString("").setIsOptional(true).build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, pctlOptionName, false, "Specifies a PCTL formula that is to be checked on the model.")
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("formula", "The formula to check.").build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, pctlFileOptionName, false, "Specifies the PCTL formulas that are to be checked on the model.")
@@ -154,6 +155,14 @@ namespace storm {
                 return this->getOption(symbolicOptionName).getArgumentByName("filename").getValueAsString();
             }
             
+            bool GeneralSettings::isSymbolicRewardModelNameSet() const {
+                return this->getOption(symbolicOptionName).getArgumentByName("rewardmodel").getHasBeenSet();
+            }
+            
+            std::string GeneralSettings::getSymbolicRewardModelName() const {
+                return this->getOption(symbolicOptionName).getArgumentByName("rewardmodel").getValueAsString();
+            }
+            
             bool GeneralSettings::isPctlPropertySet() const {
                 return this->getOption(pctlOptionName).getHasOptionBeenSet();
             }

src/settings/modules/GeneralSettings.h

@@ -39,7 +39,6 @@ namespace storm {
                  */
                 bool isVersionSet() const;
 				
-				
                 /*!
                  * Retrieves the name of the module for which to show the help or "all" to indicate that the full help
                  * needs to be shown.
@@ -128,6 +127,20 @@ namespace storm {
                  */
                 std::string getSymbolicModelFilename() const;
                 
+                /*!
+                 * Retrieves whether the name of a reward model was passed to the symbolic option.
+                 *
+                 * @return True iff the name of a reward model was passed to the symbolic option.
+                 */
+                bool isSymbolicRewardModelNameSet() const;
+                
+                /*!
+                 * Retrieves the name of the reward model if one was set using the symbolic option.
+                 *
+                 * @return The name of the selected reward model.
+                 */
+                std::string getSymbolicRewardModelName() const;
+
                 /*!
                  * Retrieves whether the pctl option was set.
                  *

src/storage/DeterministicModelBisimulationDecomposition.cpp

@@ -13,10 +13,7 @@ namespace storm {
     namespace storage {
         
         template<typename ValueType>
-        std::size_t DeterministicModelBisimulationDecomposition<ValueType>::Block::blockId = 0;
-        
-        template<typename ValueType>
-        DeterministicModelBisimulationDecomposition<ValueType>::Block::Block(storm::storage::sparse::state_type begin, storm::storage::sparse::state_type end, Block* prev, Block* next, std::shared_ptr<std::string> const& label) : next(next), prev(prev), begin(begin), end(end), markedAsSplitter(false), markedAsPredecessorBlock(false), markedPosition(begin), absorbing(false), id(blockId++), label(label) {
+        DeterministicModelBisimulationDecomposition<ValueType>::Block::Block(storm::storage::sparse::state_type begin, storm::storage::sparse::state_type end, Block* prev, Block* next, std::size_t id, std::shared_ptr<std::string> const& label) : next(next), prev(prev), begin(begin), end(end), markedAsSplitter(false), markedAsPredecessorBlock(false), markedPosition(begin), absorbing(false), id(id), label(label) {
             if (next != nullptr) {
                 next->prev = this;
             }
@@ -247,7 +244,7 @@ namespace storm {
         template<typename ValueType>
         DeterministicModelBisimulationDecomposition<ValueType>::Partition::Partition(std::size_t numberOfStates, bool keepSilentProbabilities) : stateToBlockMapping(numberOfStates), statesAndValues(numberOfStates), positions(numberOfStates), keepSilentProbabilities(keepSilentProbabilities), silentProbabilities() {
             // Create the block and give it an iterator to itself.
-            typename std::list<Block>::iterator it = blocks.emplace(this->blocks.end(), 0, numberOfStates, nullptr, nullptr);
+            typename std::list<Block>::iterator it = blocks.emplace(this->blocks.end(), 0, numberOfStates, nullptr, nullptr, this->blocks.size());
             it->setIterator(it);
             
             // Set up the different parts of the internal structure.
@@ -265,7 +262,7 @@ namespace storm {
         
         template<typename ValueType>
         DeterministicModelBisimulationDecomposition<ValueType>::Partition::Partition(std::size_t numberOfStates, storm::storage::BitVector const& prob0States, storm::storage::BitVector const& prob1States, std::string const& otherLabel, std::string const& prob1Label, bool keepSilentProbabilities) : stateToBlockMapping(numberOfStates), statesAndValues(numberOfStates), positions(numberOfStates), keepSilentProbabilities(keepSilentProbabilities), silentProbabilities() {
-            typename std::list<Block>::iterator firstIt = blocks.emplace(this->blocks.end(), 0, prob0States.getNumberOfSetBits(), nullptr, nullptr);
+            typename std::list<Block>::iterator firstIt = blocks.emplace(this->blocks.end(), 0, prob0States.getNumberOfSetBits(), nullptr, nullptr, this->blocks.size());
             Block& firstBlock = *firstIt;
             firstBlock.setIterator(firstIt);
 
@@ -278,7 +275,7 @@ namespace storm {
             }
             firstBlock.setAbsorbing(true);
 
-            typename std::list<Block>::iterator secondIt = blocks.emplace(this->blocks.end(), position, position + prob1States.getNumberOfSetBits(), &firstBlock, nullptr, std::shared_ptr<std::string>(new std::string(prob1Label)));
+            typename std::list<Block>::iterator secondIt = blocks.emplace(this->blocks.end(), position, position + prob1States.getNumberOfSetBits(), &firstBlock, nullptr, this->blocks.size(), std::shared_ptr<std::string>(new std::string(prob1Label)));
             Block& secondBlock = *secondIt;
             secondBlock.setIterator(secondIt);
             
@@ -290,7 +287,7 @@ namespace storm {
             }
             secondBlock.setAbsorbing(true);
             
-            typename std::list<Block>::iterator thirdIt = blocks.emplace(this->blocks.end(), position, numberOfStates, &secondBlock, nullptr, otherLabel == "true" ? std::shared_ptr<std::string>(nullptr) : std::shared_ptr<std::string>(new std::string(otherLabel)));
+            typename std::list<Block>::iterator thirdIt = blocks.emplace(this->blocks.end(), position, numberOfStates, &secondBlock, nullptr, this->blocks.size(), otherLabel == "true" ? std::shared_ptr<std::string>(nullptr) : std::shared_ptr<std::string>(new std::string(otherLabel)));
             Block& thirdBlock = *thirdIt;
             thirdBlock.setIterator(thirdIt);
             
@@ -411,7 +408,7 @@ namespace storm {
             }
             
             // Actually create the new block and insert it at the correct position.
-            typename std::list<Block>::iterator selfIt = this->blocks.emplace(block.getIterator(), block.getBegin(), position, block.getPreviousBlockPointer(), &block, block.getLabelPtr());
+            typename std::list<Block>::iterator selfIt = this->blocks.emplace(block.getIterator(), block.getBegin(), position, block.getPreviousBlockPointer(), &block, this->blocks.size(), block.getLabelPtr());
             selfIt->setIterator(selfIt);
             Block& newBlock = *selfIt;
             
@@ -435,7 +432,7 @@ namespace storm {
             }
             
             // Actually insert the new block.
-            typename std::list<Block>::iterator it = this->blocks.emplace(block.getIterator(), begin, block.getBegin(), block.getPreviousBlockPointer(), &block);
+            typename std::list<Block>::iterator it = this->blocks.emplace(block.getIterator(), begin, block.getBegin(), block.getPreviousBlockPointer(), &block, this->blocks.size());
             Block& newBlock = *it;
             newBlock.setIterator(it);
             
@@ -563,9 +560,16 @@ namespace storm {
             }
             std::cout << std::endl << "state to block mapping: " << std::endl;
             for (auto const& block : stateToBlockMapping) {
-                std::cout << block << " ";
+                std::cout << block << "[" << block->getId() <<"] ";
             }
             std::cout << std::endl;
+            if (this->keepSilentProbabilities) {
+                std::cout << "silent probabilities" << std::endl;
+                for (auto const& prob : silentProbabilities) {
+                    std::cout << prob << " ";
+                }
+                std::cout << std::endl;
+            }
             std::cout << "size: " << this->blocks.size() << std::endl;
             assert(this->check());
         }
@@ -576,41 +580,41 @@ namespace storm {
         }
         
         template<typename ValueType>
-        DeterministicModelBisimulationDecomposition<ValueType>::DeterministicModelBisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, bool weak, bool buildQuotient) : comparator() {
-            STORM_LOG_THROW(!model.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures.");
+        DeterministicModelBisimulationDecomposition<ValueType>::DeterministicModelBisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, boost::optional<std::set<std::string>> const& atomicPropositions, bool weak, bool buildQuotient) : comparator() {
+            STORM_LOG_THROW(!model.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);
-            partitionRefinement(model, backwardTransitions, initialPartition, bisimulationType, buildQuotient);
+            Partition initialPartition = getLabelBasedInitialPartition(model, backwardTransitions, bisimulationType, atomicPropositions);
+            partitionRefinement(model, atomicPropositions, backwardTransitions, initialPartition, bisimulationType, buildQuotient);
         }
 
         template<typename ValueType>
-        DeterministicModelBisimulationDecomposition<ValueType>::DeterministicModelBisimulationDecomposition(storm::models::Ctmc<ValueType> const& model, bool weak, bool buildQuotient) {
-            STORM_LOG_THROW(!model.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures.");
+        DeterministicModelBisimulationDecomposition<ValueType>::DeterministicModelBisimulationDecomposition(storm::models::Ctmc<ValueType> const& model, boost::optional<std::set<std::string>> const& atomicPropositions, bool weak, bool buildQuotient) {
+            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::WeakCtmc : BisimulationType::Strong;
-            Partition initialPartition = getLabelBasedInitialPartition(model, backwardTransitions, bisimulationType);
-            partitionRefinement(model, backwardTransitions, initialPartition, bisimulationType, buildQuotient);
+            Partition initialPartition = getLabelBasedInitialPartition(model, backwardTransitions, bisimulationType, atomicPropositions);
+            partitionRefinement(model, atomicPropositions, backwardTransitions, initialPartition, bisimulationType, buildQuotient);
         }
         
         template<typename ValueType>
         DeterministicModelBisimulationDecomposition<ValueType>::DeterministicModelBisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, std::string const& phiLabel, std::string const& psiLabel, bool weak, bool bounded, bool buildQuotient) {
-            STORM_LOG_THROW(!model.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures.");
+            STORM_LOG_THROW(!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.");
             storm::storage::SparseMatrix<ValueType> backwardTransitions = model.getBackwardTransitions();
             BisimulationType bisimulationType = weak ? BisimulationType::WeakDtmc : BisimulationType::Strong;
             Partition initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, phiLabel, psiLabel, bisimulationType, bounded);
-            partitionRefinement(model, model.getBackwardTransitions(), initialPartition, bisimulationType, buildQuotient);
+            partitionRefinement(model, std::set<std::string>({phiLabel, psiLabel}), model.getBackwardTransitions(), initialPartition, bisimulationType, buildQuotient);
         }
         
         template<typename ValueType>
         DeterministicModelBisimulationDecomposition<ValueType>::DeterministicModelBisimulationDecomposition(storm::models::Ctmc<ValueType> const& model, std::string const& phiLabel, std::string const& psiLabel, bool weak, bool bounded, bool buildQuotient) {
-            STORM_LOG_THROW(!model.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures.");
+            STORM_LOG_THROW(!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.");
             storm::storage::SparseMatrix<ValueType> backwardTransitions = model.getBackwardTransitions();
             BisimulationType bisimulationType = weak ? BisimulationType::WeakCtmc : BisimulationType::Strong;
             Partition initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, phiLabel, psiLabel, bisimulationType, bounded);
-            partitionRefinement(model, model.getBackwardTransitions(), initialPartition, bisimulationType, buildQuotient);
+            partitionRefinement(model, std::set<std::string>({phiLabel, psiLabel}), model.getBackwardTransitions(), initialPartition, bisimulationType, buildQuotient);
         }
         
         template<typename ValueType>
@@ -621,7 +625,7 @@ namespace storm {
         
         template<typename ValueType>
         template<typename ModelType>
-        void DeterministicModelBisimulationDecomposition<ValueType>::buildQuotient(ModelType const& model, Partition const& partition, BisimulationType bisimulationType) {
+        void DeterministicModelBisimulationDecomposition<ValueType>::buildQuotient(ModelType const& model, boost::optional<std::set<std::string>> const& selectedAtomicPropositions, Partition const& partition, BisimulationType bisimulationType) {
             // In order to create the quotient model, we need to construct
             // (a) the new transition matrix,
             // (b) the new labeling,
@@ -632,7 +636,8 @@ namespace storm {
             
             // Prepare the new state labeling for (b).
             storm::models::AtomicPropositionsLabeling newLabeling(this->size(), model.getStateLabeling().getNumberOfAtomicPropositions());
-            std::set<std::string> atomicPropositionsSet = model.getStateLabeling().getAtomicPropositions();
+            std::set<std::string> atomicPropositionsSet = selectedAtomicPropositions ? selectedAtomicPropositions.get() : model.getStateLabeling().getAtomicPropositions();
+            atomicPropositionsSet.insert("init");
             std::vector<std::string> atomicPropositions = std::vector<std::string>(atomicPropositionsSet.begin(), atomicPropositionsSet.end());
             for (auto const& ap : atomicPropositions) {
                 newLabeling.addAtomicProposition(ap);
@@ -646,7 +651,8 @@ namespace storm {
                 // they all behave equally.
                 storm::storage::sparse::state_type representativeState = *block.begin();
                 
-                // However, for weak bisimulation, we need to make sure the representative state is a non-silent one.
+                // However, for weak bisimulation, we need to make sure the representative state is a non-silent one (if
+                // there is any such state).
                 if (bisimulationType == BisimulationType::WeakDtmc) {
                     for (auto const& state : block) {
                         if (!partition.isSilent(state, comparator)) {
@@ -731,7 +737,7 @@ namespace storm {
         
         template<typename ValueType>
         template<typename ModelType>
-        void DeterministicModelBisimulationDecomposition<ValueType>::partitionRefinement(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Partition& partition, BisimulationType bisimulationType, bool buildQuotient) {
+        void DeterministicModelBisimulationDecomposition<ValueType>::partitionRefinement(ModelType const& model, boost::optional<std::set<std::string>> const& atomicPropositions, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Partition& partition, BisimulationType bisimulationType, bool buildQuotient) {
             std::chrono::high_resolution_clock::time_point totalStart = std::chrono::high_resolution_clock::now();
 
             // Initially, all blocks are potential splitter, so we insert them in the splitterQueue.
@@ -769,7 +775,7 @@ namespace storm {
 
             // If we are required to build the quotient model, do so now.
             if (buildQuotient) {
-                this->buildQuotient(model, partition, bisimulationType);
+                this->buildQuotient(model, atomicPropositions, partition, bisimulationType);
             }
 
             std::chrono::high_resolution_clock::duration extractionTime = std::chrono::high_resolution_clock::now() - extractionStart;
@@ -1188,6 +1194,12 @@ namespace storm {
             std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::utility::graph::performProb01(backwardTransitions, phiLabel == "true" ? storm::storage::BitVector(model.getNumberOfStates(), true) : model.getLabeledStates(phiLabel), model.getLabeledStates(psiLabel));
             Partition partition(model.getNumberOfStates(), statesWithProbability01.first, bounded ? model.getLabeledStates(psiLabel) : statesWithProbability01.second, phiLabel, psiLabel, bisimulationType == BisimulationType::WeakDtmc);
             
+            // If the model has state rewards, we need to consider them, because otherwise reward properties are not
+            // preserved.
+            if (model.hasStateRewards()) {
+                this->splitRewards(model, partition);
+            }
+            
             // If we are creating the initial partition for weak bisimulation, we need to (a) split off all divergent
             // states of each initial block and (b) initialize the vector of silent probabilities held by the partition.
             if (bisimulationType == BisimulationType::WeakDtmc) {
@@ -1268,14 +1280,30 @@ namespace storm {
         
         template<typename ValueType>
         template<typename ModelType>
-        typename DeterministicModelBisimulationDecomposition<ValueType>::Partition DeterministicModelBisimulationDecomposition<ValueType>::getLabelBasedInitialPartition(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, BisimulationType bisimulationType) {
+        typename DeterministicModelBisimulationDecomposition<ValueType>::Partition DeterministicModelBisimulationDecomposition<ValueType>::getLabelBasedInitialPartition(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, BisimulationType bisimulationType, boost::optional<std::set<std::string>> const& atomicPropositions) {
             Partition partition(model.getNumberOfStates(), bisimulationType == BisimulationType::WeakDtmc);
+            
+            if (atomicPropositions) {
+                for (auto const& label : atomicPropositions.get()) {
+                    if (label == "init") {
+                        continue;
+                    }
+                    partition.splitLabel(model.getLabeledStates(label));
+                }
+            } else {
                 for (auto const& label : model.getStateLabeling().getAtomicPropositions()) {
                     if (label == "init") {
                         continue;
                     }
                     partition.splitLabel(model.getLabeledStates(label));
                 }
+            }
+            
+            // If the model has state rewards, we need to consider them, because otherwise reward properties are not
+            // preserved.
+            if (model.hasStateRewards()) {
+                this->splitRewards(model, partition);
+            }
             
             // If we are creating the initial partition for weak bisimulation, we need to (a) split off all divergent
             // states of each initial block and (b) initialize the vector of silent probabilities held by the partition.
@@ -1304,6 +1332,47 @@ namespace storm {
             }
         }
         
+        template<typename ValueType>
+        template<typename ModelType>
+        void DeterministicModelBisimulationDecomposition<ValueType>::splitRewards(ModelType const& model, Partition& partition) {
+            if (model.hasStateRewards()) {
+                return;
+            }
+            
+            for (auto& block : partition.getBlocks()) {
+                std::sort(partition.getBegin(block), partition.getEnd(block), [&model] (std::pair<storm::storage::sparse::state_type, ValueType> const& a, std::pair<storm::storage::sparse::state_type, ValueType> const& b) { return model.getStateRewardVector()[a.first] < model.getStateRewardVector()[b.first]; } );
+                
+                // Update the positions vector.
+                storm::storage::sparse::state_type position = block.getBegin();
+                for (auto stateIt = partition.getBegin(block), stateIte = partition.getEnd(block); stateIt != stateIte; ++stateIt, ++position) {
+                    partition.setPosition(stateIt->first, position);
+                }
+                
+                // Finally, we need to scan the ranges of states that agree on the probability.
+                typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator begin = partition.getBegin(block);
+                typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator current = begin;
+                typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator end = partition.getEnd(block) - 1;
+                storm::storage::sparse::state_type currentIndex = block.getBegin();
+                
+                // Now we can check whether the block needs to be split, which is the case iff the rewards for the first
+                // and the last state are different.
+                bool blockSplit = !comparator.isEqual(begin->second, end->second);
+                while (!comparator.isEqual(begin->second, end->second)) {
+                    // Now we scan for the first state in the block that disagrees on the reward value. Note that we do
+                    // not have to check currentIndex for staying within bounds, because we know the matching state is
+                    // within bounds.
+                    ValueType const& currentValue = begin->second;
+                    
+                    ++begin;
+                    ++currentIndex;
+                    while (begin != end && comparator.isEqual(begin->second, currentValue)) {
+                        ++begin;
+                        ++currentIndex;
+                    }
+                }
+            }
+        }
+        
         template class DeterministicModelBisimulationDecomposition<double>;
         
 #ifdef PARAMETRIC_SYSTEMS

src/storage/DeterministicModelBisimulationDecomposition.h

@@ -25,19 +25,23 @@ namespace storm {
              * Decomposes the given DTMC into equivalence classes under weak or strong bisimulation.
              *
              * @param model The model to decompose.
+             * @param A set of atomic propositions that is to be respected. If not given, all atomic propositions of the
+             * model will be respected. If built, the quotient model will only contain the respected atomic propositions.
              * @param weak A flag indication whether a weak bisimulation is to be computed.
              * @param buildQuotient Sets whether or not the quotient model is to be built.
              */
-            DeterministicModelBisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, bool weak = false, bool buildQuotient = false);
+            DeterministicModelBisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, boost::optional<std::set<std::string>> const& atomicPropositions = boost::optional<std::set<std::string>>(), bool weak = false, bool buildQuotient = false);
 
             /*!
              * Decomposes the given CTMC into equivalence classes under weak or strong bisimulation.
              *
              * @param model The model to decompose.
+             * @param A set of atomic propositions that is to be respected. If not given, all atomic propositions of the
+             * model will be respected. If built, the quotient model will only contain the respected atomic propositions.
              * @param weak A flag indication whether a weak bisimulation is to be computed.
              * @param buildQuotient Sets whether or not the quotient model is to be built.
              */
-            DeterministicModelBisimulationDecomposition(storm::models::Ctmc<ValueType> const& model, bool weak = false, bool buildQuotient = false);
+            DeterministicModelBisimulationDecomposition(storm::models::Ctmc<ValueType> const& model, boost::optional<std::set<std::string>> const& atomicPropositions = boost::optional<std::set<std::string>>(), bool weak = false, bool buildQuotient = false);
             
             /*!
              * Decomposes the given DTMC into equivalence classes under strong bisimulation in a way that onle safely
@@ -83,7 +87,7 @@ namespace storm {
                 typedef typename std::list<Block>::const_iterator const_iterator;
                 
                 // Creates a new block with the given begin and end.
-                Block(storm::storage::sparse::state_type begin, storm::storage::sparse::state_type end, Block* prev, Block* next, std::shared_ptr<std::string> const& label = nullptr);
+                Block(storm::storage::sparse::state_type begin, storm::storage::sparse::state_type end, Block* prev, Block* next, std::size_t id, std::shared_ptr<std::string> const& label = nullptr);
                 
                 // Prints the block.
                 void print(Partition const& partition) const;
@@ -226,9 +230,6 @@ namespace storm {
                 
                 // The label of the block or nullptr if it has none.
                 std::shared_ptr<std::string> label;
-                
-                // A counter for the IDs of the blocks.
-                static std::size_t blockId;
             };
             
             class Partition {
@@ -394,6 +395,8 @@ namespace storm {
              * getQuotient().
              *
              * @param model The model on whose state space to compute the coarses strong bisimulation relation.
+             * @param atomicPropositions The set of atomic propositions that the bisimulation considers. If not given,
+             * all atomic propositions are considered.
              * @param backwardTransitions The backward transitions of the model.
              * @param The initial partition.
              * @param bisimulationType The kind of bisimulation that is to be computed.
@@ -401,7 +404,7 @@ namespace storm {
              * method.
              */
             template<typename ModelType>
-            void partitionRefinement(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Partition& partition, BisimulationType bisimulationType, bool buildQuotient);
+            void partitionRefinement(ModelType const& model, boost::optional<std::set<std::string>> const& atomicPropositions, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Partition& partition, BisimulationType bisimulationType, bool buildQuotient);
             
             /*!
              * Refines the partition based on the provided splitter. After calling this method all blocks are stable
@@ -445,12 +448,15 @@ namespace storm {
              *
              * @param model The model whose state space was used for computing the equivalence classes. This is used for
              * determining the transitions of each equivalence class.
+             * @param selectedAtomicPropositions The set of atomic propositions that was considered by the bisimulation. The
+             * quotient will only have these atomic propositions. If not given, all atomic propositions will be
+             * considered.
              * @param partition The previously computed partition. This is used for quickly retrieving the block of a
              * state.
              * @param bisimulationType The kind of bisimulation that is to be computed.
              */
             template<typename ModelType>
-            void buildQuotient(ModelType const& model, Partition const& partition, BisimulationType bisimulationType);
+            void buildQuotient(ModelType const& model, boost::optional<std::set<std::string>> const& selectedAtomicPropositions, Partition const& partition, BisimulationType bisimulationType);
 
             /*!
              * Creates the measure-driven initial partition for reaching psi states from phi states.
@@ -474,10 +480,12 @@ namespace storm {
              * @param model The model whose state space is partitioned based on its labels.
              * @param backwardTransitions The backward transitions of the model.
              * @param bisimulationType The kind of bisimulation that is to be computed.
+             * @param atomicPropositions The set of atomic propositions to respect. If not given, then all atomic
+             * propositions of the model are respected.
              * @return The resulting partition.
              */
             template<typename ModelType>
-            Partition getLabelBasedInitialPartition(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, BisimulationType bisimulationType);
+            Partition getLabelBasedInitialPartition(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, BisimulationType bisimulationType, boost::optional<std::set<std::string>> const& atomicPropositions = boost::optional<std::set<std::string>>());
             
             /*!
              * Splits all blocks of the given partition into a block that contains all divergent states and another block
@@ -500,6 +508,15 @@ namespace storm {
             template<typename ModelType>
             void initializeSilentProbabilities(ModelType const& model, Partition& partition);
             
+            /*!
+             * Splits all blocks of the partition in a way such that the states of each block agree on the rewards.
+             *
+             * @param model The model from which to look-up the rewards.
+             * @param partition The partition that is to be split.
+             */
+            template<typename ModelType>
+            void splitRewards(ModelType const& model, Partition& partition);
+            
             // If required, a quotient model is built and stored in this member.
             std::shared_ptr<storm::models::AbstractDeterministicModel<ValueType>> quotient;
             

src/storage/StateBlock.h

@@ -10,7 +10,7 @@
 namespace storm {
     namespace storage {
         
-        // Typedef the most common state container
+        // Typedef the most common state container.
         typedef boost::container::flat_set<sparse::state_type> FlatSetStateContainer;
         
         std::ostream& operator<<(std::ostream& out, FlatSetStateContainer const& block);

src/storage/prism/Program.cpp

@@ -145,6 +145,10 @@ namespace storm {
             return variableNameToModuleIndexPair->second;
         }
         
+        bool Program::hasRewardModel() const {
+            return !this->rewardModels.empty();
+        }
+        
         std::vector<storm::prism::RewardModel> const& Program::getRewardModels() const {
             return this->rewardModels;
         }
@@ -159,6 +163,11 @@ namespace storm {
             return this->getRewardModels()[nameIndexPair->second];
         }
         
+        RewardModel const& Program::getRewardModel(uint_fast64_t index) const {
+            STORM_LOG_THROW(this->getNumberOfRewardModels() > index, storm::exceptions::OutOfRangeException, "Reward model with index " << index << " does not exist.");
+            return this->rewardModels[index];
+        }
+        
         std::vector<Label> const& Program::getLabels() const {
             return this->labels;
         }

src/storage/prism/Program.h

@@ -219,6 +219,13 @@ namespace storm {
              */
             uint_fast64_t getModuleIndexByVariable(std::string const& variableName) const;
             
+            /*!
+             * Retrieves whether the program has reward models.
+             *
+             * @return True iff the program has at least one reward model.
+             */
+            bool hasRewardModel() const;
+            
             /*!
              * Retrieves the reward models of the program.
              *
@@ -241,6 +248,14 @@ namespace storm {
              */
             RewardModel const& getRewardModel(std::string const& rewardModelName) const;
             
+            /*!
+             * Retrieves the reward model with the given index.
+             *
+             * @param index The index of the reward model to return.
+             * @return The reward model with the given index.
+             */
+            RewardModel const& getRewardModel(uint_fast64_t index) const;
+            
             /*!
              * Retrieves all labels that are defined by the probabilitic program.
              *

src/storage/prism/RewardModel.cpp

@@ -10,6 +10,10 @@ namespace storm {
             return this->rewardModelName;
         }
         
+        bool RewardModel::empty() const {
+            return !this->hasStateRewards() && !this->hasTransitionRewards();
+        }
+        
         bool RewardModel::hasStateRewards() const {
             return this->stateRewards.size() > 0;
         }

src/storage/prism/RewardModel.h

@@ -40,6 +40,13 @@ namespace storm {
              */
             std::string const& getName() const;
             
+            /*!
+             * Checks whether the reward model is empty, i.e. contains no state or transition rewards.
+             *
+             * @return True iff the reward model is empty.
+             */
+            bool empty() const;
+            
             /*!
              * Retrieves whether there are any state rewards.
              *

src/utility/cli.h

@@ -262,7 +262,7 @@ namespace storm {
                     storm::prism::Program program = storm::parser::PrismParser::parse(programFile);
                     
                     // Then, build the model from the symbolic description.
-                    result = storm::adapters::ExplicitModelAdapter<ValueType>::translateProgram(program, constants);
+                    result = storm::adapters::ExplicitModelAdapter<double>::translateProgram(program, settings.isSymbolicRewardModelNameSet() ? program.getRewardModel(settings.getSymbolicRewardModelName()) : storm::prism::RewardModel(), constants);
                 } else {
                     STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model.");
                 }
@@ -275,7 +275,7 @@ namespace storm {
                     std::shared_ptr<storm::models::Dtmc<double>> dtmc = result->template as<storm::models::Dtmc<double>>();
                     
                     STORM_PRINT(std::endl << "Performing bisimulation minimization..." << std::endl);
-                    storm::storage::DeterministicModelBisimulationDecomposition<double> bisimulationDecomposition(*dtmc, storm::settings::bisimulationSettings().isWeakBisimulationSet(), true);
+                    storm::storage::DeterministicModelBisimulationDecomposition<double> bisimulationDecomposition(*dtmc, boost::optional<std::set<std::string>>(), storm::settings::bisimulationSettings().isWeakBisimulationSet(), true);
                     
                     result = bisimulationDecomposition.getQuotient();
                     

test/functional/storage/DeterministicModelBisimulationDecompositionTest.cpp

@@ -0,0 +1,62 @@
+#include "gtest/gtest.h"
+#include "storm-config.h"
+#include "src/parser/AutoParser.h"
+#include "storage/DeterministicModelBisimulationDecomposition.h"
+
+TEST(DeterministicModelBisimulationDecomposition, Die) {
+	std::shared_ptr<storm::models::AbstractModel<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/die/die.tra", STORM_CPP_BASE_PATH "/examples/dtmc/die/die.lab", "", "");
+    
+    ASSERT_EQ(abstractModel->getType(), storm::models::DTMC);
+	std::shared_ptr<storm::models::Dtmc<double>> dtmc = abstractModel->as<storm::models::Dtmc<double>>();
+
+    storm::storage::DeterministicModelBisimulationDecomposition<double> bisim(*dtmc, boost::optional<std::set<std::string>>(), false, true);
+    std::shared_ptr<storm::models::AbstractModel<double>> result;
+    ASSERT_NO_THROW(result = bisim.getQuotient());
+
+    EXPECT_EQ(storm::models::DTMC, result->getType());
+    EXPECT_EQ(13, result->getNumberOfStates());
+    EXPECT_EQ(20, result->getNumberOfTransitions());
+
+    storm::storage::DeterministicModelBisimulationDecomposition<double> bisim2(*dtmc, std::set<std::string>({"one"}), false, true);
+    ASSERT_NO_THROW(result = bisim2.getQuotient());
+    
+    EXPECT_EQ(storm::models::DTMC, result->getType());
+    EXPECT_EQ(5, result->getNumberOfStates());
+    EXPECT_EQ(8, result->getNumberOfTransitions());
+    
+    storm::storage::DeterministicModelBisimulationDecomposition<double> bisim3(*dtmc, std::set<std::string>({"one"}), true, true);
+    ASSERT_NO_THROW(result = bisim3.getQuotient());
+    
+    EXPECT_EQ(storm::models::DTMC, result->getType());
+    EXPECT_EQ(5, result->getNumberOfStates());
+    EXPECT_EQ(8, result->getNumberOfTransitions());
+}
+
+TEST(DeterministicModelBisimulationDecomposition, Crowds) {
+	std::shared_ptr<storm::models::AbstractModel<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds5_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds5_5.lab", "", "");
+    
+    ASSERT_EQ(abstractModel->getType(), storm::models::DTMC);
+	std::shared_ptr<storm::models::Dtmc<double>> dtmc = abstractModel->as<storm::models::Dtmc<double>>();
+
+    storm::storage::DeterministicModelBisimulationDecomposition<double> bisim(*dtmc, boost::optional<std::set<std::string>>(), false, true);
+    std::shared_ptr<storm::models::AbstractModel<double>> result;
+    ASSERT_NO_THROW(result = bisim.getQuotient());
+    
+    EXPECT_EQ(storm::models::DTMC, result->getType());
+    EXPECT_EQ(334, result->getNumberOfStates());
+    EXPECT_EQ(546, result->getNumberOfTransitions());
+    
+    storm::storage::DeterministicModelBisimulationDecomposition<double> bisim2(*dtmc, std::set<std::string>({"observe0Greater1"}), false, true);
+    ASSERT_NO_THROW(result = bisim2.getQuotient());
+    
+    EXPECT_EQ(storm::models::DTMC, result->getType());
+    EXPECT_EQ(65, result->getNumberOfStates());
+    EXPECT_EQ(105, result->getNumberOfTransitions());
+
+    storm::storage::DeterministicModelBisimulationDecomposition<double> bisim3(*dtmc, std::set<std::string>({"observe0Greater1"}), true, true);
+    ASSERT_NO_THROW(result = bisim3.getQuotient());
+    
+    EXPECT_EQ(storm::models::DTMC, result->getType());
+    EXPECT_EQ(43, result->getNumberOfStates());
+    EXPECT_EQ(83, result->getNumberOfTransitions());
+}