diff --git a/src/models/symbolic/Model.h b/src/models/symbolic/Model.h index 3b8804ebe..085c5075f 100644 --- a/src/models/symbolic/Model.h +++ b/src/models/symbolic/Model.h @@ -43,9 +43,11 @@ namespace storm { /*! * Base class for all symbolic models. */ - template + template class Model : public storm::models::ModelBase { public: + typedef CValueType ValueType; + static const storm::dd::DdType DdType = Type; typedef StandardRewardModel RewardModelType; diff --git a/src/utility/storm.h b/src/utility/storm.h index fb96b7420..701caa634 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -85,7 +85,6 @@ namespace storm { std::vector> parseFormulasForProgram(std::string const& inputString, storm::prism::Program const& program); - template storm::storage::ModelFormulasPair buildSymbolicModel(storm::prism::Program const& program, std::vector> const& formulas) { storm::storage::ModelFormulasPair result; @@ -169,8 +168,10 @@ namespace storm { return model; } - template, ModelType>::value, bool>::type = 0> - std::shared_ptr performBisimulationMinimization(std::shared_ptr model, std::vector> const& formulas, storm::storage::BisimulationType type) { + template + std::shared_ptr> performBisimulationMinimization(std::shared_ptr> model, std::vector> const& formulas, storm::storage::BisimulationType type) { + using ValueType = typename ModelType::ValueType; + STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Dtmc) || model->isOfType(storm::models::ModelType::Ctmc) || model->isOfType(storm::models::ModelType::Mdp), storm::exceptions::InvalidSettingsException, "Bisimulation minimization is currently only available for DTMCs, CTMCs and MDPs."); model->reduceToStateBasedRewards(); @@ -183,25 +184,27 @@ namespace storm { } } - template, ModelType>::value, bool>::type = 0> - std::shared_ptr preprocessModel(std::shared_ptr model, std::vector> const& formulas) { - if (storm::settings::generalSettings().isBisimulationSet()) { + template + std::shared_ptr> performBisimulationMinimization(std::shared_ptr> model, std::shared_ptr const& formula, storm::storage::BisimulationType type) { + return performBisimulationMinimization(model, {formula}, type); + } + + + + template + std::shared_ptr preprocessModel(std::shared_ptr model, std::vector> const& formulas) { + if (model->isSparseModel() && storm::settings::generalSettings().isBisimulationSet()) { storm::storage::BisimulationType bisimType = storm::storage::BisimulationType::Strong; if (storm::settings::bisimulationSettings().isWeakBisimulationSet()) { bisimType = storm::storage::BisimulationType::Weak; } STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::InvalidSettingsException, "Bisimulation minimization is currently only available for sparse models."); - return performBisimulationMinimization(model, formulas, bisimType); + return performBisimulationMinimization(model->template as>(), formulas, bisimType); } return model; } - template, ModelType >::value, bool>::type = 0> - std::shared_ptr preprocessModel(std::shared_ptr model, std::vector> const& formulas) { - // No preprocessing available yet. - return model; - } template void generateCounterexample(storm::prism::Program const& program, std::shared_ptr> model, std::shared_ptr const& formula) {