From eea940b625da4a5c094f2290d5302676302be679 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 21 Jun 2018 13:36:08 +0200 Subject: [PATCH] Refactoring for transformation DFT->GSPN->JANI --- src/storm-dft-cli/storm-dft.cpp | 10 +++++++++- src/storm-dft/api/storm-dft.cpp | 21 ++++++++++---------- src/storm-dft/api/storm-dft.h | 35 ++++++++++++++++++++++++--------- 3 files changed, 45 insertions(+), 21 deletions(-) diff --git a/src/storm-dft-cli/storm-dft.cpp b/src/storm-dft-cli/storm-dft.cpp index 4ded8bf55..1d7f52ffc 100644 --- a/src/storm-dft-cli/storm-dft.cpp +++ b/src/storm-dft-cli/storm-dft.cpp @@ -52,7 +52,15 @@ void processOptions() { if (dftGspnSettings.isTransformToGspn()) { // Transform to GSPN - storm::api::transformToGSPN(*dft); + std::pair, uint64_t> pair = storm::api::transformToGSPN(*dft); + std::shared_ptr gspn = pair.first; + uint64_t toplevelFailedPlace = pair.second; + + // Export + storm::api::handleGSPNExportSettings(*gspn); + + // Transform to Jani + std::shared_ptr model = storm::api::transformToJani(*gspn, toplevelFailedPlace); return; } diff --git a/src/storm-dft/api/storm-dft.cpp b/src/storm-dft/api/storm-dft.cpp index fb6994224..9d0b88fed 100644 --- a/src/storm-dft/api/storm-dft.cpp +++ b/src/storm-dft/api/storm-dft.cpp @@ -29,7 +29,7 @@ namespace storm { } template<> - void transformToGSPN(storm::storage::DFT const& dft) { + std::pair, uint64_t> transformToGSPN(storm::storage::DFT const& dft) { storm::settings::modules::FaultTreeSettings const& ftSettings = storm::settings::getModule(); storm::settings::modules::DftGspnSettings const& dftGspnSettings = storm::settings::getModule(); @@ -46,15 +46,15 @@ namespace storm { storm::transformations::dft::DftToGspnTransformator gspnTransformator(dft); auto priorities = gspnTransformator.computePriorities(); gspnTransformator.transform(priorities, dontCareElements, !dftGspnSettings.isDisableSmartTransformation(), dftGspnSettings.isMergeDCFailed()); - storm::gspn::GSPN* gspn = gspnTransformator.obtainGSPN(); - uint64_t toplevelFailedPlace = gspnTransformator.toplevelFailedPlaceId(); + std::shared_ptr gspn(gspnTransformator.obtainGSPN()); + return std::make_pair(gspn, gspnTransformator.toplevelFailedPlaceId()); + } - // Export - storm::api::handleGSPNExportSettings(*gspn); + std::shared_ptr transformToJani(storm::gspn::GSPN const& gspn, uint64_t toplevelFailedPlace) { + storm::builder::JaniGSPNBuilder builder(gspn); + std::shared_ptr model(builder.build()); - std::shared_ptr const& exprManager = gspn->getExpressionManager(); - storm::builder::JaniGSPNBuilder builder(*gspn); - storm::jani::Model* model = builder.build(); + 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(); @@ -70,12 +70,11 @@ namespace storm { storm::api::exportJaniModel(*model, {storm::jani::Property("time-bounded", tbUntil), storm::jani::Property("mttf", rewFormula)}, janiSettings.getJaniFilename()); } - delete model; - delete gspn; + return model; } template<> - void transformToGSPN(storm::storage::DFT const& dft) { + std::pair, uint64_t> transformToGSPN(storm::storage::DFT const& dft) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Transformation to GSPN not supported for this data type."); } diff --git a/src/storm-dft/api/storm-dft.h b/src/storm-dft/api/storm-dft.h index db6d7b3e4..3746923bd 100644 --- a/src/storm-dft/api/storm-dft.h +++ b/src/storm-dft/api/storm-dft.h @@ -24,7 +24,7 @@ namespace storm { */ template std::shared_ptr> loadDFTGalileo(std::string const& file) { - return std::make_shared>(storm::parser::DFTGalileoParser::parseDFT(file)); + return std::make_shared>(storm::parser::DFTGalileoParser::parseDFT(file)); } /*! @@ -36,8 +36,8 @@ namespace storm { */ template std::shared_ptr> loadDFTJson(std::string const& file) { - storm::parser::DFTJsonParser parser; - return std::make_shared>(parser.parseJson(file)); + storm::parser::DFTJsonParser parser; + return std::make_shared>(parser.parseJson(file)); } /*! @@ -52,8 +52,10 @@ namespace storm { * * @return Result. */ - template - typename storm::modelchecker::DFTModelChecker::dft_results analyzeDFT(storm::storage::DFT const& dft, std::vector> const& properties, bool symred, bool allowModularisation, bool enableDC, bool printOutput) { + template + typename storm::modelchecker::DFTModelChecker::dft_results + analyzeDFT(storm::storage::DFT const& dft, std::vector> const& properties, bool symred, bool allowModularisation, + bool enableDC, bool printOutput) { storm::modelchecker::DFTModelChecker modelChecker; typename storm::modelchecker::DFTModelChecker::dft_results results = modelChecker.check(dft, properties, symred, allowModularisation, enableDC, 0.0); if (printOutput) { @@ -76,10 +78,13 @@ namespace storm { * * @return Result. */ - template - typename storm::modelchecker::DFTModelChecker::dft_results analyzeDFTApprox(storm::storage::DFT const& dft, std::vector> const& properties, bool symred, bool allowModularisation, bool enableDC, double approximationError, bool printOutput) { + template + typename storm::modelchecker::DFTModelChecker::dft_results + analyzeDFTApprox(storm::storage::DFT const& dft, std::vector> const& properties, bool symred, + bool allowModularisation, bool enableDC, double approximationError, bool printOutput) { storm::modelchecker::DFTModelChecker modelChecker; - typename storm::modelchecker::DFTModelChecker::dft_results results = modelChecker.check(dft, properties, symred, allowModularisation, enableDC, approximationError); + typename storm::modelchecker::DFTModelChecker::dft_results results = modelChecker.check(dft, properties, symred, allowModularisation, enableDC, + approximationError); if (printOutput) { modelChecker.printTimings(); modelChecker.printResults(); @@ -109,9 +114,21 @@ namespace storm { * Transform DFT to GSPN. * * @param dft DFT. + * + * @return Pair of GSPN and id of failed place corresponding to the top level element. */ template - void transformToGSPN(storm::storage::DFT const& dft); + std::pair, uint64_t> transformToGSPN(storm::storage::DFT const& dft); + + /*! + * Transform GSPN to Jani model. + * + * @param gspn GSPN. + * @param toplevelFailedPlace Id of the failed place in the GSPN for the top level element in the DFT. + * + * @return JANI model. + */ + std::shared_ptr transformToJani(storm::gspn::GSPN const& gspn, uint64_t toplevelFailedPlace); } }