Implemented a method for generating a choiceLabeling based on the stateIds

Former-commit-id: d1eedecc22

src/models/AbstractDeterministicModel.h

@@ -110,6 +110,23 @@ class AbstractDeterministicModel: public AbstractModel<T> {
                 outStream << "}" << std::endl;
             }
         }
+
+		/*!
+		 * Assigns this model a new set of choiceLabels, giving each state a label with the stateId
+		 * @return void
+		 */
+		virtual void setStateIdBasedChoiceLabeling() override {
+			std::vector<std::list<uint_fast64_t>> newChoiceLabeling;
+
+			size_t stateCount = this->getNumberOfStates();
+			newChoiceLabeling.resize(stateCount);
+
+			for (size_t state = 0; state < stateCount; ++state) {
+				newChoiceLabeling.at(state).push_back(state);
+			}
+
+			this->choiceLabeling.reset(newChoiceLabeling);
+		}
 };
 
 } // namespace models

src/models/AbstractModel.h

@@ -443,6 +443,11 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
 			return result;
 		}
 
+		/*!
+		 * Assigns this model a new set of choiceLabels, giving each choice the stateId
+		 * @return void
+		 */
+		virtual void setStateIdBasedChoiceLabeling() = 0;
 protected:
         /*!
          * Exports the model to the dot-format and prints the result to the given stream.
@@ -523,6 +528,8 @@ protected:
 		/*! A matrix representing the likelihoods of moving between states. */
 		storm::storage::SparseMatrix<T> transitionMatrix;
 
+		/*! The labeling that is associated with the choices for each state. */
+        boost::optional<std::vector<std::list<uint_fast64_t>>> choiceLabeling;
 private:
 		/*! The labeling of the states of the model. */
 		storm::models::AtomicPropositionsLabeling stateLabeling;
@@ -532,9 +539,6 @@ private:
 
 		/*! The transition-based rewards of the model. */
 		boost::optional<storm::storage::SparseMatrix<T>> transitionRewardMatrix;
-    
-        /*! The labeling that is associated with the choices for each state. */
-        boost::optional<std::vector<std::list<uint_fast64_t>>> choiceLabeling;
 };
 
 } // namespace models

src/models/AbstractNondeterministicModel.h

@@ -219,7 +219,26 @@ class AbstractNondeterministicModel: public AbstractModel<T> {
                 outStream << "}" << std::endl;
             }
         }
-    
+		
+		/*!
+		 * Assigns this model a new set of choiceLabels, giving each choice a label with the stateId
+		 * @return void
+		 */
+		virtual void setStateIdBasedChoiceLabeling() override {
+			std::vector<std::list<uint_fast64_t>> newChoiceLabeling;
+
+			size_t stateCount = this->getNumberOfStates();
+			size_t choiceCount = this->getNumberOfChoices();
+			newChoiceLabeling.resize(choiceCount);
+
+			for (size_t state = 0; state < stateCount; ++state) {
+				for (size_t choice = this->nondeterministicChoiceIndices.at(state); choice < this->nondeterministicChoiceIndices.at(state + 1); ++choice) {
+					newChoiceLabeling.at(choice).push_back(state);
+				}
+			}
+
+			this->choiceLabeling.reset(newChoiceLabeling);
+		}
 	private:
 		/*! A vector of indices mapping states to the choices (rows) in the transition matrix. */
 		std::vector<uint_fast64_t> nondeterministicChoiceIndices;