From d295f6e77732c659e0b5f21d8a788b37d9e32545 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 10 Jul 2019 15:06:44 +0200 Subject: [PATCH 01/13] 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 From 6ce429efc48c3cd23edc32fed756920ff27fe313 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 12 Jul 2019 10:23:22 +0200 Subject: [PATCH 02/13] Added missing include --- src/storm/utility/DDEncodingExporter.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm/utility/DDEncodingExporter.cpp b/src/storm/utility/DDEncodingExporter.cpp index 89cbdb56e..ba2082f66 100644 --- a/src/storm/utility/DDEncodingExporter.cpp +++ b/src/storm/utility/DDEncodingExporter.cpp @@ -1,6 +1,6 @@ #include "storm/utility/DDEncodingExporter.h" #include "storm/utility/file.h" - +#include "storm/models/symbolic/StandardRewardModel.h" namespace storm { namespace exporter { From 4f063cd2331ba714a7ac30e2b59d2358544f374c Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Thu, 11 Jul 2019 20:36:57 +0200 Subject: [PATCH 03/13] tackling problems on unix --- src/storm/utility/DDEncodingExporter.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/storm/utility/DDEncodingExporter.cpp b/src/storm/utility/DDEncodingExporter.cpp index ba2082f66..bb897ec6d 100644 --- a/src/storm/utility/DDEncodingExporter.cpp +++ b/src/storm/utility/DDEncodingExporter.cpp @@ -17,12 +17,12 @@ namespace storm { storm::utility::openFile(filename,filestream,true,true); filestream << "%initial" << std::endl; storm::utility::closeFile(filestream); - symbolicModel->getInitialStates().exportToText(filename); + symbolicModel->getInitialStates().template toAdd().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); + symbolicModel->getStates(label).template toAdd().exportToText(filename); } } From f5b6bc84ba1d4921c9b00f8571c1f9476d852a75 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Fri, 12 Jul 2019 10:38:05 +0200 Subject: [PATCH 04/13] circumvent problems with the bdd export --- src/storm/utility/DDEncodingExporter.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm/utility/DDEncodingExporter.cpp b/src/storm/utility/DDEncodingExporter.cpp index bb897ec6d..7ad4c303c 100644 --- a/src/storm/utility/DDEncodingExporter.cpp +++ b/src/storm/utility/DDEncodingExporter.cpp @@ -32,4 +32,4 @@ namespace storm { 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 +} From 9ad8209a650caad894ee8ed4249165245867dbde Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Tue, 16 Jul 2019 16:04:07 +0200 Subject: [PATCH 05/13] clarify that a formula needs to be added to do anything in storm-pomdp --- src/storm-pomdp-cli/storm-pomdp.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/storm-pomdp-cli/storm-pomdp.cpp b/src/storm-pomdp-cli/storm-pomdp.cpp index 075a1e7dc..ec888bd02 100644 --- a/src/storm-pomdp-cli/storm-pomdp.cpp +++ b/src/storm-pomdp-cli/storm-pomdp.cpp @@ -204,8 +204,12 @@ int main(const int argc, const char** argv) { STORM_PRINT_AND_LOG(" done." << std::endl); } + } else { + STORM_LOG_WARN("Nothing to be done. Did you forget to specify a formula?"); } + + // All operations have now been performed, so we clean up everything and terminate. storm::utility::cleanUp(); return 0; From 3efee0d35dd5ca7dbda92ac24e96f950d7c2d12c Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Tue, 16 Jul 2019 16:05:43 +0200 Subject: [PATCH 06/13] changelog update: export of mtbdds --- CHANGELOG.md | 1 + 1 file changed, 1 insertion(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index add4eeb9a..300f9dad5 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -21,6 +21,7 @@ Version 1.3.x - Fixed sparse bisimulation of MDPs (which failed if all non-absorbing states in the quotient are initial) - Fixed linking with Mathsat on macOS - Fixed compilation for macOS mojave +- Support for export of MTBDDs from storm ### Version 1.3.0 (2018/12) - Slightly improved scheduler extraction From 31b50d76e9c08bbd0d445cbad6d918e279d956b7 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 17 Jul 2019 14:22:48 +0200 Subject: [PATCH 07/13] clearer error message --- src/storm-parsers/parser/ValueParser.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm-parsers/parser/ValueParser.cpp b/src/storm-parsers/parser/ValueParser.cpp index 61cd5c0ac..918c89bac 100644 --- a/src/storm-parsers/parser/ValueParser.cpp +++ b/src/storm-parsers/parser/ValueParser.cpp @@ -7,7 +7,7 @@ namespace storm { template void ValueParser::addParameter(std::string const& parameter) { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameters are not supported in this build."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameters are not supported in this build (Have you checked storm-pars?)."); } template<> From 976f85cc25d551acd8b7b0df9811f140fe2bcfc3 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Fri, 19 Jul 2019 00:10:55 +0200 Subject: [PATCH 08/13] drn export for labels with whitespace is now put into quotation marks --- src/storm/utility/DirectEncodingExporter.cpp | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/src/storm/utility/DirectEncodingExporter.cpp b/src/storm/utility/DirectEncodingExporter.cpp index 61487bb25..568223489 100644 --- a/src/storm/utility/DirectEncodingExporter.cpp +++ b/src/storm/utility/DirectEncodingExporter.cpp @@ -1,3 +1,4 @@ +#include #include "DirectEncodingExporter.h" #include "storm/adapters/RationalFunctionAdapter.h" @@ -88,9 +89,15 @@ namespace storm { os << " {" << sparseModel->template as>()->getObservation(group) << "}"; } - // Write labels + // Write labels. Only labels with a whitespace are put in (double) quotation marks. for(auto const& label : sparseModel->getStateLabeling().getLabelsOfState(group)) { - os << " " << label; + STORM_LOG_THROW(std::count( label.begin(), label.end(), '\"' ) == 0, storm::exceptions::NotSupportedException, "Labels with quotation marks are not supported in the DRN format and therefore may not be exported."); + // TODO consider escaping the quotation marks. Not sure whether that is a good idea. + if (std::count_if( label.begin(), label.end(), isspace ) > 0) { + os << " \"" << label << "\""; + } else { + os << " " << label; + } } os << std::endl; From 779e5ce5aebe5b49eb4e73c04eaca9d10cda2dec Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 19 Jul 2019 14:47:01 +0200 Subject: [PATCH 09/13] DRNParser: Check if target state is valid --- src/storm-parsers/parser/DirectEncodingParser.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/storm-parsers/parser/DirectEncodingParser.cpp b/src/storm-parsers/parser/DirectEncodingParser.cpp index 5e4eee7ab..b4d590342 100644 --- a/src/storm-parsers/parser/DirectEncodingParser.cpp +++ b/src/storm-parsers/parser/DirectEncodingParser.cpp @@ -255,6 +255,7 @@ namespace storm { std::string valueStr = line.substr(posColon+2); ValueType value = valueParser.parseValue(valueStr); STORM_LOG_TRACE("Transition " << row << " -> " << target << ": " << value); + STORM_LOG_THROW(target < stateSize, storm::exceptions::WrongFormatException, "Target state " << target << " is greater than state size " << stateSize); builder.addNextValue(row, target, value); } } From 174c1a86c0a5ce4d5def3d7cd2278400aa3dedff Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 19 Jul 2019 14:47:44 +0200 Subject: [PATCH 10/13] DRNParser: Parse labels with and without quotation marks (thanks to pair programming and regex magic --- .../parser/DirectEncodingParser.cpp | 26 ++++++++++++++++++- 1 file changed, 25 insertions(+), 1 deletion(-) diff --git a/src/storm-parsers/parser/DirectEncodingParser.cpp b/src/storm-parsers/parser/DirectEncodingParser.cpp index b4d590342..46519f81c 100644 --- a/src/storm-parsers/parser/DirectEncodingParser.cpp +++ b/src/storm-parsers/parser/DirectEncodingParser.cpp @@ -2,6 +2,8 @@ #include #include +#include + #include #include @@ -215,7 +217,29 @@ namespace storm { // Parse labels if (!line.empty()) { std::vector labels; - boost::split(labels, line, boost::is_any_of(" ")); + // Labels are separated by whitespace and can optionally be enclosed in quotation marks + // Regex for labels with two cases: + // * Enclosed in quotation marks: \"([^\"]+?)\"(?=(\s|$|\")) + // - First part matches string enclosed in quotation marks with no quotation mark inbetween (\"([^\"]+?)\") + // - second part is lookahead which ensures that after the matched part either whitespace, end of line or a new quotation mark follows (?=(\s|$|\")) + // * Separated by whitespace: [^\s\"]+?(?=(\s|$)) + // - First part matches string without whitespace and quotation marks [^\s\"]+? + // - Second part is again lookahead matching whitespace or end of line (?=(\s|$)) + std::regex labelRegex(R"(\"([^\"]+?)\"(?=(\s|$|\"))|([^\s\"]+?(?=(\s|$))))"); + + // Iterate over matches + auto match_begin = std::sregex_iterator(line.begin(), line.end(), labelRegex); + auto match_end = std::sregex_iterator(); + for (std::sregex_iterator i = match_begin; i != match_end; ++i) { + std::smatch match = *i; + // Find matched group and add as label + if (match.length(1) > 0) { + labels.push_back(match.str(1)); + } else { + labels.push_back(match.str(3)); + } + } + for (std::string label : labels) { if (!modelComponents->stateLabeling.containsLabel(label)) { modelComponents->stateLabeling.addLabel(label); From b84879685297955844d59394432839385224a829 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Wed, 10 Jul 2019 12:56:37 +0200 Subject: [PATCH 11/13] Nativepolytope: Fixed a bug in quickhull when invoked on just a single point. --- .../nativepolytopeconversion/QuickHull.cpp | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/src/storm/storage/geometry/nativepolytopeconversion/QuickHull.cpp b/src/storm/storage/geometry/nativepolytopeconversion/QuickHull.cpp index 76a1a92a6..67a9f2942 100644 --- a/src/storm/storage/geometry/nativepolytopeconversion/QuickHull.cpp +++ b/src/storm/storage/geometry/nativepolytopeconversion/QuickHull.cpp @@ -128,11 +128,17 @@ namespace storm { // get one hyperplane that holds all points const uint_fast64_t dimension = points.front().rows(); EigenVector refPoint = points.front(); - EigenMatrix constraints(points.size() - 1, dimension); - for (unsigned row = 1; row < points.size(); ++row) { - constraints.row(row - 1) = points[row] - refPoint; + EigenVector normal; + if (points.size() == 1) { + normal.resize(dimension); + normal(0) = storm::utility::one(); + } else { + EigenMatrix constraints(points.size() - 1, dimension); + for (unsigned row = 1; row < points.size(); ++row) { + constraints.row(row - 1) = points[row] - refPoint; + } + normal = constraints.fullPivLu().kernel().col(0); } - EigenVector normal = constraints.fullPivLu().kernel().col(0); // Eigen returns the column vector 0...0 if the kernel is empty (i.e., there is no such hyperplane) if (normal.isZero()) { From 0b1b0d97e2841913370a63bad937e60c97565051 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Fri, 26 Jul 2019 08:42:39 +0200 Subject: [PATCH 12/13] utility/graph: fixed behavior of getReachableStates when an initial state is not in the constrained set. --- src/storm/utility/graph.cpp | 12 +++++++++--- src/storm/utility/graph.h | 1 + 2 files changed, 10 insertions(+), 3 deletions(-) diff --git a/src/storm/utility/graph.cpp b/src/storm/utility/graph.cpp index c1f1216ad..b774c65da 100644 --- a/src/storm/utility/graph.cpp +++ b/src/storm/utility/graph.cpp @@ -37,16 +37,22 @@ namespace storm { uint_fast64_t numberOfStates = transitionMatrix.getRowGroupCount(); // Initialize the stack used for the DFS with the states. - std::vector stack(initialStates.begin(), initialStates.end()); + std::vector stack; + stack.reserve(initialStates.size()); + for (auto const& state : initialStates) { + if (constraintStates.get(state)) { + stack.push_back(state); + } + } // Initialize the stack for the step bound, if the number of steps is bounded. std::vector stepStack; std::vector remainingSteps; if (useStepBound) { stepStack.reserve(numberOfStates); - stepStack.insert(stepStack.begin(), initialStates.getNumberOfSetBits(), maximalSteps); + stepStack.insert(stepStack.begin(), stack.size(), maximalSteps); remainingSteps.resize(numberOfStates); - for (auto state : initialStates) { + for (auto state : stack) { remainingSteps[state] = maximalSteps; } } diff --git a/src/storm/utility/graph.h b/src/storm/utility/graph.h index 6f65bbcfa..d6f12cc94 100644 --- a/src/storm/utility/graph.h +++ b/src/storm/utility/graph.h @@ -60,6 +60,7 @@ namespace storm { * Performs a forward depth-first search through the underlying graph structure to identify the states that * are reachable from the given set only passing through a constrained set of states until some target * have been reached. + * If an initial state or a (constrained-reachable) target state is not in the constrained set, it will be added to the reachable states but not explored. * * @param transitionMatrix The transition relation of the graph structure to search. * @param initialStates The set of states from which to start the search. From 492348542ffcc1b58f9290bc0319dcf0d8836133 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Fri, 26 Jul 2019 08:44:55 +0200 Subject: [PATCH 13/13] SubsystemBuilder: Fix deadlocks with a selfloop (if requested) --- .../models/sparse/StandardRewardModel.cpp | 24 ++++- src/storm/models/sparse/StandardRewardModel.h | 10 +- src/storm/storage/SparseMatrix.cpp | 48 ++++++++-- src/storm/storage/SparseMatrix.h | 5 + src/storm/storage/sparse/ChoiceOrigins.cpp | 4 + src/storm/storage/sparse/ChoiceOrigins.h | 7 +- src/storm/transformer/SubsystemBuilder.cpp | 95 ++++++++++++++----- src/storm/transformer/SubsystemBuilder.h | 9 +- 8 files changed, 163 insertions(+), 39 deletions(-) diff --git a/src/storm/models/sparse/StandardRewardModel.cpp b/src/storm/models/sparse/StandardRewardModel.cpp index e37de0562..190449ea6 100644 --- a/src/storm/models/sparse/StandardRewardModel.cpp +++ b/src/storm/models/sparse/StandardRewardModel.cpp @@ -339,6 +339,24 @@ namespace storm { void StandardRewardModel::setStateActionRewardValue(uint_fast64_t row, ValueType const& value) { this->optionalStateActionRewardVector.get()[row] = value; } + + template + template + void StandardRewardModel::clearRewardAtState(uint_fast64_t state, storm::storage::SparseMatrix const& transitions) { + if (hasStateRewards()) { + getStateRewardVector()[state] = storm::utility::zero(); + } + if (hasStateActionRewards()) { + for (uint_fast64_t choice = transitions.getRowGroupIndices()[state]; choice < transitions.getRowGroupIndices()[state + 1]; ++choice) { + getStateActionRewardVector()[choice] = storm::utility::zero(); + } + } + if (hasTransitionRewards()) { + for (auto& entry : getTransitionRewardMatrix().getRowGroup(state)) { + entry.setValue(storm::utility::zero()); + } + } + } template bool StandardRewardModel::empty() const { @@ -412,7 +430,7 @@ namespace storm { template storm::storage::BitVector StandardRewardModel::getChoicesWithZeroReward(storm::storage::SparseMatrix const& transitionMatrix) const; template storm::storage::BitVector StandardRewardModel::getChoicesWithFilter(storm::storage::SparseMatrix const& transitionMatrix, std::function const& filter) const; template double StandardRewardModel::getTotalStateActionReward(uint_fast64_t stateIndex, uint_fast64_t choiceIndex, storm::storage::SparseMatrix const& transitionMatrix, double const& stateRewardWeight, double const& actionRewardWeight) const; - + template void StandardRewardModel::clearRewardAtState(uint_fast64_t state, storm::storage::SparseMatrix const& transitionMatrix); template void StandardRewardModel::reduceToStateBasedRewards(storm::storage::SparseMatrix const& transitionMatrix, bool reduceToStateRewards, std::vector const* weights); template void StandardRewardModel::setStateActionReward(uint_fast64_t choiceIndex, double const & newValue); template void StandardRewardModel::setStateReward(uint_fast64_t state, double const & newValue); @@ -440,6 +458,7 @@ namespace storm { template storm::storage::BitVector StandardRewardModel::getChoicesWithFilter(storm::storage::SparseMatrix const& transitionMatrix, std::function const& filter) const; template storm::RationalNumber StandardRewardModel::getTotalStateActionReward(uint_fast64_t stateIndex, uint_fast64_t choiceIndex, storm::storage::SparseMatrix const& transitionMatrix, storm::RationalNumber const& stateRewardWeight, storm::RationalNumber const& actionRewardWeight) const; template void StandardRewardModel::reduceToStateBasedRewards(storm::storage::SparseMatrix const& transitionMatrix, bool reduceToStateRewards, std::vector const* weights); + template void StandardRewardModel::clearRewardAtState(uint_fast64_t state, storm::storage::SparseMatrix const& transitionMatrix); template void StandardRewardModel::setStateActionReward(uint_fast64_t choiceIndex, storm::RationalNumber const & newValue); template void StandardRewardModel::setStateReward(uint_fast64_t state, storm::RationalNumber const & newValue); template class StandardRewardModel; @@ -452,7 +471,7 @@ namespace storm { template storm::storage::BitVector StandardRewardModel::getStatesWithFilter(storm::storage::SparseMatrix const& transitionMatrix, std::function const& filter) const; template storm::storage::BitVector StandardRewardModel::getChoicesWithZeroReward(storm::storage::SparseMatrix const& transitionMatrix) const; template storm::storage::BitVector StandardRewardModel::getChoicesWithFilter(storm::storage::SparseMatrix const& transitionMatrix, std::function const& filter) const; - + template void StandardRewardModel::clearRewardAtState(uint_fast64_t state, storm::storage::SparseMatrix const& transitionMatrix); template std::vector StandardRewardModel::getTotalActionRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& stateRewardWeights) const; template storm::RationalFunction StandardRewardModel::getTotalStateActionReward(uint_fast64_t stateIndex, uint_fast64_t choiceIndex, storm::storage::SparseMatrix const& transitionMatrix, storm::RationalFunction const& stateRewardWeight, storm::RationalFunction const& actionRewardWeight) const; template void StandardRewardModel::reduceToStateBasedRewards(storm::storage::SparseMatrix const& transitionMatrix, bool reduceToStateRewards, std::vector const* weights); @@ -471,6 +490,7 @@ namespace storm { template void StandardRewardModel::setStateActionReward(uint_fast64_t choiceIndex, storm::Interval const & newValue); template void StandardRewardModel::setStateReward(uint_fast64_t state, double const & newValue); template void StandardRewardModel::setStateReward(uint_fast64_t state, storm::Interval const & newValue); + template void StandardRewardModel::clearRewardAtState(uint_fast64_t state, storm::storage::SparseMatrix const& transitionMatrix); template void StandardRewardModel::reduceToStateBasedRewards(storm::storage::SparseMatrix const& transitionMatrix, bool reduceToStateRewards, std::vector const* weights); template class StandardRewardModel; template std::ostream& operator<<(std::ostream& out, StandardRewardModel const& rewardModel); diff --git a/src/storm/models/sparse/StandardRewardModel.h b/src/storm/models/sparse/StandardRewardModel.h index cdfce6038..ac725d06c 100644 --- a/src/storm/models/sparse/StandardRewardModel.h +++ b/src/storm/models/sparse/StandardRewardModel.h @@ -123,9 +123,13 @@ namespace storm { */ template void setStateActionReward(uint_fast64_t choiceIndex, T const& newValue); - - //ValueType maximalStateActionReward() const; - + + /*! + * Sets all available rewards at this state to zero. + */ + template + void clearRewardAtState(uint_fast64_t state, storm::storage::SparseMatrix const& transitions); + /*! * Retrieves an optional value that contains the state-action reward vector if there is one. * diff --git a/src/storm/storage/SparseMatrix.cpp b/src/storm/storage/SparseMatrix.cpp index cdeaaf9a2..b3e8cd8c3 100644 --- a/src/storm/storage/SparseMatrix.cpp +++ b/src/storm/storage/SparseMatrix.cpp @@ -690,17 +690,30 @@ namespace storm { // If the row has no elements in it, we cannot make it absorbing, because we would need to move all elements // in the vector of nonzeros otherwise. if (columnValuePtr >= columnValuePtrEnd) { - throw storm::exceptions::InvalidStateException() << "Illegal call to SparseMatrix::makeRowDirac: cannot make row " << row << " absorbing, but there is no entry in this row."; + throw storm::exceptions::InvalidStateException() << "Illegal call to SparseMatrix::makeRowDirac: cannot make row " << row << " absorbing, because there is no entry in this row."; } + iterator lastColumnValuePtr = this->end(row) - 1; - // If there is at least one entry in this row, we can just set it to one, modify its column value to the + // If there is at least one entry in this row, we can set it to one, modify its column value to the // one given by the parameter and set all subsequent elements of this row to zero. - columnValuePtr->setColumn(column); - columnValuePtr->setValue(storm::utility::one()); - ++columnValuePtr; - for (; columnValuePtr != columnValuePtrEnd; ++columnValuePtr) { + // However, we want to preserve that column indices within a row are ascending, so we pick an entry that is close to the desired column index + while (columnValuePtr->getColumn() < column && columnValuePtr != lastColumnValuePtr) { + if (!storm::utility::isZero(columnValuePtr->getValue())) { + --this->nonzeroEntryCount; + } + columnValuePtr->setValue(storm::utility::zero()); + ++columnValuePtr; + } + // At this point, we have found the first entry whose column is >= the desired column (or the last entry of the row, if no such column exist) + if (storm::utility::isZero(columnValuePtr->getValue())) { ++this->nonzeroEntryCount; - columnValuePtr->setColumn(0); + } + columnValuePtr->setValue(storm::utility::one()); + columnValuePtr->setColumn(column); + for (++columnValuePtr; columnValuePtr != columnValuePtrEnd; ++columnValuePtr) { + if (!storm::utility::isZero(columnValuePtr->getValue())) { + --this->nonzeroEntryCount; + } columnValuePtr->setValue(storm::utility::zero()); } } @@ -1060,6 +1073,27 @@ namespace storm { return result; } + template + void SparseMatrix::dropZeroEntries() { + updateNonzeroEntryCount(); + if (getNonzeroEntryCount() != getEntryCount()) { + SparseMatrixBuilder builder(getRowCount(), getColumnCount(), getNonzeroEntryCount(), true); + for (index_type row = 0; row < getRowCount(); ++row) { + for (auto const& entry : getRow(row)) { + if (!storm::utility::isZero(entry.getValue())) { + builder.addNextValue(row, entry.getColumn(), entry.getValue()); + } + } + } + SparseMatrix result = builder.build(); + // Add a row grouping if necessary. + if (!hasTrivialRowGrouping()) { + result.setRowGroupIndices(getRowGroupIndices()); + } + *this = std::move(result); + } + } + template SparseMatrix SparseMatrix::selectRowsFromRowGroups(std::vector const& rowGroupToRowIndexMapping, bool insertDiagonalEntries) const { // First, we need to count how many non-zero entries the resulting matrix will have and reserve space for diff --git a/src/storm/storage/SparseMatrix.h b/src/storm/storage/SparseMatrix.h index dbdd4086d..125b3bd39 100644 --- a/src/storm/storage/SparseMatrix.h +++ b/src/storm/storage/SparseMatrix.h @@ -726,6 +726,11 @@ namespace storm { */ SparseMatrix filterEntries(storm::storage::BitVector const& rowFilter) const; + /*! + * Removes all zero entries from this. + */ + void dropZeroEntries(); + /** * Compares two rows. * @param i1 Index of first row diff --git a/src/storm/storage/sparse/ChoiceOrigins.cpp b/src/storm/storage/sparse/ChoiceOrigins.cpp index ac554af10..56c512f37 100644 --- a/src/storm/storage/sparse/ChoiceOrigins.cpp +++ b/src/storm/storage/sparse/ChoiceOrigins.cpp @@ -73,6 +73,10 @@ namespace storm { return cloneWithNewIndexToIdentifierMapping(std::move(indexToIdentifierMapping)); } + void ChoiceOrigins::clearOriginOfChoice(uint_fast64_t choiceIndex) { + indexToIdentifier[choiceIndex] = getIdentifierForChoicesWithNoOrigin(); + } + std::shared_ptr ChoiceOrigins::selectChoices(std::vector const& selectedChoices) const { std::vector indexToIdentifierMapping; indexToIdentifierMapping.reserve(selectedChoices.size()); diff --git a/src/storm/storage/sparse/ChoiceOrigins.h b/src/storm/storage/sparse/ChoiceOrigins.h index 0645ca466..902fdd031 100644 --- a/src/storm/storage/sparse/ChoiceOrigins.h +++ b/src/storm/storage/sparse/ChoiceOrigins.h @@ -68,6 +68,11 @@ namespace storm { */ std::shared_ptr selectChoices(storm::storage::BitVector const& selectedChoices) const; + /* + * Removes origin information of the given choice. + */ + void clearOriginOfChoice(uint_fast64_t choiceIndex); + /* * Derive new choice origins from this by selecting the given choices. * If an invalid choice index is selected, the corresponding choice will get the identifier for choices with no origin. @@ -90,7 +95,7 @@ namespace storm { */ virtual void computeIdentifierInfos() const = 0; - std::vector const indexToIdentifier; + std::vector indexToIdentifier; // cached identifier infos might be empty if identifiers have not been generated yet. mutable std::vector identifierToInfo; diff --git a/src/storm/transformer/SubsystemBuilder.cpp b/src/storm/transformer/SubsystemBuilder.cpp index daca08a5d..44449c5ce 100644 --- a/src/storm/transformer/SubsystemBuilder.cpp +++ b/src/storm/transformer/SubsystemBuilder.cpp @@ -16,6 +16,7 @@ #include "storm/utility/builder.h" #include "storm/exceptions/InvalidArgumentException.h" +#include "storm/exceptions/InvalidOperationException.h" #include "storm/exceptions/UnexpectedException.h" namespace storm { @@ -37,6 +38,7 @@ namespace storm { } else { STORM_LOG_THROW(originalModel.isOfType(storm::models::ModelType::Dtmc) || originalModel.isOfType(storm::models::ModelType::Mdp), storm::exceptions::UnexpectedException, "Unexpected model type."); } + // Nothing to be done if the model has deadlock States } template @@ -59,6 +61,7 @@ namespace storm { template SubsystemBuilderReturnType internalBuildSubsystem(storm::models::sparse::Model const& originalModel, storm::storage::BitVector const& subsystemStates, storm::storage::BitVector const& subsystemActions, SubsystemBuilderOptions const& options ) { + auto const& groupIndices = originalModel.getTransitionMatrix().getRowGroupIndices(); SubsystemBuilderReturnType result; uint_fast64_t subsystemStateCount = subsystemStates.getNumberOfSetBits(); if (options.buildStateMapping) { @@ -67,21 +70,20 @@ namespace storm { if (options.buildActionMapping) { result.newToOldActionIndexMapping.reserve(subsystemActions.getNumberOfSetBits()); } - if (options.buildKeptActions) { - result.keptActions = storm::storage::BitVector(originalModel.getTransitionMatrix().getRowCount(), false); - + storm::storage::BitVector deadlockStates; + if (options.fixDeadlocks) { + deadlockStates.resize(subsystemStates.size(), false); } - + // Get the set of actions that stay in the subsystem. + // Also establish the mappings if requested. + storm::storage::BitVector keptActions(originalModel.getTransitionMatrix().getRowCount(), false); for (auto subsysState : subsystemStates) { if (options.buildStateMapping) { result.newToOldStateIndexMapping.push_back(subsysState); } - bool keepAtLeastOneAction = !options.checkTransitionsOutside; // For debug mode only. - bool atLeastOneActionSelected = false; // For debug mode only. - for (uint_fast64_t row = subsystemActions.getNextSetIndex(originalModel.getTransitionMatrix().getRowGroupIndices()[subsysState]); row < originalModel.getTransitionMatrix().getRowGroupIndices()[subsysState+1]; row = subsystemActions.getNextSetIndex(row+1)) { + bool hasDeadlock = true; + for (uint_fast64_t row = subsystemActions.getNextSetIndex(groupIndices[subsysState]); row < groupIndices[subsysState+1]; row = subsystemActions.getNextSetIndex(row + 1)) { bool allRowEntriesStayInSubsys = true; - atLeastOneActionSelected = true; - if (options.checkTransitionsOutside) { for (auto const &entry : originalModel.getTransitionMatrix().getRow(row)) { if (!subsystemStates.get(entry.getColumn())) { @@ -91,42 +93,87 @@ namespace storm { } } if (allRowEntriesStayInSubsys) { - keepAtLeastOneAction = true; + if (options.buildActionMapping) { + result.newToOldActionIndexMapping.push_back(row); + } + keptActions.set(row, true); + hasDeadlock = false; } + } + if (hasDeadlock) { + STORM_LOG_THROW(options.fixDeadlocks, storm::exceptions::InvalidOperationException, "Expected that in each state, at least one action is selected. Got a deadlock state instead. (violated at " << subsysState << ")"); if (options.buildActionMapping) { - result.newToOldActionIndexMapping.push_back(row); - } - if (options.buildKeptActions) { - result.keptActions.set(row, allRowEntriesStayInSubsys); + result.newToOldActionIndexMapping.push_back(std::numeric_limits::max()); } + deadlockStates.set(subsysState); } - if (!atLeastOneActionSelected && options.fixDeadlocks) { - - } - STORM_LOG_ASSERT(atLeastOneActionSelected, "Expected that in each state, at least one action is selected. (violated at " << subsysState << ")"); - STORM_LOG_ASSERT(keepAtLeastOneAction, "Expected that in each state, at least one action is preserved at least one action is selected. (violated at " << subsysState << ")"); } - + // If we have deadlock states we keep an action in each rowgroup of a deadlock states. + bool hasDeadlockStates = !deadlockStates.empty(); + if (options.buildKeptActions) { + // store them now, before changing them. + result.keptActions = keptActions; + } + for (auto const& deadlockState : deadlockStates) { + keptActions.set(groupIndices[deadlockState], true); + } + // Transform the components of the model storm::storage::sparse::ModelComponents components; - components.transitionMatrix = originalModel.getTransitionMatrix().getSubmatrix(false, result.keptActions, subsystemStates); + if (hasDeadlockStates) { + // make deadlock choices a selfloop + components.transitionMatrix = originalModel.getTransitionMatrix(); + components.transitionMatrix.makeRowGroupsAbsorbing(deadlockStates); + components.transitionMatrix.dropZeroEntries(); + components.transitionMatrix = components.transitionMatrix.getSubmatrix(false, keptActions, subsystemStates); + } else { + components.transitionMatrix = originalModel.getTransitionMatrix().getSubmatrix(false, keptActions, subsystemStates); + } components.stateLabeling = originalModel.getStateLabeling().getSubLabeling(subsystemStates); for (auto const& rewardModel : originalModel.getRewardModels()){ - components.rewardModels.insert(std::make_pair(rewardModel.first, transformRewardModel(rewardModel.second, subsystemStates, result.keptActions))); + components.rewardModels.insert(std::make_pair(rewardModel.first, transformRewardModel(rewardModel.second, subsystemStates, keptActions))); } if (originalModel.hasChoiceLabeling()) { - components.choiceLabeling = originalModel.getChoiceLabeling().getSubLabeling(result.keptActions); + components.choiceLabeling = originalModel.getChoiceLabeling().getSubLabeling(keptActions); } if (originalModel.hasStateValuations()) { components.stateValuations = originalModel.getStateValuations().selectStates(subsystemStates); } if (originalModel.hasChoiceOrigins()) { - components.choiceOrigins = originalModel.getChoiceOrigins()->selectChoices(result.keptActions); + components.choiceOrigins = originalModel.getChoiceOrigins()->selectChoices(keptActions); + } + + if (hasDeadlockStates) { + auto subDeadlockStates = deadlockStates % subsystemStates; + assert(deadlockStates.getNumberOfSetBits() == subDeadlockStates.getNumberOfSetBits()); + // erase rewards, choice labels, choice origins + for (auto& rewModel : components.rewardModels) { + for (auto const& state : subDeadlockStates) { + rewModel.second.clearRewardAtState(state, components.transitionMatrix); + } + } + if (components.choiceLabeling) { + storm::storage::BitVector nonDeadlockChoices(components.transitionMatrix.getRowCount(), true); + for (auto const& state : subDeadlockStates) { + auto const& choice = components.transitionMatrix.getRowGroupIndices()[state]; + nonDeadlockChoices.set(choice, false); + } + for (auto const& label : components.choiceLabeling.get().getLabels()) { + components.choiceLabeling->setChoices(label, components.choiceLabeling->getChoices(label) & nonDeadlockChoices); + } + } + if (components.choiceOrigins) { + for (auto const& state : subDeadlockStates) { + auto const& choice = components.transitionMatrix.getRowGroupIndices()[state]; + components.choiceOrigins.get()->clearOriginOfChoice(choice); + } + } } transformModelSpecificComponents(originalModel, subsystemStates, components); result.model = storm::utility::builder::buildModelFromComponents(originalModel.getType(), std::move(components)); + STORM_LOG_DEBUG("Subsystem Builder is done. Resulting model has " << result.model->getNumberOfStates() << " states."); return result; } diff --git a/src/storm/transformer/SubsystemBuilder.h b/src/storm/transformer/SubsystemBuilder.h index 9f18bfb1a..cf7aefaaf 100644 --- a/src/storm/transformer/SubsystemBuilder.h +++ b/src/storm/transformer/SubsystemBuilder.h @@ -17,6 +17,7 @@ namespace storm { // Gives for each state in the resulting model the corresponding state in the original model. std::vector newToOldStateIndexMapping; // Gives for each action in the resulting model the corresponding action in the original model. + // If this action was introduced to fix a deadlock, it will get index std::numeric_limits::max() std::vector newToOldActionIndexMapping; // marks the actions of the original model that are still available in the subsystem storm::storage::BitVector keptActions; @@ -27,7 +28,7 @@ namespace storm { bool buildStateMapping = true; bool buildActionMapping = false; bool buildKeptActions = true; - bool fixDeadlocks = true; + bool fixDeadlocks = false; }; /* @@ -40,7 +41,9 @@ namespace storm { * * it originates from a state that is part of the subsystem AND * * it does not contain a transition leading to a state outside of the subsystem. * - * If this introduces a deadlock state (i.e., a state without an action) an exception is thrown. + * If this introduces a deadlock state (i.e., a state without an action) it is either + * * fixed by inserting a selfloop (if fixDeadlocks is true) or + * * an exception is thrown (otherwise). * * @param originalModel The original model. * @param subsystemStates The selected states. @@ -49,5 +52,7 @@ namespace storm { */ template > SubsystemBuilderReturnType buildSubsystem(storm::models::sparse::Model const& originalModel, storm::storage::BitVector const& subsystemStates, storm::storage::BitVector const& subsystemActions, bool keepUnreachableStates = true, SubsystemBuilderOptions options = SubsystemBuilderOptions()); + + } }