Multiobjective: added setting for relative precision and encoding type.

src/storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.cpp

@@ -5,6 +5,7 @@
 #include "storm/utility/constants.h"
 #include "storm/utility/macros.h"
 
+#include "storm/exceptions/IllegalArgumentException.h"
 namespace storm {
         
     MultiObjectiveModelCheckerEnvironment::MultiObjectiveModelCheckerEnvironment() {
@@ -17,6 +18,22 @@ namespace storm {
         }
         
         precision = storm::utility::convertNumber<storm::RationalNumber>(multiobjectiveSettings.getPrecision());
+        if (multiobjectiveSettings.getPrecisionAbsolute()) {
+            precisionType = PrecisionType::Absolute;
+        } else if (multiobjectiveSettings.getPrecisionRelativeToDiff()) {
+            precisionType = PrecisionType::RelativeToDiff;
+        } else {
+            STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unhandled precision type.");
+        }
+        
+        if (multiobjectiveSettings.isAutoEncodingSet()) {
+            encodingType = EncodingType::Auto;
+        } else if (multiobjectiveSettings.isClassicEncodingSet()) {
+            encodingType = EncodingType::Classic;
+        } else if (multiobjectiveSettings.isFlowEncodingSet()) {
+            encodingType = EncodingType::Flow;
+        }
+        
         if (multiobjectiveSettings.isMaxStepsSet()) {
             maxSteps = multiobjectiveSettings.getMaxSteps();
         }
@@ -87,6 +104,22 @@ namespace storm {
         precision = value;
     }
     
+    typename MultiObjectiveModelCheckerEnvironment::PrecisionType const& MultiObjectiveModelCheckerEnvironment::getPrecisionType() const {
+        return precisionType;
+    }
+    
+    void MultiObjectiveModelCheckerEnvironment::setPrecisionType(PrecisionType const& value) {
+        precisionType = value;
+    }
+    
+    typename MultiObjectiveModelCheckerEnvironment::EncodingType const& MultiObjectiveModelCheckerEnvironment::getEncodingType() const {
+        return encodingType;
+    }
+    
+    void MultiObjectiveModelCheckerEnvironment::setEncodingType(EncodingType const& value) {
+        encodingType = value;
+    }
+    
     bool MultiObjectiveModelCheckerEnvironment::isMaxStepsSet() const {
         return maxSteps.is_initialized();
     }

src/storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.h

@@ -12,6 +12,17 @@ namespace storm {
     class MultiObjectiveModelCheckerEnvironment {
     public:
         
+        enum class PrecisionType {
+            Absolute, /// Absolute precision
+            RelativeToDiff /// Relative to the difference between largest and smallest objective value(s)
+        };
+        
+        enum class EncodingType {
+            Auto, /// Pick automatically
+            Classic, /// The classic backwards encoding
+            Flow /// The encoding as a flow network
+        };
+        
         MultiObjectiveModelCheckerEnvironment();
         ~MultiObjectiveModelCheckerEnvironment();
         
@@ -31,6 +42,11 @@ namespace storm {
         
         storm::RationalNumber const& getPrecision() const;
         void setPrecision(storm::RationalNumber const& value);
+        PrecisionType const& getPrecisionType() const;
+        void setPrecisionType(PrecisionType const& value);
+        
+        EncodingType const& getEncodingType() const;
+        void setEncodingType(EncodingType const& value);
         
         bool isMaxStepsSet() const;
         uint64_t const& getMaxSteps() const;
@@ -49,6 +65,8 @@ namespace storm {
         storm::modelchecker::multiobjective::MultiObjectiveMethod method;
         boost::optional<std::string> plotPathUnderApprox, plotPathOverApprox, plotPathParetoPoints;
         storm::RationalNumber precision;
+        PrecisionType precisionType;
+        EncodingType encodingType;
         boost::optional<uint64_t> maxSteps;
         boost::optional<storm::storage::SchedulerClass> schedulerRestriction;
         bool printResults;

src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp

@@ -22,6 +22,7 @@ namespace storm {
             
             template <class SparseModelType, typename GeometryValueType>
             std::unique_ptr<CheckResult> SparsePcaaParetoQuery<SparseModelType, GeometryValueType>::check(Environment const& env) {
+                STORM_LOG_THROW(env.modelchecker().multi().getPrecisionType() == MultiObjectiveModelCheckerEnvironment::PrecisionType::Absolute, storm::exceptions::IllegalArgumentException, "Unhandled multiobjective precision type.");
 
                 // Set the precision of the weight vector checker
                 typename SparseModelType::ValueType weightedPrecision = storm::utility::convertNumber<typename SparseModelType::ValueType>(env.modelchecker().multi().getPrecision());
@@ -51,6 +52,7 @@ namespace storm {
             
             template <class SparseModelType, typename GeometryValueType>
             void SparsePcaaParetoQuery<SparseModelType, GeometryValueType>::exploreSetOfAchievablePoints(Environment const& env) {
+                STORM_LOG_THROW(env.modelchecker().multi().getPrecisionType() == MultiObjectiveModelCheckerEnvironment::PrecisionType::Absolute, storm::exceptions::IllegalArgumentException, "Unhandled multiobjective precision type.");
 
                 //First consider the objectives individually
                 for(uint_fast64_t objIndex = 0; objIndex<this->objectives.size() && !this->maxStepsPerformed(env); ++objIndex) {

src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp

@@ -138,6 +138,7 @@ namespace storm {
 
             template <class SparseModelType, typename GeometryValueType>
             GeometryValueType SparsePcaaQuantitativeQuery<SparseModelType, GeometryValueType>::improveSolution(Environment const& env) {
+                STORM_LOG_THROW(env.modelchecker().multi().getPrecisionType() == MultiObjectiveModelCheckerEnvironment::PrecisionType::Absolute, storm::exceptions::IllegalArgumentException, "Unhandled multiobjective precision type.");
                 this->diracWeightVectorsToBeChecked.clear(); // Only check weight vectors that can actually improve the solution
             
                 WeightVector directionOfOptimizingObjective(this->objectives.size(), storm::utility::zero<GeometryValueType>());
@@ -185,6 +186,7 @@ namespace storm {
             template <class SparseModelType, typename GeometryValueType>
             void SparsePcaaQuantitativeQuery<SparseModelType, GeometryValueType>::updateWeightedPrecisionInImprovingPhase(Environment const& env, WeightVector const& weights) {
                 STORM_LOG_THROW(!storm::utility::isZero(weights[this->indexOfOptimizingObjective]), exceptions::UnexpectedException, "The chosen weight-vector gives zero weight for the objective that is to be optimized.");
+                STORM_LOG_THROW(env.modelchecker().multi().getPrecisionType() == MultiObjectiveModelCheckerEnvironment::PrecisionType::Absolute, storm::exceptions::IllegalArgumentException, "Unhandled multiobjective precision type.");
                 // If weighs[indexOfOptimizingObjective] is low, the computation of the weightVectorChecker needs to be more precise.
                 // Our heuristic ensures that if p is the new vertex of the under-approximation, then max{ eps | p' = p + (0..0 eps 0..0) is in the over-approximation } <= multiobjective_precision/0.9
                     GeometryValueType weightedPrecision = weights[this->indexOfOptimizingObjective] * storm::utility::convertNumber<GeometryValueType>(env.modelchecker().multi().getPrecision());

src/storm/settings/modules/MultiObjectiveSettings.cpp

@@ -18,21 +18,27 @@ namespace storm {
             const std::string MultiObjectiveSettings::maxStepsOptionName = "maxsteps";
             const std::string MultiObjectiveSettings::schedulerRestrictionOptionName = "schedrest";
             const std::string MultiObjectiveSettings::printResultsOptionName = "printres";
+            const std::string MultiObjectiveSettings::encodingOptionName = "encoding";
             
             MultiObjectiveSettings::MultiObjectiveSettings() : ModuleSettings(moduleName) {
                 std::vector<std::string> methods = {"pcaa", "constraintbased"};
                 this->addOption(storm::settings::OptionBuilder(moduleName, methodOptionName, true, "The method to be used for multi objective model checking.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the method to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(methods)).setDefaultValueString("pcaa").build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, exportPlotOptionName, true, "Saves data for plotting of pareto curves and achievable values.").setIsAdvanced()
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("directory", "A path to an existing directory in which the results will be saved.").build()).build());
+                std::vector<std::string> precTypes = {"abs", "reldiff"};
                 this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, true, "The precision used for the approximation of numerical- and pareto queries.").setIsAdvanced()
-                                .addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision.").setDefaultValueDouble(1e-04).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
+                                .addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision.").setDefaultValueDouble(1e-04).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build())
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("type", "The type of precision.").setDefaultValueString("abs").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(precTypes)).build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, maxStepsOptionName, true, "Aborts the computation after the given number of refinement steps (= computed pareto optimal points).").setIsAdvanced()
                                 .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("value", "the threshold for the number of refinement steps to be performed.").build()).build());
                 std::vector<std::string> memoryPatterns = {"positional", "goalmemory", "arbitrary"};
                 this->addOption(storm::settings::OptionBuilder(moduleName, schedulerRestrictionOptionName, false, "Restricts the class of considered schedulers to non-randomized schedulers with the provided memory pattern.")
-                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("memorypattern", "The Pattern of the memory.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(memoryPatterns)).build())
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("memorypattern", "The Pattern of the memory.").setDefaultValueString("positional").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(memoryPatterns)).build())
                                 .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("memorystates", "The Number of memory states (only if supported by the pattern).").setDefaultValueUnsignedInteger(0).build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, printResultsOptionName, true, "Prints intermediate results of the computation to standard output.").build());
+                std::vector<std::string> encodingTypes = {"auto", "classic", "flow"};
+                this->addOption(storm::settings::OptionBuilder(moduleName, encodingOptionName, true, "The prefered type of encoding for constraint-based methods.")
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("type", "The type.").setDefaultValueString("auto").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(encodingTypes)).build()).build());
             }
             
             storm::modelchecker::multiobjective::MultiObjectiveMethod MultiObjectiveSettings::getMultiObjectiveMethod() const {
@@ -61,6 +67,14 @@ namespace storm {
                 return this->getOption(precisionOptionName).getArgumentByName("value").getValueAsDouble();
             }
             
+            bool MultiObjectiveSettings::getPrecisionRelativeToDiff() const {
+                return this->getOption(precisionOptionName).getArgumentByName("type").getValueAsString() == "reldiff";
+            }
+            
+            bool MultiObjectiveSettings::getPrecisionAbsolute() const {
+                return this->getOption(precisionOptionName).getArgumentByName("type").getValueAsString() == "abs";
+            }
+            
             bool MultiObjectiveSettings::isMaxStepsSet() const {
                 return this->getOption(maxStepsOptionName).getHasOptionBeenSet();
             }
@@ -99,6 +113,18 @@ namespace storm {
                 return this->getOption(printResultsOptionName).getHasOptionBeenSet();
             }
             
+            bool MultiObjectiveSettings::isClassicEncodingSet() const {
+                return this->getOption(encodingOptionName).getArgumentByName("type").getValueAsString() == "classic";
+            }
+            
+            bool MultiObjectiveSettings::isFlowEncodingSet() const {
+                return this->getOption(encodingOptionName).getArgumentByName("type").getValueAsString() == "flow";
+            }
+            
+            bool MultiObjectiveSettings::isAutoEncodingSet() const {
+                return this->getOption(encodingOptionName).getArgumentByName("type").getValueAsString() == "auto";
+            }
+            
             bool MultiObjectiveSettings::check() const {
                 std::shared_ptr<storm::settings::ArgumentValidator<std::string>> validator = ArgumentValidatorFactory::createWritableFileValidator();
                 

src/storm/settings/modules/MultiObjectiveSettings.h

@@ -43,6 +43,16 @@ namespace storm {
 				 */
 				double getPrecision() const;
 				
+				/**
+				 * Retrieves whether the desired precision is considered to be absolute.
+				 */
+				bool getPrecisionAbsolute() const;
+				
+				/**
+				 * Retrieves whether the desired precision is considered to be relative to the difference between highest and lowest objective value(s)
+				 */
+				bool getPrecisionRelativeToDiff() const;
+				
                 /*!
                  * Retrieves whether or not a threshold for the number of performed refinement steps is given.
                  *
@@ -74,6 +84,20 @@ namespace storm {
 				 */
 				bool isPrintResultsSet() const;
 				
+				/*!
+				 * Retrieves whether the classic encoding for constraint-based methods is to be preferred.
+				 */
+                bool isClassicEncodingSet() const;
+                
+				/*!
+				 * Retrieves whether the flow encoding for constraint-based methods is to be preferred.
+				 */
+                bool isFlowEncodingSet() const;
+                
+				/*!
+				 * Retrieves whether the encoding for constraint-based methods should be picked automatically.
+				 */
+                bool isAutoEncodingSet() const;
                 
                 /*!
                  * Checks whether the settings are consistent. If they are inconsistent, an exception is thrown.
@@ -92,6 +116,7 @@ namespace storm {
 				const static std::string maxStepsOptionName;
 				const static std::string schedulerRestrictionOptionName;
 				const static std::string printResultsOptionName;
+				const static std::string encodingOptionName;
             };
             
         } // namespace modules