From b901b2ce7decb98fb5b6db647299194b0ffaa698 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Sun, 14 Jan 2018 23:50:03 +0100
Subject: [PATCH] Started on GSPN to Json export
---
src/storm-dft-cli/storm-dft.cpp | 2 +-
.../settings/modules/GSPNExportSettings.cpp | 11 ++++++-
.../settings/modules/GSPNExportSettings.h | 8 +++++
src/storm-gspn/storage/gspn/GSPN.cpp | 8 +++--
src/storm-gspn/storage/gspn/GSPN.h | 9 +++++-
.../storage/gspn/GspnJsonExporter.cpp | 24 ++++++++++++++
.../storage/gspn/GspnJsonExporter.h | 32 +++++++++++++++++++
src/storm-gspn/storm-gspn.h | 7 ++++
8 files changed, 96 insertions(+), 5 deletions(-)
create mode 100644 src/storm-gspn/storage/gspn/GspnJsonExporter.cpp
create mode 100644 src/storm-gspn/storage/gspn/GspnJsonExporter.h
diff --git a/src/storm-dft-cli/storm-dft.cpp b/src/storm-dft-cli/storm-dft.cpp
index 478a438e1..1905a26b6 100644
--- a/src/storm-dft-cli/storm-dft.cpp
+++ b/src/storm-dft-cli/storm-dft.cpp
@@ -117,7 +117,7 @@ void processOptions() {
storm::builder::JaniGSPNBuilder builder(*gspn);
storm::jani::Model* model = builder.build();
storm::jani::Variable const& topfailedVar = builder.getPlaceVariable(toplevelFailedPlace);
-
+
storm::expressions::Expression targetExpression = exprManager->integer(1) == topfailedVar.getExpressionVariable().getExpression();
auto evtlFormula = std::make_shared<storm::logic::AtomicExpressionFormula>(targetExpression);
auto tbFormula = std::make_shared<storm::logic::BoundedUntilFormula>(std::make_shared<storm::logic::BooleanLiteralFormula>(true), evtlFormula, storm::logic::TimeBound(false, exprManager->integer(0)), storm::logic::TimeBound(false, exprManager->integer(10)), storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Time));
diff --git a/src/storm-gspn/settings/modules/GSPNExportSettings.cpp b/src/storm-gspn/settings/modules/GSPNExportSettings.cpp
index a3c46f250..5b7653eef 100644
--- a/src/storm-gspn/settings/modules/GSPNExportSettings.cpp
+++ b/src/storm-gspn/settings/modules/GSPNExportSettings.cpp
@@ -19,6 +19,7 @@ namespace storm {
const std::string GSPNExportSettings::writeToPnmlOptionName = "to-pnml";
const std::string GSPNExportSettings::writeToPnproOptionName = "to-pnpro";
+ const std::string GSPNExportSettings::writeToJsonOptionName = "to-json";
const std::string GSPNExportSettings::writeStatsOptionName = "to-stats";
const std::string GSPNExportSettings::displayStatsOptionName = "show-stats";
@@ -29,6 +30,7 @@ namespace storm {
this->addOption(storm::settings::OptionBuilder(moduleName, writeToDotOptionName, false, "Destination for the dot output.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "path to file").build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, writeToPnmlOptionName, false, "Destination for the pnml output").addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "path to file").build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, writeToPnproOptionName, false, "Destination for the pnpro output").addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "path to file").build()).build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, writeToJsonOptionName, false, "Destination for the json output").addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "path to file").build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, writeStatsOptionName, false, "Destination for the stats file").addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "path to file").build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, displayStatsOptionName, false, "Print stats to stdout").build());
}
@@ -56,7 +58,14 @@ namespace storm {
std::string GSPNExportSettings::getWriteToPnproFilename() const {
return this->getOption(writeToPnproOptionName).getArgumentByName("filename").getValueAsString();
}
-
+
+ bool GSPNExportSettings::isWriteToJsonSet() const {
+ return this->getOption(writeToJsonOptionName).getHasOptionBeenSet();
+ }
+
+ std::string GSPNExportSettings::getWriteToJsonFilename() const {
+ return this->getOption(writeToJsonOptionName).getArgumentByName("filename").getValueAsString();
+ }
bool GSPNExportSettings::isDisplayStatsSet() const {
return this->getOption(displayStatsOptionName).getHasOptionBeenSet();
diff --git a/src/storm-gspn/settings/modules/GSPNExportSettings.h b/src/storm-gspn/settings/modules/GSPNExportSettings.h
index 554cce223..ce203a841 100644
--- a/src/storm-gspn/settings/modules/GSPNExportSettings.h
+++ b/src/storm-gspn/settings/modules/GSPNExportSettings.h
@@ -37,6 +37,13 @@ namespace storm {
*
*/
std::string getWriteToPnproFilename() const;
+
+ bool isWriteToJsonSet() const;
+
+ /**
+ *
+ */
+ std::string getWriteToJsonFilename() const;
bool isDisplayStatsSet() const;
@@ -54,6 +61,7 @@ namespace storm {
static const std::string writeToDotOptionName;
static const std::string writeToPnmlOptionName;
static const std::string writeToPnproOptionName;
+ static const std::string writeToJsonOptionName;
static const std::string displayStatsOptionName;
static const std::string writeStatsOptionName;
diff --git a/src/storm-gspn/storage/gspn/GSPN.cpp b/src/storm-gspn/storage/gspn/GSPN.cpp
index 4a093b30e..3a603cb8b 100644
--- a/src/storm-gspn/storage/gspn/GSPN.cpp
+++ b/src/storm-gspn/storage/gspn/GSPN.cpp
@@ -6,8 +6,7 @@
#include "storm/utility/macros.h"
#include "storm/exceptions/InvalidArgumentException.h"
-
-
+#include "storm-gspn/storage/gspn/GspnJsonExporter.h"
namespace storm {
namespace gspn {
@@ -610,6 +609,11 @@ namespace storm {
stream << space << "</net>" << std::endl;
stream << "</pnml>" << std::endl;
}
+
+ void GSPN::toJson(std::ostream &stream) const {
+ return storm::gspn::GspnJsonExporter::toStream(*this, stream);
+ }
+
void GSPN::writeStatsToStream(std::ostream& stream) const {
stream << "Number of places: " << getNumberOfPlaces() << std::endl;
diff --git a/src/storm-gspn/storage/gspn/GSPN.h b/src/storm-gspn/storage/gspn/GSPN.h
index 19101ffe4..6a0d58143 100644
--- a/src/storm-gspn/storage/gspn/GSPN.h
+++ b/src/storm-gspn/storage/gspn/GSPN.h
@@ -168,7 +168,14 @@ namespace storm {
void toPnpro(std::ostream& stream) const;
// TODO doc
void toPnml(std::ostream& stream) const;
-
+
+ /*!
+ * Export GSPN in Json format.
+ *
+ * @param stream Outputstream.
+ */
+ void toJson(std::ostream& stream) const;
+
void writeStatsToStream(std::ostream& stream) const;
private:
storm::gspn::Place* getPlace(uint64_t id);
diff --git a/src/storm-gspn/storage/gspn/GspnJsonExporter.cpp b/src/storm-gspn/storage/gspn/GspnJsonExporter.cpp
new file mode 100644
index 000000000..de87952cc
--- /dev/null
+++ b/src/storm-gspn/storage/gspn/GspnJsonExporter.cpp
@@ -0,0 +1,24 @@
+#include "GspnJsonExporter.h"
+
+#include "storm/exceptions/NotImplementedException.h"
+#include "storm/exceptions/FileIoException.h"
+
+#include <algorithm>
+#include <string>
+
+namespace storm {
+ namespace gspn {
+
+ size_t GspnJsonExporter::currentId = 0;
+
+ void GspnJsonExporter::toStream(storm::gspn::GSPN const& gspn, std::ostream& os) {
+ os << translate(gspn).dump(4) << std::endl;
+ }
+
+ modernjson::json GspnJsonExporter::translate(storm::gspn::GSPN const& gspn) {
+ modernjson::json jsonGspn;
+ currentId = 0;
+ return jsonGspn;
+ }
+ }
+}
diff --git a/src/storm-gspn/storage/gspn/GspnJsonExporter.h b/src/storm-gspn/storage/gspn/GspnJsonExporter.h
new file mode 100644
index 000000000..86e0cec01
--- /dev/null
+++ b/src/storm-gspn/storage/gspn/GspnJsonExporter.h
@@ -0,0 +1,32 @@
+#pragma once
+
+#include "storm/utility/macros.h"
+
+#include "storm-gspn/storage/gspn/GSPN.h"
+
+// JSON parser
+#include "json.hpp"
+namespace modernjson {
+ using json = nlohmann::basic_json<std::map, std::vector, std::string, bool, int64_t, uint64_t, double, std::allocator>;
+}
+
+namespace storm {
+ namespace gspn {
+
+ /**
+ * Exports a GSPN into the JSON format for visualizing it.
+ */
+ class GspnJsonExporter {
+
+ public:
+ static void toStream(storm::gspn::GSPN const& gspn, std::ostream& os);
+
+ static modernjson::json translate(storm::gspn::GSPN const& gspn);
+
+ private:
+ static size_t currentId;
+
+ };
+
+ }
+}
diff --git a/src/storm-gspn/storm-gspn.h b/src/storm-gspn/storm-gspn.h
index e0d6dd3a6..cc9fd9add 100644
--- a/src/storm-gspn/storm-gspn.h
+++ b/src/storm-gspn/storm-gspn.h
@@ -41,6 +41,13 @@ namespace storm {
gspn.toPnml(fs);
storm::utility::closeFile(fs);
}
+
+ if (exportSettings.isWriteToJsonSet()) {
+ std::ofstream fs;
+ storm::utility::openFile(exportSettings.getWriteToJsonFilename(), fs);
+ gspn.toJson(fs);
+ storm::utility::closeFile(fs);
+ }
if (exportSettings.isDisplayStatsSet()) {
std::cout << "============GSPN Statistics==============" << std::endl;