From 3430a663355f110e52f7a82f869bb5fc51111820 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Fri, 10 Mar 2017 16:37:08 +0100
Subject: [PATCH] fix for command line invokation of PLA

---
 src/storm/utility/storm.h | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

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<typename storm::storage::ParameterRegion<storm::RationalFunction>::CoefficientType>(storm::settings::getModule<storm::settings::modules::CoreSettings>().getParameterLiftingThreshold());
         std::vector<std::pair<storm::storage::ParameterRegion<storm::RationalFunction>, storm::modelchecker::parametric::RegionCheckResult>> result;
         
-        std::cout << "Performing parameter lifting for property " << formula << " on initial region " << initialRegion.toString(true) << " with refinementThreshold " << storm::utility::convertNumber<double>(refinementThreshold) << " ...";
+        std::cout << "Performing parameter lifting for property " << *formula << " on initial region " << initialRegion.toString(true) << " with refinementThreshold " << storm::utility::convertNumber<double>(refinementThreshold) << " ...";
         std::cout.flush();
         
+        storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction> task(*formula, true);
         
         if (markovModel->isOfType(storm::models::ModelType::Dtmc)) {
             storm::modelchecker::parametric::ParameterLifting <storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*markovModel->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>());
-            parameterLiftingContext.specifyFormula(*formula);
+            parameterLiftingContext.specifyFormula(task);
             result = parameterLiftingContext.performRegionRefinement(initialRegion, refinementThreshold);
         } else if (markovModel->isOfType(storm::models::ModelType::Mdp)) {
             storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double> parameterLiftingContext(*markovModel->template as<storm::models::sparse::Mdp<storm::RationalFunction>>());
-            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.");