diff --git a/src/storm-dft/api/storm-dft.cpp b/src/storm-dft/api/storm-dft.cpp new file mode 100644 index 000000000..91632739e --- /dev/null +++ b/src/storm-dft/api/storm-dft.cpp @@ -0,0 +1,67 @@ +#include "storm-dft/api/storm-dft.h" + +namespace storm { + namespace api { + + template<> + void exportDFTToJson(storm::storage::DFT const& dft, std::string const& file) { + storm::storage::DftJsonExporter::toFile(dft, file); + } + + template<> + void exportDFTToJson(storm::storage::DFT const& dft, std::string const& file) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Export to JSON not supported for this data type."); + } + + template<> + void exportDFTToSMT(storm::storage::DFT const& dft, std::string const& file) { + storm::modelchecker::DFTASFChecker asfChecker(dft); + asfChecker.convert(); + asfChecker.toFile(file); + } + + template<> + void exportDFTToSMT(storm::storage::DFT const& dft, std::string const& file) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Export to SMT does not support this data type."); + } + + template<> + void transformToGSPN(storm::storage::DFT const& dft) { + // Transform to GSPN + storm::transformations::dft::DftToGspnTransformator gspnTransformator(dft); + bool smart = true; + gspnTransformator.transform(smart); + 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()); + } + + delete model; + delete gspn; + } + + template<> + void 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 fe9a51917..003c03f14 100644 --- a/src/storm-dft/api/storm-dft.h +++ b/src/storm-dft/api/storm-dft.h @@ -83,18 +83,6 @@ namespace storm { return results; } - - /*! - * Export DFT to JSON file. - * - * @param dft DFT. - * @param file File. - */ - template - typename std::enable_if::value, void>::type exportDFTToJson(storm::storage::DFT const& dft, std::string const& file) { - storm::storage::DftJsonExporter::toFile(dft, file); - } - /*! * Export DFT to JSON file. * @@ -102,22 +90,7 @@ namespace storm { * @param file File. */ template - typename std::enable_if::value, void>::type exportDFTToJson(storm::storage::DFT const& dft, std::string const& file) { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Export to JSON not supported for this data type."); - } - - /*! - * Export DFT to SMT encoding. - * - * @param dft DFT. - * @param file File. - */ - template - typename std::enable_if::value, void>::type exportDFTToSMT(storm::storage::DFT const& dft, std::string const& file) { - storm::modelchecker::DFTASFChecker asfChecker(dft); - asfChecker.convert(); - asfChecker.toFile(file); - } + void exportDFTToJson(storm::storage::DFT const& dft, std::string const& file); /*! * Export DFT to SMT encoding. @@ -126,47 +99,7 @@ namespace storm { * @param file File. */ template - typename std::enable_if::value, void>::type exportDFTToSMT(storm::storage::DFT const& dft, std::string const& file) { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Export to SMT does not support this data type."); - } - - /*! - * Transform DFT to GSPN. - * - * @param dft DFT. - */ - template - typename std::enable_if::value, void>::type transformToGSPN(storm::storage::DFT const& dft) { - // Transform to GSPN - storm::transformations::dft::DftToGspnTransformator gspnTransformator(dft); - bool smart = true; - gspnTransformator.transform(smart); - 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()); - } - - delete model; - delete gspn; - } + void exportDFTToSMT(storm::storage::DFT const& dft, std::string const& file); /*! * Transform DFT to GSPN. @@ -174,9 +107,7 @@ namespace storm { * @param dft DFT. */ template - typename std::enable_if::value, void>::type transformToGSPN(storm::storage::DFT const& dft) { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Transformation to GSPN not supported for this data type."); - } + void transformToGSPN(storm::storage::DFT const& dft); } }