export of bdds into dot and text format

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)

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

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;

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];

src/storm-cli-utilities/model-handling.h

@@ -386,7 +386,15 @@ namespace storm {
         
         template <storm::dd::DdType DdType, typename ValueType>
         void exportDdModel(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& model, SymbolicInput const& input) {
-            // Intentionally left empty.
+            auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
+
+            if (ioSettings.isExportDdSet()) {
+                storm::api::exportSparseModelAsDrdd(model, ioSettings.getExportDdFilename());
+            }
+
+            if (ioSettings.isExportDotSet()) {
+                storm::api::exportSymbolicModelAsDot(model, ioSettings.getExportDotFilename());
+            }
         }
         
         template <storm::dd::DdType DdType, typename ValueType>

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"
 
@@ -24,6 +25,11 @@ namespace storm {
             storm::utility::closeFile(stream);
         }
 
+        template<storm::dd::DdType Type, typename ValueType>
+        void exportSparseModelAsDrdd(std::shared_ptr<storm::models::symbolic::Model<Type,ValueType>> const& model, std::string const& filename) {
+            storm::exporter::explicitExportSymbolicModel(filename, model);
+        }
+        
         template <typename ValueType>
         void exportSparseModelAsDot(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, std::string const& filename) {
             std::ofstream stream;
@@ -32,5 +38,9 @@ namespace storm {
             storm::utility::closeFile(stream);
         }
 
+        template<storm::dd::DdType Type, typename ValueType>
+        void exportSymbolicModelAsDot(std::shared_ptr<storm::models::symbolic::Model<Type,ValueType>> const& model, std::string const& filename) {
+            model->writeDotToFile(filename);
+        }
     }
 }

src/storm/models/symbolic/Model.cpp

@@ -369,6 +369,16 @@ namespace storm {
                 return std::is_same<ValueType, storm::RationalFunction>::value;
             }
 
+            template<storm::dd::DdType Type, typename ValueType>
+            void Model<Type, ValueType>::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<storm::dd::DdType Type, typename ValueType>
             bool Model<Type, ValueType>::hasParameters() const {
                 if (!this->supportsParameters()) {
@@ -404,6 +414,9 @@ namespace storm {
                 return parameters;
             }
 
+
+
+
             template<storm::dd::DdType Type, typename ValueType>
             template<typename NewValueType>
             typename std::enable_if<!std::is_same<ValueType, NewValueType>::value, std::shared_ptr<Model<Type, NewValueType>>>::type Model<Type, ValueType>::toValueType() const {

src/storm/models/symbolic/Model.h

@@ -343,6 +343,8 @@ namespace storm {
                 template<typename NewValueType>
                 typename std::enable_if<std::is_same<ValueType, NewValueType>::value, std::shared_ptr<Model<Type, NewValueType>>>::type toValueType() const;
 
+                void writeDotToFile(std::string const& filename) const;
+
             protected:
                 /*!
                  * Sets the transition matrix of the model.

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());
@@ -125,6 +128,14 @@ namespace storm {
                 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();
             }

src/storm/settings/modules/IOSettings.h

@@ -61,10 +61,24 @@ namespace storm {
                 /*!
                  * 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;

src/storm/storage/dd/Add.cpp

@@ -1010,6 +1010,11 @@ namespace storm {
             internalAdd.exportToDot(filename, this->getDdManager().getDdVariableNames(), showVariablesIfPossible);
         }
 
+        template<DdType LibraryType, typename ValueType>
+        void Add<LibraryType, ValueType>::exportToText(std::string const& filename) const {
+            internalAdd.exportToText(filename);
+        }
+        
         template<DdType LibraryType, typename ValueType>
         AddIterator<LibraryType, ValueType> Add<LibraryType, ValueType>::begin(bool enumerateDontCareMetaVariables) const {
             uint_fast64_t numberOfDdVariables = 0;

src/storm/storage/dd/Add.h

@@ -694,6 +694,8 @@ namespace storm {
              */
             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.
              *

src/storm/storage/dd/Bdd.cpp

@@ -492,6 +492,11 @@ namespace storm {
             internalBdd.exportToDot(filename, this->getDdManager().getDdVariableNames(), showVariablesIfPossible);
         }
 
+        template<DdType LibraryType>
+        void Bdd<LibraryType>::exportToText(std::string const& filename) const {
+            internalBdd.exportToText(filename);
+        }
+        
         template<DdType LibraryType>
         Bdd<LibraryType> Bdd<LibraryType>::getCube(DdManager<LibraryType> const& manager, std::set<storm::expressions::Variable> const& metaVariables) {
             Bdd<LibraryType> cube = manager.getBddOne();

src/storm/storage/dd/Bdd.h

@@ -380,6 +380,8 @@ namespace storm {
             
             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.
              *

src/storm/storage/dd/Dd.h

@@ -104,6 +104,13 @@ namespace storm {
              */
             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.
              *

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 {
@@ -159,6 +160,10 @@ namespace storm {
             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()) {
                 return;

src/storm/storage/dd/Odd.h

@@ -134,6 +134,13 @@ namespace storm {
              */
             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.
              *

src/storm/storage/dd/cudd/InternalCuddAdd.cpp

@@ -146,13 +146,17 @@ namespace storm {
 
         template<typename ValueType>
         template<typename TargetValueType>
-        typename std::enable_if<std::is_same<ValueType, TargetValueType>::value, InternalAdd<DdType::CUDD, TargetValueType>>::type InternalAdd<DdType::CUDD, ValueType>::toValueType() const {
+        typename std::enable_if<std::is_same<ValueType, TargetValueType>::value, InternalAdd < DdType::CUDD, TargetValueType>>
+
+        ::type InternalAdd<DdType::CUDD, ValueType>::toValueType() const {
             return *this;
         }
 
         template<typename ValueType>
         template<typename TargetValueType>
-        typename std::enable_if<!std::is_same<ValueType, TargetValueType>::value, InternalAdd<DdType::CUDD, TargetValueType>>::type InternalAdd<DdType::CUDD, ValueType>::toValueType() const {
+        typename std::enable_if<!std::is_same<ValueType, TargetValueType>::value, InternalAdd < DdType::CUDD, TargetValueType>>
+
+        ::type InternalAdd<DdType::CUDD, ValueType>::toValueType() const {
             STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation not supported");
         }
 
@@ -399,6 +403,11 @@ namespace storm {
             }
         }
 
+        template<typename ValueType>
+        void InternalAdd<DdType::CUDD, ValueType>::exportToText(std::string const &) const {
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation not supported");
+        }
+
         template<typename ValueType>
         AddIterator<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::begin(DdManager<DdType::CUDD> const& fullDdManager, InternalBdd<DdType::CUDD> const&, uint_fast64_t, std::set<storm::expressions::Variable> const& metaVariables, bool enumerateDontCareMetaVariables) const {
             int* cube;

src/storm/storage/dd/cudd/InternalCuddAdd.h

@@ -516,6 +516,12 @@ namespace storm {
              */
             void exportToDot(std::string const& filename, std::vector<std::string> 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.
              *

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 {
@@ -212,6 +213,10 @@ namespace storm {
             }
         }
 
+        void InternalBdd<DdType::CUDD>::exportToText(std::string const&) const {
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation not supported");
+        }
+        
         cudd::BDD InternalBdd<DdType::CUDD>::getCuddBdd() const {
             return this->cuddBdd;
         }

src/storm/storage/dd/cudd/InternalCuddBdd.h

@@ -329,6 +329,13 @@ namespace storm {
              */
             void exportToDot(std::string const& filename, std::vector<std::string> 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.
              *

src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp

@@ -802,11 +802,19 @@ namespace storm {
         template<typename ValueType>
         void InternalAdd<DdType::Sylvan, ValueType>::exportToDot(std::string const& filename, std::vector<std::string> 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<typename ValueType>
+        void InternalAdd<DdType::Sylvan, ValueType>::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<typename ValueType>
         AddIterator<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::begin(DdManager<DdType::Sylvan> const& fullDdManager, InternalBdd<DdType::Sylvan> const& variableCube, uint_fast64_t numberOfDdVariables, std::set<storm::expressions::Variable> const& metaVariables, bool enumerateDontCareMetaVariables) const {
             return AddIterator<DdType::Sylvan, ValueType>::createBeginIterator(fullDdManager, this->getSylvanMtbdd(), variableCube.getSylvanBdd(), numberOfDdVariables, &metaVariables, enumerateDontCareMetaVariables);

src/storm/storage/dd/sylvan/InternalSylvanAdd.h

@@ -507,6 +507,13 @@ namespace storm {
              */
             void exportToDot(std::string const& filename, std::vector<std::string> 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.
 			*/

src/storm/storage/dd/sylvan/InternalSylvanBdd.cpp

@@ -233,11 +233,17 @@ namespace storm {
         }
         
         void InternalBdd<DdType::Sylvan>::exportToDot(std::string const& filename, std::vector<std::string> 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<DdType::Sylvan>::exportToText(std::string const& filename) const {
+            FILE* filePointer = fopen(filename.c_str() , "a+");
+            this->sylvanBdd.PrintText(filePointer);
+            fclose(filePointer);
+        }
+        
         sylvan::Bdd& InternalBdd<DdType::Sylvan>::getSylvanBdd() {
             return sylvanBdd;
         }

src/storm/storage/dd/sylvan/InternalSylvanBdd.h

@@ -318,6 +318,13 @@ namespace storm {
              */
             void exportToDot(std::string const& filename, std::vector<std::string> 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.
              *

src/storm/utility/DDEncodingExporter.cpp

@@ -0,0 +1,35 @@
+#include "storm/utility/DDEncodingExporter.h"
+#include "storm/utility/file.h"
+
+
+namespace storm {
+    namespace exporter {
+
+
+        template<storm::dd::DdType Type, typename ValueType>
+        void explicitExportSymbolicModel(std::string const& filename, std::shared_ptr <storm::models::symbolic::Model<Type, ValueType>> 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<storm::dd::DdType::CUDD,double>(std::string const&, std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD, double>> sparseModel);
+        template void explicitExportSymbolicModel<storm::dd::DdType::Sylvan,double>(std::string const&, std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan, double>> sparseModel);
+
+        template void explicitExportSymbolicModel<storm::dd::DdType::Sylvan, storm::RationalNumber>(std::string const&, std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan, storm::RationalNumber>> sparseModel);
+        template void explicitExportSymbolicModel<storm::dd::DdType::Sylvan, storm::RationalFunction>(std::string const&, std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan, storm::RationalFunction>> sparseModel);
+    }
+}

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<storm::dd::DdType Type,typename ValueType>
+        void explicitExportSymbolicModel(std::string const& filename, std::shared_ptr<storm::models::symbolic::Model<Type,ValueType>> symbolicModel);
+
+
+
+    }
+}