From 5c900e4e14c6e86d6ee43b04051b54a9f7cb6956 Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@rwth-aachen.de>
Date: Wed, 14 Dec 2016 17:58:58 +0100
Subject: [PATCH] stats for gspn
---
src/storm-dft-cli/storm-dyftee.cpp | 1 +
src/storm-gspn/storage/gspn/GSPN.cpp | 14 +++++++++
src/storm-gspn/storage/gspn/GSPN.h | 10 +++++--
src/storm-gspn/storm-gspn.h | 30 ++++++++++++++++++-
.../settings/modules/GSPNExportSettings.cpp | 16 ++++++++++
.../settings/modules/GSPNExportSettings.h | 9 ++++++
6 files changed, 77 insertions(+), 3 deletions(-)
diff --git a/src/storm-dft-cli/storm-dyftee.cpp b/src/storm-dft-cli/storm-dyftee.cpp
index 6c54dc226..7be07940c 100644
--- a/src/storm-dft-cli/storm-dyftee.cpp
+++ b/src/storm-dft-cli/storm-dyftee.cpp
@@ -136,6 +136,7 @@ int main(const int argc, const char** argv) {
gspnTransformator.transform();
storm::gspn::GSPN* gspn = gspnTransformator.obtainGSPN();
uint64_t toplevelFailedPlace = gspnTransformator.toplevelFailedPlaceId();
+
storm::handleGSPNExportSettings(*gspn);
std::shared_ptr<storm::expressions::ExpressionManager> exprManager(new storm::expressions::ExpressionManager());
diff --git a/src/storm-gspn/storage/gspn/GSPN.cpp b/src/storm-gspn/storage/gspn/GSPN.cpp
index 5a7f819de..74f5983ae 100644
--- a/src/storm-gspn/storage/gspn/GSPN.cpp
+++ b/src/storm-gspn/storage/gspn/GSPN.cpp
@@ -36,6 +36,14 @@ namespace storm {
uint64_t GSPN::getNumberOfPlaces() const {
return places.size();
}
+
+ uint64_t GSPN::getNumberOfImmediateTransitions() const {
+ return immediateTransitions.size();
+ }
+
+ uint64_t GSPN::getNumberOfTimedTransitions() const {
+ return timedTransitions.size();
+ }
std::vector<storm::gspn::TimedTransition<GSPN::RateType>> const& GSPN::getTimedTransitions() const {
return this->timedTransitions;
@@ -565,6 +573,12 @@ namespace storm {
stream << space << "</net>" << std::endl;
stream << "</pnml>" << std::endl;
}
+
+ void GSPN::writeStatsToStream(std::ostream& stream) const {
+ stream << "Number of places: " << getNumberOfPlaces() << std::endl;
+ stream << "Number of timed transitions: " << getNumberOfTimedTransitions() << std::endl;
+ stream << "Number of immediate transitions: " << getNumberOfImmediateTransitions() << std::endl;
+ }
}
}
diff --git a/src/storm-gspn/storage/gspn/GSPN.h b/src/storm-gspn/storage/gspn/GSPN.h
index 7086a6c1c..b58a6adc5 100644
--- a/src/storm-gspn/storage/gspn/GSPN.h
+++ b/src/storm-gspn/storage/gspn/GSPN.h
@@ -37,6 +37,10 @@ namespace storm {
* @return The number of places.
*/
uint64_t getNumberOfPlaces() const;
+
+ uint64_t getNumberOfImmediateTransitions() const;
+
+ uint64_t getNumberOfTimedTransitions() const;
/*!
*
@@ -146,9 +150,11 @@ namespace storm {
*/
bool isValid() const;
// TODO doc
- void toPnpro(std::ostream &stream) const;
+ void toPnpro(std::ostream& stream) const;
// TODO doc
- void toPnml(std::ostream &stream) const;
+ void toPnml(std::ostream& stream) const;
+
+ void writeStatsToStream(std::ostream& stream) const;
private:
storm::gspn::Place* getPlace(uint64_t id);
storm::gspn::Place* getPlace(std::string const& name);
diff --git a/src/storm-gspn/storm-gspn.h b/src/storm-gspn/storm-gspn.h
index 3af59a9c1..3a3f9d55a 100644
--- a/src/storm-gspn/storm-gspn.h
+++ b/src/storm-gspn/storm-gspn.h
@@ -22,11 +22,39 @@ namespace storm {
if (exportSettings.isWriteToDotSet()) {
std::ofstream fs;
fs.open(exportSettings.getWriteToDotFilename());
- gspn.writeDotToStream(std::cout);
gspn.writeDotToStream(fs);
fs.close();
}
+ if (exportSettings.isWriteToPnproSet()) {
+ std::ofstream fs;
+ fs.open(exportSettings.getWriteToPnproFilename());
+ gspn.toPnpro(fs);
+ fs.close();
+ }
+
+ if (exportSettings.isWriteToPnmlSet()) {
+ std::ofstream fs;
+ fs.open(exportSettings.getWriteToPnmlFilename());
+ gspn.toPnml(fs);
+ fs.close();
+ }
+
+ if (exportSettings.isDisplayStatsSet()) {
+ std::cout << "============GSPN Statistics==============" << std::endl;
+ gspn.writeStatsToStream(std::cout);
+ std::cout << "=========================================" << std::endl;
+ }
+
+ if (exportSettings.isWriteStatsToFileSet()) {
+ std::ofstream fs;
+ fs.open(exportSettings.getWriteStatsFilename());
+ gspn.writeStatsToStream(fs);
+ fs.close();
+ }
+
+
+
}
}
\ No newline at end of file
diff --git a/src/storm/settings/modules/GSPNExportSettings.cpp b/src/storm/settings/modules/GSPNExportSettings.cpp
index 9be15c75e..8a5c315dc 100644
--- a/src/storm/settings/modules/GSPNExportSettings.cpp
+++ b/src/storm/settings/modules/GSPNExportSettings.cpp
@@ -19,6 +19,8 @@ namespace storm {
const std::string GSPNExportSettings::writeToPnmlOptionName = "to-pnml";
const std::string GSPNExportSettings::writeToPnproOptionName = "to-pnpro";
+ const std::string GSPNExportSettings::writeStatsOptionName = "to-stats";
+ const std::string GSPNExportSettings::displayStatsOptionName = "show-stats";
//const std::string GSPNExportSettings::janiFileOptionShortName = "dotoutput";
@@ -27,6 +29,8 @@ 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, 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());
}
bool GSPNExportSettings::isWriteToDotSet() const {
@@ -54,6 +58,18 @@ namespace storm {
}
+ bool GSPNExportSettings::isDisplayStatsSet() const {
+ return this->getOption(displayStatsOptionName).getHasOptionBeenSet();
+ }
+
+ bool GSPNExportSettings::isWriteStatsToFileSet() const {
+ return this->getOption(writeStatsOptionName).getHasOptionBeenSet();
+ }
+
+ std::string GSPNExportSettings::getWriteStatsFilename() const {
+ return this->getOption(writeStatsOptionName).getArgumentByName("filename").getValueAsString();
+ }
+
void GSPNExportSettings::finalize() {
}
diff --git a/src/storm/settings/modules/GSPNExportSettings.h b/src/storm/settings/modules/GSPNExportSettings.h
index 32ae422ba..554cce223 100644
--- a/src/storm/settings/modules/GSPNExportSettings.h
+++ b/src/storm/settings/modules/GSPNExportSettings.h
@@ -38,6 +38,12 @@ namespace storm {
*/
std::string getWriteToPnproFilename() const;
+ bool isDisplayStatsSet() const;
+
+ bool isWriteStatsToFileSet() const;
+
+ std::string getWriteStatsFilename() const;
+
bool check() const override;
void finalize() override;
@@ -48,6 +54,9 @@ namespace storm {
static const std::string writeToDotOptionName;
static const std::string writeToPnmlOptionName;
static const std::string writeToPnproOptionName;
+ static const std::string displayStatsOptionName;
+ static const std::string writeStatsOptionName;
+
//static const std::string writeToDotOptionShortName;
};