diff --git a/src/storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.cpp b/src/storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.cpp index 454e9141a..38ffc9e11 100644 --- a/src/storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.cpp +++ b/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() { diff --git a/src/storm/settings/modules/MultiObjectiveSettings.cpp b/src/storm/settings/modules/MultiObjectiveSettings.cpp index 9d0cc8863..00d719f14 100644 --- a/src/storm/settings/modules/MultiObjectiveSettings.cpp +++ b/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 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 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> 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 diff --git a/src/storm/settings/modules/MultiObjectiveSettings.h b/src/storm/settings/modules/MultiObjectiveSettings.h index 577b57308..b2718ca04 100644 --- a/src/storm/settings/modules/MultiObjectiveSettings.h +++ b/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 diff --git a/src/storm/storage/SchedulerClass.cpp b/src/storm/storage/SchedulerClass.cpp index 42efb0160..e894f9553 100644 --- a/src/storm/storage/SchedulerClass.cpp +++ b/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); + } + } } diff --git a/src/storm/storage/SchedulerClass.h b/src/storm/storage/SchedulerClass.h index 05b32dd16..2a0b92c07 100644 --- a/src/storm/storage/SchedulerClass.h +++ b/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; }; } }