From 3483e794127c4a7ff9f1dee53b0b13a320889f02 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Sun, 5 Mar 2017 19:59:35 +0100
Subject: [PATCH] Parse parameters in JSON

---
 src/storm-dft/parser/DFTGalileoParser.cpp |  1 -
 src/storm-dft/parser/DFTJsonParser.cpp    | 15 +++++++++++----
 2 files changed, 11 insertions(+), 5 deletions(-)

diff --git a/src/storm-dft/parser/DFTGalileoParser.cpp b/src/storm-dft/parser/DFTGalileoParser.cpp
index c5a88716c..38dec9bf0 100644
--- a/src/storm-dft/parser/DFTGalileoParser.cpp
+++ b/src/storm-dft/parser/DFTGalileoParser.cpp
@@ -5,7 +5,6 @@
 #include <boost/algorithm/string.hpp>
 #include <boost/lexical_cast.hpp>
 #include <boost/algorithm/string/replace.hpp>
-#include "storm/storage/expressions/ExpressionManager.h"
 #include "storm/exceptions/NotImplementedException.h"
 #include "storm/exceptions/FileIoException.h"
 #include "storm/exceptions/NotSupportedException.h"
diff --git a/src/storm-dft/parser/DFTJsonParser.cpp b/src/storm-dft/parser/DFTJsonParser.cpp
index 07454416f..83710b482 100644
--- a/src/storm-dft/parser/DFTJsonParser.cpp
+++ b/src/storm-dft/parser/DFTJsonParser.cpp
@@ -5,7 +5,6 @@
 #include <boost/algorithm/string.hpp>
 #include <boost/lexical_cast.hpp>
 #include <boost/algorithm/string/replace.hpp>
-#include "storm/storage/expressions/ExpressionManager.h"
 #include "storm/exceptions/NotImplementedException.h"
 #include "storm/exceptions/FileIoException.h"
 #include "storm/exceptions/NotSupportedException.h"
@@ -42,9 +41,17 @@ namespace storm {
             parsedJson << file;
             storm::utility::closeFile(file);
 
-            storm::expressions::Variable var = manager->declareRationalVariable("x");
-            identifierMapping.emplace(var.getName(), var);
-            parser.setIdentifierMapping(identifierMapping);
+            json parameters = parsedJson.at("parameters");
+#ifdef STORM_HAVE_CARL
+            STORM_LOG_THROW((std::is_same<ValueType, storm::RationalFunction>::value), storm::exceptions::NotSupportedException, "Parameters only allowed when using rational functions.");
+            for (auto it = parameters.begin(); it != parameters.end(); ++it) {
+                std::string parameter = it.key();
+                storm::expressions::Variable var = manager->declareRationalVariable(parameter);
+                identifierMapping.emplace(var.getName(), var);
+                parser.setIdentifierMapping(identifierMapping);
+                STORM_LOG_TRACE("Added parameter: " << var.getName());
+            }
+#endif
 
             json nodes = parsedJson.at("nodes");