diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index 52d6dff39..32e609bbb 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/src/storm-pars-cli/storm-pars.cpp @@ -209,22 +209,31 @@ namespace storm { std::function(std::shared_ptr const& formula)> verificationCallback; std::function const&)> postprocessingCallback; + STORM_PRINT_AND_LOG(std::endl); + if (regionSettings.isHypothesisSet()) { + STORM_PRINT_AND_LOG("Checking hypothesis " << regionSettings.getHypothesis() << " on "); + } else { + STORM_PRINT_AND_LOG("Analyzing "); + } if (regions.size() == 1) { - STORM_PRINT_AND_LOG(std::endl << "Analyzing parameter region " << regions.front()); + STORM_PRINT_AND_LOG("parameter region " << regions.front()); } else { - STORM_PRINT_AND_LOG(std::endl << "Analyzing " << regions.size() << " parameter regions"); + STORM_PRINT_AND_LOG(regions.size() << " parameter regions"); } - auto engine = regionSettings.getRegionCheckEngine(); STORM_PRINT_AND_LOG(" using " << engine); // Check the given set of regions with or without refinement if (regionSettings.isRefineSet()) { STORM_LOG_THROW(regions.size() == 1, storm::exceptions::NotSupportedException, "Region refinement is not supported for multiple initial regions."); - STORM_PRINT_AND_LOG(" with iterative refinement until " << (1.0 - regionSettings.getRefinementThreshold()) * 100.0 << "% is covered." << std::endl); + STORM_PRINT_AND_LOG(" with iterative refinement until " << (1.0 - regionSettings.getCoverageThreshold()) * 100.0 << "% is covered." << (regionSettings.isDepthLimitSet() ? " Depth limit is " + std::to_string(regionSettings.getDepthLimit()) + "." : "") << std::endl); verificationCallback = [&] (std::shared_ptr const& formula) { - ValueType refinementThreshold = storm::utility::convertNumber(regionSettings.getRefinementThreshold()); - std::unique_ptr> result = storm::api::checkAndRefineRegionWithSparseEngine(model, storm::api::createTask(formula, true), regions.front(), engine, refinementThreshold); + ValueType refinementThreshold = storm::utility::convertNumber(regionSettings.getCoverageThreshold()); + boost::optional optionalDepthLimit; + if (regionSettings.isDepthLimitSet()) { + optionalDepthLimit = regionSettings.getDepthLimit(); + } + std::unique_ptr> result = storm::api::checkAndRefineRegionWithSparseEngine(model, storm::api::createTask(formula, true), regions.front(), engine, refinementThreshold, optionalDepthLimit, regionSettings.getHypothesis()); return result; }; } else { @@ -237,7 +246,7 @@ namespace storm { postprocessingCallback = [&] (std::unique_ptr const& result) { if (parametricSettings.exportResultToFile()) { - storm::api::exportRegionCheckResultToFile(result, parametricSettings.exportResultPath(), false); + storm::api::exportRegionCheckResultToFile(result, parametricSettings.exportResultPath()); } }; diff --git a/src/storm-pars/settings/modules/RegionSettings.cpp b/src/storm-pars/settings/modules/RegionSettings.cpp index 2dba3c300..97714b439 100644 --- a/src/storm-pars/settings/modules/RegionSettings.cpp +++ b/src/storm-pars/settings/modules/RegionSettings.cpp @@ -1,3 +1,4 @@ +#include #include "storm-pars/settings/modules/RegionSettings.h" #include "storm/settings/Option.h" @@ -7,6 +8,7 @@ #include "storm/utility/macros.h" #include "storm/exceptions/IllegalArgumentValueException.h" +#include "storm/exceptions/InvalidOperationException.h" namespace storm { namespace settings { @@ -15,6 +17,8 @@ namespace storm { const std::string RegionSettings::moduleName = "region"; const std::string RegionSettings::regionOptionName = "region"; const std::string RegionSettings::regionShortOptionName = "reg"; + const std::string RegionSettings::hypothesisOptionName = "hypothesis"; + const std::string RegionSettings::hypothesisShortOptionName = "hyp"; const std::string RegionSettings::refineOptionName = "refine"; const std::string RegionSettings::checkEngineOptionName = "engine"; const std::string RegionSettings::printNoIllustrationOptionName = "noillustration"; @@ -24,8 +28,13 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, regionOptionName, false, "Sets the region(s) considered for analysis.").setShortName(regionShortOptionName) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("regioninput", "The region(s) given in format a<=x<=b,c<=y<=d seperated by ';'. Can also be a file.").build()).build()); + std::vector hypotheses = {"unknown", "allsat", "allviolated"}; + this->addOption(storm::settings::OptionBuilder(moduleName, hypothesisOptionName, false, "Sets a hypothesis for region analysis. If given, the region(s) are only analyzed w.r.t. that hypothesis.").setShortName(hypothesisShortOptionName) + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("hypothesis", "The hypothesis.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(hypotheses)).setDefaultValueString("unknown").build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, refineOptionName, false, "Enables region refinement.") - .addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("threshold", "Refinement converges if the fraction of unknown area falls below this threshold.").setDefaultValueDouble(0.05).addValidatorDouble(storm::settings::ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0,1.0)).build()).build()); + .addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("coverage-threshold", "Refinement converges if the fraction of unknown area falls below this threshold.").setDefaultValueDouble(0.05).addValidatorDouble(storm::settings::ArgumentValidatorFactory::createDoubleRangeValidatorIncluding(0.0,1.0)).build()) + .addArgument(storm::settings::ArgumentBuilder::createIntegerArgument("depth-limit", "If given, limits the number of times a region is refined.").setDefaultValueInteger(-1).build()).build()); std::vector engines = {"pl", "exactpl", "validatingpl"}; this->addOption(storm::settings::OptionBuilder(moduleName, checkEngineOptionName, true, "Sets which engine is used for analyzing regions.") @@ -44,12 +53,44 @@ namespace storm { return this->getOption(regionOptionName).getArgumentByName("regioninput").getValueAsString(); } + bool RegionSettings::isHypothesisSet() const { + return this->getOption(hypothesisOptionName).getHasOptionBeenSet(); + } + + storm::modelchecker::RegionResultHypothesis RegionSettings::getHypothesis() const { + std::string hypString = this->getOption(hypothesisOptionName).getArgumentByName("hypothesis").getValueAsString(); + + storm::modelchecker::RegionResultHypothesis result; + + if (hypString == "unknown") { + result = storm::modelchecker::RegionResultHypothesis::Unknown; + } else if (hypString == "allsat") { + result = storm::modelchecker::RegionResultHypothesis::AllSat; + } else if (hypString == "allviolated") { + result = storm::modelchecker::RegionResultHypothesis::AllViolated; + } else { + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Hypothesis " << hypString << " not known."); + } + + return result; + } + bool RegionSettings::isRefineSet() const { return this->getOption(refineOptionName).getHasOptionBeenSet(); } - double RegionSettings::getRefinementThreshold() const { - return this->getOption(refineOptionName).getArgumentByName("threshold").getValueAsDouble(); + double RegionSettings::getCoverageThreshold() const { + return this->getOption(refineOptionName).getArgumentByName("coverage-threshold").getValueAsDouble(); + } + + bool RegionSettings::isDepthLimitSet() const { + return this->getOption(refineOptionName).getArgumentByName("depth-limit").getHasBeenSet() && this->getOption(refineOptionName).getArgumentByName("depth-limit").getValueAsInteger() >= 0; + } + + uint64_t RegionSettings::getDepthLimit() const { + int64_t depth = this->getOption(refineOptionName).getArgumentByName("depth-limit").getValueAsInteger(); + STORM_LOG_THROW(depth >= 0, storm::exceptions::InvalidOperationException, "Tried to retrieve the depth limit but it was not set."); + return (uint64_t) depth; } storm::modelchecker::RegionCheckEngine RegionSettings::getRegionCheckEngine() const { diff --git a/src/storm-pars/settings/modules/RegionSettings.h b/src/storm-pars/settings/modules/RegionSettings.h index e668a3146..0efb45d2f 100644 --- a/src/storm-pars/settings/modules/RegionSettings.h +++ b/src/storm-pars/settings/modules/RegionSettings.h @@ -1,6 +1,7 @@ #pragma once #include "storm-pars/modelchecker/region/RegionCheckEngine.h" +#include "storm-pars/modelchecker/region/RegionResultHypothesis.h" #include "storm/settings/modules/ModuleSettings.h" @@ -29,6 +30,16 @@ namespace storm { */ std::string getRegionString() const; + /*! + * Retrieves whether region(s) were declared + */ + bool isHypothesisSet() const; + + /*! + * Retrieves the region definition string + */ + storm::modelchecker::RegionResultHypothesis getHypothesis() const; + /*! * Retrieves whether region refinement is enabled */ @@ -38,8 +49,18 @@ namespace storm { * Retrieves the threshold considered for iterative region refinement. * The refinement converges as soon as the fraction of unknown area falls below this threshold */ - double getRefinementThreshold() const; + double getCoverageThreshold() const; + /*! + * Retrieves whether a depth threshold has been set for refinement + */ + bool isDepthLimitSet() const; + + /*! + * Returns the depth threshold (if set). It is illegal to call this method if no depth threshold has been set. + */ + uint64_t getDepthLimit() const; + /*! * Retrieves which type of region check should be performed */ @@ -60,6 +81,8 @@ namespace storm { private: const static std::string regionOptionName; const static std::string regionShortOptionName; + const static std::string hypothesisOptionName; + const static std::string hypothesisShortOptionName; const static std::string refineOptionName; const static std::string checkEngineOptionName; const static std::string printNoIllustrationOptionName;