diff --git a/src/models/symbolic/Model.h b/src/models/symbolic/Model.h index b70c39b97..4dc6ff31e 100644 --- a/src/models/symbolic/Model.h +++ b/src/models/symbolic/Model.h @@ -38,6 +38,7 @@ namespace storm { template class Model : public storm::models::ModelBase { public: + static const storm::dd::DdType DdType = Type; typedef StandardRewardModel RewardModelType; Model(Model const& other) = default; diff --git a/src/storage/bisimulation/BisimulationDecomposition.cpp b/src/storage/bisimulation/BisimulationDecomposition.cpp index ba35bc455..120f88f88 100644 --- a/src/storage/bisimulation/BisimulationDecomposition.cpp +++ b/src/storage/bisimulation/BisimulationDecomposition.cpp @@ -276,9 +276,11 @@ namespace storm { } template class BisimulationDecomposition>; + template class BisimulationDecomposition>; #ifdef STORM_HAVE_CARL template class BisimulationDecomposition>; + template class BisimulationDecomposition>; #endif } } diff --git a/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp b/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp index c30058475..9a739cea3 100644 --- a/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp +++ b/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp @@ -364,9 +364,11 @@ namespace storm { } template class DeterministicModelBisimulationDecomposition>; + template class DeterministicModelBisimulationDecomposition>; #ifdef STORM_HAVE_CARL template class DeterministicModelBisimulationDecomposition>; + template class DeterministicModelBisimulationDecomposition>; #endif } } diff --git a/src/utility/storm.h b/src/utility/storm.h index 38e78f364..2eea34738 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -112,34 +112,50 @@ namespace storm { return result; } - - template - std::shared_ptr preprocessModel(std::shared_ptr model, std::vector> const& formulas) { + + template + std::shared_ptr performSparseBisimulationMinimization(std::shared_ptr model, std::vector> const& formulas) { + std::cout << "Performing bisimulation minimization... "; + typename storm::storage::DeterministicModelBisimulationDecomposition::Options options; + if (!formulas.empty()) { + options = typename storm::storage::DeterministicModelBisimulationDecomposition::Options(*model, formulas); + } + if (storm::settings::bisimulationSettings().isWeakBisimulationSet()) { + options.type = storm::storage::BisimulationType::Weak; + options.bounded = false; + } + + storm::storage::DeterministicModelBisimulationDecomposition bisimulationDecomposition(*model, options); + model = bisimulationDecomposition.getQuotient(); + std::cout << "done." << std::endl << std::endl; + return model; + } + + template, ModelType>::value, bool>::type = 0> + std::shared_ptr preprocessModel(std::shared_ptr model, std::vector> const& formulas) { if (storm::settings::generalSettings().isBisimulationSet()) { + STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::InvalidSettingsException, "Bisimulation minimization is currently only available for sparse models."); - std::shared_ptr> sparseModel = model->template as>(); - STORM_LOG_THROW(model->getType() == storm::models::ModelType::Dtmc || model->getType() == storm::models::ModelType::Ctmc, storm::exceptions::InvalidSettingsException, "Bisimulation minimization is currently only available for DTMCs."); - std::shared_ptr> dtmc = sparseModel->template as>(); + STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Dtmc) || model->isOfType(storm::models::ModelType::Ctmc), storm::exceptions::InvalidSettingsException, "Bisimulation minimization is currently only available for DTMCs and CTMCs."); - dtmc->reduceToStateBasedRewards(); + model->reduceToStateBasedRewards(); - std::cout << "Performing bisimulation minimization... "; - typename storm::storage::DeterministicModelBisimulationDecomposition::Options options; - if (!formulas.empty()) { - options = typename storm::storage::DeterministicModelBisimulationDecomposition::Options(*sparseModel, formulas); - } - if (storm::settings::bisimulationSettings().isWeakBisimulationSet()) { - options.type = storm::storage::BisimulationType::Weak; - options.bounded = false; + if (model->isOfType(storm::models::ModelType::Dtmc)) { + return performSparseBisimulationMinimization>(model->template as>(), formulas); + } else { + return performSparseBisimulationMinimization>(model->template as>(), formulas); } - - storm::storage::DeterministicModelBisimulationDecomposition bisimulationDecomposition(*dtmc, options); - model = bisimulationDecomposition.getQuotient(); - std::cout << "done." << std::endl << std::endl; + } 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) { if (storm::settings::counterexampleGeneratorSettings().isMinimalCommandSetGenerationSet()) {