pretty printing of rational functions, rewards in the drn format, option for full build

Former-commit-id: 39676106c2 [formerly b80f259a87]
Former-commit-id: e6f493d6f9

src/settings/modules/IOSettings.cpp

@@ -29,6 +29,7 @@ namespace storm {
             const std::string IOSettings::constantsOptionShortName = "const";
             const std::string IOSettings::prismCompatibilityOptionName = "prismcompat";
             const std::string IOSettings::prismCompatibilityOptionShortName = "pc";
+            const std::string IOSettings::fullModelBuildOptionName = "buildfull";
             
             IOSettings::IOSettings() : ModuleSettings(moduleName) {
                 this->addOption(storm::settings::OptionBuilder(moduleName, prismCompatibilityOptionName, false, "Enables PRISM compatibility. This may be necessary to process some PRISM models.").setShortName(prismCompatibilityOptionShortName).build());
@@ -44,6 +45,8 @@ namespace storm {
                 this->addOption(storm::settings::OptionBuilder(moduleName, janiInputOptionName, false, "Parses the model given in the JANI format.")
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the JANI input.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, prismToJaniOptionName, false, "If set, the input PRISM model is transformed to JANI.").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, fullModelBuildOptionName, false, "If set, include all rewards and labels.").build());
+                
 
                 std::vector<std::string> explorationOrders = {"dfs", "bfs"};
                 this->addOption(storm::settings::OptionBuilder(moduleName, explorationOrderOptionName, false, "Sets which exploration order to use.").setShortName(explorationOrderOptionShortName)
@@ -57,6 +60,7 @@ namespace storm {
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the choice labels.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, constantsOptionName, false, "Specifies the constant replacements to use in symbolic models. Note that this requires the model to be given as an symbolic model (i.e., via --" + prismInputOptionName + " or --" + janiInputOptionName + ").").setShortName(constantsOptionShortName)
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("values", "A comma separated list of constants and their value, e.g. a=1,b=2,c=3.").setDefaultValueString("").build()).build());
+                
             }
 
             bool IOSettings::isExportDotSet() const {
@@ -164,6 +168,10 @@ namespace storm {
             bool IOSettings::isPrismCompatibilityEnabled() const {
                 return this->getOption(prismCompatibilityOptionName).getHasOptionBeenSet();
             }
+            
+            bool IOSettings::isBuildFullModelSet() const {
+                return this->getOption(fullModelBuildOptionName).getHasOptionBeenSet();
+            }
 
 			void IOSettings::finalize() {
             }

src/settings/modules/IOSettings.h

@@ -206,6 +206,13 @@ namespace storm {
                  * @return True iff the PRISM compatibility mode was enabled.
                  */
                 bool isPrismCompatibilityEnabled() const;
+                
+                /*!
+                 * Retrieves whether the full model should be build, that is, the model including all labels and rewards.
+                 *
+                 * @return true iff the full model should be build.
+                 */
+                bool isBuildFullModelSet() const;
 
                 bool check() const override;
                 void finalize() override;
@@ -231,6 +238,7 @@ namespace storm {
                 static const std::string constantsOptionShortName;
                 static const std::string prismCompatibilityOptionName;
                 static const std::string prismCompatibilityOptionShortName;
+                static const std::string fullModelBuildOptionName;
             };
 
         } // namespace modules

src/utility/ExplicitExporter.cpp

@@ -1,6 +1,7 @@
 #include "ExplicitExporter.h"
 
 #include "src/adapters/CarlAdapter.h"
+#include "src/utility/constants.h"
 #include "src/utility/macros.h"
 #include "src/exceptions/NotImplementedException.h"
 #include "src/models/sparse/Dtmc.h"
@@ -13,7 +14,7 @@ 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." );
+            STORM_LOG_THROW(sparseModel->getType() == storm::models::ModelType::Mdp || sparseModel->getType() == storm::models::ModelType::Dtmc , 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;
@@ -23,28 +24,71 @@ namespace storm {
                os << p << " ";
             }
             os << std::endl;
-            os << "@nr_states" << std::endl  << mdp->getNumberOfStates() <<  std::endl;
+            os << "@nr_states" << std::endl  << sparseModel->getNumberOfStates() <<  std::endl;
             os << "@model" << std::endl;
-            storm::storage::SparseMatrix<ValueType> const& matrix = mdp->getTransitionMatrix();
+            storm::storage::SparseMatrix<ValueType> const& matrix = sparseModel->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)) {
+                
+                bool first = true;
+                for (auto const& rewardModelEntry : sparseModel->getRewardModels()) {
+                    if (first) {
+                        os << " [";
+                        first = false;
+                    } else {
+                        os << ", ";
+                    }
+                    
+                    if(rewardModelEntry.second.hasStateRewards()) {
+                        os << rewardModelEntry.second.getStateRewardVector().at(group);
+                    } else {
+                        os << "0";
+                    }
+                    
+                }
+                if (!first) {
+                    os << "]";
+                }
+                
+                for(auto const& label : sparseModel->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];
+                typename storm::storage::SparseMatrix<ValueType>::index_type start = matrix.hasTrivialRowGrouping() ? group : matrix.getRowGroupIndices()[group];
+                typename storm::storage::SparseMatrix<ValueType>::index_type end = matrix.hasTrivialRowGrouping() ? group + 1 : 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()) {
+                    bool first = true;
+                    for (auto const& rewardModelEntry : sparseModel->getRewardModels()) {
+                        if (first) {
+                            os << " [";
+                            first = false;
+                        } else {
+                            os << ", ";
+                        }
+                        
+                        if(rewardModelEntry.second.hasStateActionRewards()) {
+                            os << storm::utility::to_string(rewardModelEntry.second.getStateActionRewardVector().at(i));
+                        } else {
+                            os << "0";
+                        }
+                        
+                    }
+                    if (!first) {
+                        os << "]";
+                    }
+
+                    
+                    
+                    if(sparseModel->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;
+                        os << "\t\t" << it->getColumn() << " : " << storm::utility::to_string(it->getValue()) << std::endl;
                     }
                     
                 }

src/utility/constants.cpp

@@ -56,7 +56,31 @@ namespace storm {
         bool isInteger(uint_fast64_t const& number) {
             return true;
         }
-
+        
+        template<typename ValueType>
+        std::string to_string(ValueType const& value) {
+            std::stringstream ss;
+            ss << value;
+            return ss.str();
+        }
+        
+        template<>
+        std::string to_string(RationalFunction const& f) {
+            std::stringstream ss;
+            if (f.isConstant())  {
+                if (f.denominator().isOne()) {
+                    ss << f.nominatorAsNumber();
+                } else {
+                    ss << f.nominatorAsNumber() << "/" << f.denominatorAsNumber();
+                }
+            } else if (f.denominator().isOne()) {
+                ss << f.nominatorAsPolynomial().coefficient() * f.nominatorAsPolynomial().polynomial();
+            } else {
+                ss << "(" << f.nominatorAsPolynomial() << ")/(" << f.denominatorAsPolynomial() << ")";
+            }
+            return ss.str();
+        }
+ 
 #ifdef STORM_HAVE_CARL
         template<>
         bool isOne(storm::RationalNumber const& a) {
@@ -275,6 +299,11 @@ namespace storm {
         template bool isInteger(float const& number);
 
         template float simplify(float value);
+        
+        template std::string to_string(float const& value);
+        template std::string to_string(double const& value);
+        template std::string to_string(storm::RationalNumber const& value);
+        template std::string to_string(storm::RationalFunction const& value);
 
         template storm::storage::MatrixEntry<storm::storage::sparse::state_type, float> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, float> matrixEntry);
         template storm::storage::MatrixEntry<storm::storage::sparse::state_type, float>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, float>& matrixEntry);

src/utility/constants.h

@@ -11,6 +11,7 @@
 
 #include <limits>
 #include <cstdint>
+#include <string>
 
 namespace storm {
     
@@ -59,6 +60,9 @@ namespace storm {
         
         template<typename ValueType>
         bool isInteger(ValueType const& number);
+        
+        template<typename ValueType>
+        std::string to_string(ValueType const& value);
     }
 }
 

src/utility/storm.h

@@ -108,7 +108,15 @@ namespace storm {
 
     template<typename ValueType>
     std::shared_ptr<storm::models::sparse::Model<ValueType>> buildSparseModel(storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) {
+        
+        
         storm::generator::NextStateGeneratorOptions options(formulas);
+        
+        
+        if (storm::settings::getModule<storm::settings::modules::IOSettings>().isBuildFullModelSet()) {
+            options.setBuildAllLabels();
+            options.setBuildAllRewardModels();
+        }
 
         // Generate command labels if we are going to build a counterexample later.
         if (storm::settings::getModule<storm::settings::modules::CounterexampleGeneratorSettings>().isMinimalCommandSetGenerationSet()) {