Enable parsing of parametric DRN

src/storm/cli/cli.cpp

@@ -303,9 +303,18 @@ namespace storm {
                 if (ioSettings.isPropertySet()) {
                     properties = storm::parsePropertiesForExplicit(ioSettings.getProperty(), propertyFilter);
                 }
-                
-                buildAndCheckExplicitModel<double>(properties, true);
+
+                if (generalSettings.isParametricSet()) {
+#ifdef STORM_HAVE_CARL
+                    buildAndCheckExplicitModel<storm::RationalFunction>(properties, true);
+#else
+                    STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "No parameters are supported in this build.");
+#endif
+                } else {
+                    buildAndCheckExplicitModel<double>(properties, true);
+                }
             } else {
+
                 STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model.");
             }
         }

src/storm/cli/entrypoints.h

@@ -409,6 +409,35 @@ namespace storm {
                 verifySparseModel<ValueType>(model->as<storm::models::sparse::Model<ValueType>>(), properties, onlyInitialStatesRelevant);
             }
         }
+
+#ifdef STORM_HAVE_CARL
+        template<>
+        void buildAndCheckExplicitModel<storm::RationalFunction>(std::vector<storm::jani::Property> const& properties, bool onlyInitialStatesRelevant) {
+            storm::settings::modules::IOSettings const& settings = storm::settings::getModule<storm::settings::modules::IOSettings>();
+
+            STORM_LOG_THROW(settings.isExplicitSet() || settings.isExplicitDRNSet(), storm::exceptions::InvalidStateException, "Unable to build explicit model without model files.");
+
+            storm::utility::Stopwatch modelBuildingWatch(true);
+            std::shared_ptr<storm::models::ModelBase> model;
+            STORM_LOG_THROW(!settings.isExplicitSet(), storm::exceptions::NotSupportedException, "Parametric explicit model files are not supported.");
+            model = buildExplicitDRNModel<storm::RationalFunction>(settings.getExplicitDRNFilename());
+            modelBuildingWatch.stop();
+            STORM_PRINT_AND_LOG("Time for model construction: " << modelBuildingWatch << "." << std::endl);
+
+            // Preprocess the model if needed.
+            BRANCH_ON_MODELTYPE(model, model, storm::RationalFunction, storm::dd::DdType::CUDD, preprocessModel, extractFormulasFromProperties(properties));
+
+            // Print some information about the model.
+            model->printModelInformationToStream(std::cout);
+
+            // Verify the model, if a formula was given.
+            if (!properties.empty()) {
+                STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::InvalidStateException, "Expected sparse model.");
+                verifySparseModel<storm::RationalFunction>(model->as<storm::models::sparse::Model<storm::RationalFunction>>(), properties, onlyInitialStatesRelevant);
+            }
+        }
+#endif
+
     }
 }
 

src/storm/parser/DirectEncodingParser.cpp

@@ -20,8 +20,8 @@
 namespace storm {
     namespace parser {
 
-        template<>
-        void ValueParser<double>::addParameter(std::string const& parameter) {
+        template<typename ValueType>
+        void ValueParser<ValueType>::addParameter(std::string const& parameter) {
             STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameters are not supported in this build.");
         }
 

src/storm/utility/DirectEncodingExporter.cpp

@@ -16,7 +16,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) {
+        void explicitExportSparseModel(std::ostream& os, std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel, std::vector<std::string> const& parameters) {
 
             // Notice that for CTMCs we write the rate matrix instead of probabilities
 
@@ -33,8 +33,14 @@ namespace storm {
             os << "// Original model type: " << sparseModel->getType() << std::endl;
             os << "@type: " << sparseModel->getType() << std::endl;
             os << "@parameters" << std::endl;
-            for (auto const& p : parameters) {
-               os << p << " ";
+            if (parameters.empty()) {
+                for (std::string const& parameter : getParameters(sparseModel)) {
+                    os << parameter << " ";
+                }
+            } else {
+                for (std::string const& parameter : parameters) {
+                    os << parameter << " ";
+                }
             }
             os << std::endl;
             os << "@nr_states" << std::endl  << sparseModel->getNumberOfStates() <<  std::endl;
@@ -119,12 +125,33 @@ namespace storm {
             } // end matrix iteration
             
         }
-        
-        
-        
+
+        template<typename ValueType>
+        std::vector<std::string> getParameters(std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel) {
+            return {};
+        }
+
         template void explicitExportSparseModel<double>(std::ostream& os, std::shared_ptr<storm::models::sparse::Model<double>> sparseModel, std::vector<std::string> const& parameters);
 
 #ifdef STORM_HAVE_CARL
+        template<>
+        std::vector<std::string> getParameters(std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> sparseModel) {
+            std::vector<std::string> parameters;
+            std::set<storm::RationalFunctionVariable> parametersProb = storm::models::sparse::getProbabilityParameters(*sparseModel);
+            for (auto const& parameter : parametersProb) {
+                std::stringstream stream;
+                stream << parameter;
+                parameters.push_back(stream.str());
+            }
+            std::set<storm::RationalFunctionVariable> parametersReward = storm::models::sparse::getRewardParameters(*sparseModel);
+            for (auto const& parameter : parametersReward) {
+                std::stringstream stream;
+                stream << parameter;
+                parameters.push_back(stream.str());
+            }
+            return 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);
 #endif

src/storm/utility/DirectEncodingExporter.h

@@ -16,6 +16,15 @@ namespace storm {
          */
         template<typename ValueType>
         void explicitExportSparseModel(std::ostream& os, std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel, std::vector<std::string> const& parameters);
+
+        /*!
+         * Accumalate parameters in the model.
+         *
+         * @param sparseModel Model.
+         * @return List of parameters in the model.
+         */
+        template<typename ValueType>
+        std::vector<std::string> getParameters(std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel);
         
     }
 }