From b24ba75909a12cfb2b5eda3fe396d2bdda72e3d7 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Thu, 3 Aug 2017 16:56:39 +0200 Subject: [PATCH] option to only get welldefinedness constraints for a parametric model --- src/storm-pars-cli/storm-pars.cpp | 23 +++++++++++++++++-- src/storm-pars/api/export.h | 10 ++++---- .../settings/modules/ParametricSettings.cpp | 7 +++++- .../settings/modules/ParametricSettings.h | 6 +++++ 4 files changed, 39 insertions(+), 7 deletions(-) diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index ce78713ee..0836f1e0d 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/src/storm-pars-cli/storm-pars.cpp @@ -194,7 +194,7 @@ namespace storm { auto parametricSettings = storm::settings::getModule(); if (parametricSettings.exportResultToFile() && model->isOfType(storm::models::ModelType::Dtmc)) { auto dtmc = model->template as>(); - storm::api::exportParametricResultToFile(result->asExplicitQuantitativeCheckResult()[*model->getInitialStates().begin()],storm::analysis::ConstraintCollector(*dtmc), parametricSettings.exportResultPath()); + storm::api::exportParametricResultToFile(boost::make_optional(result->asExplicitQuantitativeCheckResult()[*model->getInitialStates().begin()]),storm::analysis::ConstraintCollector(*dtmc), parametricSettings.exportResultPath()); } }); } @@ -272,6 +272,7 @@ namespace storm { void processInputWithValueTypeAndDdlib(SymbolicInput& input) { auto coreSettings = storm::settings::getModule(); auto ioSettings = storm::settings::getModule(); + auto parSettings = storm::settings::getModule(); 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> regions = parseRegions(model); - + + + if (model) { storm::cli::exportModel(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::api::exportParametricResultToFile(boost::none, storm::analysis::ConstraintCollector(*dtmc),parSettings.exportResultPath()); + return; + } else { + STORM_LOG_THROW(parSettings.exportResultToFile(), storm::exceptions::NotImplementedException, "Constraints for MDPs and CTMCs not implemented."); + + } + + } + + if (model) { verifyParametricModel(model, input, regions); } } diff --git a/src/storm-pars/api/export.h b/src/storm-pars/api/export.h index cae413bd8..69a6405de 100644 --- a/src/storm-pars/api/export.h +++ b/src/storm-pars/api/export.h @@ -7,19 +7,21 @@ namespace storm { namespace api { template - void exportParametricResultToFile(ValueType const& result, storm::analysis::ConstraintCollector const& constraintCollector, std::string const& path) { + void exportParametricResultToFile(boost::optional , storm::analysis::ConstraintCollector 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 const& constraintCollector, std::string const& path) { + inline void exportParametricResultToFile(boost::optional result, storm::analysis::ConstraintCollector const& constraintCollector, std::string const& path) { std::ofstream filestream; storm::utility::openFile(path, filestream); filestream << "$Parameters: "; - std::set vars = result.gatherVariables(); + auto const& vars = constraintCollector.getVariables(); std::copy(vars.begin(), vars.end(), std::ostream_iterator(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 stringConstraints; std::transform(constraintCollector.getWellformedConstraints().begin(), constraintCollector.getWellformedConstraints().end(), std::back_inserter(stringConstraints), [](carl::Formula const& c) -> std::string { return c.toString();}); diff --git a/src/storm-pars/settings/modules/ParametricSettings.cpp b/src/storm-pars/settings/modules/ParametricSettings.cpp index a50ef941e..28975aa5c 100644 --- a/src/storm-pars/settings/modules/ParametricSettings.cpp +++ b/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 diff --git a/src/storm-pars/settings/modules/ParametricSettings.h b/src/storm-pars/settings/modules/ParametricSettings.h index 436faa92d..e610f033d 100644 --- a/src/storm-pars/settings/modules/ParametricSettings.h +++ b/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