From dfd1fec8c591b8e7e85fc0e2268046aa7ef71920 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Tue, 29 Jan 2019 20:46:27 +0100
Subject: [PATCH] Fixed compile issues

---
 src/storm-pars-cli/storm-pars.cpp |  2 +-
 src/storm-pars/api/region.h       |  4 ++--
 src/storm/api/transformation.h    | 10 +++++-----
 3 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp
index 4495f26c1..bf3ac8f38 100644
--- a/src/storm-pars-cli/storm-pars.cpp
+++ b/src/storm-pars-cli/storm-pars.cpp
@@ -145,7 +145,7 @@ namespace storm {
             }
             
             if (parametricSettings.transformContinuousModel() && (result.first->isOfType(storm::models::ModelType::Ctmc) || result.first->isOfType(storm::models::ModelType::MarkovAutomaton))) {
-                result.first = storm::api::transformContinuousToDiscreteTimeSparseModel(std::move(*result.first->template as<storm::models::sparse::Model<ValueType>>()), storm::api::extractFormulasFromProperties(input.properties));
+                result.first = storm::api::transformContinuousToDiscreteTimeSparseModel(std::move(*result.first->template as<storm::models::sparse::Model<ValueType>>()), storm::api::extractFormulasFromProperties(input.properties)).first;
                 result.second = true;
             }
             
diff --git a/src/storm-pars/api/region.h b/src/storm-pars/api/region.h
index ee8d44bff..c032426e5 100644
--- a/src/storm-pars/api/region.h
+++ b/src/storm-pars/api/region.h
@@ -91,7 +91,7 @@ namespace storm {
             if (consideredModel->isOfType(storm::models::ModelType::Ctmc) || consideredModel->isOfType(storm::models::ModelType::MarkovAutomaton)) {
                     STORM_LOG_WARN("Parameter lifting not supported for continuous time models. Transforming continuous model to discrete model...");
                     std::vector<std::shared_ptr<storm::logic::Formula const>> taskFormulaAsVector { task.getFormula().asSharedPointer() };
-                    consideredModel = storm::api::transformContinuousToDiscreteTimeSparseModel(consideredModel, taskFormulaAsVector);
+                    consideredModel = storm::api::transformContinuousToDiscreteTimeSparseModel(consideredModel, taskFormulaAsVector).first;
                     STORM_LOG_THROW(consideredModel->isOfType(storm::models::ModelType::Dtmc) || consideredModel->isOfType(storm::models::ModelType::Mdp), storm::exceptions::UnexpectedException, "Transformation to discrete time model has failed.");
             }
             
@@ -121,7 +121,7 @@ namespace storm {
             if (consideredModel->isOfType(storm::models::ModelType::Ctmc) || consideredModel->isOfType(storm::models::ModelType::MarkovAutomaton)) {
                     STORM_LOG_WARN("Parameter lifting not supported for continuous time models. Transforming continuous model to discrete model...");
                     std::vector<std::shared_ptr<storm::logic::Formula const>> taskFormulaAsVector { task.getFormula().asSharedPointer() };
-                    consideredModel = storm::api::transformContinuousToDiscreteTimeSparseModel(consideredModel, taskFormulaAsVector);
+                    consideredModel = storm::api::transformContinuousToDiscreteTimeSparseModel(consideredModel, taskFormulaAsVector).first;
                     STORM_LOG_THROW(consideredModel->isOfType(storm::models::ModelType::Dtmc) || consideredModel->isOfType(storm::models::ModelType::Mdp), storm::exceptions::UnexpectedException, "Transformation to discrete time model has failed.");
             }
             
diff --git a/src/storm/api/transformation.h b/src/storm/api/transformation.h
index 4c51e1fa4..d2a84d9f7 100644
--- a/src/storm/api/transformation.h
+++ b/src/storm/api/transformation.h
@@ -24,7 +24,7 @@ namespace storm {
             while(model->hasRewardModel(timeRewardName)) {
                 timeRewardName += "_";
             }
-            auto newFormulas = transformer.checkAndTransformFormulas(formulas, timeRewardName)
+            auto newFormulas = transformer.checkAndTransformFormulas(formulas, timeRewardName);
             STORM_LOG_WARN_COND(newFormulas.size() == formulas.size(), "Transformation of a " << model->getType() << " to a discrete time model does not preserve all properties.");
             
             if (model->isOfType(storm::models::ModelType::Ctmc)) {
@@ -34,7 +34,7 @@ namespace storm {
             } else {
                 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Transformation of a " << model->getType() << " to a discrete time model is not supported");
             }
-            return nullptr;
+            return std::make_pair(nullptr, newFormulas);;
         }
 
         /*!
@@ -51,8 +51,8 @@ namespace storm {
             while(model.hasRewardModel(timeRewardName)) {
                 timeRewardName += "_";
             }
-            auto newFormulas = transformer.checkAndTransformFormulas(formulas, timeRewardName)
-            STORM_LOG_WARN_COND(newFormulas.size() == formulas.size(), "Transformation of a " << model->getType() << " to a discrete time model does not preserve all properties.");
+            auto newFormulas = transformer.checkAndTransformFormulas(formulas, timeRewardName);
+            STORM_LOG_WARN_COND(newFormulas.size() == formulas.size(), "Transformation of a " << model.getType() << " to a discrete time model does not preserve all properties.");
            
             if (model.isOfType(storm::models::ModelType::Ctmc)) {
                 return std::make_pair(transformer.transform(std::move(*model.template as<storm::models::sparse::Ctmc<ValueType>>())), newFormulas);
@@ -61,7 +61,7 @@ namespace storm {
             } else {
                 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Transformation of a " << model.getType() << " to a discrete time model is not supported.");
             }
-            return nullptr;
+            return std::make_pair(nullptr, newFormulas);;
             
         }