Adapted region settings and CLI to new features.

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

@@ -209,22 +209,31 @@ namespace storm {
             std::function<std::unique_ptr<storm::modelchecker::CheckResult>(std::shared_ptr<storm::logic::Formula const> const& formula)> verificationCallback;
             std::function<void(std::unique_ptr<storm::modelchecker::CheckResult> 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<storm::logic::Formula const> const& formula) {
-                                        ValueType refinementThreshold = storm::utility::convertNumber<ValueType>(regionSettings.getRefinementThreshold());
-                                        std::unique_ptr<storm::modelchecker::RegionRefinementCheckResult<ValueType>> result = storm::api::checkAndRefineRegionWithSparseEngine<ValueType>(model, storm::api::createTask<ValueType>(formula, true), regions.front(), engine, refinementThreshold);
+                                        ValueType refinementThreshold = storm::utility::convertNumber<ValueType>(regionSettings.getCoverageThreshold());
+                                        boost::optional<uint64_t> optionalDepthLimit;
+                                        if (regionSettings.isDepthLimitSet()) {
+                                            optionalDepthLimit = regionSettings.getDepthLimit();
+                                        }
+                                        std::unique_ptr<storm::modelchecker::RegionRefinementCheckResult<ValueType>> result = storm::api::checkAndRefineRegionWithSparseEngine<ValueType>(model, storm::api::createTask<ValueType>(formula, true), regions.front(), engine, refinementThreshold, optionalDepthLimit, regionSettings.getHypothesis());
                                         return result;
                                     };
             } else {
@@ -237,7 +246,7 @@ namespace storm {
             
             postprocessingCallback = [&] (std::unique_ptr<storm::modelchecker::CheckResult> const& result) {
                                         if (parametricSettings.exportResultToFile()) {
-                                            storm::api::exportRegionCheckResultToFile<ValueType>(result, parametricSettings.exportResultPath(), false);
+                                            storm::api::exportRegionCheckResultToFile<ValueType>(result, parametricSettings.exportResultPath());
                                         }
                                     };
             

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

@@ -1,3 +1,4 @@
+#include <storm-pars/modelchecker/region/RegionResultHypothesis.h>
 #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<std::string> 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<std::string> 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 {

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;