deterministicScheds: changed setting to --purescheds and added memory pattern 'counter'

src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.cpp

@@ -44,6 +44,8 @@ namespace storm {
                             model = storm::transformer::MemoryIncorporation<SparseModelType>::incorporateGoalMemory(originalModel, originalFormula.getSubformulas());
                         } else if (schedRestr.getMemoryPattern() == storm::storage::SchedulerClass::MemoryPattern::Arbitrary && schedRestr.getMemoryStates() > 1) {
                             model = storm::transformer::MemoryIncorporation<SparseModelType>::incorporateFullMemory(originalModel, schedRestr.getMemoryStates());
+                        } else if (schedRestr.getMemoryPattern() == storm::storage::SchedulerClass::MemoryPattern::Counter && schedRestr.getMemoryStates() > 1) {
+                            model = storm::transformer::MemoryIncorporation<SparseModelType>::incorporateCountingMemory(originalModel, schedRestr.getMemoryStates());
                         } else if (schedRestr.isPositional()) {
                             model = std::make_shared<SparseModelType>(originalModel);
                         } else {

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<std::string> memoryPatterns = {"positional", "goalmemory", "arbitrary"};
+                std::vector<std::string> 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<std::string> 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 + ".");
                 }

src/storm/storage/SchedulerClass.h

@@ -11,6 +11,7 @@ namespace storm {
             enum class MemoryPattern {
                 Arbitrary,
                 GoalMemory,
+                Counter
             };
             
             SchedulerClass();

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<SparseModelType>(model, memory).build();
         }
+        
+        template <class SparseModelType>
+        std::shared_ptr<SparseModelType> MemoryIncorporation<SparseModelType>::incorporateCountingMemory(SparseModelType const& model, uint64_t memoryStates) {
+            auto memory = storm::storage::NondeterministicMemoryStructureBuilder().build(storm::storage::NondeterministicMemoryStructurePattern::SelectiveCounter, memoryStates);
+            return storm::storage::SparseModelNondeterministicMemoryProduct<SparseModelType>(model, memory).build();
+        }
 
         template class MemoryIncorporation<storm::models::sparse::Mdp<double>>;
         template class MemoryIncorporation<storm::models::sparse::MarkovAutomaton<double>>;

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<SparseModelType> 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<SparseModelType> incorporateCountingMemory(SparseModelType const& model, uint64_t memoryStates);
 
         };
     }