From d295f6e77732c659e0b5f21d8a788b37d9e32545 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 10 Jul 2019 15:06:44 +0200 Subject: [PATCH] export of bdds into dot and text format --- resources/3rdparty/CMakeLists.txt | 2 + .../sylvan/src/sylvan_obj_bdd_storm.hpp | 2 + .../sylvan/src/sylvan_obj_mtbdd_storm.hpp | 1 + .../3rdparty/sylvan/src/sylvan_obj_storm.cpp | 16 ++ src/storm-cli-utilities/model-handling.h | 10 +- src/storm/api/export.h | 12 +- src/storm/models/symbolic/Model.cpp | 17 +- src/storm/models/symbolic/Model.h | 2 + src/storm/settings/modules/IOSettings.cpp | 11 + src/storm/settings/modules/IOSettings.h | 21 +- src/storm/storage/dd/Add.cpp | 5 + src/storm/storage/dd/Add.h | 2 + src/storm/storage/dd/Bdd.cpp | 5 + src/storm/storage/dd/Bdd.h | 2 + src/storm/storage/dd/Dd.h | 7 + src/storm/storage/dd/Odd.cpp | 5 + src/storm/storage/dd/Odd.h | 7 + src/storm/storage/dd/cudd/InternalCuddAdd.cpp | 267 +++++++++--------- src/storm/storage/dd/cudd/InternalCuddAdd.h | 8 +- src/storm/storage/dd/cudd/InternalCuddBdd.cpp | 5 + src/storm/storage/dd/cudd/InternalCuddBdd.h | 9 +- .../storage/dd/sylvan/InternalSylvanAdd.cpp | 10 +- .../storage/dd/sylvan/InternalSylvanAdd.h | 9 +- .../storage/dd/sylvan/InternalSylvanBdd.cpp | 8 +- .../storage/dd/sylvan/InternalSylvanBdd.h | 9 +- src/storm/utility/DDEncodingExporter.cpp | 35 +++ src/storm/utility/DDEncodingExporter.h | 20 ++ 27 files changed, 365 insertions(+), 142 deletions(-) create mode 100644 src/storm/utility/DDEncodingExporter.cpp create mode 100644 src/storm/utility/DDEncodingExporter.h diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt index 5fc6d8275..9710d943a 100644 --- a/resources/3rdparty/CMakeLists.txt +++ b/resources/3rdparty/CMakeLists.txt @@ -478,7 +478,9 @@ ExternalProject_Add( LOG_BUILD ON DEPENDS ${sylvan_dep} BUILD_BYPRODUCTS ${STORM_3RDPARTY_BINARY_DIR}/sylvan/src/libsylvan${STATIC_EXT} + BUILD_ALWAYS 1 ) +# BUILD ALWAYS ON due to: https://stackoverflow.com/questions/46708124/cmake-doesnt-rebuild-externalproject-on-changes ExternalProject_Get_Property(sylvan source_dir) ExternalProject_Get_Property(sylvan binary_dir) diff --git a/resources/3rdparty/sylvan/src/sylvan_obj_bdd_storm.hpp b/resources/3rdparty/sylvan/src/sylvan_obj_bdd_storm.hpp index bdb71bf81..e1e885a21 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj_bdd_storm.hpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj_bdd_storm.hpp @@ -2,6 +2,8 @@ Mtbdd toDoubleMtbdd() const; Mtbdd toInt64Mtbdd() const; Mtbdd toStormRationalNumberMtbdd() const; + +void PrintText(FILE *out) const; #if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) Mtbdd toStormRationalFunctionMtbdd() const; #endif diff --git a/resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp b/resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp index 71b6f2106..d41976f5f 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp @@ -7,6 +7,7 @@ double NonZeroCount(size_t variableCount) const; bool isValid() const; void PrintDot(FILE *out) const; std::string GetShaHash() const; +void PrintText(FILE *out) const; Mtbdd Minus(const Mtbdd &other) const; Mtbdd Divide(const Mtbdd &other) const; diff --git a/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp b/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp index efd50edb5..0420d112c 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp @@ -1,4 +1,5 @@ #include "storm_wrapper.h" +#include "sylvan_bdd.h" #include "sylvan_mtbdd_storm.h" #include "sylvan_storm_rational_number.h" #include "sylvan_storm_rational_function.h" @@ -20,6 +21,14 @@ Sylvan::initCustomMtbdd() Functions added to sylvan's Bdd class. *********************************************/ +void +Bdd::PrintText(FILE *out) const { + sylvan_serialize_reset(); + size_t v = sylvan_serialize_add(bdd); + fprintf(out, "bdd%s,", bdd&sylvan_complement?"-":"+"); + sylvan_serialize_totext(out); +} + Mtbdd Bdd::toDoubleMtbdd() const { LACE_ME; @@ -92,6 +101,13 @@ Mtbdd::PrintDot(FILE *out) const { mtbdd_fprintdot(out, mtbdd); } +void +Mtbdd::PrintText(FILE *out) const { + LACE_ME; + MTBDD dds[1] = { mtbdd }; + mtbdd_writer_totext(out, dds, 1); +} + std::string Mtbdd::GetShaHash() const { char buf[65]; diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index 1d71c3639..155707f10 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -386,7 +386,15 @@ namespace storm { template void exportDdModel(std::shared_ptr> const& model, SymbolicInput const& input) { - // Intentionally left empty. + auto ioSettings = storm::settings::getModule(); + + if (ioSettings.isExportDdSet()) { + storm::api::exportSparseModelAsDrdd(model, ioSettings.getExportDdFilename()); + } + + if (ioSettings.isExportDotSet()) { + storm::api::exportSymbolicModelAsDot(model, ioSettings.getExportDotFilename()); + } } template diff --git a/src/storm/api/export.h b/src/storm/api/export.h index 39a3ba1b3..f1342ef5a 100644 --- a/src/storm/api/export.h +++ b/src/storm/api/export.h @@ -3,6 +3,7 @@ #include "storm/settings/SettingsManager.h" #include "storm/utility/DirectEncodingExporter.h" +#include "storm/utility/DDEncodingExporter.h" #include "storm/utility/file.h" #include "storm/utility/macros.h" @@ -23,6 +24,11 @@ namespace storm { storm::exporter::explicitExportSparseModel(stream, model, parameterNames); storm::utility::closeFile(stream); } + + template + void exportSparseModelAsDrdd(std::shared_ptr> const& model, std::string const& filename) { + storm::exporter::explicitExportSymbolicModel(filename, model); + } template void exportSparseModelAsDot(std::shared_ptr> const& model, std::string const& filename) { @@ -31,6 +37,10 @@ namespace storm { model->writeDotToStream(stream); storm::utility::closeFile(stream); } - + + template + void exportSymbolicModelAsDot(std::shared_ptr> const& model, std::string const& filename) { + model->writeDotToFile(filename); + } } } diff --git a/src/storm/models/symbolic/Model.cpp b/src/storm/models/symbolic/Model.cpp index f7a9f367f..58c497109 100644 --- a/src/storm/models/symbolic/Model.cpp +++ b/src/storm/models/symbolic/Model.cpp @@ -368,7 +368,17 @@ namespace storm { bool Model::supportsParameters() const { return std::is_same::value; } - + + template + void Model::writeDotToFile(std::string const& filename) const { + + this->getTransitionMatrix().exportToDot(filename, true); + this->getInitialStates().exportToDot(filename, true); + for (auto const& lab : this->getLabels()) { + this->getStates(lab).exportToDot(filename,true); + } + } + template bool Model::hasParameters() const { if (!this->supportsParameters()) { @@ -403,7 +413,10 @@ namespace storm { std::set const& Model::getParameters() const { return parameters; } - + + + + template template typename std::enable_if::value, std::shared_ptr>>::type Model::toValueType() const { diff --git a/src/storm/models/symbolic/Model.h b/src/storm/models/symbolic/Model.h index 7b3500bd1..0146b33b8 100644 --- a/src/storm/models/symbolic/Model.h +++ b/src/storm/models/symbolic/Model.h @@ -343,6 +343,8 @@ namespace storm { template typename std::enable_if::value, std::shared_ptr>>::type toValueType() const; + void writeDotToFile(std::string const& filename) const; + protected: /*! * Sets the transition matrix of the model. diff --git a/src/storm/settings/modules/IOSettings.cpp b/src/storm/settings/modules/IOSettings.cpp index eb0602e10..43bf02306 100644 --- a/src/storm/settings/modules/IOSettings.cpp +++ b/src/storm/settings/modules/IOSettings.cpp @@ -19,6 +19,7 @@ namespace storm { const std::string IOSettings::moduleName = "io"; const std::string IOSettings::exportDotOptionName = "exportdot"; const std::string IOSettings::exportExplicitOptionName = "exportexplicit"; + const std::string IOSettings::exportDdOptionName = "exportdd"; const std::string IOSettings::exportJaniDotOptionName = "exportjanidot"; const std::string IOSettings::exportCdfOptionName = "exportcdf"; const std::string IOSettings::exportCdfOptionShortName = "cdf"; @@ -56,6 +57,8 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, exportCdfOptionName, false, "Exports the cumulative density function for reward bounded properties into a .csv file.").setIsAdvanced().setShortName(exportCdfOptionShortName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("directory", "A path to an existing directory where the cdf files will be stored.").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, exportExplicitOptionName, "", "If given, the loaded model will be written to the specified file in the drn format.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "the name of the file to which the model is to be writen.").build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, exportDdOptionName, "", "If given, the loaded model will be written to the specified file in the drdd format.") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "the name of the file to which the model is to be writen.").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, explicitOptionName, false, "Parses the model given in an explicit (sparse) representation.").setShortName(explicitOptionShortName) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("transition filename", "The name of the file from which to read the transitions.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("labeling filename", "The name of the file from which to read the state labeling.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build()); @@ -124,6 +127,14 @@ namespace storm { std::string IOSettings::getExportExplicitFilename() const { return this->getOption(exportExplicitOptionName).getArgumentByName("filename").getValueAsString(); } + + bool IOSettings::isExportDdSet() const { + return this->getOption(exportDdOptionName).getHasOptionBeenSet(); + } + + std::string IOSettings::getExportDdFilename() const { + return this->getOption(exportDdOptionName).getArgumentByName("filename").getValueAsString(); + } bool IOSettings::isExportCdfSet() const { return this->getOption(exportCdfOptionName).getHasOptionBeenSet(); diff --git a/src/storm/settings/modules/IOSettings.h b/src/storm/settings/modules/IOSettings.h index a23ade12f..e4ff6adf2 100644 --- a/src/storm/settings/modules/IOSettings.h +++ b/src/storm/settings/modules/IOSettings.h @@ -59,12 +59,26 @@ namespace storm { bool isExportExplicitSet() const; /*! - * Retrieves thename in which to write the model in explicit format, if the option was set. + * Retrieves the name in which to write the model in explicit format, if the option was set. * - * @return The name of the file in which to write the exported mode. + * @return The name of the file in which to write the exported model. */ std::string getExportExplicitFilename() const; - + + /*! + * Retrieves whether the export-to-dd option was set + * + * @return True if the export-to-explicit option was set + */ + bool isExportDdSet() const; + + /*! + * Retrieves the name in which to write the model in dd format, if the option was set. + * + * @return The name of the file in which to write the exported model. + */ + std::string getExportDdFilename() const; + /*! * Retrieves whether the cumulative density function for reward bounded properties should be exported */ @@ -308,6 +322,7 @@ namespace storm { static const std::string exportDotOptionName; static const std::string exportJaniDotOptionName; static const std::string exportExplicitOptionName; + static const std::string exportDdOptionName; static const std::string exportCdfOptionName; static const std::string exportCdfOptionShortName; static const std::string explicitOptionName; diff --git a/src/storm/storage/dd/Add.cpp b/src/storm/storage/dd/Add.cpp index 7f1cb1517..5f1b05586 100644 --- a/src/storm/storage/dd/Add.cpp +++ b/src/storm/storage/dd/Add.cpp @@ -1009,6 +1009,11 @@ namespace storm { void Add::exportToDot(std::string const& filename, bool showVariablesIfPossible) const { internalAdd.exportToDot(filename, this->getDdManager().getDdVariableNames(), showVariablesIfPossible); } + + template + void Add::exportToText(std::string const& filename) const { + internalAdd.exportToText(filename); + } template AddIterator Add::begin(bool enumerateDontCareMetaVariables) const { diff --git a/src/storm/storage/dd/Add.h b/src/storm/storage/dd/Add.h index 94a512482..2d94b07fc 100644 --- a/src/storm/storage/dd/Add.h +++ b/src/storm/storage/dd/Add.h @@ -693,6 +693,8 @@ namespace storm { * @param filename The name of the file to which the DD is to be exported. */ void exportToDot(std::string const& filename, bool showVariablesIfPossible = true) const override; + + virtual void exportToText(std::string const& filename) const override; /*! * Retrieves an iterator that points to the first meta variable assignment with a non-zero function value. diff --git a/src/storm/storage/dd/Bdd.cpp b/src/storm/storage/dd/Bdd.cpp index 62aa7ccb1..766fdaa5e 100644 --- a/src/storm/storage/dd/Bdd.cpp +++ b/src/storm/storage/dd/Bdd.cpp @@ -491,6 +491,11 @@ namespace storm { void Bdd::exportToDot(std::string const& filename, bool showVariablesIfPossible) const { internalBdd.exportToDot(filename, this->getDdManager().getDdVariableNames(), showVariablesIfPossible); } + + template + void Bdd::exportToText(std::string const& filename) const { + internalBdd.exportToText(filename); + } template Bdd Bdd::getCube(DdManager const& manager, std::set const& metaVariables) { diff --git a/src/storm/storage/dd/Bdd.h b/src/storm/storage/dd/Bdd.h index acb7e9122..09295d1ff 100644 --- a/src/storm/storage/dd/Bdd.h +++ b/src/storm/storage/dd/Bdd.h @@ -379,6 +379,8 @@ namespace storm { virtual uint_fast64_t getLevel() const override; virtual void exportToDot(std::string const& filename, bool showVariablesIfPossible = true) const override; + + virtual void exportToText(std::string const& filename) const override; /*! * Retrieves the cube of all given meta variables. diff --git a/src/storm/storage/dd/Dd.h b/src/storm/storage/dd/Dd.h index e3f7890fb..b8d774eda 100644 --- a/src/storm/storage/dd/Dd.h +++ b/src/storm/storage/dd/Dd.h @@ -103,6 +103,13 @@ namespace storm { * @param filename The name of the file to which the DD is to be exported. */ virtual void exportToDot(std::string const& filename, bool showVariablesIfPossible = true) const = 0; + + /*! + * Exports the DD to the given file in the dot format. + * + * @param filename The name of the file to which the DD is to be exported. + */ + virtual void exportToText(std::string const& filename) const = 0; /*! * Retrieves the manager that is responsible for this DD. diff --git a/src/storm/storage/dd/Odd.cpp b/src/storm/storage/dd/Odd.cpp index ff3a1a3ef..10fd878a9 100644 --- a/src/storm/storage/dd/Odd.cpp +++ b/src/storm/storage/dd/Odd.cpp @@ -11,6 +11,7 @@ #include "storm/utility/file.h" #include "storm/adapters/RationalFunctionAdapter.h" +#include "storm/exceptions/NotSupportedException.h" namespace storm { namespace dd { @@ -158,6 +159,10 @@ namespace storm { dotFile << "}" << std::endl; storm::utility::closeFile(dotFile); } + + void Odd::exportToText(std::string const& filename) const { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation not supported"); + } void getEncodingRec(Odd const& odd, uint64_t index, uint64_t offset, storm::storage::BitVector& result) { if (odd.isTerminalNode()) { diff --git a/src/storm/storage/dd/Odd.h b/src/storm/storage/dd/Odd.h index ac23142f4..03c4a1d23 100644 --- a/src/storm/storage/dd/Odd.h +++ b/src/storm/storage/dd/Odd.h @@ -133,6 +133,13 @@ namespace storm { * @param filename The name of the file to which to write the dot output. */ void exportToDot(std::string const& filename) const; + + /*! + * Exports the ODD in the text format to the given file. + * + * @param filename The name of the file to which to write the dot output. + */ + void exportToText(std::string const& filename) const; /*! * Retrieves the encoding for the given offset. diff --git a/src/storm/storage/dd/cudd/InternalCuddAdd.cpp b/src/storm/storage/dd/cudd/InternalCuddAdd.cpp index 9ed21a92a..d94e6cadc 100644 --- a/src/storm/storage/dd/cudd/InternalCuddAdd.cpp +++ b/src/storm/storage/dd/cudd/InternalCuddAdd.cpp @@ -16,173 +16,177 @@ namespace storm { namespace dd { template - InternalAdd::InternalAdd(InternalDdManager const* ddManager, cudd::ADD cuddAdd) : ddManager(ddManager), cuddAdd(cuddAdd) { + InternalAdd::InternalAdd(InternalDdManager const *ddManager, cudd::ADD cuddAdd) : ddManager(ddManager), cuddAdd(cuddAdd) { // Intentionally left empty. } - + template - bool InternalAdd::operator==(InternalAdd const& other) const { + bool InternalAdd::operator==(InternalAdd const &other) const { return this->getCuddAdd() == other.getCuddAdd(); } - + template - bool InternalAdd::operator!=(InternalAdd const& other) const { + bool InternalAdd::operator!=(InternalAdd const &other) const { return !(*this == other); } - + template - InternalAdd InternalAdd::operator+(InternalAdd const& other) const { + InternalAdd InternalAdd::operator+(InternalAdd const &other) const { return InternalAdd(ddManager, this->getCuddAdd() + other.getCuddAdd()); } - + template - InternalAdd& InternalAdd::operator+=(InternalAdd const& other) { + InternalAdd &InternalAdd::operator+=(InternalAdd const &other) { this->cuddAdd = this->getCuddAdd() + other.getCuddAdd(); return *this; } - + template - InternalAdd InternalAdd::operator*(InternalAdd const& other) const { + InternalAdd InternalAdd::operator*(InternalAdd const &other) const { return InternalAdd(ddManager, this->getCuddAdd() * other.getCuddAdd()); } - + template - InternalAdd& InternalAdd::operator*=(InternalAdd const& other) { + InternalAdd &InternalAdd::operator*=(InternalAdd const &other) { this->cuddAdd = this->getCuddAdd() * other.getCuddAdd(); return *this; } - + template - InternalAdd InternalAdd::operator-(InternalAdd const& other) const { + InternalAdd InternalAdd::operator-(InternalAdd const &other) const { return InternalAdd(ddManager, this->getCuddAdd() - other.getCuddAdd()); } - + template - InternalAdd& InternalAdd::operator-=(InternalAdd const& other) { + InternalAdd &InternalAdd::operator-=(InternalAdd const &other) { this->cuddAdd = this->getCuddAdd() - other.getCuddAdd(); return *this; } - + template - InternalAdd InternalAdd::operator/(InternalAdd const& other) const { + InternalAdd InternalAdd::operator/(InternalAdd const &other) const { return InternalAdd(ddManager, this->getCuddAdd().Divide(other.getCuddAdd())); } - + template - InternalAdd& InternalAdd::operator/=(InternalAdd const& other) { + InternalAdd &InternalAdd::operator/=(InternalAdd const &other) { this->cuddAdd = this->getCuddAdd().Divide(other.getCuddAdd()); return *this; } - + template - InternalBdd InternalAdd::equals(InternalAdd const& other) const { + InternalBdd InternalAdd::equals(InternalAdd const &other) const { return InternalBdd(ddManager, this->getCuddAdd().EqualsBdd(other.getCuddAdd())); } - + template - InternalBdd InternalAdd::notEquals(InternalAdd const& other) const { + InternalBdd InternalAdd::notEquals(InternalAdd const &other) const { return InternalBdd(ddManager, this->getCuddAdd().NotEqualsBdd(other.getCuddAdd())); } - + template - InternalBdd InternalAdd::less(InternalAdd const& other) const { + InternalBdd InternalAdd::less(InternalAdd const &other) const { return InternalBdd(ddManager, this->getCuddAdd().LessThanBdd(other.getCuddAdd())); } - + template - InternalBdd InternalAdd::lessOrEqual(InternalAdd const& other) const { + InternalBdd InternalAdd::lessOrEqual(InternalAdd const &other) const { return InternalBdd(ddManager, this->getCuddAdd().LessThanOrEqualBdd(other.getCuddAdd())); } - + template - InternalBdd InternalAdd::greater(InternalAdd const& other) const { + InternalBdd InternalAdd::greater(InternalAdd const &other) const { return InternalBdd(ddManager, this->getCuddAdd().GreaterThanBdd(other.getCuddAdd())); } - + template - InternalBdd InternalAdd::greaterOrEqual(InternalAdd const& other) const { + InternalBdd InternalAdd::greaterOrEqual(InternalAdd const &other) const { return InternalBdd(ddManager, this->getCuddAdd().GreaterThanOrEqualBdd(other.getCuddAdd())); } - + template - InternalAdd InternalAdd::pow(InternalAdd const& other) const { + InternalAdd InternalAdd::pow(InternalAdd const &other) const { return InternalAdd(ddManager, this->getCuddAdd().Pow(other.getCuddAdd())); } - + template - InternalAdd InternalAdd::mod(InternalAdd const& other) const { + InternalAdd InternalAdd::mod(InternalAdd const &other) const { return InternalAdd(ddManager, this->getCuddAdd().Mod(other.getCuddAdd())); } - + template - InternalAdd InternalAdd::logxy(InternalAdd const& other) const { + InternalAdd InternalAdd::logxy(InternalAdd const &other) const { return InternalAdd(ddManager, this->getCuddAdd().LogXY(other.getCuddAdd())); } - + template - InternalAdd InternalAdd::floor() const { + InternalAdd InternalAdd::floor() const { return InternalAdd(ddManager, this->getCuddAdd().Floor()); } - + template - InternalAdd InternalAdd::ceil() const { + InternalAdd InternalAdd::ceil() const { return InternalAdd(ddManager, this->getCuddAdd().Ceil()); } - + template - InternalAdd InternalAdd::sharpenKwekMehlhorn(size_t precision) const { + InternalAdd InternalAdd::sharpenKwekMehlhorn(size_t precision) const { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation not supported"); } - + template - InternalAdd InternalAdd::minimum(InternalAdd const& other) const { + InternalAdd InternalAdd::minimum(InternalAdd const &other) const { return InternalAdd(ddManager, this->getCuddAdd().Minimum(other.getCuddAdd())); } - + template - InternalAdd InternalAdd::maximum(InternalAdd const& other) const { + InternalAdd InternalAdd::maximum(InternalAdd const &other) const { return InternalAdd(ddManager, this->getCuddAdd().Maximum(other.getCuddAdd())); } - + template template - typename std::enable_if::value, InternalAdd>::type InternalAdd::toValueType() const { + typename std::enable_if::value, InternalAdd < DdType::CUDD, TargetValueType>> + + ::type InternalAdd::toValueType() const { return *this; } template template - typename std::enable_if::value, InternalAdd>::type InternalAdd::toValueType() const { + typename std::enable_if::value, InternalAdd < DdType::CUDD, TargetValueType>> + + ::type InternalAdd::toValueType() const { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation not supported"); } template - InternalAdd InternalAdd::sumAbstract(InternalBdd const& cube) const { + InternalAdd InternalAdd::sumAbstract(InternalBdd const &cube) const { return InternalAdd(ddManager, this->getCuddAdd().ExistAbstract(cube.toAdd().getCuddAdd())); } - + template - InternalAdd InternalAdd::minAbstract(InternalBdd const& cube) const { + InternalAdd InternalAdd::minAbstract(InternalBdd const &cube) const { return InternalAdd(ddManager, this->getCuddAdd().MinAbstract(cube.toAdd().getCuddAdd())); } - - template - InternalBdd InternalAdd::minAbstractRepresentative(InternalBdd const& cube) const { - return InternalBdd(ddManager, this->getCuddAdd().MinAbstractRepresentative(cube.toAdd().getCuddAdd())); + + template + InternalBdd InternalAdd::minAbstractRepresentative(InternalBdd const &cube) const { + return InternalBdd(ddManager, this->getCuddAdd().MinAbstractRepresentative(cube.toAdd().getCuddAdd())); } - + template - InternalAdd InternalAdd::maxAbstract(InternalBdd const& cube) const { + InternalAdd InternalAdd::maxAbstract(InternalBdd const &cube) const { return InternalAdd(ddManager, this->getCuddAdd().MaxAbstract(cube.toAdd().getCuddAdd())); } - - template - InternalBdd InternalAdd::maxAbstractRepresentative(InternalBdd const& cube) const { - return InternalBdd(ddManager, this->getCuddAdd().MaxAbstractRepresentative(cube.toAdd().getCuddAdd())); + + template + InternalBdd InternalAdd::maxAbstractRepresentative(InternalBdd const &cube) const { + return InternalBdd(ddManager, this->getCuddAdd().MaxAbstractRepresentative(cube.toAdd().getCuddAdd())); } - + template - bool InternalAdd::equalModuloPrecision(InternalAdd const& other, ValueType const& precision, bool relative) const { + bool InternalAdd::equalModuloPrecision(InternalAdd const &other, ValueType const &precision, bool relative) const { if (relative) { return this->getCuddAdd().EqualSupNormRel(other.getCuddAdd(), precision); } else { @@ -191,14 +195,14 @@ namespace storm { } template<> - bool InternalAdd::equalModuloPrecision(InternalAdd const& other, storm::RationalNumber const& precision, bool relative) const { + bool InternalAdd::equalModuloPrecision(InternalAdd const &other, storm::RationalNumber const &precision, bool relative) const { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation not supported."); } - + template - InternalAdd InternalAdd::swapVariables(std::vector> const& from, std::vector> const& to) const { - std::vector fromAdd; - std::vector toAdd; + InternalAdd InternalAdd::swapVariables(std::vector > const &from, std::vector > const &to) const { + std::vector fromAdd; + std::vector toAdd; STORM_LOG_ASSERT(fromAdd.size() == toAdd.size(), "Sizes of vectors do not match."); for (auto it1 = from.begin(), ite1 = from.end(), it2 = to.begin(); it1 != ite1; ++it1, ++it2) { fromAdd.push_back(it1->getCuddBdd().Add()); @@ -206,30 +210,30 @@ namespace storm { } return InternalAdd(ddManager, this->getCuddAdd().SwapVariables(fromAdd, toAdd)); } - + template - InternalAdd InternalAdd::permuteVariables(std::vector> const& from, std::vector> const& to) const { + InternalAdd InternalAdd::permuteVariables(std::vector > const &from, std::vector > const &to) const { // Build the full permutation. uint64_t numberOfVariables = ddManager->getCuddManager().ReadSize(); - int* permutation = new int[numberOfVariables]; + int *permutation = new int[numberOfVariables]; for (uint64_t variable = 0; variable < numberOfVariables; ++variable) { permutation[variable] = variable; } - + for (auto it1 = from.begin(), ite1 = from.end(), it2 = to.begin(); it1 != ite1; ++it1, ++it2) { permutation[it1->getIndex()] = it2->getIndex(); } - InternalAdd result(ddManager, this->getCuddAdd().Permute(permutation)); - + InternalAdd result(ddManager, this->getCuddAdd().Permute(permutation)); + delete[] permutation; return result; } - + template - InternalAdd InternalAdd::multiplyMatrix(InternalAdd const& otherMatrix, std::vector> const& summationDdVariables) const { + InternalAdd InternalAdd::multiplyMatrix(InternalAdd const &otherMatrix, std::vector > const &summationDdVariables) const { // Create the CUDD summation variables. - std::vector summationAdds; - for (auto const& ddVariable : summationDdVariables) { + std::vector summationAdds; + for (auto const &ddVariable : summationDdVariables) { summationAdds.push_back(ddVariable.toAdd().getCuddAdd()); } @@ -237,72 +241,72 @@ namespace storm { // return InternalAdd(ddManager, this->getCuddAdd().Triangle(otherMatrix.getCuddAdd(), summationAdds)); return InternalAdd(ddManager, this->getCuddAdd().MatrixMultiply(otherMatrix.getCuddAdd(), summationAdds)); } - + template - InternalAdd InternalAdd::multiplyMatrix(InternalBdd const& otherMatrix, std::vector> const& summationDdVariables) const { + InternalAdd InternalAdd::multiplyMatrix(InternalBdd const &otherMatrix, std::vector > const &summationDdVariables) const { return this->multiplyMatrix(otherMatrix.template toAdd(), summationDdVariables); } - + template - InternalBdd InternalAdd::greater(ValueType const& value) const { + InternalBdd InternalAdd::greater(ValueType const &value) const { return InternalBdd(ddManager, this->getCuddAdd().BddStrictThreshold(value)); } template<> - InternalBdd InternalAdd::greater(storm::RationalNumber const& value) const { + InternalBdd InternalAdd::greater(storm::RationalNumber const &value) const { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation not supported."); } template - InternalBdd InternalAdd::greaterOrEqual(ValueType const& value) const { + InternalBdd InternalAdd::greaterOrEqual(ValueType const &value) const { return InternalBdd(ddManager, this->getCuddAdd().BddThreshold(value)); } template<> - InternalBdd InternalAdd::greaterOrEqual(storm::RationalNumber const& value) const { + InternalBdd InternalAdd::greaterOrEqual(storm::RationalNumber const &value) const { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation not supported."); } - + template - InternalBdd InternalAdd::less(ValueType const& value) const { + InternalBdd InternalAdd::less(ValueType const &value) const { return InternalBdd(ddManager, ~this->getCuddAdd().BddThreshold(value)); } - + template<> - InternalBdd InternalAdd::less(storm::RationalNumber const& value) const { + InternalBdd InternalAdd::less(storm::RationalNumber const &value) const { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation not supported."); } - + template - InternalBdd InternalAdd::lessOrEqual(ValueType const& value) const { + InternalBdd InternalAdd::lessOrEqual(ValueType const &value) const { return InternalBdd(ddManager, ~this->getCuddAdd().BddStrictThreshold(value)); } - + template<> - InternalBdd InternalAdd::lessOrEqual(storm::RationalNumber const& value) const { + InternalBdd InternalAdd::lessOrEqual(storm::RationalNumber const &value) const { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation not supported."); } - + template - InternalBdd InternalAdd::notZero() const { + InternalBdd InternalAdd::notZero() const { return InternalBdd(ddManager, this->getCuddAdd().BddPattern()); } - + template - InternalAdd InternalAdd::constrain(InternalAdd const& constraint) const { + InternalAdd InternalAdd::constrain(InternalAdd const &constraint) const { return InternalAdd(ddManager, this->getCuddAdd().Constrain(constraint.getCuddAdd())); } - + template - InternalAdd InternalAdd::restrict(InternalAdd const& constraint) const { + InternalAdd InternalAdd::restrict(InternalAdd const &constraint) const { return InternalAdd(ddManager, this->getCuddAdd().Restrict(constraint.getCuddAdd())); } - + template - InternalBdd InternalAdd::getSupport() const { + InternalBdd InternalAdd::getSupport() const { return InternalBdd(ddManager, this->getCuddAdd().Support()); } - + template uint_fast64_t InternalAdd::getNonZeroCount(uint_fast64_t numberOfDdVariables) const { // If the number of DD variables is zero, CUDD returns a number greater 0 for constant nodes different from @@ -312,93 +316,98 @@ namespace storm { } return static_cast(this->getCuddAdd().CountMinterm(static_cast(numberOfDdVariables))); } - + template uint_fast64_t InternalAdd::getLeafCount() const { return static_cast(this->getCuddAdd().CountLeaves()); } - + template uint_fast64_t InternalAdd::getNodeCount() const { return static_cast(this->getCuddAdd().nodeCount()); } - + template ValueType InternalAdd::getMin() const { cudd::ADD constantMinAdd = this->getCuddAdd().FindMin(); return storm::utility::convertNumber(Cudd_V(constantMinAdd.getNode())); } - + template ValueType InternalAdd::getMax() const { cudd::ADD constantMaxAdd = this->getCuddAdd().FindMax(); return storm::utility::convertNumber(Cudd_V(constantMaxAdd.getNode())); } - + template ValueType InternalAdd::getValue() const { return storm::utility::convertNumber(Cudd_V(this->getCuddAdd().getNode())); } - + template bool InternalAdd::isOne() const { return this->getCuddAdd().IsOne(); } - + template bool InternalAdd::isZero() const { return this->getCuddAdd().IsZero(); } - + template bool InternalAdd::isConstant() const { return Cudd_IsConstant(this->getCuddAdd().getNode()); } - + template uint_fast64_t InternalAdd::getIndex() const { return static_cast(this->getCuddAdd().NodeReadIndex()); } - + template uint_fast64_t InternalAdd::getLevel() const { return static_cast(ddManager->getCuddManager().ReadPerm(this->getIndex())); } - + template - void InternalAdd::exportToDot(std::string const& filename, std::vector const& ddVariableNamesAsStrings, bool showVariablesIfPossible) const { + void InternalAdd::exportToDot(std::string const &filename, std::vector const &ddVariableNamesAsStrings, bool showVariablesIfPossible) const { // Build the name input of the DD. - std::vector ddNames; + std::vector ddNames; std::string ddName("f"); ddNames.push_back(new char[ddName.size() + 1]); std::copy(ddName.c_str(), ddName.c_str() + 2, ddNames.back()); - + // Now build the variables names. - std::vector ddVariableNames; - for (auto const& element : ddVariableNamesAsStrings) { + std::vector ddVariableNames; + for (auto const &element : ddVariableNamesAsStrings) { ddVariableNames.push_back(new char[element.size() + 1]); std::copy(element.c_str(), element.c_str() + element.size() + 1, ddVariableNames.back()); } - + // Open the file, dump the DD and close it again. - FILE* filePointer = fopen(filename.c_str() , "w"); - std::vector cuddAddVector = { this->getCuddAdd() }; + FILE *filePointer = fopen(filename.c_str(), "w"); + std::vector cuddAddVector = {this->getCuddAdd()}; if (showVariablesIfPossible) { ddManager->getCuddManager().DumpDot(cuddAddVector, ddVariableNames.data(), &ddNames[0], filePointer); } else { ddManager->getCuddManager().DumpDot(cuddAddVector, nullptr, &ddNames[0], filePointer); } fclose(filePointer); - + // Finally, delete the names. - for (char* element : ddNames) { + for (char *element : ddNames) { delete[] element; } - for (char* element : ddVariableNames) { + for (char *element : ddVariableNames) { delete[] element; } } - + + template + void InternalAdd::exportToText(std::string const &) const { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation not supported"); + } + template AddIterator InternalAdd::begin(DdManager const& fullDdManager, InternalBdd const&, uint_fast64_t, std::set const& metaVariables, bool enumerateDontCareMetaVariables) const { int* cube; diff --git a/src/storm/storage/dd/cudd/InternalCuddAdd.h b/src/storm/storage/dd/cudd/InternalCuddAdd.h index e5af927e8..21788a7a7 100644 --- a/src/storm/storage/dd/cudd/InternalCuddAdd.h +++ b/src/storm/storage/dd/cudd/InternalCuddAdd.h @@ -515,7 +515,13 @@ namespace storm { * @param ddVariableNamesAsString The names of the DD variables to display in the dot file. */ void exportToDot(std::string const& filename, std::vector const& ddVariableNamesAsStrings, bool showVariablesIfPossible = true) const; - + + /*! + * Exports the DD to the given file in a textual format as specified in Sylvan. + * + * @param filename The name of the file to which the DD is to be exported. + */ + void exportToText(std::string const& filename) const; /*! * Retrieves an iterator that points to the first meta variable assignment with a non-zero function value. * diff --git a/src/storm/storage/dd/cudd/InternalCuddBdd.cpp b/src/storm/storage/dd/cudd/InternalCuddBdd.cpp index 41aee2517..a850d6329 100644 --- a/src/storm/storage/dd/cudd/InternalCuddBdd.cpp +++ b/src/storm/storage/dd/cudd/InternalCuddBdd.cpp @@ -9,6 +9,7 @@ #include "storm/storage/PairHash.h" #include "storm/utility/macros.h" +#include "storm/exceptions/NotSupportedException.h" namespace storm { namespace dd { @@ -211,6 +212,10 @@ namespace storm { delete element; } } + + void InternalBdd::exportToText(std::string const&) const { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation not supported"); + } cudd::BDD InternalBdd::getCuddBdd() const { return this->cuddBdd; diff --git a/src/storm/storage/dd/cudd/InternalCuddBdd.h b/src/storm/storage/dd/cudd/InternalCuddBdd.h index 2a8d8dd52..203204c6a 100644 --- a/src/storm/storage/dd/cudd/InternalCuddBdd.h +++ b/src/storm/storage/dd/cudd/InternalCuddBdd.h @@ -328,7 +328,14 @@ namespace storm { * @param ddVariableNamesAsStrings The names of the variables to display in the dot file. */ void exportToDot(std::string const& filename, std::vector const& ddVariableNamesAsStrings, bool showVariablesIfPossible = true) const; - + + /*! + * Exports the DD to the given file in a textual format as specified in Sylvan. + * + * @param filename The name of the file to which the DD is to be exported. + */ + void exportToText(std::string const& filename) const; + /*! * Converts a BDD to an equivalent ADD. * diff --git a/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp b/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp index fc0829f22..8ede93854 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp +++ b/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp @@ -802,10 +802,18 @@ namespace storm { template void InternalAdd::exportToDot(std::string const& filename, std::vector const&, bool) const { // Open the file, dump the DD and close it again. - FILE* filePointer = fopen(filename.c_str() , "w"); + FILE* filePointer = fopen(filename.c_str() , "a+"); this->sylvanMtbdd.PrintDot(filePointer); fclose(filePointer); } + + template + void InternalAdd::exportToText(std::string const& filename) const { + // Open the file, dump the DD and close it again. + FILE* filePointer = fopen(filename.c_str() , "a+"); + this->sylvanMtbdd.PrintText(filePointer); + fclose(filePointer); + } template AddIterator InternalAdd::begin(DdManager const& fullDdManager, InternalBdd const& variableCube, uint_fast64_t numberOfDdVariables, std::set const& metaVariables, bool enumerateDontCareMetaVariables) const { diff --git a/src/storm/storage/dd/sylvan/InternalSylvanAdd.h b/src/storm/storage/dd/sylvan/InternalSylvanAdd.h index ccdc61414..6e9238481 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanAdd.h +++ b/src/storm/storage/dd/sylvan/InternalSylvanAdd.h @@ -506,6 +506,13 @@ namespace storm { * @param ddVariableNamesAsString The names of the DD variables to display in the dot file. */ void exportToDot(std::string const& filename, std::vector const& ddVariableNamesAsStrings, bool showVariablesIfPossible = true) const; + + /*! + * Exports the DD to the given file in a textual format as specified in Sylvan. + * + * @param filename The name of the file to which the DD is to be exported. + */ + void exportToText(std::string const& filename) const; /*! * Retrieves an iterator that points to the first meta variable assignment with a non-zero function value. @@ -778,7 +785,7 @@ namespace storm { #ifdef STORM_HAVE_CARL /*! - * Retrieves the sylvan representation of the given storm::RatíonalFunction. + * Retrieves the sylvan representation of the given storm::Rat�onalFunction. * * @return The sylvan node for the given value. */ diff --git a/src/storm/storage/dd/sylvan/InternalSylvanBdd.cpp b/src/storm/storage/dd/sylvan/InternalSylvanBdd.cpp index 2ca68d944..7f511770d 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanBdd.cpp +++ b/src/storm/storage/dd/sylvan/InternalSylvanBdd.cpp @@ -233,10 +233,16 @@ namespace storm { } void InternalBdd::exportToDot(std::string const& filename, std::vector const&, bool) const { - FILE* filePointer = fopen(filename.c_str() , "w"); + FILE* filePointer = fopen(filename.c_str() , "a+"); this->sylvanBdd.PrintDot(filePointer); fclose(filePointer); } + + void InternalBdd::exportToText(std::string const& filename) const { + FILE* filePointer = fopen(filename.c_str() , "a+"); + this->sylvanBdd.PrintText(filePointer); + fclose(filePointer); + } sylvan::Bdd& InternalBdd::getSylvanBdd() { return sylvanBdd; diff --git a/src/storm/storage/dd/sylvan/InternalSylvanBdd.h b/src/storm/storage/dd/sylvan/InternalSylvanBdd.h index e5c5a3df2..0dadbf8a4 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanBdd.h +++ b/src/storm/storage/dd/sylvan/InternalSylvanBdd.h @@ -317,7 +317,14 @@ namespace storm { * @param ddVariableNamesAsStrings The names of the variables to display in the dot file. */ void exportToDot(std::string const& filename, std::vector const& ddVariableNamesAsStrings, bool showVariablesIfPossible = true) const; - + + /*! + * Exports the DD to the given file in a textual format as specified in Sylvan. + * + * @param filename The name of the file to which the DD is to be exported. + */ + void exportToText(std::string const& filename) const; + /*! * Converts a BDD to an equivalent ADD. * diff --git a/src/storm/utility/DDEncodingExporter.cpp b/src/storm/utility/DDEncodingExporter.cpp new file mode 100644 index 000000000..89cbdb56e --- /dev/null +++ b/src/storm/utility/DDEncodingExporter.cpp @@ -0,0 +1,35 @@ +#include "storm/utility/DDEncodingExporter.h" +#include "storm/utility/file.h" + + +namespace storm { + namespace exporter { + + + template + void explicitExportSymbolicModel(std::string const& filename, std::shared_ptr > symbolicModel) { + std::ofstream filestream; + storm::utility::openFile(filename,filestream); + filestream << "// storm exported dd" << std::endl; + filestream << "%transitions" << std::endl; + storm::utility::closeFile(filestream); + symbolicModel->getTransitionMatrix().exportToText(filename); + storm::utility::openFile(filename,filestream,true,true); + filestream << "%initial" << std::endl; + storm::utility::closeFile(filestream); + symbolicModel->getInitialStates().exportToText(filename); + for(auto const& label : symbolicModel->getLabels()) { + storm::utility::openFile(filename,filestream,true,true); + filestream << std::endl << "%label " << label << std::endl; + storm::utility::closeFile(filestream); + symbolicModel->getStates(label).exportToText(filename); + } + } + + template void explicitExportSymbolicModel(std::string const&, std::shared_ptr> sparseModel); + template void explicitExportSymbolicModel(std::string const&, std::shared_ptr> sparseModel); + + template void explicitExportSymbolicModel(std::string const&, std::shared_ptr> sparseModel); + template void explicitExportSymbolicModel(std::string const&, std::shared_ptr> sparseModel); + } +} \ No newline at end of file diff --git a/src/storm/utility/DDEncodingExporter.h b/src/storm/utility/DDEncodingExporter.h new file mode 100644 index 000000000..0e92b13e7 --- /dev/null +++ b/src/storm/utility/DDEncodingExporter.h @@ -0,0 +1,20 @@ +#pragma once + +#include "storm/models/symbolic/Model.h" + +namespace storm { + namespace exporter { + + /*! + * Exports a sparse model into the explicit drdd format. + * + * @param filename File path + * @param symbolicModel Model to export + */ + template + void explicitExportSymbolicModel(std::string const& filename, std::shared_ptr> symbolicModel); + + + + } +} \ No newline at end of file