From 4a7a82627f3978080c92a0b89d03ceece549015b Mon Sep 17 00:00:00 2001 From: TimQu Date: Mon, 30 Jul 2018 14:16:18 +0200 Subject: [PATCH] storm-gspn and storm-dft now use functionalities of storm-conv --- src/storm-dft/api/storm-dft.cpp | 33 ++++++++----------- src/storm-dft/settings/DftSettings.cpp | 2 +- src/storm-gspn-cli/storm-gspn.cpp | 8 +---- src/storm-gspn/CMakeLists.txt | 2 +- src/storm-gspn/api/storm-gspn.cpp | 14 +++++++- src/storm-gspn/api/storm-gspn.h | 4 ++- .../settings/modules/GSPNExportSettings.cpp | 11 ++++++- .../settings/modules/GSPNExportSettings.h | 11 ++++++- 8 files changed, 53 insertions(+), 32 deletions(-) diff --git a/src/storm-dft/api/storm-dft.cpp b/src/storm-dft/api/storm-dft.cpp index 91632739e..19c97a67f 100644 --- a/src/storm-dft/api/storm-dft.cpp +++ b/src/storm-dft/api/storm-dft.cpp @@ -34,25 +34,20 @@ namespace storm { storm::gspn::GSPN* gspn = gspnTransformator.obtainGSPN(); uint64_t toplevelFailedPlace = gspnTransformator.toplevelFailedPlaceId(); - storm::api::handleGSPNExportSettings(*gspn); - - std::shared_ptr const& exprManager = gspn->getExpressionManager(); - 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(targetExpression); - auto tbFormula = std::make_shared(std::make_shared(true), evtlFormula, storm::logic::TimeBound(false, exprManager->integer(0)), storm::logic::TimeBound(false, exprManager->integer(10)), storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Time)); - auto tbUntil = std::make_shared(tbFormula); - - auto evFormula = std::make_shared(evtlFormula, storm::logic::FormulaContext::Time); - auto rewFormula = std::make_shared(evFormula, storm::logic::OperatorInformation(), storm::logic::RewardMeasureType::Expectation); - - storm::settings::modules::JaniExportSettings const& janiSettings = storm::settings::getModule(); - if (janiSettings.isJaniFileSet()) { - storm::api::exportJaniModel(*model, {storm::jani::Property("time-bounded", tbUntil), storm::jani::Property("mttf", rewFormula)}, janiSettings.getJaniFilename()); - } + storm::api::handleGSPNExportSettings(*gspn, [&]std::vector(storm::builder::JaniGSPNBuilder const& builder) { + 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(); + auto evtlFormula = std::make_shared(targetExpression); + auto tbFormula = std::make_shared(std::make_shared(true), evtlFormula, storm::logic::TimeBound(false, exprManager->integer(0)), storm::logic::TimeBound(false, exprManager->integer(10)), storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Time)); + auto tbUntil = std::make_shared(tbFormula); + + auto evFormula = std::make_shared(evtlFormula, storm::logic::FormulaContext::Time); + auto rewFormula = std::make_shared(evFormula, storm::logic::OperatorInformation(), storm::logic::RewardMeasureType::Expectation); + return {storm::jani::Property("time-bounded", tbUntil), storm::jani::Property("mttf", rewFormula)}; + } + ); delete model; delete gspn; diff --git a/src/storm-dft/settings/DftSettings.cpp b/src/storm-dft/settings/DftSettings.cpp index 361ccdc8f..b5c206d51 100644 --- a/src/storm-dft/settings/DftSettings.cpp +++ b/src/storm-dft/settings/DftSettings.cpp @@ -19,7 +19,7 @@ #include "storm/settings/modules/GameSolverSettings.h" #include "storm/settings/modules/BisimulationSettings.h" #include "storm/settings/modules/ResourceSettings.h" -#include "storm/settings/modules/JaniExportSettings.h" +#include "storm-conv/settings/modules/JaniExportSettings.h" #include "storm-gspn/settings/modules/GSPNSettings.h" #include "storm-gspn/settings/modules/GSPNExportSettings.h" diff --git a/src/storm-gspn-cli/storm-gspn.cpp b/src/storm-gspn-cli/storm-gspn.cpp index 46da4fea5..aff3a8fce 100644 --- a/src/storm-gspn-cli/storm-gspn.cpp +++ b/src/storm-gspn-cli/storm-gspn.cpp @@ -112,14 +112,8 @@ int main(const int argc, const char **argv) { gspn->setCapacities(capacities); } - storm::api::handleGSPNExportSettings(*gspn); + storm::api::handleGSPNExportSettings(*gspn, [&]std::vector(storm::builder::JaniGSPNBuilder const&) { return properties }); - if(storm::settings::getModule().isJaniFileSet()) { - storm::jani::Model* model = storm::api::buildJani(*gspn); - storm::api::exportJaniModel(*model, properties, storm::settings::getModule().getJaniFilename()); - delete model; - } - delete gspn; return 0; diff --git a/src/storm-gspn/CMakeLists.txt b/src/storm-gspn/CMakeLists.txt index 9312af543..a09b83621 100644 --- a/src/storm-gspn/CMakeLists.txt +++ b/src/storm-gspn/CMakeLists.txt @@ -12,7 +12,7 @@ file(GLOB_RECURSE STORM_GSPN_HEADERS ${PROJECT_SOURCE_DIR}/src/storm-gspn/*/*.h) add_library(storm-gspn SHARED ${STORM_GSPN_SOURCES} ${STORM_GSPN_HEADERS}) list(APPEND STORM_TARGETS storm-gspn) set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE) -target_link_libraries(storm-gspn storm ${STORM_GSPN_LINK_LIBRARIES}) +target_link_libraries(storm-gspn storm storm-conv ${STORM_GSPN_LINK_LIBRARIES}) # installation install(TARGETS storm-gspn EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) diff --git a/src/storm-gspn/api/storm-gspn.cpp b/src/storm-gspn/api/storm-gspn.cpp index 08796386b..7b4200189 100644 --- a/src/storm-gspn/api/storm-gspn.cpp +++ b/src/storm-gspn/api/storm-gspn.cpp @@ -3,6 +3,8 @@ #include "storm/settings/SettingsManager.h" #include "storm/utility/file.h" #include "storm-gspn/settings/modules/GSPNExportSettings.h" +#include "storm-conv/settings/modules/JaniExportSettings.h" +#include "storm-conv/api/storm-conv.h" namespace storm { @@ -13,7 +15,7 @@ namespace storm { return builder.build(); } - void handleGSPNExportSettings(storm::gspn::GSPN const& gspn) { + void handleGSPNExportSettings(storm::gspn::GSPN const& gspn, std::vector const& properties) { storm::settings::modules::GSPNExportSettings const& exportSettings = storm::settings::getModule(); if (exportSettings.isWriteToDotSet()) { std::ofstream fs; @@ -55,6 +57,16 @@ namespace storm { gspn.writeStatsToStream(fs); storm::utility::closeFile(fs); } + + if (exportSettings.isWriteToJaniSet()) { + auto const& jani = storm::settings::getModule(); + storm::converter::JaniConversionOptions options(jani); + + storm::jani::Model* model = storm::api::buildJani(gspn); + storm::api::postprocessJani(*model, options); + storm::api::exportJaniToFile(*model, properties, storm::settings::getModule().getWriteToJaniFilename()); + delete model; + } } } diff --git a/src/storm-gspn/api/storm-gspn.h b/src/storm-gspn/api/storm-gspn.h index 7687c35e4..7d2360946 100644 --- a/src/storm-gspn/api/storm-gspn.h +++ b/src/storm-gspn/api/storm-gspn.h @@ -12,6 +12,8 @@ namespace storm { */ storm::jani::Model* buildJani(storm::gspn::GSPN const& gspn); - void handleGSPNExportSettings(storm::gspn::GSPN const& gspn); + void handleGSPNExportSettings(storm::gspn::GSPN const& gspn, + std::function(storm::builder::JaniGSPNBuilder const&)> const& janiProperyGetter = [](storm::builder::JaniGSPNBuilder const&) { return std::vector(); }); + } } diff --git a/src/storm-gspn/settings/modules/GSPNExportSettings.cpp b/src/storm-gspn/settings/modules/GSPNExportSettings.cpp index 5b7653eef..295f963e2 100644 --- a/src/storm-gspn/settings/modules/GSPNExportSettings.cpp +++ b/src/storm-gspn/settings/modules/GSPNExportSettings.cpp @@ -1,5 +1,4 @@ #include "storm-gspn/settings/modules/GSPNExportSettings.h" -#include "storm/settings/modules/JaniExportSettings.h" #include "storm/settings/SettingsManager.h" #include "storm/settings/SettingMemento.h" @@ -20,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::writeToJaniOptionName = "to-jani"; const std::string GSPNExportSettings::writeStatsOptionName = "to-stats"; const std::string GSPNExportSettings::displayStatsOptionName = "show-stats"; @@ -31,6 +31,7 @@ namespace storm { 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, writeToJaniOptionName, false, "Destination for the jani 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()); } @@ -67,6 +68,14 @@ namespace storm { return this->getOption(writeToJsonOptionName).getArgumentByName("filename").getValueAsString(); } + bool GSPNExportSettings::isWriteToJaniSet() const { + return this->getOption(writeToJaniOptionName).getHasOptionBeenSet(); + } + + std::string GSPNExportSettings::getWriteToJaniFilename() const { + return this->getOption(writeToJaniOptionName).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 ce203a841..fbe45a4eb 100644 --- a/src/storm-gspn/settings/modules/GSPNExportSettings.h +++ b/src/storm-gspn/settings/modules/GSPNExportSettings.h @@ -10,7 +10,7 @@ namespace storm { class GSPNExportSettings : public ModuleSettings { public: /*! - * Creates a new JaniExport setting + * Creates a new GSPNExport setting */ GSPNExportSettings(); @@ -45,6 +45,14 @@ namespace storm { */ std::string getWriteToJsonFilename() const; + + bool isWriteToJaniSet() const; + + /** + * + */ + std::string getWriteToJaniFilename() const; + bool isDisplayStatsSet() const; bool isWriteStatsToFileSet() const; @@ -62,6 +70,7 @@ namespace storm { static const std::string writeToPnmlOptionName; static const std::string writeToPnproOptionName; static const std::string writeToJsonOptionName; + static const std::string writeToJaniOptionName; static const std::string displayStatsOptionName; static const std::string writeStatsOptionName;