first version of explicit format export [mdps/no rewards only currently]

Former-commit-id: 078efab44d [formerly a1a444a014]
Former-commit-id: 321bc64e6f

src/cli/entrypoints.h

@@ -4,6 +4,7 @@
 #include "src/utility/storm.h"
 
 #include "src/storage/SymbolicModelDescription.h"
+#include "src/utility/ExplicitExporter.h"
 
 #include "src/exceptions/NotImplementedException.h"
 #include "src/exceptions/InvalidSettingsException.h"
@@ -216,6 +217,14 @@ namespace storm {
             } else {
                 verifySparseModel<ValueType>(sparseModel, formulas, onlyInitialStatesRelevant);
             }
+            
+            // And export if required.
+            if(storm::settings::getModule<storm::settings::modules::IOSettings>().isExportExplicitSet()) {
+                std::ofstream ofs;
+                ofs.open(storm::settings::getModule<storm::settings::modules::IOSettings>().getExportExplicitFilename(), std::ofstream::out);
+                storm::exporter::explicitExportSparseModel(ofs, sparseModel, model.getParameterNames());
+                ofs.close();
+            }
         }
         
         template<typename ValueType>

src/settings/modules/IOSettings.cpp

@@ -14,7 +14,7 @@ namespace storm {
             
             const std::string IOSettings::moduleName = "io";
             const std::string IOSettings::exportDotOptionName = "exportdot";
-            const std::string IOSettings::exportMatOptionName = "exportmat";
+            const std::string IOSettings::exportExplicitOptionName = "exportexplicit";
             const std::string IOSettings::explicitOptionName = "explicit";
             const std::string IOSettings::explicitOptionShortName = "exp";
             const std::string IOSettings::prismInputOptionName = "prism";
@@ -34,7 +34,7 @@ namespace storm {
                 this->addOption(storm::settings::OptionBuilder(moduleName, prismCompatibilityOptionName, false, "Enables PRISM compatibility. This may be necessary to process some PRISM models.").setShortName(prismCompatibilityOptionShortName).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, exportDotOptionName, "", "If given, the loaded model will be written to the specified file in the dot format.")
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to which the model is to be written.").build()).build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, exportMatOptionName, "", "If given, the loaded model will be written to the specified file in the mat format.")
+                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, 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.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build())
@@ -66,6 +66,14 @@ namespace storm {
             std::string IOSettings::getExportDotFilename() const {
                 return this->getOption(exportDotOptionName).getArgumentByName("filename").getValueAsString();
             }
+            
+            bool IOSettings::isExportExplicitSet() const {
+                return this->getOption(exportExplicitOptionName).getHasOptionBeenSet();
+            }
+            
+            std::string IOSettings::getExportExplicitFilename() const {
+                return this->getOption(exportExplicitOptionName).getArgumentByName("filename").getValueAsString();
+            }
 
             bool IOSettings::isExplicitSet() const {
                 return this->getOption(explicitOptionName).getHasOptionBeenSet();

src/settings/modules/IOSettings.h

@@ -35,6 +35,22 @@ namespace storm {
                  */
                 std::string getExportDotFilename() const;
 
+                
+                /*!
+                 * Retrieves whether the export-to-explicit option was set
+                 *
+                 * @return True if the export-to-explicit option was set
+                 */
+                bool isExportExplicitSet() const;
+                
+                
+                /*!
+                 * Retrieves thename 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.
+                 */
+                std::string getExportExplicitFilename() const;
+                
                 /*!
                  * Retrieves whether the explicit option was set.
                  *
@@ -200,7 +216,7 @@ namespace storm {
             private:
                 // Define the string names of the options as constants.
                 static const std::string exportDotOptionName;
-                static const std::string exportMatOptionName;
+                static const std::string exportExplicitOptionName;
                 static const std::string explicitOptionName;
                 static const std::string explicitOptionShortName;
                 static const std::string prismInputOptionName;

src/storage/SymbolicModelDescription.cpp

@@ -57,6 +57,20 @@ namespace storm {
             return boost::get<storm::prism::Program>(modelDescription.get());
         }
         
+        std::vector<std::string> SymbolicModelDescription::getParameterNames() const {
+            std::vector<std::string> result;
+            if(isJaniModel()) {
+                for(auto const& c : asJaniModel().getUndefinedConstants()) {
+                    result.push_back(c.get().getName());
+                }
+            } else {
+                for(auto const& c : asPrismProgram().getUndefinedConstants()) {
+                    result.push_back(c.get().getName());
+                }
+            }
+            return result;
+        }
+        
         SymbolicModelDescription SymbolicModelDescription::toJani(bool makeVariablesGlobal) const {
             if (this->isJaniModel()) {
                 return *this;

src/storage/SymbolicModelDescription.h

@@ -27,6 +27,8 @@ namespace storm {
             storm::jani::Model const& asJaniModel() const;
             storm::prism::Program const& asPrismProgram() const;
             
+            std::vector<std::string> getParameterNames() const;
+            
             SymbolicModelDescription toJani(bool makeVariablesGlobal = true) const;
             
             SymbolicModelDescription preprocess(std::string const& constantDefinitionString = "") const;

src/utility/ExplicitExporter.cpp

@@ -0,0 +1,62 @@
+#include "ExplicitExporter.h"
+
+#include "src/adapters/CarlAdapter.h"
+#include "src/utility/macros.h"
+#include "src/exceptions/NotImplementedException.h"
+#include "src/models/sparse/Dtmc.h"
+#include "src/models/sparse/Mdp.h"
+
+#include "src/models/sparse/StandardRewardModel.h"
+
+
+namespace storm {
+    namespace exporter {
+        template<typename ValueType>
+        void explicitExportSparseModel(std::ostream& os, std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel,  std::vector<std::string> const& parameters) {
+            STORM_LOG_THROW(sparseModel->getType() == storm::models::ModelType::Mdp, storm::exceptions::NotImplementedException, "This functionality is not yet implemented." );
+            std::shared_ptr<storm::models::sparse::Mdp<ValueType>> mdp = sparseModel->template as<storm::models::sparse::Mdp<ValueType>>();
+
+            os << "// Exported by Storm" << std::endl;
+            os << "@type: mdp" << std::endl;
+            os << "@parameters" << std::endl;
+            for (auto const& p : parameters) {
+               os << p << " ";
+            }
+            os << std::endl;
+            os << "@nr_states" << std::endl  << mdp->getNumberOfStates() <<  std::endl;
+            os << "@model" << std::endl;
+            storm::storage::SparseMatrix<ValueType> const& matrix = mdp->getTransitionMatrix();
+            
+            for (typename storm::storage::SparseMatrix<ValueType>::index_type group = 0; group < matrix.getRowGroupCount(); ++group) {
+                os << "state " << group;
+                for(auto const& label : mdp->getStateLabeling().getLabelsOfState(group)) {
+                    os << " " << label;
+                }
+                os << std::endl;
+                typename storm::storage::SparseMatrix<ValueType>::index_type start = matrix.getRowGroupIndices()[group];
+                typename storm::storage::SparseMatrix<ValueType>::index_type end = matrix.getRowGroupIndices()[group + 1];
+                
+                for (typename storm::storage::SparseMatrix<ValueType>::index_type i = start; i < end; ++i) {
+                    // Print the actual row.
+                    os << "\taction";
+                    if(mdp->hasChoiceLabeling()) {
+                        //TODO
+                    }
+                    os << std::endl;
+                    for(auto it = matrix.begin(i); it != matrix.end(i); ++it) {
+                        os << "\t\t" << it->getColumn() << " : " << it->getValue() << std::endl;
+                    }
+                    
+                }
+            }
+            
+        }
+        
+        
+        
+        template void explicitExportSparseModel<double>(std::ostream& os, std::shared_ptr<storm::models::sparse::Model<double>> sparseModel, std::vector<std::string> const& parameters);
+        
+        template void explicitExportSparseModel<storm::RationalNumber>(std::ostream& os, std::shared_ptr<storm::models::sparse::Model<storm::RationalNumber>> sparseModel, std::vector<std::string> const& parameters);
+        template void explicitExportSparseModel<storm::RationalFunction>(std::ostream& os, std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> sparseModel, std::vector<std::string> const& parameters);
+    }
+}

src/utility/ExplicitExporter.h

@@ -0,0 +1,15 @@
+#pragma once
+#include <iostream>
+#include <memory>
+
+#include "src/models/sparse/Model.h"
+
+namespace storm {
+    namespace exporter {
+        
+        template<typename ValueType>
+        void explicitExportSparseModel(std::ostream& os, std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel, std::vector<std::string> const& parameters);
+        
+        
+    }
+}