From 8f179217d0502936e609d7af987d3e54f930f4b5 Mon Sep 17 00:00:00 2001 From: TimQu Date: Mon, 30 Jul 2018 20:48:53 +0200 Subject: [PATCH] fixes for storm-dft and storm-gspn --- src/storm-dft/api/storm-dft.cpp | 6 +++--- src/storm-gspn-cli/storm-gspn.cpp | 2 +- src/storm-gspn/api/storm-gspn.cpp | 9 +++++---- src/storm-gspn/builder/JaniGSPNBuilder.h | 2 +- src/storm-gspn/settings/modules/GSPNSettings.cpp | 3 --- src/storm-gspn/settings/modules/GSPNSettings.h | 2 -- 6 files changed, 10 insertions(+), 14 deletions(-) diff --git a/src/storm-dft/api/storm-dft.cpp b/src/storm-dft/api/storm-dft.cpp index 19c97a67f..72105a763 100644 --- a/src/storm-dft/api/storm-dft.cpp +++ b/src/storm-dft/api/storm-dft.cpp @@ -34,7 +34,7 @@ namespace storm { storm::gspn::GSPN* gspn = gspnTransformator.obtainGSPN(); uint64_t toplevelFailedPlace = gspnTransformator.toplevelFailedPlaceId(); - storm::api::handleGSPNExportSettings(*gspn, [&]std::vector(storm::builder::JaniGSPNBuilder const& builder) { + storm::api::handleGSPNExportSettings(*gspn, [&](storm::builder::JaniGSPNBuilder const& builder) { std::shared_ptr const& exprManager = gspn->getExpressionManager(); storm::jani::Variable const& topfailedVar = builder.getPlaceVariable(toplevelFailedPlace); @@ -45,11 +45,11 @@ namespace storm { 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)}; + std::vector res({storm::jani::Property("time-bounded", tbUntil), storm::jani::Property("mttf", rewFormula)}); + return res; } ); - delete model; delete gspn; } diff --git a/src/storm-gspn-cli/storm-gspn.cpp b/src/storm-gspn-cli/storm-gspn.cpp index aff3a8fce..4db249042 100644 --- a/src/storm-gspn-cli/storm-gspn.cpp +++ b/src/storm-gspn-cli/storm-gspn.cpp @@ -112,7 +112,7 @@ int main(const int argc, const char **argv) { gspn->setCapacities(capacities); } - storm::api::handleGSPNExportSettings(*gspn, [&]std::vector(storm::builder::JaniGSPNBuilder const&) { return properties }); + storm::api::handleGSPNExportSettings(*gspn, [&](storm::builder::JaniGSPNBuilder const&) { return properties; }); delete gspn; return 0; diff --git a/src/storm-gspn/api/storm-gspn.cpp b/src/storm-gspn/api/storm-gspn.cpp index 7b4200189..45e579db1 100644 --- a/src/storm-gspn/api/storm-gspn.cpp +++ b/src/storm-gspn/api/storm-gspn.cpp @@ -15,7 +15,7 @@ namespace storm { return builder.build(); } - void handleGSPNExportSettings(storm::gspn::GSPN const& gspn, std::vector const& properties) { + void handleGSPNExportSettings(storm::gspn::GSPN const& gspn, std::function(storm::builder::JaniGSPNBuilder const&)> const& janiProperyGetter) { storm::settings::modules::GSPNExportSettings const& exportSettings = storm::settings::getModule(); if (exportSettings.isWriteToDotSet()) { std::ofstream fs; @@ -62,12 +62,13 @@ namespace storm { auto const& jani = storm::settings::getModule(); storm::converter::JaniConversionOptions options(jani); - storm::jani::Model* model = storm::api::buildJani(gspn); + storm::builder::JaniGSPNBuilder builder(gspn); + storm::jani::Model* model = builder.build(); + storm::api::postprocessJani(*model, options); - storm::api::exportJaniToFile(*model, properties, storm::settings::getModule().getWriteToJaniFilename()); + storm::api::exportJaniToFile(*model, janiProperyGetter(builder), storm::settings::getModule().getWriteToJaniFilename()); delete model; } } - } } diff --git a/src/storm-gspn/builder/JaniGSPNBuilder.h b/src/storm-gspn/builder/JaniGSPNBuilder.h index 474d04807..db890e36c 100644 --- a/src/storm-gspn/builder/JaniGSPNBuilder.h +++ b/src/storm-gspn/builder/JaniGSPNBuilder.h @@ -21,7 +21,7 @@ namespace storm { storm::jani::Model* build(std::string const& automatonName = "gspn_automaton"); - storm::jani::Variable const& getPlaceVariable(uint64_t placeId) { + storm::jani::Variable const& getPlaceVariable(uint64_t placeId) const { return *vars.at(placeId); } diff --git a/src/storm-gspn/settings/modules/GSPNSettings.cpp b/src/storm-gspn/settings/modules/GSPNSettings.cpp index 74bd7e28f..2cca4b2f9 100644 --- a/src/storm-gspn/settings/modules/GSPNSettings.cpp +++ b/src/storm-gspn/settings/modules/GSPNSettings.cpp @@ -16,15 +16,12 @@ namespace storm { const std::string GSPNSettings::gspnFileOptionName = "gspnfile"; const std::string GSPNSettings::gspnFileOptionShortName = "gspn"; - const std::string GSPNSettings::gspnToJaniOptionName = "to-jani"; - const std::string GSPNSettings::gspnToJaniOptionShortName = "tj"; const std::string GSPNSettings::capacitiesFileOptionName = "capacitiesfile"; const std::string GSPNSettings::capacitiesFileOptionShortName = "capacities"; GSPNSettings::GSPNSettings() : ModuleSettings(moduleName) { this->addOption(storm::settings::OptionBuilder(moduleName, gspnFileOptionName, false, "Parses the GSPN.").setShortName(gspnFileOptionShortName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "path to file").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, gspnToJaniOptionName, false, "Transform to JANI.").setShortName(gspnToJaniOptionShortName).build()); this->addOption(storm::settings::OptionBuilder(moduleName, capacitiesFileOptionName, false, "Capacaties as invariants for places.").setShortName(capacitiesFileOptionShortName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "path to file").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build()); } diff --git a/src/storm-gspn/settings/modules/GSPNSettings.h b/src/storm-gspn/settings/modules/GSPNSettings.h index 161990bf8..e5128c30e 100644 --- a/src/storm-gspn/settings/modules/GSPNSettings.h +++ b/src/storm-gspn/settings/modules/GSPNSettings.h @@ -43,8 +43,6 @@ namespace storm { private: static const std::string gspnFileOptionName; static const std::string gspnFileOptionShortName; - static const std::string gspnToJaniOptionName; - static const std::string gspnToJaniOptionShortName; static const std::string capacitiesFileOptionName; static const std::string capacitiesFileOptionShortName;