diff --git a/src/storm/builder/ChoiceInformationBuilder.cpp b/src/storm/builder/ChoiceInformationBuilder.cpp index b51c68b15..53d61c2f9 100644 --- a/src/storm/builder/ChoiceInformationBuilder.cpp +++ b/src/storm/builder/ChoiceInformationBuilder.cpp @@ -16,13 +16,17 @@ namespace storm { dataOfOrigins.push_back(originData); } - storm::models::sparse::ChoiceLabeling ChoiceInformationBuilder::buildChoiceLabeling(uint_fast64_t totalNumberOfChoices) { - storm::models::sparse::ChoiceLabeling result(totalNumberOfChoices); - for (auto& label : labels) { - label.second.resize(totalNumberOfChoices, false); - result.addLabel(label.first, std::move(label.second)); + boost::optional 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); + result.addLabel(label.first, std::move(label.second)); + } + return result; } - return result; } std::vector ChoiceInformationBuilder::buildDataOfChoiceOrigins(uint_fast64_t totalNumberOfChoices) { diff --git a/src/storm/builder/ChoiceInformationBuilder.h b/src/storm/builder/ChoiceInformationBuilder.h index ca29e3fe1..1f9445330 100644 --- a/src/storm/builder/ChoiceInformationBuilder.h +++ b/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 buildChoiceLabeling(uint_fast64_t totalNumberOfChoices); std::vector buildDataOfChoiceOrigins(uint_fast64_t totalNumberOfChoices); diff --git a/src/storm/builder/ExplicitModelBuilder.cpp b/src/storm/builder/ExplicitModelBuilder.cpp index 02d286dd4..b932b86ef 100644 --- a/src/storm/builder/ExplicitModelBuilder.cpp +++ b/src/storm/builder/ExplicitModelBuilder.cpp @@ -74,16 +74,16 @@ namespace storm { std::shared_ptr> resultModel; switch (generator->getModelType()) { case storm::generator::ModelType::DTMC: - resultModel = std::shared_ptr>(new storm::models::sparse::Dtmc(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.rewardModels) )); //, std::move(modelComponents.choiceLabeling))); + resultModel = std::shared_ptr>(new storm::models::sparse::Dtmc(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>(new storm::models::sparse::Ctmc(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.rewardModels) )); //, std::move(modelComponents.choiceLabeling))); + resultModel = std::shared_ptr>(new storm::models::sparse::Ctmc(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>(new storm::models::sparse::Mdp(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.rewardModels) )); //, std::move(modelComponents.choiceLabeling))); + resultModel = std::shared_ptr>(new storm::models::sparse::Mdp(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>(new storm::models::sparse::MarkovAutomaton(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), *std::move(modelComponents.markovianStates), std::move(modelComponents.rewardModels) )); //, std::move(modelComponents.choiceLabeling))); + resultModel = std::shared_ptr>(new storm::models::sparse::MarkovAutomaton(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."); diff --git a/src/storm/builder/ExplicitModelBuilder.h b/src/storm/builder/ExplicitModelBuilder.h index d1cea0e7e..9e540b32c 100644 --- a/src/storm/builder/ExplicitModelBuilder.h +++ b/src/storm/builder/ExplicitModelBuilder.h @@ -65,7 +65,7 @@ namespace storm { std::unordered_map> rewardModels; // A vector that stores a labeling for each choice. - storm::models::sparse::ChoiceLabeling choiceLabeling; + boost::optional choiceLabeling; // A vector that stores which states are markovian. boost::optional markovianStates; diff --git a/src/storm/cli/entrypoints.h b/src/storm/cli/entrypoints.h index 8f51a69a5..028d6b466 100644 --- a/src/storm/cli/entrypoints.h +++ b/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> sparseModel = markovModel->template as>(); diff --git a/src/storm/models/sparse/ItemLabeling.cpp b/src/storm/models/sparse/ItemLabeling.cpp index be049bf84..eba424a70 100644 --- a/src/storm/models/sparse/ItemLabeling.cpp +++ b/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; } diff --git a/src/storm/models/sparse/Model.cpp b/src/storm/models/sparse/Model.cpp index de16edab1..85ada28b6 100644 --- a/src/storm/models/sparse/Model.cpp +++ b/src/storm/models/sparse/Model.cpp @@ -206,11 +206,13 @@ namespace storm { template void Model::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; } diff --git a/src/storm/models/sparse/StateLabeling.cpp b/src/storm/models/sparse/StateLabeling.cpp index a0efebdc2..ef0315669 100644 --- a/src/storm/models/sparse/StateLabeling.cpp +++ b/src/storm/models/sparse/StateLabeling.cpp @@ -18,7 +18,6 @@ namespace storm { StateLabeling::StateLabeling(ItemLabeling const&& itemLab) : ItemLabeling(itemLab) { // Intentionally left empty. } - bool StateLabeling::operator==(StateLabeling const& other) const { if (itemCount != other.itemCount) { @@ -37,19 +36,14 @@ namespace storm { } return true; } - - StateLabeling StateLabeling::getSubLabeling(storm::storage::BitVector const& states) const { return StateLabeling(ItemLabeling::getSubLabeling(states)); } - - std::set 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); @@ -58,7 +52,6 @@ namespace storm { bool StateLabeling::getStateHasLabel(std::string const& label, storm::storage::sparse::state_type state) const { 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; } diff --git a/src/storm/storage/BitVector.cpp b/src/storm/storage/BitVector.cpp index 532e923e3..5933aac6f 100644 --- a/src/storm/storage/BitVector.cpp +++ b/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; }