diff --git a/src/storm/builder/ExplicitModelBuilder.cpp b/src/storm/builder/ExplicitModelBuilder.cpp index 8fedf075b..2b120f8ac 100644 --- a/src/storm/builder/ExplicitModelBuilder.cpp +++ b/src/storm/builder/ExplicitModelBuilder.cpp @@ -80,22 +80,24 @@ namespace storm { return storm::utility::builder::buildModelFromComponents(storm::models::ModelType::Pomdp, buildModelComponents()); case storm::generator::ModelType::MA: return storm::utility::builder::buildModelFromComponents(storm::models::ModelType::MarkovAutomaton, buildModelComponents()); + case storm::generator::ModelType::SMG: + return storm::utility::builder::buildModelFromComponents(storm::models::ModelType::Smg, buildModelComponents()); default: STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error while creating model: cannot handle this model type."); } - + return nullptr; } - + template StateType ExplicitModelBuilder::getOrAddStateIndex(CompressedState const& state) { StateType newIndex = static_cast(stateStorage.getNumberOfStates()); - + // Check, if the state was already registered. std::pair actualIndexBucketPair = stateStorage.stateToId.findOrAddAndGetBucket(state, newIndex); - + StateType actualIndex = actualIndexBucketPair.first; - + if (actualIndex == newIndex) { if (options.explorationOrder == ExplorationOrder::Dfs) { statesToExplore.emplace_front(state, actualIndex); diff --git a/src/storm/models/ModelType.cpp b/src/storm/models/ModelType.cpp index d556448bb..1e89ec163 100644 --- a/src/storm/models/ModelType.cpp +++ b/src/storm/models/ModelType.cpp @@ -19,6 +19,8 @@ namespace storm { return ModelType::S2pg; } else if (type == "POMDP") { return ModelType::Pomdp; + } else if (type == "SMG") { + return ModelType::Smg; } else { STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Type " << type << "not known."); } @@ -44,6 +46,9 @@ namespace storm { case ModelType::Pomdp: os << "POMDP"; break; + case ModelType::Smg: + os << "Smg"; + break; default: STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Unknown model type."); } diff --git a/src/storm/models/ModelType.h b/src/storm/models/ModelType.h index b183a598d..d9d7b0dc8 100644 --- a/src/storm/models/ModelType.h +++ b/src/storm/models/ModelType.h @@ -7,11 +7,11 @@ namespace storm { namespace models { // All supported model types. enum class ModelType { - Dtmc, Ctmc, Mdp, MarkovAutomaton, S2pg, Pomdp + Dtmc, Ctmc, Mdp, MarkovAutomaton, S2pg, Pomdp, Smg }; ModelType getModelType(std::string const& type); - + std::ostream& operator<<(std::ostream& os, ModelType const& type); } } diff --git a/src/storm/utility/builder.cpp b/src/storm/utility/builder.cpp index 481ed8020..0caa0edb3 100644 --- a/src/storm/utility/builder.cpp +++ b/src/storm/utility/builder.cpp @@ -6,13 +6,14 @@ #include "storm/models/sparse/Mdp.h" #include "storm/models/sparse/Pomdp.h" #include "storm/models/sparse/MarkovAutomaton.h" +#include "storm/models/sparse/Smg.h" #include "storm/exceptions/InvalidModelException.h" namespace storm { namespace utility { namespace builder { - + template std::shared_ptr> buildModelFromComponents(storm::models::ModelType modelType, storm::storage::sparse::ModelComponents&& components) { switch (modelType) { @@ -28,10 +29,12 @@ namespace storm { return std::make_shared>(std::move(components)); case storm::models::ModelType::S2pg: return std::make_shared>(std::move(components)); + case storm::models::ModelType::Smg: + return std::make_shared>(std::move(components)); } STORM_LOG_THROW(false, storm::exceptions::InvalidModelException, "Unknown model type"); } - + template std::shared_ptr> buildModelFromComponents(storm::models::ModelType modelType, storm::storage::sparse::ModelComponents&& components); template std::shared_ptr>> buildModelFromComponents(storm::models::ModelType modelType, storm::storage::sparse::ModelComponents>&& components); template std::shared_ptr> buildModelFromComponents(storm::models::ModelType modelType, storm::storage::sparse::ModelComponents&& components);