Improved LpMinMaxLinearEquationSolver, set relevant values in topo solvers (#568)

* Added options to tweak the LP encoding
* Use RawMode instead of storm::expressions
* Add ViToLp Method to warm-start the procedure
* Topological solvers can now (optionally, if enabled) set relevant values for each SCC

---------

Co-authored-by: Sebastian Junges <[email protected]>

Author: tquatmann

src/storm/environment/SubEnvironment.cpp

@@ -58,6 +58,7 @@ template class SubEnvironment<NativeSolverEnvironment>;
 template class SubEnvironment<LongRunAverageSolverEnvironment>;
 template class SubEnvironment<TimeBoundedSolverEnvironment>;
 template class SubEnvironment<MinMaxSolverEnvironment>;
+template class SubEnvironment<MinMaxLpSolverEnvironment>;
 template class SubEnvironment<MultiplierEnvironment>;
 template class SubEnvironment<OviSolverEnvironment>;
 template class SubEnvironment<GameSolverEnvironment>;

src/storm/environment/solver/AllSolverEnvironments.h

@@ -4,6 +4,7 @@
 #include "storm/environment/solver/GameSolverEnvironment.h"
 #include "storm/environment/solver/GmmxxSolverEnvironment.h"
 #include "storm/environment/solver/LongRunAverageSolverEnvironment.h"
+#include "storm/environment/solver/MinMaxLpSolverEnvironment.h"
 #include "storm/environment/solver/MinMaxSolverEnvironment.h"
 #include "storm/environment/solver/MultiplierEnvironment.h"
 #include "storm/environment/solver/NativeSolverEnvironment.h"

src/storm/environment/solver/MinMaxLpSolverEnvironment.cpp

@@ -0,0 +1,33 @@
+#include "storm/environment/solver/MinMaxLpSolverEnvironment.h"
+#include "storm/settings/SettingsManager.h"
+#include "storm/settings/modules/MinMaxEquationSolverSettings.h"
+
+namespace storm {
+
+MinMaxLpSolverEnvironment::MinMaxLpSolverEnvironment() {
+    auto const& minMaxSettings = storm::settings::getModule<storm::settings::modules::MinMaxEquationSolverSettings>();
+    useNonTrivialBounds = minMaxSettings.getLpUseNonTrivialBounds();
+    optimizeOnlyForInitialState = minMaxSettings.getLpUseOnlyInitialStateAsObjective();
+    useEqualityForSingleActions = minMaxSettings.getLpUseEqualityForTrivialActions();
+}
+
+void MinMaxLpSolverEnvironment::setUseEqualityForSingleActions(bool newValue) {
+    useEqualityForSingleActions = newValue;
+}
+void MinMaxLpSolverEnvironment::setOptimizeOnlyForInitialState(bool newValue) {
+    optimizeOnlyForInitialState = newValue;
+}
+void MinMaxLpSolverEnvironment::setUseNonTrivialBounds(bool newValue) {
+    useNonTrivialBounds = newValue;
+}
+
+bool MinMaxLpSolverEnvironment::getUseEqualityForSingleActions() const {
+    return useEqualityForSingleActions;
+}
+bool MinMaxLpSolverEnvironment::getOptimizeOnlyForInitialState() const {
+    return optimizeOnlyForInitialState;
+}
+bool MinMaxLpSolverEnvironment::getUseNonTrivialBounds() const {
+    return useNonTrivialBounds;
+}
+}  // namespace storm

src/storm/environment/solver/MinMaxLpSolverEnvironment.h

@@ -0,0 +1,22 @@
+#pragma once
+
+namespace storm {
+class MinMaxLpSolverEnvironment {
+   public:
+    MinMaxLpSolverEnvironment();
+    virtual ~MinMaxLpSolverEnvironment() = default;
+
+    void setUseEqualityForSingleActions(bool newValue);
+    void setOptimizeOnlyForInitialState(bool newValue);
+    void setUseNonTrivialBounds(bool newValue);
+
+    bool getUseEqualityForSingleActions() const;
+    bool getOptimizeOnlyForInitialState() const;
+    bool getUseNonTrivialBounds() const;
+
+   private:
+    bool useEqualityForSingleActions;
+    bool optimizeOnlyForInitialState;
+    bool useNonTrivialBounds;
+};
+}  // namespace storm

src/storm/environment/solver/MinMaxSolverEnvironment.cpp

@@ -1,5 +1,6 @@
 #include "storm/environment/solver/MinMaxSolverEnvironment.h"
 
+#include "storm/environment/solver/MinMaxLpSolverEnvironment.h"
 #include "storm/settings/SettingsManager.h"
 #include "storm/settings/modules/MinMaxEquationSolverSettings.h"
 #include "storm/utility/constants.h"
@@ -76,6 +77,13 @@ void MinMaxSolverEnvironment::setMultiplicationStyle(storm::solver::Multiplicati
     multiplicationStyle = value;
 }
 
+MinMaxLpSolverEnvironment const& MinMaxSolverEnvironment::lp() const {
+    return lpEnvironment.get();
+}
+MinMaxLpSolverEnvironment& MinMaxSolverEnvironment::lp() {
+    return lpEnvironment.get();
+}
+
 bool MinMaxSolverEnvironment::isForceRequireUnique() const {
     return forceRequireUnique;
 }

src/storm/environment/solver/MinMaxSolverEnvironment.h

@@ -8,6 +8,8 @@
 
 namespace storm {
 
+class MinMaxLpSolverEnvironment;
+
 class MinMaxSolverEnvironment {
    public:
     MinMaxSolverEnvironment();
@@ -26,6 +28,8 @@ class MinMaxSolverEnvironment {
     void setMultiplicationStyle(storm::solver::MultiplicationStyle value);
     bool isForceRequireUnique() const;
     void setForceRequireUnique(bool value);
+    MinMaxLpSolverEnvironment const& lp() const;
+    MinMaxLpSolverEnvironment& lp();
 
    private:
     storm::solver::MinMaxMethod minMaxMethod;
@@ -35,5 +39,6 @@ class MinMaxSolverEnvironment {
     bool considerRelativeTerminationCriterion;
     storm::solver::MultiplicationStyle multiplicationStyle;
     bool forceRequireUnique;
+    SubEnvironment<MinMaxLpSolverEnvironment> lpEnvironment;
 };
 }  // namespace storm

src/storm/environment/solver/TopologicalSolverEnvironment.cpp

@@ -15,6 +15,7 @@ TopologicalSolverEnvironment::TopologicalSolverEnvironment() {
 
     underlyingMinMaxMethod = topologicalSettings.getUnderlyingMinMaxMethod();
     underlyingMinMaxMethodSetFromDefault = topologicalSettings.isUnderlyingMinMaxMethodSetFromDefaultValue();
+    extendRelevantValues = topologicalSettings.isExtendRelevantValues();
 }
 
 TopologicalSolverEnvironment::~TopologicalSolverEnvironment() {
@@ -51,4 +52,12 @@ void TopologicalSolverEnvironment::setUnderlyingMinMaxMethod(storm::solver::MinM
     underlyingMinMaxMethod = value;
 }
 
+bool TopologicalSolverEnvironment::isExtendRelevantValues() const {
+    return extendRelevantValues;
+}
+
+void TopologicalSolverEnvironment::setExtendRelevantValues(bool value) {
+    extendRelevantValues = value;
+}
+
 }  // namespace storm

src/storm/environment/solver/TopologicalSolverEnvironment.h

@@ -19,11 +19,15 @@ class TopologicalSolverEnvironment {
     bool const& isUnderlyingMinMaxMethodSetFromDefault() const;
     void setUnderlyingMinMaxMethod(storm::solver::MinMaxMethod value);
 
+    bool isExtendRelevantValues() const;
+    void setExtendRelevantValues(bool value);
+
    private:
     storm::solver::EquationSolverType underlyingEquationSolverType;
     bool underlyingEquationSolverTypeSetFromDefault;
 
     storm::solver::MinMaxMethod underlyingMinMaxMethod;
     bool underlyingMinMaxMethodSetFromDefault;
+    bool extendRelevantValues;
 };
 }  // namespace storm

src/storm/settings/modules/MinMaxEquationSolverSettings.cpp

@@ -19,12 +19,20 @@ const std::string precisionOptionName = "precision";
 const std::string absoluteOptionName = "absolute";
 const std::string valueIterationMultiplicationStyleOptionName = "vimult";
 const std::string forceUniqueSolutionRequirementOptionName = "force-require-unique";
+const std::string lpEqualityForUniqueActionsOptionName = "lp-eq-unique-actions";
+const std::string lpUseNonTrivialBoundsOptionName = "lp-use-nontrivial-bounds";
+const std::string lpOptimizeOnlyInitialStateOptionName = "lp-objective-type";
 
 MinMaxEquationSolverSettings::MinMaxEquationSolverSettings() : ModuleSettings(moduleName) {
-    std::vector<std::string> minMaxSolvingTechniques = {
-        "vi",     "value-iteration",    "pi",  "policy-iteration",      "lp",  "linear-programming",         "rs",          "ratsearch",
-        "ii",     "interval-iteration", "svi", "sound-value-iteration", "ovi", "optimistic-value-iteration", "topological", "vi-to-pi",
-        "acyclic"};
+    std::vector<std::string> minMaxSolvingTechniques = {"vi",          "value-iteration",
+                                                        "pi",          "policy-iteration",
+                                                        "lp",          "linear-programming",
+                                                        "rs",          "ratsearch",
+                                                        "ii",          "interval-iteration",
+                                                        "svi",         "sound-value-iteration",
+                                                        "ovi",         "optimistic-value-iteration",
+                                                        "topological", "vi-to-pi",
+                                                        "vi-to-lp",    "acyclic"};
     this->addOption(
         storm::settings::OptionBuilder(moduleName, solvingMethodOptionName, false, "Sets which min/max linear equation solving technique is preferred.")
             .setIsAdvanced()
@@ -69,6 +77,25 @@ MinMaxEquationSolverSettings::MinMaxEquationSolverSettings() : ModuleSettings(mo
                                                    "simplify solving but causes some overhead.")
                         .setIsAdvanced()
                         .build());
+
+    this->addOption(storm::settings::OptionBuilder(moduleName, lpEqualityForUniqueActionsOptionName, false,
+                                                   "If set, enforce equality in the LP encoding for actions with a unique state.")
+                        .setIsAdvanced()
+                        .build());
+
+    this->addOption(storm::settings::OptionBuilder(moduleName, lpUseNonTrivialBoundsOptionName, false, "If set, use nontrivial bounds in the LP encoding")
+                        .setIsAdvanced()
+                        .build());
+
+    std::vector<std::string> optimizationObjectiveTypes = {"all", "onlyinitial"};
+    this->addOption(
+        storm::settings::OptionBuilder(moduleName, lpOptimizeOnlyInitialStateOptionName, false, "What objective to prefer")
+            .setIsAdvanced()
+            .addArgument(storm::settings::ArgumentBuilder::createStringArgument("optimization-type", "What kind of optimization objective to prefer.")
+                             .addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(optimizationObjectiveTypes))
+                             .setDefaultValueString("all")
+                             .build())
+            .build());
 }
 
 storm::solver::MinMaxMethod MinMaxEquationSolverSettings::getMinMaxEquationSolvingMethod() const {
@@ -91,6 +118,8 @@ storm::solver::MinMaxMethod MinMaxEquationSolverSettings::getMinMaxEquationSolvi
         return storm::solver::MinMaxMethod::Topological;
     } else if (minMaxEquationSolvingTechnique == "vi-to-pi") {
         return storm::solver::MinMaxMethod::ViToPi;
+    } else if (minMaxEquationSolvingTechnique == "vi-to-lp") {
+        return storm::solver::MinMaxMethod::ViToLp;
     } else if (minMaxEquationSolvingTechnique == "acyclic") {
         return storm::solver::MinMaxMethod::Acyclic;
     }
@@ -147,6 +176,18 @@ bool MinMaxEquationSolverSettings::isForceUniqueSolutionRequirementSet() const {
     return this->getOption(forceUniqueSolutionRequirementOptionName).getHasOptionBeenSet();
 }
 
+bool MinMaxEquationSolverSettings::getLpUseOnlyInitialStateAsObjective() const {
+    return this->getOption(lpOptimizeOnlyInitialStateOptionName).getArgumentByName("optimization-type").getValueAsString() == "onlyinitial";
+}
+
+bool MinMaxEquationSolverSettings::getLpUseNonTrivialBounds() const {
+    return this->getOption(lpUseNonTrivialBoundsOptionName).getHasOptionBeenSet();
+}
+
+bool MinMaxEquationSolverSettings::getLpUseEqualityForTrivialActions() const {
+    return this->getOption(lpEqualityForUniqueActionsOptionName).getHasOptionBeenSet();
+}
+
 }  // namespace modules
 }  // namespace settings
 }  // namespace storm

src/storm/settings/modules/MinMaxEquationSolverSettings.h

@@ -95,6 +95,19 @@ class MinMaxEquationSolverSettings : public ModuleSettings {
      */
     bool isForceUniqueSolutionRequirementSet() const;
 
+    /*!
+     * Retrieves whether only initial states should occur in the optimization objective.
+     */
+    bool getLpUseOnlyInitialStateAsObjective() const;
+    /*!
+     * Retrieves whether additional bounds should be used when constructing the LP.
+     */
+    bool getLpUseNonTrivialBounds() const;
+    /*!
+     * Retrieves whether equality should be enforced where possible
+     */
+    bool getLpUseEqualityForTrivialActions() const;
+
     // The name of the module.
     static const std::string moduleName;
 };