diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp index 7548fd323..889496265 100644 --- a/src/storm/storage/jani/JSONExporter.cpp +++ b/src/storm/storage/jani/JSONExporter.cpp @@ -516,7 +516,7 @@ namespace storm { - 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) { std::ofstream ofs; ofs.open (filepath, std::ofstream::out ); if(ofs.is_open()) { @@ -526,7 +526,7 @@ namespace storm { } } - 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) { if(checkValid) { janiModel.checkValid(); } @@ -759,13 +759,13 @@ namespace storm { } - void JsonExporter::convertProperties( std::vector> const& formulas, storm::jani::Model const& model) { + void JsonExporter::convertProperties( std::vector const& formulas, storm::jani::Model const& model) { std::vector properties; uint64_t index = 0; for(auto const& f : formulas) { modernjson::json propDecl; - propDecl["name"] = "prop" + std::to_string(index); - propDecl["expression"] = convertFilterExpression(storm::jani::FilterExpression(f), model); + propDecl["name"] = f.getName(); + propDecl["expression"] = convertFilterExpression(f.getFilter(), model); ++index; properties.push_back(propDecl); } diff --git a/src/storm/storage/jani/JSONExporter.h b/src/storm/storage/jani/JSONExporter.h index 1008ec097..1eceb5d2e 100644 --- a/src/storm/storage/jani/JSONExporter.h +++ b/src/storm/storage/jani/JSONExporter.h @@ -4,6 +4,7 @@ #include "storm/storage/expressions/ExpressionVisitor.h" #include "storm/logic/FormulaVisitor.h" #include "Model.h" +#include "storm/storage/jani/Property.h" #include "storm/adapters/NumberAdapter.h" // JSON parser #include "json.hpp" @@ -66,12 +67,13 @@ 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); + static void toStream(storm::jani::Model const& janiModel, std::vector const& formulas, std::ostream& ostream, bool checkValid = false); + private: void convertModel(storm::jani::Model const& model); - void convertProperties(std::vector> const& formulas, storm::jani::Model const& model); + void convertProperties(std::vector const& formulas, storm::jani::Model const& model); void appendVariableDeclaration(storm::jani::Variable const& variable); modernjson::json finalize() { diff --git a/src/storm/utility/storm.cpp b/src/storm/utility/storm.cpp index 62c499fbd..9a0e6faba 100644 --- a/src/storm/utility/storm.cpp +++ b/src/storm/utility/storm.cpp @@ -36,9 +36,9 @@ namespace storm{ if (storm::settings::getModule().isExportAsStandardJaniSet()) { storm::jani::Model normalisedModel = model; normalisedModel.makeStandardJaniCompliant(); - storm::jani::JsonExporter::toFile(normalisedModel, formulasInProperties(properties), filepath); + storm::jani::JsonExporter::toFile(normalisedModel, properties, filepath); } else { - storm::jani::JsonExporter::toFile(model, formulasInProperties(properties), filepath); + storm::jani::JsonExporter::toFile(model, properties, filepath); } }