started to work on local EC-detection

Former-commit-id: 0f36a1bf78

src/modelchecker/reachability/SparseMdpLearningModelChecker.cpp

@@ -13,6 +13,7 @@
 
 #include "src/settings/SettingsManager.h"
 #include "src/settings/modules/GeneralSettings.h"
+#include "src/settings/modules/LearningSettings.h"
 
 #include "src/utility/macros.h"
 #include "src/exceptions/InvalidOperationException.h"
@@ -42,7 +43,7 @@ namespace storm {
             
             StateGeneration stateGeneration(program, variableInformation, getTargetStateExpression(subformula));
             
-            ExplorationInformation explorationInformation(variableInformation.getTotalBitOffset(true));
+            ExplorationInformation explorationInformation(variableInformation.getTotalBitOffset(true), storm::settings::learningSettings().isLocalECDetectionSet());
             explorationInformation.optimizationDirection = checkTask.isOptimizationDirectionSet() ? checkTask.getOptimizationDirection() : storm::OptimizationDirection::Maximize;
             
             // The first row group starts at action 0.
@@ -361,18 +362,29 @@ namespace storm {
             // Outline:
             // 1. construct a sparse transition matrix of the relevant part of the state space.
             // 2. use this matrix to compute an MEC decomposition.
-            // 3. if non-empty analyze the decomposition for accepting/rejecting MECs.
+            // 3. if non-empty, analyze the decomposition for accepting/rejecting MECs.
             
             // Start with 1.
             storm::storage::SparseMatrixBuilder<ValueType> builder(0, 0, 0, false, true, 0);
             
             // Determine the set of states that was expanded.
             std::vector<StateType> relevantStates;
-            for (StateType state = 0; state < explorationInformation.stateStorage.numberOfStates; ++state) {
-                // Add the state to the relevant states if it's unexplored. Additionally, if we are computing minimal
-                // probabilities, we only consider it relevant if it's not a target state.
-                if (!explorationInformation.isUnexplored(state) && (explorationInformation.maximize() || !comparator.isOne(bounds.getLowerBoundForState(state, explorationInformation)))) {
-                    relevantStates.push_back(state);
+            if (explorationInformation.useLocalECDetection()) {
+                for (auto const& stateActionPair : stack) {
+                    if (explorationInformation.maximize() || !comparator.isOne(bounds.getLowerBoundForState(stateActionPair.first, explorationInformation))) {
+                        relevantStates.push_back(stateActionPair.first);
+                    }
+                }
+                std::sort(relevantStates.begin(), relevantStates.end());
+                auto newEnd = std::unique(relevantStates.begin(), relevantStates.end());
+                relevantStates.resize(std::distance(relevantStates.begin(), newEnd));
+            } else {
+                for (StateType state = 0; state < explorationInformation.stateStorage.numberOfStates; ++state) {
+                    // Add the state to the relevant states if it's unexplored. Additionally, if we are computing minimal
+                    // probabilities, we only consider it relevant if it's not a target state.
+                    if (!explorationInformation.isUnexplored(state) && (explorationInformation.maximize() || !comparator.isOne(bounds.getLowerBoundForState(state, explorationInformation)))) {
+                        relevantStates.push_back(state);
+                    }
                 }
             }
             StateType sink = relevantStates.size();

src/modelchecker/reachability/SparseMdpLearningModelChecker.h

@@ -87,7 +87,7 @@ namespace storm {
             
             // A structure containing the data assembled during exploration.
             struct ExplorationInformation {
-                ExplorationInformation(uint_fast64_t bitsPerBucket, ActionType const& unexploredMarker = std::numeric_limits<ActionType>::max()) : stateStorage(bitsPerBucket), unexploredMarker(unexploredMarker) {
+                ExplorationInformation(uint_fast64_t bitsPerBucket, bool localECDetection, ActionType const& unexploredMarker = std::numeric_limits<ActionType>::max()) : stateStorage(bitsPerBucket), unexploredMarker(unexploredMarker), localECDetection(localECDetection) {
                     // Intentionally left empty.
                 }
                 
@@ -104,6 +104,7 @@ namespace storm {
                 StateSet terminalStates;
                 
                 std::unordered_map<StateType, ActionSetPointer> stateToLeavingActionsOfEndComponent;
+                bool localECDetection;
                 
                 void setInitialStates(std::vector<StateType> const& initialStates) {
                     stateStorage.initialStateIndices = initialStates;
@@ -199,6 +200,14 @@ namespace storm {
                 bool minimize() const {
                     return !maximize();
                 }
+                
+                bool useLocalECDetection() const {
+                    return localECDetection;
+                }
+
+                bool useGlobalECDetection() const {
+                    return !useLocalECDetection();
+                }
             };
             
             // A struct containg the lower and upper bounds per state and action.

src/settings/SettingsManager.cpp

@@ -26,6 +26,7 @@
 #include "src/settings/modules/ParametricSettings.h"
 #include "src/settings/modules/SparseDtmcEliminationModelCheckerSettings.h"
 #include "src/settings/modules/TopologicalValueIterationEquationSolverSettings.h"
+#include "src/settings/modules/LearningSettings.h"
 #include "src/utility/macros.h"
 #include "src/settings/Option.h"
 
@@ -547,5 +548,9 @@ namespace storm {
         storm::settings::modules::SparseDtmcEliminationModelCheckerSettings const& sparseDtmcEliminationModelCheckerSettings() {
             return dynamic_cast<storm::settings::modules::SparseDtmcEliminationModelCheckerSettings const&>(manager().getModule(storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::moduleName));
         }
+        
+        storm::settings::modules::LearningSettings const& learningSettings() {
+            return dynamic_cast<storm::settings::modules::LearningSettings const&>(manager().getModule(storm::settings::modules::LearningSettings::moduleName));
+        }
     }
 }

src/settings/SettingsManager.h

@@ -25,6 +25,7 @@ namespace storm {
             class TopologicalValueIterationEquationSolverSettings;
             class ParametricSettings;
             class SparseDtmcEliminationModelCheckerSettings;
+            class LearningSettings;
             class ModuleSettings;
         }
         class Option;
@@ -330,6 +331,12 @@ namespace storm {
          * @return An object that allows accessing the settings of the elimination-based DTMC model checker.
          */
         storm::settings::modules::SparseDtmcEliminationModelCheckerSettings const& sparseDtmcEliminationModelCheckerSettings();
+
+        /* Retrieves the settings of the learning engine.
+         *
+         * @return An object that allows accessing the settings of the learning engine.
+         */
+        storm::settings::modules::LearningSettings const& learningSettings();
         
     } // namespace settings
 } // namespace storm

src/settings/modules/LearningSettings.cpp

@@ -0,0 +1,52 @@
+#include "src/settings/modules/LearningSettings.h"
+#include "src/settings/modules/GeneralSettings.h"
+#include "src/settings/Option.h"
+#include "src/settings/OptionBuilder.h"
+#include "src/settings/ArgumentBuilder.h"
+#include "src/settings/Argument.h"
+#include "src/settings/SettingsManager.h"
+
+namespace storm {
+    namespace settings {
+        namespace modules {
+            
+            const std::string LearningSettings::moduleName = "learning";
+            const std::string LearningSettings::ecDetectionTypeOptionName = "ecdetection";
+            
+            LearningSettings::LearningSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) {
+                std::vector<std::string> types = { "local", "global" };
+                this->addOption(storm::settings::OptionBuilder(moduleName, ecDetectionTypeOptionName, true, "Sets the kind of EC-detection used. Available are: { local, global }.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the type to use.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(types)).setDefaultValueString("local").build()).build());
+            }
+            
+            bool LearningSettings::isLocalECDetectionSet() const {
+                if (this->getOption(ecDetectionTypeOptionName).getArgumentByName("name").getValueAsString() == "local") {
+                    return true;
+                }
+                return false;
+            }
+            
+            bool LearningSettings::isGlobalECDetectionSet() const {
+                if (this->getOption(ecDetectionTypeOptionName).getArgumentByName("name").getValueAsString() == "global") {
+                    return true;
+                }
+                return false;
+            }
+            
+            LearningSettings::ECDetectionType LearningSettings::getECDetectionType() const {
+                std::string typeAsString = this->getOption(ecDetectionTypeOptionName).getArgumentByName("name").getValueAsString();
+                if (typeAsString == "local") {
+                    return LearningSettings::ECDetectionType::Local;
+                } else if (typeAsString == "global") {
+                    return LearningSettings::ECDetectionType::Global;
+                }
+                STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown EC-detection type '" << typeAsString << "'.");
+            }
+            
+            bool LearningSettings::check() const {
+                bool optionsSet = this->getOption(ecDetectionTypeOptionName).getHasOptionBeenSet();
+                STORM_LOG_WARN_COND(storm::settings::generalSettings().getEngine() == storm::settings::modules::GeneralSettings::Engine::Learning || !optionsSet, "Bisimulation minimization is not selected, so setting options for bisimulation has no effect.");
+                return true;
+            }
+        } // namespace modules
+    } // namespace settings
+} // namespace storm

src/settings/modules/LearningSettings.h

@@ -0,0 +1,59 @@
+#ifndef STORM_SETTINGS_MODULES_LEARNINGSETTINGS_H_
+#define STORM_SETTINGS_MODULES_LEARNINGSETTINGS_H_
+
+#include "src/settings/modules/ModuleSettings.h"
+
+namespace storm {
+    namespace settings {
+        namespace modules {
+            
+            /*!
+             * This class represents the learning settings.
+             */
+            class LearningSettings : public ModuleSettings {
+            public:
+                // An enumeration of all available EC-detection types.
+                enum class ECDetectionType { Local, Global };
+                
+                /*!
+                 * Creates a new set of learning settings that is managed by the given manager.
+                 *
+                 * @param settingsManager The responsible manager.
+                 */
+                LearningSettings(storm::settings::SettingsManager& settingsManager);
+                
+                /*!
+                 * Retrieves whether local EC-detection is to be used.
+                 *
+                 * @return True iff local EC-detection is to be used.
+                 */
+                bool isLocalECDetectionSet() const;
+                
+                /*!
+                 * Retrieves whether global EC-detection is to be used.
+                 *
+                 * @return True iff global EC-detection is to be used.
+                 */
+                bool isGlobalECDetectionSet() const;
+                
+                /*!
+                 * Retrieves the selected EC-detection type.
+                 *
+                 * @return The selected EC-detection type.
+                 */
+                ECDetectionType getECDetectionType() const;
+                
+                virtual bool check() const override;
+                
+                // The name of the module.
+                static const std::string moduleName;
+                
+            private:
+                // Define the string names of the options as constants.
+                static const std::string ecDetectionTypeOptionName;
+            };
+        } // namespace modules
+    } // namespace settings
+} // namespace storm
+
+#endif /* STORM_SETTINGS_MODULES_LEARNINGSETTINGS_H_ */