added option to make the json export more compact

src/storm-conv-cli/storm-conv.cpp

@@ -86,11 +86,11 @@ namespace storm {
             auto janiModelProperties = storm::api::convertPrismToJani(prismProg, properties, options);
             
             if (outputFilename != "") {
-                storm::api::exportJaniToFile(janiModelProperties.first, janiModelProperties.second, outputFilename);
+                storm::api::exportJaniToFile(janiModelProperties.first, janiModelProperties.second, outputFilename, jani.isCompactJsonSet());
             }
             
             if (output.isStdOutOutputEnabled()) {
-                storm::api::printJaniToStream(janiModelProperties.first, janiModelProperties.second, std::cout);
+                storm::api::printJaniToStream(janiModelProperties.first, janiModelProperties.second, std::cout, jani.isCompactJsonSet());
             }
         }
         

src/storm-conv/api/storm-conv.cpp

@@ -58,12 +58,12 @@ namespace storm {
             return res;
         }
         
-        void exportJaniToFile(storm::jani::Model const& model, std::vector<storm::jani::Property> const& properties, std::string const& filename) {
-            storm::jani::JsonExporter::toFile(model, properties, filename);
+        void exportJaniToFile(storm::jani::Model const& model, std::vector<storm::jani::Property> const& properties, std::string const& filename, bool compact) {
+            storm::jani::JsonExporter::toFile(model, properties, filename, true, compact);
         }
         
-        void printJaniToStream(storm::jani::Model const& model, std::vector<storm::jani::Property> const& properties, std::ostream& ostream) {
-            storm::jani::JsonExporter::toStream(model, properties, ostream);
+        void printJaniToStream(storm::jani::Model const& model, std::vector<storm::jani::Property> const& properties, std::ostream& ostream, bool compact) {
+            storm::jani::JsonExporter::toStream(model, properties, ostream, true, compact);
         }
 
         

src/storm-conv/api/storm-conv.h

@@ -19,9 +19,9 @@ namespace storm {
 
         std::pair<storm::jani::Model, std::vector<storm::jani::Property>> convertPrismToJani(storm::prism::Program const& program, std::vector<storm::jani::Property> const& properties = std::vector<storm::jani::Property>(), storm::converter::PrismToJaniConverterOptions options = storm::converter::PrismToJaniConverterOptions());
         
-        void exportJaniToFile(storm::jani::Model const& model, std::vector<storm::jani::Property> const& properties, std::string const& filename);
+        void exportJaniToFile(storm::jani::Model const& model, std::vector<storm::jani::Property> const& properties, std::string const& filename, bool compact = false);
         
-        void printJaniToStream(storm::jani::Model const& model, std::vector<storm::jani::Property> const& properties, std::ostream& ostream);
+        void printJaniToStream(storm::jani::Model const& model, std::vector<storm::jani::Property> const& properties, std::ostream& ostream, bool compact = false);
 
         
     }

src/storm-conv/settings/modules/JaniExportSettings.cpp

@@ -19,6 +19,7 @@ namespace storm {
             const std::string JaniExportSettings::exportFlattenOptionName = "flatten";
             const std::string JaniExportSettings::locationVariablesOptionName = "location-variables";
             const std::string JaniExportSettings::globalVariablesOptionName = "globalvars";
+            const std::string JaniExportSettings::compactJsonOptionName = "compactjson";
 
             
             JaniExportSettings::JaniExportSettings() : ModuleSettings(moduleName) {
@@ -26,6 +27,7 @@ namespace storm {
                 this->addOption(storm::settings::OptionBuilder(moduleName, standardCompliantOptionName, false, "Export in standard compliant variant.").setShortName(standardCompliantOptionShortName).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, exportFlattenOptionName, false, "Flattens the composition of Automata to obtain an equivalent model that contains exactly one automaton").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, globalVariablesOptionName, false, "If set, variables will preferably be made global, e.g., to guarantee the same variable order as in the input file.").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, compactJsonOptionName, false, "If set, the size of the resulting jani file will be reduced at the cost of (human-)readability.").build());
             }
             
             bool JaniExportSettings::isExportAsStandardJaniSet() const {
@@ -59,6 +61,10 @@ namespace storm {
             bool JaniExportSettings::isGlobalVarsSet() const {
                 return this->getOption(globalVariablesOptionName).getHasOptionBeenSet();
             }
+
+            bool JaniExportSettings::isCompactJsonSet() const {
+                return this->getOption(compactJsonOptionName).getHasOptionBeenSet();
+            }
             
             void JaniExportSettings::finalize() {
                 

src/storm-conv/settings/modules/JaniExportSettings.h

@@ -31,6 +31,8 @@ namespace storm {
                 bool isLocationVariablesSet() const;
                 
                 bool isGlobalVarsSet() const;
+                
+                bool isCompactJsonSet() const;
 
                 std::vector<std::pair<std::string, std::string>> getLocationVariables() const;
 
@@ -47,6 +49,7 @@ namespace storm {
                 static const std::string exportFlattenOptionName;
                 static const std::string locationVariablesOptionName;
                 static const std::string globalVariablesOptionName;
+                static const std::string compactJsonOptionName;
                 
             };
         }

src/storm-gspn/api/storm-gspn.cpp

@@ -72,7 +72,7 @@ namespace storm {
                 if (exportSettings.isAddJaniPropertiesSet()) {
                     properties.insert(properties.end(), builder.getStandardProperties().begin(), builder.getStandardProperties().end());
                 }
-                storm::api::exportJaniToFile(*model, properties, exportSettings.getWriteToJaniFilename());
+                storm::api::exportJaniToFile(*model, properties, exportSettings.getWriteToJaniFilename(), jani.isCompactJsonSet());
                 delete model;
             }
         }

src/storm-pgcl-cli/storm-pgcl.cpp

@@ -43,7 +43,7 @@ void handleJani(storm::jani::Model& model) {
     storm::converter::JaniConversionOptions options(jani);
     storm::api::postprocessJani(model, options);
     if (storm::settings::getModule<storm::settings::modules::PGCLSettings>().isToJaniSet()) {
-        storm::api::exportJaniToFile(model, {}, storm::settings::getModule<storm::settings::modules::PGCLSettings>().getWriteToJaniFilename());
+        storm::api::exportJaniToFile(model, {}, storm::settings::getModule<storm::settings::modules::PGCLSettings>().getWriteToJaniFilename(), jani.isCompactJsonSet());
     } else {
         storm::api::printJaniToStream(model, {}, std::cout);
     }

src/storm/storage/jani/JSONExporter.cpp

@@ -625,21 +625,27 @@ namespace storm {
             return modernjson::json(expression.getValueAsDouble());
         }
         
-        void JsonExporter::toFile(storm::jani::Model const& janiModel, std::vector<storm::jani::Property> 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, bool compact) {
             std::ofstream stream;
             storm::utility::openFile(filepath, stream);
-            toStream(janiModel, formulas, stream, checkValid);
+            toStream(janiModel, formulas, stream, checkValid, compact);
             storm::utility::closeFile(stream);
         }
         
-        void JsonExporter::toStream(storm::jani::Model const& janiModel,  std::vector<storm::jani::Property> 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, bool compact) {
             if(checkValid) {
                 janiModel.checkValid();
             }
             JsonExporter exporter;
-            exporter.convertModel(janiModel);
+            exporter.convertModel(janiModel, !compact);
             exporter.convertProperties(formulas, janiModel);
-            os << exporter.finalize().dump(4) << std::endl;
+            if (compact) {
+                // Dump without line breaks/indents
+                os << exporter.finalize().dump() << std::endl;
+            } else {
+                // Dump with line breaks and indention with 4 spaces
+                os << exporter.finalize().dump(4) << std::endl;
+            }
         }
         
         modernjson::json buildActionArray(std::vector<storm::jani::Action> const& actions) {

src/storm/storage/jani/JSONExporter.h

@@ -75,8 +75,8 @@ namespace storm {
             JsonExporter() = default;
             
         public:
-            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);
+            static void toFile(storm::jani::Model const& janiModel, std::vector<storm::jani::Property> const& formulas, std::string const& filepath, bool checkValid = true, bool compact = false);
+            static void toStream(storm::jani::Model const& janiModel, std::vector<storm::jani::Property> const& formulas, std::ostream& ostream, bool checkValid = false, bool compact = false);
             
             
         private: