writing the correct model name into the jani file

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);

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) {

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;
+            
         };
     }
 }

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.

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.