From 394ef9f5b3605e22539cf4901f3cabcc342b053a Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Thu, 16 Aug 2018 17:36:41 +0200
Subject: [PATCH] writing the correct model name into the jani file

---
 src/storm-conv-cli/storm-conv.cpp             | 23 +++++++++++++++++--
 src/storm-conv/api/storm-conv.cpp             | 15 +++++++++++-
 .../converter/options/JaniConversionOptions.h |  5 ++++
 src/storm/storage/jani/Model.cpp              |  4 ++++
 src/storm/storage/jani/Model.h                |  7 +++++-
 5 files changed, 50 insertions(+), 4 deletions(-)

diff --git a/src/storm-conv-cli/storm-conv.cpp b/src/storm-conv-cli/storm-conv.cpp
index 04169b2dc..294beea6b 100644
--- a/src/storm-conv-cli/storm-conv.cpp
+++ b/src/storm-conv-cli/storm-conv.cpp
@@ -51,20 +51,39 @@ namespace storm {
             options.allVariablesGlobal = jani.isGlobalVarsSet();
             options.suffix = "";
             options.janiOptions = storm::converter::JaniConversionOptions(jani);
-            auto janiModelProperties = storm::api::convertPrismToJani(prismProg, properties, options);
             
             std::string outputFilename = "";
             if (output.isJaniOutputFilenameSet()) {
                 outputFilename = output.getJaniOutputFilename();
             } else if (input.isPrismInputSet() && !output.isStdOutOutputEnabled()) {
+                outputFilename = input.getPrismInputFilename();
+                // Remove extension if present
+                auto dotPos = outputFilename.rfind('.');
+                if (dotPos != std::string::npos) {
+                    outputFilename.erase(dotPos);
+                }
                 std::string suffix = "";
                 if (input.isConstantsSet()) {
                     suffix = input.getConstantDefinitionString();
                     std::replace(suffix.begin(), suffix.end(), ',', '_');
+                    std::replace(suffix.begin(), suffix.end(), '=', '-');
                 }
                 suffix = suffix + ".jani";
-                outputFilename = input.getPrismInputFilename() + suffix;
+                outputFilename += suffix;
+            }
+            auto startOfFilename = outputFilename.rfind("/");
+            if (startOfFilename == std::string::npos) {
+                startOfFilename = 0;
+            } else {
+                ++startOfFilename;
             }
+            auto endOfFilename = outputFilename.rfind(".");
+            if (endOfFilename == std::string::npos) {
+                endOfFilename = outputFilename.size();
+            }
+            options.janiOptions.modelName = outputFilename.substr(startOfFilename, endOfFilename - startOfFilename);
+
+            auto janiModelProperties = storm::api::convertPrismToJani(prismProg, properties, options);
             
             if (outputFilename != "") {
                 storm::api::exportJaniToFile(janiModelProperties.first, janiModelProperties.second, outputFilename);
diff --git a/src/storm-conv/api/storm-conv.cpp b/src/storm-conv/api/storm-conv.cpp
index 1b52092bb..a8d88a502 100644
--- a/src/storm-conv/api/storm-conv.cpp
+++ b/src/storm-conv/api/storm-conv.cpp
@@ -5,6 +5,9 @@
 #include "storm/storage/jani/JaniLocationExpander.h"
 #include "storm/storage/jani/JSONExporter.h"
 
+#include "storm/settings/SettingsManager.h"
+#include "storm/settings/modules/CoreSettings.h"
+
 namespace storm {
     namespace api {
         
@@ -19,12 +22,22 @@ namespace storm {
             }
 
             if (options.exportFlattened) {
-                janiModel = janiModel.flattenComposition();
+                std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory;
+                if (storm::settings::hasModule<storm::settings::modules::CoreSettings>()) {
+                    smtSolverFactory = std::make_shared<storm::utility::solver::SmtSolverFactory>();
+                } else {
+                    smtSolverFactory = std::make_shared<storm::utility::solver::Z3SmtSolverFactory>();
+                }
+                janiModel = janiModel.flattenComposition(smtSolverFactory);
             }
 
             if (options.standardCompliant) {
                 janiModel.makeStandardJaniCompliant();
             }
+            
+            if (options.modelName) {
+                janiModel.setName(options.modelName.get());
+            }
         }
         
         std::pair<storm::jani::Model, std::vector<storm::jani::Property>> convertPrismToJani(storm::prism::Program const& program, std::vector<storm::jani::Property> const& properties, storm::converter::PrismToJaniConverterOptions options) {
diff --git a/src/storm-conv/converter/options/JaniConversionOptions.h b/src/storm-conv/converter/options/JaniConversionOptions.h
index bb809f1ea..000d9cc3b 100644
--- a/src/storm-conv/converter/options/JaniConversionOptions.h
+++ b/src/storm-conv/converter/options/JaniConversionOptions.h
@@ -2,6 +2,8 @@
 
 #include <string>
 #include <vector>
+#include <boost/optional.hpp>
+
 #include "storm-conv/settings/modules/JaniExportSettings.h"
 
 namespace storm {
@@ -21,6 +23,9 @@ namespace storm {
             /// If set, the model is transformed into a single automaton
             bool exportFlattened;
             
+            /// If given, the model will get this name
+            boost::optional<std::string> modelName;
+            
         };
     }
 }
diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp
index 222d31326..089ac7f0e 100644
--- a/src/storm/storage/jani/Model.cpp
+++ b/src/storm/storage/jani/Model.cpp
@@ -116,6 +116,10 @@ namespace storm {
             return name;
         }
         
+        void Model::setName(std::string const& newName) {
+            name = newName;
+        }
+        
         struct ConditionalMetaEdge {
             ConditionalMetaEdge() : actionIndex(0) {
                 // Intentionally left empty.
diff --git a/src/storm/storage/jani/Model.h b/src/storm/storage/jani/Model.h
index 2954b1c9f..644f90f20 100644
--- a/src/storm/storage/jani/Model.h
+++ b/src/storm/storage/jani/Model.h
@@ -77,10 +77,15 @@ namespace storm {
             ModelType const& getModelType() const;
             
             /*!
-             * Retrievest the name of the model.
+             * Retrieves the name of the model.
              */
             std::string const& getName() const;
             
+            /*!
+             * Sets the name of the model.
+             */
+            void setName(std::string const& newName);
+            
             /*!
              * Flatten the composition to obtain an equivalent model that contains exactly one automaton that has the
              * standard composition.