option to only get welldefinedness constraints for a parametric model

src/storm-pars-cli/storm-pars.cpp

@@ -194,7 +194,7 @@ namespace storm {
                                             auto parametricSettings = storm::settings::getModule<storm::settings::modules::ParametricSettings>();
                                             if (parametricSettings.exportResultToFile() && model->isOfType(storm::models::ModelType::Dtmc)) {
                                                 auto dtmc = model->template as<storm::models::sparse::Dtmc<ValueType>>();
-                                                storm::api::exportParametricResultToFile(result->asExplicitQuantitativeCheckResult<ValueType>()[*model->getInitialStates().begin()],storm::analysis::ConstraintCollector<ValueType>(*dtmc), parametricSettings.exportResultPath());
+                                                storm::api::exportParametricResultToFile(boost::make_optional<ValueType>(result->asExplicitQuantitativeCheckResult<ValueType>()[*model->getInitialStates().begin()]),storm::analysis::ConstraintCollector<ValueType>(*dtmc), parametricSettings.exportResultPath());
                                             }
                                         });
         }
@@ -272,6 +272,7 @@ namespace storm {
         void processInputWithValueTypeAndDdlib(SymbolicInput& input) {
             auto coreSettings = storm::settings::getModule<storm::settings::modules::CoreSettings>();
             auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
+            auto parSettings = storm::settings::getModule<storm::settings::modules::ParametricSettings>();
             
             auto engine = coreSettings.getEngine();
             STORM_LOG_THROW(engine == storm::settings::modules::CoreSettings::Engine::Sparse || engine == storm::settings::modules::CoreSettings::Engine::Hybrid || engine == storm::settings::modules::CoreSettings::Engine::Dd, storm::exceptions::InvalidSettingsException, "The selected engine is not supported for parametric models.");
@@ -296,9 +297,27 @@ namespace storm {
             }
             
             std::vector<storm::storage::ParameterRegion<ValueType>> regions = parseRegions<ValueType>(model);
-            
+
+
+
             if (model) {
                 storm::cli::exportModel<DdType, ValueType>(model, input);
+            }
+
+            if (parSettings.onlyObtainConstraints()) {
+                STORM_LOG_THROW(parSettings.exportResultToFile(), storm::exceptions::InvalidSettingsException, "When computing constraints, export path has to be specified.");
+                if (model->isOfType(storm::models::ModelType::Dtmc)) {
+                    auto dtmc = model->template as<storm::models::sparse::Dtmc<ValueType>>();
+                    storm::api::exportParametricResultToFile<ValueType>(boost::none, storm::analysis::ConstraintCollector<ValueType>(*dtmc),parSettings.exportResultPath());
+                    return;
+                } else {
+                    STORM_LOG_THROW(parSettings.exportResultToFile(), storm::exceptions::NotImplementedException, "Constraints for MDPs and CTMCs not implemented.");
+
+                }
+
+            }
+
+            if (model) {
                 verifyParametricModel<DdType, ValueType>(model, input, regions);
             }
         }

src/storm-pars/api/export.h

@@ -7,19 +7,21 @@ namespace storm {
     namespace api {
 
         template <typename ValueType>
-        void exportParametricResultToFile(ValueType const& result, storm::analysis::ConstraintCollector<ValueType> const& constraintCollector, std::string const& path) {
+        void exportParametricResultToFile(boost::optional<ValueType> , storm::analysis::ConstraintCollector<ValueType> const& constraintCollector, std::string const& path) {
             STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Cannot export non-parametric result.");
         }
 
         template <>
-        inline void exportParametricResultToFile(storm::RationalFunction const& result, storm::analysis::ConstraintCollector<storm::RationalFunction> const& constraintCollector, std::string const& path) {
+        inline void exportParametricResultToFile(boost::optional<storm::RationalFunction> result, storm::analysis::ConstraintCollector<storm::RationalFunction> const& constraintCollector, std::string const& path) {
             std::ofstream filestream;
             storm::utility::openFile(path, filestream);
             filestream << "$Parameters: ";
-            std::set<storm::RationalFunctionVariable> vars = result.gatherVariables();
+            auto const& vars = constraintCollector.getVariables();
             std::copy(vars.begin(), vars.end(), std::ostream_iterator<storm::RationalFunctionVariable>(filestream, "; "));
             filestream << std::endl;
-            filestream << "$Result: " << result.toString(false, true) << std::endl;
+            if(result) {
+                filestream << "$Result: " << result->toString(false, true) << std::endl;
+            }
             filestream << "$Well-formed Constraints: " << std::endl;
             std::vector<std::string> stringConstraints;
             std::transform(constraintCollector.getWellformedConstraints().begin(), constraintCollector.getWellformedConstraints().end(), std::back_inserter(stringConstraints), [](carl::Formula<typename storm::Polynomial::PolyType> const& c) ->  std::string { return c.toString();});

src/storm-pars/settings/modules/ParametricSettings.cpp

@@ -17,12 +17,14 @@ namespace storm {
             const std::string ParametricSettings::derivativesOptionName = "derivatives";
             const std::string ParametricSettings::transformContinuousOptionName = "transformcontinuous";
             const std::string ParametricSettings::transformContinuousShortOptionName = "tc";
+            const std::string ParametricSettings::onlyWellformednessConstraintsOptionName = "onlyconstraints";
             
             ParametricSettings::ParametricSettings() : ModuleSettings(moduleName) {
                 this->addOption(storm::settings::OptionBuilder(moduleName, exportResultOptionName, false, "A path to a file where the parametric result should be saved.")
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("path", "the location.").addValidatorString(ArgumentValidatorFactory::createWritableFileValidator()).build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, derivativesOptionName, false, "Sets whether to generate the derivatives of the resulting rational function.").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, transformContinuousOptionName, false, "Sets whether to transform a continuous time input model to a discrete time model.").setShortName(transformContinuousShortOptionName).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, onlyWellformednessConstraintsOptionName, false, "Sets whether you only want to obtain the wellformedness constraints").build());
             }
             
             bool ParametricSettings::exportResultToFile() const {
@@ -40,7 +42,10 @@ namespace storm {
             bool ParametricSettings::transformContinuousModel() const {
                 return this->getOption(transformContinuousOptionName).getHasOptionBeenSet();
             }
-            
+
+            bool ParametricSettings::onlyObtainConstraints() const {
+                return this->getOption(onlyWellformednessConstraintsOptionName).getHasOptionBeenSet();
+            }
 
         } // namespace modules
     } // namespace settings

src/storm-pars/settings/modules/ParametricSettings.h

@@ -41,6 +41,11 @@ namespace storm {
                  * Retrieves whether Continuous time models should be transformed to discrete time models
                  */
                 bool transformContinuousModel() const;
+
+                /*
+                 * Retrieves whether instead of model checking, only the wellformedness constraints should be obtained.
+                 */
+                bool onlyObtainConstraints() const;
 				
                 const static std::string moduleName;
                 
@@ -49,6 +54,7 @@ namespace storm {
                 const static std::string derivativesOptionName;
                 const static std::string transformContinuousOptionName;
                 const static std::string transformContinuousShortOptionName;
+                const static std::string onlyWellformednessConstraintsOptionName;
             };
             
         } // namespace modules