From 7ee196bdbb9529ebd0dcfa7d6949596d740e1ecb Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Wed, 12 Sep 2018 16:19:41 +0200
Subject: [PATCH] jani2jani conversions in storm-conv

---
 src/storm-conv-cli/storm-conv.cpp | 53 ++++++++++++++++++++++++++++++-
 1 file changed, 52 insertions(+), 1 deletion(-)

diff --git a/src/storm-conv-cli/storm-conv.cpp b/src/storm-conv-cli/storm-conv.cpp
index 1977cfdb7..72cba3e3d 100644
--- a/src/storm-conv-cli/storm-conv.cpp
+++ b/src/storm-conv-cli/storm-conv.cpp
@@ -52,6 +52,7 @@ namespace storm {
             options.suffix = "";
             options.janiOptions = storm::converter::JaniConversionOptions(jani);
             
+            // Get the name of the output file
             std::string outputFilename = "";
             if (output.isJaniOutputFilenameSet()) {
                 outputFilename = output.getJaniOutputFilename();
@@ -71,6 +72,8 @@ namespace storm {
                 suffix = suffix + ".jani";
                 outputFilename += suffix;
             }
+            
+            // Find a good model name
             auto startOfFilename = outputFilename.rfind("/");
             if (startOfFilename == std::string::npos) {
                 startOfFilename = 0;
@@ -83,6 +86,7 @@ namespace storm {
             }
             options.janiOptions.modelName = outputFilename.substr(startOfFilename, endOfFilename - startOfFilename);
 
+            
             auto janiModelProperties = storm::api::convertPrismToJani(prismProg, properties, options);
             
             if (outputFilename != "") {
@@ -124,6 +128,53 @@ namespace storm {
             }
         }
         
+        void processJaniInputJaniOutput(storm::jani::Model const& janiModel, std::vector<storm::jani::Property> const& properties) {
+            auto const& output = storm::settings::getModule<storm::settings::modules::ConversionOutputSettings>();
+            auto const& input = storm::settings::getModule<storm::settings::modules::ConversionInputSettings>();
+            auto const& jani = storm::settings::getModule<storm::settings::modules::JaniExportSettings>();
+            
+            storm::converter::JaniConversionOptions options(jani);
+            
+            // Get the name of the output file
+            std::string outputFilename = "";
+            if (output.isJaniOutputFilenameSet()) {
+                outputFilename = output.getJaniOutputFilename();
+            } else if (input.isJaniInputSet() && !output.isStdOutOutputEnabled()) {
+                outputFilename = input.getJaniInputFilename();
+                // Remove extension if present
+                auto dotPos = outputFilename.rfind('.');
+                if (dotPos != std::string::npos) {
+                    outputFilename.erase(dotPos);
+                }
+                outputFilename += "_converted.jani";
+            }
+            
+            // Get a good model name from the output filename
+            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.modelName = outputFilename.substr(startOfFilename, endOfFilename - startOfFilename);
+
+            auto transformedJaniModel = janiModel;
+            auto transformedProperties = properties;
+            storm::api::transformJani(transformedJaniModel, transformedProperties, options);
+            
+            if (outputFilename != "") {
+                storm::api::exportJaniToFile(transformedJaniModel, transformedProperties, outputFilename, jani.isCompactJsonSet());
+            }
+            
+            if (output.isStdOutOutputEnabled()) {
+                storm::api::printJaniToStream(transformedJaniModel, transformedProperties, std::cout, jani.isCompactJsonSet());
+            }
+        }
+        
         void processJaniInput() {
             auto const& input = storm::settings::getModule<storm::settings::modules::ConversionInputSettings>();
 
@@ -150,7 +201,7 @@ namespace storm {
             // Branch on the type of output
             auto const& output = storm::settings::getModule<storm::settings::modules::ConversionOutputSettings>();
             if (output.isJaniOutputSet()) {
-//                processJaniInputJaniOutput(janiModel.asJaniModel(), properties);
+                processJaniInputJaniOutput(janiModel.asJaniModel(), properties);
             } else {
                 STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "There is either no outputformat specified or the provided combination of input and output format is not compatible.");
             }