fixed several minor bugs regarding the choicelabeling

src/storm/builder/ChoiceInformationBuilder.cpp

@@ -16,7 +16,10 @@ namespace storm {
             dataOfOrigins.push_back(originData);
         }
         
-        storm::models::sparse::ChoiceLabeling ChoiceInformationBuilder::buildChoiceLabeling(uint_fast64_t totalNumberOfChoices) {
+        boost::optional<storm::models::sparse::ChoiceLabeling> ChoiceInformationBuilder::buildChoiceLabeling(uint_fast64_t totalNumberOfChoices) {
+            if (labels.empty()) {
+                return boost::none;
+            } else {
                 storm::models::sparse::ChoiceLabeling result(totalNumberOfChoices);
                 for (auto& label : labels) {
                     label.second.resize(totalNumberOfChoices, false);
@@ -24,6 +27,7 @@ namespace storm {
                 }
                 return result;
             }
+        }
             
         std::vector<boost::any> ChoiceInformationBuilder::buildDataOfChoiceOrigins(uint_fast64_t totalNumberOfChoices) {
             dataOfOrigins.resize(totalNumberOfChoices);

src/storm/builder/ChoiceInformationBuilder.h

@@ -27,7 +27,7 @@ namespace storm {
             
             void addOriginData(boost::any const& originData, uint_fast64_t choiceIndex);
             
-            storm::models::sparse::ChoiceLabeling buildChoiceLabeling(uint_fast64_t totalNumberOfChoices);
+            boost::optional<storm::models::sparse::ChoiceLabeling> buildChoiceLabeling(uint_fast64_t totalNumberOfChoices);
             
             std::vector<boost::any> buildDataOfChoiceOrigins(uint_fast64_t totalNumberOfChoices);
             

src/storm/builder/ExplicitModelBuilder.cpp

@@ -74,16 +74,16 @@ namespace storm {
             std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> resultModel;
             switch (generator->getModelType()) {
                 case storm::generator::ModelType::DTMC:
-                    resultModel = std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>>(new storm::models::sparse::Dtmc<ValueType, RewardModelType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.rewardModels)    )); //, std::move(modelComponents.choiceLabeling)));
+                    resultModel = std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>>(new storm::models::sparse::Dtmc<ValueType, RewardModelType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.rewardModels), std::move(modelComponents.choiceLabeling)));
                     break;
                 case storm::generator::ModelType::CTMC:
-                    resultModel = std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>>(new storm::models::sparse::Ctmc<ValueType, RewardModelType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.rewardModels)    )); //, std::move(modelComponents.choiceLabeling)));
+                    resultModel = std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>>(new storm::models::sparse::Ctmc<ValueType, RewardModelType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.rewardModels), std::move(modelComponents.choiceLabeling)));
                     break;
                 case storm::generator::ModelType::MDP:
-                    resultModel = std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>>(new storm::models::sparse::Mdp<ValueType, RewardModelType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.rewardModels)    )); //, std::move(modelComponents.choiceLabeling)));
+                    resultModel = std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>>(new storm::models::sparse::Mdp<ValueType, RewardModelType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.rewardModels), std::move(modelComponents.choiceLabeling)));
                     break;
                 case storm::generator::ModelType::MA:
-                    resultModel = std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>>(new storm::models::sparse::MarkovAutomaton<ValueType, RewardModelType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), *std::move(modelComponents.markovianStates), std::move(modelComponents.rewardModels)    )); //, std::move(modelComponents.choiceLabeling)));
+                    resultModel = std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>>(new storm::models::sparse::MarkovAutomaton<ValueType, RewardModelType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), *std::move(modelComponents.markovianStates), std::move(modelComponents.rewardModels), std::move(modelComponents.choiceLabeling)));
                     break;
                 default:
                     STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error while creating model: cannot handle this model type.");

src/storm/builder/ExplicitModelBuilder.h

@@ -65,7 +65,7 @@ namespace storm {
                 std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<typename RewardModelType::ValueType>> rewardModels;
                 
                 // A vector that stores a labeling for each choice.
-                storm::models::sparse::ChoiceLabeling choiceLabeling;
+                boost::optional<storm::models::sparse::ChoiceLabeling> choiceLabeling;
                 
                 // A vector that stores which states are markovian.
                 boost::optional<storm::storage::BitVector> markovianStates;

src/storm/cli/entrypoints.h

@@ -325,7 +325,7 @@ namespace storm {
             markovModel->printModelInformationToStream(std::cout);
             
             // Preprocess the model.
-            STORM_LOG_WARN_COND(builderResult.hasStateValuations() || builderResult.hasChoiceOrigins(), "state valuations and choice origins might be invalidated if the model is preprocessed..."); // TODO: check this more carefully.
+            STORM_LOG_WARN_COND(!builderResult.hasStateValuations() && !builderResult.hasChoiceOrigins(), "State valuations and Choice origins might be invalidated if the model is preprocessed..."); // TODO: check this more carefully.
             BRANCH_ON_SPARSE_MODELTYPE(markovModel, markovModel, ValueType, preprocessModel, formulas);
             std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel = markovModel->template as<storm::models::sparse::Model<ValueType>>();
             

src/storm/models/sparse/ItemLabeling.cpp

@@ -121,7 +121,7 @@ namespace storm {
             }
 
             void ItemLabeling::printLabelingInformationToStream(std::ostream& out) const {
-                out << "Labels: \t" << this->getNumberOfLabels() << std::endl;
+                out << this->getNumberOfLabels() << " labels" << std::endl;
                 for (auto const& labelIndexPair : this->nameToLabelingIndexMap) {
                     out << "   * " << labelIndexPair.first << " -> " << this->labelings[labelIndexPair.second].getNumberOfSetBits() << " item(s)" << std::endl;
                 }

src/storm/models/sparse/Model.cpp

@@ -206,11 +206,13 @@ namespace storm {
             template<typename ValueType, typename RewardModelType>
             void Model<ValueType, RewardModelType>::printModelInformationFooterToStream(std::ostream& out) const {
                 this->printRewardModelsInformationToStream(out);
+                out << "State Labels: \t";
                 this->getStateLabeling().printLabelingInformationToStream(out);
+                out << "Choice Labels: \t";
                 if (this->hasChoiceLabeling()) {
                     this->getChoiceLabeling().printLabelingInformationToStream(out);
                 } else {
-                    out << "Choice Labels: \tnone";
+                    out << "none" << std::endl;
                 }
                 out << "-------------------------------------------------------------- " << std::endl;
             }

src/storm/models/sparse/StateLabeling.cpp

@@ -19,7 +19,6 @@ namespace storm {
                 // Intentionally left empty.
             }
             
-            
             bool StateLabeling::operator==(StateLabeling const& other) const {
                 if (itemCount != other.itemCount) {
                     return false;
@@ -38,19 +37,14 @@ namespace storm {
                 return true;
             }
             
-
-            
             StateLabeling StateLabeling::getSubLabeling(storm::storage::BitVector const& states) const {
                 return StateLabeling(ItemLabeling::getSubLabeling(states));
             }
             
-
-            
             std::set<std::string> StateLabeling::getLabelsOfState(storm::storage::sparse::state_type state) const {
                 return ItemLabeling::getLabelsOfItem(state);
             }
             
-            
             void StateLabeling::addLabelToState(std::string const& label, storm::storage::sparse::state_type state) {
                 return ItemLabeling::addLabelToItem(label, state);
             }
@@ -59,7 +53,6 @@ namespace storm {
                 return ItemLabeling::getItemHasLabel(label, state);
             }
             
-            
             storm::storage::BitVector const& StateLabeling::getStates(std::string const& label) const {
                 return ItemLabeling::getItems(label);
             }
@@ -74,7 +67,6 @@ namespace storm {
 
 
             std::ostream& operator<<(std::ostream& out, StateLabeling const& labeling) {
-                out << "State ";
                 labeling.printLabelingInformationToStream(out);
                 return out;
             }

src/storm/storage/BitVector.cpp

@@ -254,7 +254,9 @@ namespace storm {
         
         void BitVector::grow(uint_fast64_t minimumLength, bool init) {
             if (minimumLength > bitCount) {
-                uint_fast64_t newLength = bitCount;
+                // We double the bitcount as long as it is less then the minimum length.
+                uint_fast64_t newLength = std::max(64ull, bitCount);
+                // Note that newLength has to be initialized with a non-zero number.
                 while (newLength < minimumLength) {
                     newLength = newLength << 1;
                 }