From 9eed8b9f9447d467a0097075012f52a39255244e Mon Sep 17 00:00:00 2001 From: Mavo Date: Thu, 14 Jul 2016 15:33:13 +0200 Subject: [PATCH] Added framework for DFT->GSPN Transformator Former-commit-id: de0fd505732fcc54160b38a9fff8cb8097f07920 --- src/storm/settings/modules/DFTSettings.cpp | 7 +++++ src/storm/settings/modules/DFTSettings.h | 8 ++++++ src/storm/storm-dyftee.cpp | 27 +++++++++++++++++++ .../dft/DftToGspnTransformator.cpp | 26 +++++++++++++++++- .../dft/DftToGspnTransformator.h | 24 ++++++++++++++++- 5 files changed, 90 insertions(+), 2 deletions(-) diff --git a/src/storm/settings/modules/DFTSettings.cpp b/src/storm/settings/modules/DFTSettings.cpp index c7faca861..7799c00d9 100644 --- a/src/storm/settings/modules/DFTSettings.cpp +++ b/src/storm/settings/modules/DFTSettings.cpp @@ -33,6 +33,8 @@ namespace storm { const std::string DFTSettings::solveWithSmtOptionName = "smt"; #endif + const std::string DFTSettings::transformToGspnOptionName = "gspn"; + DFTSettings::DFTSettings() : ModuleSettings(moduleName) { this->addOption(storm::settings::OptionBuilder(moduleName, dftFileOptionName, false, "Parses the model given in the Galileo format.").setShortName(dftFileOptionShortName) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the DFT model.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); @@ -49,6 +51,7 @@ namespace storm { #ifdef STORM_HAVE_Z3 this->addOption(storm::settings::OptionBuilder(moduleName, solveWithSmtOptionName, true, "Solve the DFT with SMT.").build()); #endif + this->addOption(storm::settings::OptionBuilder(moduleName, transformToGspnOptionName, false, "Transform DFT to GSPN.").build()); } bool DFTSettings::isDftFileSet() const { @@ -123,6 +126,10 @@ namespace storm { } #endif + bool DFTSettings::isTransformToGspn() const { + return this->getOption(transformToGspnOptionName).getHasOptionBeenSet(); + } + void DFTSettings::finalize() { } diff --git a/src/storm/settings/modules/DFTSettings.h b/src/storm/settings/modules/DFTSettings.h index 433366bb8..e18d626ca 100644 --- a/src/storm/settings/modules/DFTSettings.h +++ b/src/storm/settings/modules/DFTSettings.h @@ -117,6 +117,13 @@ namespace storm { * @return The timebound. */ double getPropTimebound() const; + + /*! + * Retrieves whether the DFT should be transformed into a GSPN. + * + * @return True iff the option was set. + */ + bool isTransformToGspn() const; #ifdef STORM_HAVE_Z3 /*! @@ -153,6 +160,7 @@ namespace storm { #ifdef STORM_HAVE_Z3 static const std::string solveWithSmtOptionName; #endif + static const std::string transformToGspnOptionName; }; diff --git a/src/storm/storm-dyftee.cpp b/src/storm/storm-dyftee.cpp index 404bf1af6..987e5eb45 100644 --- a/src/storm/storm-dyftee.cpp +++ b/src/storm/storm-dyftee.cpp @@ -9,6 +9,8 @@ #include "storm/exceptions/BaseException.h" #include "storm/utility/macros.h" #include "storm/builder/DftSmtBuilder.h" +#include "storm/transformations/dft/DftToGspnTransformator.h" + #include "storm/settings/modules/GeneralSettings.h" #include "storm/settings/modules/DFTSettings.h" @@ -34,6 +36,9 @@ * * @param filename Path to DFT file in Galileo format. * @param property PCTC formula capturing the property to check. + * @param symred Flag whether symmetry reduction should be used. + * @param allowModularisation Flag whether modularisation should be applied if possible. + * @param enableDC Flag whether Don't Care propagation should be used. */ template void analyzeDFT(std::string filename, std::string property, bool symred, bool allowModularisation, bool enableDC, double approximationError) { @@ -68,6 +73,21 @@ void analyzeWithSMT(std::string filename) { //std::cout << "SMT result: " << sat << std::endl; } +/*! + * Load DFT from filename and transform into a GSPN. + * + * @param filename Path to DFT file in Galileo format. + * + */ +template +void transformDFT(std::string filename) { + std::cout << "Transforming DFT from file " << filename << std::endl; + storm::parser::DFTGalileoParser parser; + storm::storage::DFT dft = parser.parseDFT(filename); + storm::transformations::dft::DftToGspnTransformator gspnTransformator(dft); + gspnTransformator.transform(); +} + /*! * Initialize the settings manager. */ @@ -116,6 +136,13 @@ int main(const int argc, const char** argv) { if (!dftSettings.isDftFileSet()) { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model."); } + + if (dftSettings.isTransformToGspn()) { + // For now we only transform the DFT to a GSPN and then exit + transformDFT(dftSettings.getDftFilename()); + storm::utility::cleanUp(); + return 0; + } bool parametric = false; #ifdef STORM_HAVE_CARL diff --git a/src/transformations/dft/DftToGspnTransformator.cpp b/src/transformations/dft/DftToGspnTransformator.cpp index 5ad88338d..1724146a8 100644 --- a/src/transformations/dft/DftToGspnTransformator.cpp +++ b/src/transformations/dft/DftToGspnTransformator.cpp @@ -1,4 +1,5 @@ #include "src/transformations/dft/DftToGspnTransformator.h" +#include "src/exceptions/NotImplementedException.h" namespace storm { namespace transformations { @@ -9,12 +10,35 @@ namespace storm { // Intentionally left empty } + template + void DftToGspnTransformator::transform() { + mGspn = storm::gspn::GSPN(); + + // For debugging purposes + writeGspn(false); + + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "The transformation to GSPN is not yet implemented."); + } + + template + void DftToGspnTransformator::writeGspn(bool toFile) { + if (toFile) { + // Writing to file + std::ofstream file; + file.open("gspn.dot"); + mGspn.writeDotToStream(file); + file.close(); + } else { + // Writing to console + mGspn.writeDotToStream(std::cout); + } + } // Explicitly instantiate the class. template class DftToGspnTransformator; #ifdef STORM_HAVE_CARL - template class DftToGspnTransformator; + // template class DftToGspnTransformator; #endif } // namespace dft diff --git a/src/transformations/dft/DftToGspnTransformator.h b/src/transformations/dft/DftToGspnTransformator.h index fdc368a66..6790d894e 100644 --- a/src/transformations/dft/DftToGspnTransformator.h +++ b/src/transformations/dft/DftToGspnTransformator.h @@ -2,21 +2,43 @@ #define DFTTOGSPNTRANSFORMATOR_H #include +#include "src/storage/gspn/GSPN.h" namespace storm { namespace transformations { namespace dft { + /*! + * Transformator for DFT -> GSPN. + */ template class DftToGspnTransformator { public: + /*! + * Constructor. + * + * @param dft DFT + */ DftToGspnTransformator(storm::storage::DFT const& dft); + /*! + * Transform the DFT to a GSPN. + */ + void transform(); + private: storm::storage::DFT const& mDft; - + storm::gspn::GSPN mGspn; + + /*! + * Write Gspn to file or console. + * + * @param toFile If true, the GSPN will be written to a file, otherwise it will + be written to the console. + */ + void writeGspn(bool toFile); }; } }