diff --git a/src/storm-conv-cli/storm-conv.cpp b/src/storm-conv-cli/storm-conv.cpp index 294beea6b..a499fccf2 100644 --- a/src/storm-conv-cli/storm-conv.cpp +++ b/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()); } } diff --git a/src/storm-conv/api/storm-conv.cpp b/src/storm-conv/api/storm-conv.cpp index a8d88a502..aa37dd191 100644 --- a/src/storm-conv/api/storm-conv.cpp +++ b/src/storm-conv/api/storm-conv.cpp @@ -58,12 +58,12 @@ namespace storm { return res; } - void exportJaniToFile(storm::jani::Model const& model, std::vector const& properties, std::string const& filename) { - storm::jani::JsonExporter::toFile(model, properties, filename); + void exportJaniToFile(storm::jani::Model const& model, std::vector 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 const& properties, std::ostream& ostream) { - storm::jani::JsonExporter::toStream(model, properties, ostream); + void printJaniToStream(storm::jani::Model const& model, std::vector const& properties, std::ostream& ostream, bool compact) { + storm::jani::JsonExporter::toStream(model, properties, ostream, true, compact); } diff --git a/src/storm-conv/api/storm-conv.h b/src/storm-conv/api/storm-conv.h index ec8a306df..42cbf804d 100644 --- a/src/storm-conv/api/storm-conv.h +++ b/src/storm-conv/api/storm-conv.h @@ -19,9 +19,9 @@ namespace storm { std::pair> convertPrismToJani(storm::prism::Program const& program, std::vector const& properties = std::vector(), storm::converter::PrismToJaniConverterOptions options = storm::converter::PrismToJaniConverterOptions()); - void exportJaniToFile(storm::jani::Model const& model, std::vector const& properties, std::string const& filename); + void exportJaniToFile(storm::jani::Model const& model, std::vector const& properties, std::string const& filename, bool compact = false); - void printJaniToStream(storm::jani::Model const& model, std::vector const& properties, std::ostream& ostream); + void printJaniToStream(storm::jani::Model const& model, std::vector const& properties, std::ostream& ostream, bool compact = false); } diff --git a/src/storm-conv/settings/modules/JaniExportSettings.cpp b/src/storm-conv/settings/modules/JaniExportSettings.cpp index 5199a308d..707e91dac 100644 --- a/src/storm-conv/settings/modules/JaniExportSettings.cpp +++ b/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() { diff --git a/src/storm-conv/settings/modules/JaniExportSettings.h b/src/storm-conv/settings/modules/JaniExportSettings.h index 90dc532f0..2b2d6de7a 100644 --- a/src/storm-conv/settings/modules/JaniExportSettings.h +++ b/src/storm-conv/settings/modules/JaniExportSettings.h @@ -31,6 +31,8 @@ namespace storm { bool isLocationVariablesSet() const; bool isGlobalVarsSet() const; + + bool isCompactJsonSet() const; std::vector> 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; }; } diff --git a/src/storm-gspn/api/storm-gspn.cpp b/src/storm-gspn/api/storm-gspn.cpp index 7b18bc010..63da78250 100644 --- a/src/storm-gspn/api/storm-gspn.cpp +++ b/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; } } diff --git a/src/storm-pgcl-cli/storm-pgcl.cpp b/src/storm-pgcl-cli/storm-pgcl.cpp index 5ae5248b3..fe4585023 100644 --- a/src/storm-pgcl-cli/storm-pgcl.cpp +++ b/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().isToJaniSet()) { - storm::api::exportJaniToFile(model, {}, storm::settings::getModule().getWriteToJaniFilename()); + storm::api::exportJaniToFile(model, {}, storm::settings::getModule().getWriteToJaniFilename(), jani.isCompactJsonSet()); } else { storm::api::printJaniToStream(model, {}, std::cout); } diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp index deb831ed1..c957cd29b 100644 --- a/src/storm/storage/jani/JSONExporter.cpp +++ b/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 const& formulas, std::string const& filepath, bool checkValid) { + void JsonExporter::toFile(storm::jani::Model const& janiModel, std::vector 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 const& formulas, std::ostream& os, bool checkValid) { + void JsonExporter::toStream(storm::jani::Model const& janiModel, std::vector 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 const& actions) { diff --git a/src/storm/storage/jani/JSONExporter.h b/src/storm/storage/jani/JSONExporter.h index 1bf098bca..f88bb7330 100644 --- a/src/storm/storage/jani/JSONExporter.h +++ b/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 const& formulas, std::string const& filepath, bool checkValid = true); - static void toStream(storm::jani::Model const& janiModel, std::vector const& formulas, std::ostream& ostream, bool checkValid = false); + static void toFile(storm::jani::Model const& janiModel, std::vector const& formulas, std::string const& filepath, bool checkValid = true, bool compact = false); + static void toStream(storm::jani::Model const& janiModel, std::vector const& formulas, std::ostream& ostream, bool checkValid = false, bool compact = false); private: