added scheduler restriction setting

src/storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.cpp

@@ -20,6 +20,9 @@ namespace storm {
         if (multiobjectiveSettings.isMaxStepsSet()) {
             maxSteps = multiobjectiveSettings.getMaxSteps();
         }
+        if (multiobjectiveSettings.hasSchedulerRestriction()) {
+            schedulerRestriction = multiobjectiveSettings.getSchedulerRestriction();
+        }
     }
     
     MultiObjectiveModelCheckerEnvironment::~MultiObjectiveModelCheckerEnvironment() {

src/storm/settings/modules/MultiObjectiveSettings.cpp

@@ -16,6 +16,7 @@ namespace storm {
             const std::string MultiObjectiveSettings::exportPlotOptionName = "exportplot";
             const std::string MultiObjectiveSettings::precisionOptionName = "precision";
             const std::string MultiObjectiveSettings::maxStepsOptionName = "maxsteps";
+            const std::string MultiObjectiveSettings::schedulerRestrictionOptionName = "schedrest";
             
             MultiObjectiveSettings::MultiObjectiveSettings() : ModuleSettings(moduleName) {
                 std::vector<std::string> methods = {"pcaa", "constraintbased"};
@@ -26,6 +27,10 @@ namespace storm {
                                 .addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision.").setDefaultValueDouble(1e-04).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, maxStepsOptionName, true, "Aborts the computation after the given number of refinement steps (= computed pareto optimal points).")
                                 .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::createUnsignedIntegerArgument("memorystates", "The Number of memory states (only if supported by the pattern).").setDefaultValueUnsignedInteger(0).build()).build());
             }
             
             storm::modelchecker::multiobjective::MultiObjectiveMethod MultiObjectiveSettings::getMultiObjectiveMethod() const {
@@ -62,14 +67,49 @@ namespace storm {
                 return this->getOption(maxStepsOptionName).getArgumentByName("value").getValueAsUnsignedInteger();
             }
             
+            bool MultiObjectiveSettings::hasSchedulerRestriction() const {
+                return this->getOption(schedulerRestrictionOptionName).getHasOptionBeenSet();
+            }
+				
+            storm::storage::SchedulerClass MultiObjectiveSettings::getSchedulerRestriction() const {
+                storm::storage::SchedulerClass result;
+                result.setIsDeterministic(true);
+                
+                std::string pattern = this->getOption(schedulerRestrictionOptionName).getArgumentByName("memorypattern").getValueAsString();
+                uint64_t states = this->getOption(schedulerRestrictionOptionName).getArgumentByName("memorystates").getValueAsUnsignedInteger();
+                if (pattern == "positional") {
+                    result.setPositional();
+                    STORM_LOG_THROW(states <=1 , storm::exceptions::IllegalArgumentException, "The number of memory states should not be provided for the given memory pattern.");
+                } else if (pattern == "goalmemory") {
+                    result.setMemoryPattern(storm::storage::SchedulerClass::MemoryPattern::GoalMemory);
+                    STORM_LOG_THROW(states == 0, storm::exceptions::IllegalArgumentException, "The number of memory states should not be provided for the given memory pattern.");
+                } else if (pattern == "arbitrary") {
+                    STORM_LOG_THROW(states > 0, storm::exceptions::IllegalArgumentException, "Invalid number of memory states for provided Pattern. Please specify a positive number.");
+                    result.setMemoryPattern(storm::storage::SchedulerClass::MemoryPattern::Arbitrary);
+                    result.setMemoryStates(states);
+                } else {
+                    STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Invalid memory pattern: " + pattern + ".");
+                }
+                return result;
+            }
+				
             bool MultiObjectiveSettings::check() const {
                 std::shared_ptr<storm::settings::ArgumentValidator<std::string>> validator = ArgumentValidatorFactory::createWritableFileValidator();
                 
-                return !isExportPlotSet()
-                    || (validator->isValid(getExportPlotDirectory() + "boundaries.csv")
+                if (isExportPlotSet()) {
+                    if (!(validator->isValid(getExportPlotDirectory() + "boundaries.csv")
                         && validator->isValid(getExportPlotDirectory() + "overapproximation.csv")
                         && validator->isValid(getExportPlotDirectory() + "underapproximation.csv")
-                        && validator->isValid(getExportPlotDirectory() + "paretopoints.csv"));
+                        && validator->isValid(getExportPlotDirectory() + "paretopoints.csv"))) {
+                        return false;
+                    }
+                }
+    
+                if (hasSchedulerRestriction()) {
+                    getSchedulerRestriction();
+                }
+                
+                return true;
             }
 
         } // namespace modules

src/storm/settings/modules/MultiObjectiveSettings.h

@@ -3,6 +3,7 @@
 
 #include "storm/settings/modules/ModuleSettings.h"
 #include "storm/modelchecker/multiobjective/MultiObjectiveModelCheckingMethod.h"
+#include "storm/storage/SchedulerClass.h"
 
 namespace storm {
     namespace settings {
@@ -57,6 +58,16 @@ namespace storm {
                  */
                 uint_fast64_t getMaxSteps() const;
                 
+				/*!
+				 * Retrieves whether a scheduler restriction has been set.
+				 */
+				bool hasSchedulerRestriction() const;
+				
+				/*!
+				 * Retrieves the scheduler restriction if it has been set.
+				 */
+				storm::storage::SchedulerClass getSchedulerRestriction() const;
+				
                 
                 /*!
                  * Checks whether the settings are consistent. If they are inconsistent, an exception is thrown.
@@ -73,6 +84,7 @@ namespace storm {
 				const static std::string exportPlotOptionName;
 				const static std::string precisionOptionName;
 				const static std::string maxStepsOptionName;
+				const static std::string schedulerRestrictionOptionName;
             };
             
         } // namespace modules

src/storm/storage/SchedulerClass.cpp

@@ -4,7 +4,7 @@
 
 namespace storm {
     namespace storage {
-        SchedulerClass::SchedulerClass() : deterministic(false), memorystates(0) {
+        SchedulerClass::SchedulerClass() : deterministic(false), memorystates(0), memoryPattern(MemoryPattern::Arbitrary) {
             // Intentionally left empty
         }
         
@@ -21,6 +21,13 @@ namespace storm {
             return memorystates;
         }
         
+        SchedulerClass::MemoryPattern SchedulerClass::getMemoryPattern() const {
+            return memoryPattern;
+        }
+
+        bool SchedulerClass::isPositional() const {
+            return getMemoryStates() == 1 && getMemoryPattern() == MemoryPattern::Arbitrary;
+        }
         
         SchedulerClass& SchedulerClass::setIsDeterministic(bool value) {
             deterministic = value;
@@ -38,6 +45,14 @@ namespace storm {
             return *this;
         }
         
+        void SchedulerClass::setMemoryPattern(MemoryPattern const& pattern) {
+            memoryPattern = pattern;
+        }
+        
+        void SchedulerClass::setPositional() {
+            setMemoryPattern(MemoryPattern::Arbitrary);
+            setMemoryStates(1);
+        }
        
     }
 }

src/storm/storage/SchedulerClass.h

@@ -6,20 +6,30 @@ namespace storm {
     namespace storage {
         class SchedulerClass {
         public:
+            
+            enum class MemoryPattern {
+                Arbitrary,
+                GoalMemory,
+            };
+            
             SchedulerClass();
             
             bool isDeterministic() const;
             bool isMemoryBounded() const;
             uint64_t getMemoryStates() const;
-            
+            MemoryPattern getMemoryPattern() const;
+            bool isPositional() const;
             
             SchedulerClass& setIsDeterministic(bool value);
             SchedulerClass& setMemoryStates(uint64_t value);
             SchedulerClass& unsetMemoryStates();
+            void setMemoryPattern(MemoryPattern const& pattern);
+            void setPositional();
 
         private:
             bool deterministic;
             uint64_t memorystates;
+            MemoryPattern memoryPattern;
         };
     }
 }