diff --git a/src/storm/utility/storm.h b/src/storm/utility/storm.h index efdb6d03a..d2ff2e97c 100644 --- a/src/storm/utility/storm.h +++ b/src/storm/utility/storm.h @@ -324,17 +324,18 @@ namespace storm { auto refinementThreshold = storm::utility::convertNumber::CoefficientType>(storm::settings::getModule().getParameterLiftingThreshold()); std::vector, storm::modelchecker::parametric::RegionCheckResult>> result; - std::cout << "Performing parameter lifting for property " << formula << " on initial region " << initialRegion.toString(true) << " with refinementThreshold " << storm::utility::convertNumber(refinementThreshold) << " ..."; + std::cout << "Performing parameter lifting for property " << *formula << " on initial region " << initialRegion.toString(true) << " with refinementThreshold " << storm::utility::convertNumber(refinementThreshold) << " ..."; std::cout.flush(); + storm::modelchecker::CheckTask task(*formula, true); if (markovModel->isOfType(storm::models::ModelType::Dtmc)) { storm::modelchecker::parametric::ParameterLifting , double> parameterLiftingContext(*markovModel->template as>()); - parameterLiftingContext.specifyFormula(*formula); + parameterLiftingContext.specifyFormula(task); result = parameterLiftingContext.performRegionRefinement(initialRegion, refinementThreshold); } else if (markovModel->isOfType(storm::models::ModelType::Mdp)) { storm::modelchecker::parametric::ParameterLifting, double> parameterLiftingContext(*markovModel->template as>()); - parameterLiftingContext.specifyFormula(*formula); + parameterLiftingContext.specifyFormula(task); result = parameterLiftingContext.performRegionRefinement(initialRegion, refinementThreshold); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unable to perform parameterLifting on the provided model type.");