diff --git a/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.cpp b/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.cpp index 1888ab844..294a598ae 100644 --- a/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.cpp +++ b/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.cpp @@ -44,6 +44,8 @@ namespace storm { model = storm::transformer::MemoryIncorporation::incorporateGoalMemory(originalModel, originalFormula.getSubformulas()); } else if (schedRestr.getMemoryPattern() == storm::storage::SchedulerClass::MemoryPattern::Arbitrary && schedRestr.getMemoryStates() > 1) { model = storm::transformer::MemoryIncorporation::incorporateFullMemory(originalModel, schedRestr.getMemoryStates()); + } else if (schedRestr.getMemoryPattern() == storm::storage::SchedulerClass::MemoryPattern::Counter && schedRestr.getMemoryStates() > 1) { + model = storm::transformer::MemoryIncorporation::incorporateCountingMemory(originalModel, schedRestr.getMemoryStates()); } else if (schedRestr.isPositional()) { model = std::make_shared(originalModel); } else { diff --git a/src/storm/settings/modules/MultiObjectiveSettings.cpp b/src/storm/settings/modules/MultiObjectiveSettings.cpp index a263d030e..efb046cd1 100644 --- a/src/storm/settings/modules/MultiObjectiveSettings.cpp +++ b/src/storm/settings/modules/MultiObjectiveSettings.cpp @@ -16,7 +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"; + const std::string MultiObjectiveSettings::schedulerRestrictionOptionName = "purescheds"; const std::string MultiObjectiveSettings::printResultsOptionName = "printres"; const std::string MultiObjectiveSettings::encodingOptionName = "encoding"; @@ -31,9 +31,9 @@ namespace storm { .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 memoryPatterns = {"positional", "goalmemory", "arbitrary"}; + std::vector memoryPatterns = {"positional", "goalmemory", "arbitrary", "counter"}; 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.").setDefaultValueString("positional").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 encodingTypes = {"auto", "classic", "flow"}; @@ -100,9 +100,13 @@ namespace storm { 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."); + 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 if (pattern == "counter") { + 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::Counter); + result.setMemoryStates(states); } else { STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Invalid memory pattern: " + pattern + "."); } diff --git a/src/storm/storage/SchedulerClass.h b/src/storm/storage/SchedulerClass.h index caaf3c968..728643b95 100644 --- a/src/storm/storage/SchedulerClass.h +++ b/src/storm/storage/SchedulerClass.h @@ -11,6 +11,7 @@ namespace storm { enum class MemoryPattern { Arbitrary, GoalMemory, + Counter }; SchedulerClass(); diff --git a/src/storm/transformer/MemoryIncorporation.cpp b/src/storm/transformer/MemoryIncorporation.cpp index 613a9af3b..36a87e6e8 100644 --- a/src/storm/transformer/MemoryIncorporation.cpp +++ b/src/storm/transformer/MemoryIncorporation.cpp @@ -87,6 +87,12 @@ namespace storm { auto memory = storm::storage::NondeterministicMemoryStructureBuilder().build(storm::storage::NondeterministicMemoryStructurePattern::Full, memoryStates); return storm::storage::SparseModelNondeterministicMemoryProduct(model, memory).build(); } + + template + std::shared_ptr MemoryIncorporation::incorporateCountingMemory(SparseModelType const& model, uint64_t memoryStates) { + auto memory = storm::storage::NondeterministicMemoryStructureBuilder().build(storm::storage::NondeterministicMemoryStructurePattern::SelectiveCounter, memoryStates); + return storm::storage::SparseModelNondeterministicMemoryProduct(model, memory).build(); + } template class MemoryIncorporation>; template class MemoryIncorporation>; diff --git a/src/storm/transformer/MemoryIncorporation.h b/src/storm/transformer/MemoryIncorporation.h index 59ea28972..8e98c80c8 100644 --- a/src/storm/transformer/MemoryIncorporation.h +++ b/src/storm/transformer/MemoryIncorporation.h @@ -34,6 +34,11 @@ namespace storm { * Incorporates a memory structure where the nondeterminism of the model decides which successor state to choose. */ static std::shared_ptr incorporateFullMemory(SparseModelType const& model, uint64_t memoryStates); + + /*! + * Incorporates a memory structure where the nondeterminism of the model can increment a counter. + */ + static std::shared_ptr incorporateCountingMemory(SparseModelType const& model, uint64_t memoryStates); }; }