From c2ea78b880a338c3a2408834830b39de1f9e2eb2 Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@rwth-aachen.de>
Date: Thu, 15 Dec 2016 00:54:24 +0100
Subject: [PATCH] no need anymore to create files from formulas if properties
 are present anyway

---
 src/storm/storage/jani/JSONExporter.cpp | 10 +++++-----
 src/storm/storage/jani/JSONExporter.h   |  8 +++++---
 src/storm/utility/storm.cpp             |  4 ++--
 3 files changed, 12 insertions(+), 10 deletions(-)

diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp
index 7548fd323..889496265 100644
--- a/src/storm/storage/jani/JSONExporter.cpp
+++ b/src/storm/storage/jani/JSONExporter.cpp
@@ -516,7 +516,7 @@ namespace storm {
         
         
         
-        void JsonExporter::toFile(storm::jani::Model const& janiModel, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, std::string const& filepath, bool checkValid) {
+        void JsonExporter::toFile(storm::jani::Model const& janiModel, std::vector<storm::jani::Property> const& formulas, std::string const& filepath, bool checkValid) {
             std::ofstream ofs;
             ofs.open (filepath, std::ofstream::out );
             if(ofs.is_open()) {
@@ -526,7 +526,7 @@ namespace storm {
             }
         }
         
-        void JsonExporter::toStream(storm::jani::Model const& janiModel,  std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, std::ostream& os, bool checkValid) {
+        void JsonExporter::toStream(storm::jani::Model const& janiModel,  std::vector<storm::jani::Property> const& formulas, std::ostream& os, bool checkValid) {
             if(checkValid) {
                 janiModel.checkValid();
             }
@@ -759,13 +759,13 @@ namespace storm {
         }
         
         
-        void JsonExporter::convertProperties( std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, storm::jani::Model const& model) {
+        void JsonExporter::convertProperties( std::vector<storm::jani::Property> const& formulas, storm::jani::Model const& model) {
             std::vector<modernjson::json> properties;
             uint64_t index = 0;
             for(auto const& f : formulas) {
                 modernjson::json propDecl;
-                propDecl["name"] = "prop" + std::to_string(index);
-                propDecl["expression"] = convertFilterExpression(storm::jani::FilterExpression(f), model);
+                propDecl["name"] = f.getName();
+                propDecl["expression"] = convertFilterExpression(f.getFilter(), model);
                 ++index;
                 properties.push_back(propDecl);
             }
diff --git a/src/storm/storage/jani/JSONExporter.h b/src/storm/storage/jani/JSONExporter.h
index 1008ec097..1eceb5d2e 100644
--- a/src/storm/storage/jani/JSONExporter.h
+++ b/src/storm/storage/jani/JSONExporter.h
@@ -4,6 +4,7 @@
 #include "storm/storage/expressions/ExpressionVisitor.h"
 #include "storm/logic/FormulaVisitor.h"
 #include "Model.h"
+#include "storm/storage/jani/Property.h"
 #include "storm/adapters/NumberAdapter.h"
 // JSON parser
 #include "json.hpp"
@@ -66,12 +67,13 @@ namespace storm {
             JsonExporter() = default;
             
         public:
-            static void toFile(storm::jani::Model const& janiModel, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, std::string const& filepath, bool checkValid = true);
-            static void toStream(storm::jani::Model const& janiModel, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, std::ostream& ostream, bool checkValid = false);
+            static void toFile(storm::jani::Model const& janiModel, std::vector<storm::jani::Property> const& formulas, std::string const& filepath, bool checkValid = true);
+            static void toStream(storm::jani::Model const& janiModel, std::vector<storm::jani::Property> const& formulas, std::ostream& ostream, bool checkValid = false);
+            
             
         private:
             void convertModel(storm::jani::Model const& model);
-            void convertProperties(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, storm::jani::Model const& model);
+            void convertProperties(std::vector<storm::jani::Property> const& formulas, storm::jani::Model const& model);
             void appendVariableDeclaration(storm::jani::Variable const& variable);
             
             modernjson::json finalize() {
diff --git a/src/storm/utility/storm.cpp b/src/storm/utility/storm.cpp
index 62c499fbd..9a0e6faba 100644
--- a/src/storm/utility/storm.cpp
+++ b/src/storm/utility/storm.cpp
@@ -36,9 +36,9 @@ namespace storm{
         if (storm::settings::getModule<storm::settings::modules::JaniExportSettings>().isExportAsStandardJaniSet()) {
             storm::jani::Model normalisedModel = model;
             normalisedModel.makeStandardJaniCompliant();
-            storm::jani::JsonExporter::toFile(normalisedModel, formulasInProperties(properties), filepath);
+            storm::jani::JsonExporter::toFile(normalisedModel, properties, filepath);
         } else {
-            storm::jani::JsonExporter::toFile(model, formulasInProperties(properties), filepath);
+            storm::jani::JsonExporter::toFile(model, properties, filepath);
         }
     }