diff --git a/src/storm-pars/api/region.h b/src/storm-pars/api/region.h index 043f461b0..a8cc6bbe2 100644 --- a/src/storm-pars/api/region.h +++ b/src/storm-pars/api/region.h @@ -78,7 +78,7 @@ namespace storm { } template - std::unique_ptr> initializeParameterLiftingRegionModelChecker(std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task) { + std::shared_ptr> initializeParameterLiftingRegionModelChecker(std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task) { STORM_LOG_WARN_COND(storm::utility::parameterlifting::validateParameterLiftingSound(*model, task.getFormula()), "Could not validate whether parameter lifting is applicable. Please validate manually..."); @@ -93,22 +93,22 @@ namespace storm { } // Obtain the region model checker - std::unique_ptr> result; + std::shared_ptr> checker; if (consideredModel->isOfType(storm::models::ModelType::Dtmc)) { - result = std::make_unique, ConstantType>>(); + checker = std::make_shared, ConstantType>>(); } else if (consideredModel->isOfType(storm::models::ModelType::Mdp)) { - result = std::make_unique, ConstantType>>(); + checker = std::make_shared, ConstantType>>(); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform parameterLifting on the provided model type."); } - result->specify(consideredModel, task); + checker->specify(consideredModel, task); - return result; + return checker; } template - std::unique_ptr> initializeValidatingRegionModelChecker(std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task) { + std::shared_ptr> initializeValidatingRegionModelChecker(std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task) { STORM_LOG_WARN_COND(storm::utility::parameterlifting::validateParameterLiftingSound(*model, task.getFormula()), "Could not validate whether parameter lifting is applicable. Please validate manually..."); @@ -123,22 +123,22 @@ namespace storm { } // Obtain the region model checker - std::unique_ptr> result; + std::shared_ptr> checker; if (consideredModel->isOfType(storm::models::ModelType::Dtmc)) { - result = std::make_unique, ImpreciseType, PreciseType>>(); + checker = std::make_shared, ImpreciseType, PreciseType>>(); } else if (consideredModel->isOfType(storm::models::ModelType::Mdp)) { - result = std::make_unique, ImpreciseType, PreciseType>>(); + checker = std::make_shared, ImpreciseType, PreciseType>>(); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform parameterLifting on the provided model type."); } - result->specify(consideredModel, task); + checker->specify(consideredModel, task); - return result; + return checker; } template - std::unique_ptr> initializeRegionModelChecker(std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task, storm::modelchecker::RegionCheckEngine engine) { + std::shared_ptr> initializeRegionModelChecker(std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task, storm::modelchecker::RegionCheckEngine engine) { switch (engine) { case storm::modelchecker::RegionCheckEngine::ParameterLifting: return initializeParameterLiftingRegionModelChecker(model, task);