Browse Source

Started on GSPN to Json export

main
Matthias Volk 7 years ago
parent
commit
b901b2ce7d
  1. 2
      src/storm-dft-cli/storm-dft.cpp
  2. 11
      src/storm-gspn/settings/modules/GSPNExportSettings.cpp
  3. 8
      src/storm-gspn/settings/modules/GSPNExportSettings.h
  4. 8
      src/storm-gspn/storage/gspn/GSPN.cpp
  5. 9
      src/storm-gspn/storage/gspn/GSPN.h
  6. 24
      src/storm-gspn/storage/gspn/GspnJsonExporter.cpp
  7. 32
      src/storm-gspn/storage/gspn/GspnJsonExporter.h
  8. 7
      src/storm-gspn/storm-gspn.h

2
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));

11
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();

8
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;

8
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;

9
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);

24
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;
}
}
}

32
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;
};
}
}

7
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;

Loading…
Cancel
Save