From ce3b63da128b7155cf436c0e86b505d589839257 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 23 Aug 2018 17:41:58 +0200 Subject: [PATCH] Fixed json export settings --- src/storm-dft/CMakeLists.txt | 2 +- src/storm-dft/api/storm-dft.cpp | 14 ++++++++++---- .../settings/modules/DftGspnSettings.cpp | 11 ++++++++++- .../settings/modules/DftGspnSettings.h | 17 ++++++++++++++++- 4 files changed, 37 insertions(+), 7 deletions(-) diff --git a/src/storm-dft/CMakeLists.txt b/src/storm-dft/CMakeLists.txt index 48a046238..cf719ad60 100644 --- a/src/storm-dft/CMakeLists.txt +++ b/src/storm-dft/CMakeLists.txt @@ -17,7 +17,7 @@ set_target_properties(storm-dft PROPERTIES DEFINE_SYMBOL "") list(APPEND STORM_TARGETS storm-dft) set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE) -target_link_libraries(storm-dft PUBLIC storm storm-gspn storm-parsers ${STORM_DFT_LINK_LIBRARIES}) +target_link_libraries(storm-dft PUBLIC storm storm-gspn storm-conv storm-parsers ${STORM_DFT_LINK_LIBRARIES}) # Install storm headers to include directory. foreach(HEADER ${STORM_DFT_HEADERS}) diff --git a/src/storm-dft/api/storm-dft.cpp b/src/storm-dft/api/storm-dft.cpp index 5740f71bf..74750c350 100644 --- a/src/storm-dft/api/storm-dft.cpp +++ b/src/storm-dft/api/storm-dft.cpp @@ -2,6 +2,7 @@ #include "storm-dft/settings/modules/FaultTreeSettings.h" #include "storm-dft/settings/modules/DftGspnSettings.h" +#include "storm-conv/api/storm-conv.h" namespace storm { namespace api { @@ -64,9 +65,12 @@ namespace storm { } std::shared_ptr transformToJani(storm::gspn::GSPN const& gspn, uint64_t toplevelFailedPlace) { + + // Build Jani model storm::builder::JaniGSPNBuilder builder(gspn); - std::shared_ptr model(builder.build()); + std::shared_ptr model(builder.build("dft_gspn")); + // Build properties std::shared_ptr const& exprManager = gspn.getExpressionManager(); storm::jani::Variable const& topfailedVar = builder.getPlaceVariable(toplevelFailedPlace); storm::expressions::Expression targetExpression = exprManager->integer(1) == topfailedVar.getExpressionVariable().getExpression(); @@ -80,10 +84,12 @@ namespace storm { auto timeBoundedProperty = storm::jani::Property("time-bounded", tbUntil); auto mttfProperty = storm::jani::Property("mttf", rewFormula); - storm::settings::modules::JaniExportSettings const& janiSettings = storm::settings::getModule(); - if (janiSettings.isJaniFileSet()) { + + // Export Jani to file + storm::settings::modules::DftGspnSettings const& dftGspnSettings = storm::settings::getModule(); + if (dftGspnSettings.isWriteToJaniSet()) { // Currently no properties are set - storm::api::exportJaniModel(*model, {}, janiSettings.getJaniFilename()); + storm::api::exportJaniToFile(*model, {}, dftGspnSettings.getWriteToJaniFilename()); } return model; diff --git a/src/storm-dft/settings/modules/DftGspnSettings.cpp b/src/storm-dft/settings/modules/DftGspnSettings.cpp index 88fc40d94..e7eb34810 100644 --- a/src/storm-dft/settings/modules/DftGspnSettings.cpp +++ b/src/storm-dft/settings/modules/DftGspnSettings.cpp @@ -17,7 +17,7 @@ namespace storm { const std::string DftGspnSettings::disableSmartTransformationOptionName = "disable-smart"; const std::string DftGspnSettings::mergeDCFailedOptionName = "merge-dc-failed"; const std::string DftGspnSettings::extendPrioritiesOptionName = "extend-priorities"; - + const std::string DftGspnSettings::writeToJaniOptionName = "to-jani"; DftGspnSettings::DftGspnSettings() : ModuleSettings(moduleName) { this->addOption(storm::settings::OptionBuilder(moduleName, transformToGspnOptionName, false, "Transform DFT to GSPN.").build()); @@ -25,6 +25,7 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, mergeDCFailedOptionName, false, "Enable merging of Don't Care and Failed places into a combined place.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, extendPrioritiesOptionName, false, "Enable experimental calculation of transition priorities").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, writeToJaniOptionName, false, "Destination for the jani output").addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "path to file" ).build()).build()); } bool DftGspnSettings::isTransformToGspn() const { @@ -43,6 +44,14 @@ namespace storm { return this->getOption(extendPrioritiesOptionName).getHasOptionBeenSet(); } + bool DftGspnSettings::isWriteToJaniSet() const { + return this->getOption(writeToJaniOptionName).getHasOptionBeenSet(); + } + + std::string DftGspnSettings::getWriteToJaniFilename() const { + return this->getOption(writeToJaniOptionName).getArgumentByName("filename").getValueAsString(); + } + void DftGspnSettings::finalize() { } diff --git a/src/storm-dft/settings/modules/DftGspnSettings.h b/src/storm-dft/settings/modules/DftGspnSettings.h index 11531fdbb..f35295c00 100644 --- a/src/storm-dft/settings/modules/DftGspnSettings.h +++ b/src/storm-dft/settings/modules/DftGspnSettings.h @@ -41,10 +41,24 @@ namespace storm { /*! * Retrieves whether the experimental setting of priorities should be used * - * @return True if the settig is enabled is enabled. + * @return True if the setting is enabled. */ bool isExtendPriorities() const; + /*! + * Retrieves whether the GSPN should be exported as a Jani file. + * + * @return True if the Jani file should be exported. + */ + bool isWriteToJaniSet() const; + + /*! + * Retrieves the jani filename for export. + * + * @return Filename. + */ + std::string getWriteToJaniFilename() const; + bool check() const override; void finalize() override; @@ -58,6 +72,7 @@ namespace storm { static const std::string disableSmartTransformationOptionName; static const std::string mergeDCFailedOptionName; static const std::string extendPrioritiesOptionName; + static const std::string writeToJaniOptionName; }; } // namespace modules