Improved LpMinMaxLinearEquationSolver, set relevant values in topo solvers

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;
 };

src/storm/settings/modules/TopologicalEquationSolverSettings.cpp

@@ -23,6 +23,7 @@ namespace modules {
 const std::string TopologicalEquationSolverSettings::moduleName = "topological";
 const std::string TopologicalEquationSolverSettings::underlyingEquationSolverOptionName = "eqsolver";
 const std::string TopologicalEquationSolverSettings::underlyingMinMaxMethodOptionName = "minmax";
+const std::string TopologicalEquationSolverSettings::extendRelevantValuesOptionName = "relevant-values";
 
 TopologicalEquationSolverSettings::TopologicalEquationSolverSettings() : ModuleSettings(moduleName) {
  std::vector<std::string> linearEquationSolver = {"gmm++", "native", "eigen", "elimination"};
@@ -35,8 +36,8 @@ TopologicalEquationSolverSettings::TopologicalEquationSolverSettings() : ModuleS
  .build())
  .build());
  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", "vi-to-pi"};
+ "vi", "value-iteration", "pi", "policy-iteration", "lp", "linear-programming", "rs",  "ratsearch",
+ "ii", "interval-iteration", "svi", "sound-value-iteration", "ovi", "optimistic-value-iteration", "vi-to-pi", "vi-to-lp"};
  this->addOption(storm::settings::OptionBuilder(moduleName, underlyingMinMaxMethodOptionName, true,
  "Sets which minmax method is considered for solving the underlying minmax equation systems.")
  .setIsAdvanced()
@@ -45,6 +46,11 @@ TopologicalEquationSolverSettings::TopologicalEquationSolverSettings() : ModuleS
  .setDefaultValueString("value-iteration")
  .build())
  .build());
+
+ this->addOption(
+ storm::settings::OptionBuilder(moduleName, extendRelevantValuesOptionName, true, "Sets whether relevant values are set to the underlying solver.")
+ .setIsAdvanced()
+ .build());
 }
 
 bool TopologicalEquationSolverSettings::isUnderlyingEquationSolverTypeSet() const {
@@ -97,11 +103,17 @@ storm::solver::MinMaxMethod TopologicalEquationSolverSettings::getUnderlyingMinM
  return storm::solver::MinMaxMethod::OptimisticValueIteration;
  } else if (minMaxEquationSolvingTechnique == "vi-to-pi") {
  return storm::solver::MinMaxMethod::ViToPi;
+ } else if (minMaxEquationSolvingTechnique == "vi-to-lp") {
+ return storm::solver::MinMaxMethod::ViToLp;
  }
 
  STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown underlying equation solver '" << minMaxEquationSolvingTechnique << "'.");
 }
 
+bool TopologicalEquationSolverSettings::isExtendRelevantValues() const {
+ return this->getOption(extendRelevantValuesOptionName).getHasOptionBeenSet();
+}
+
 bool TopologicalEquationSolverSettings::check() const {
  if (this->isUnderlyingEquationSolverTypeSet() && getUnderlyingEquationSolverType() == storm::solver::EquationSolverType::Topological) {
  STORM_LOG_WARN("Underlying solver type of the topological solver can not be the topological solver.");

src/storm/settings/modules/TopologicalEquationSolverSettings.h

@@ -60,6 +60,11 @@ class TopologicalEquationSolverSettings : public ModuleSettings {
  */
  storm::solver::MinMaxMethod getUnderlyingMinMaxMethod() const;
 
+ /*!
+ * If true, the relevant states of each SCC are computed and passed to the underlying equation solver.
+ */
+ bool isExtendRelevantValues() const;
+
  bool check() const override;
 
  // The name of the module.
@@ -69,6 +74,7 @@ class TopologicalEquationSolverSettings : public ModuleSettings {
  // Define the string names of the options as constants.
  static const std::string underlyingEquationSolverOptionName;
  static const std::string underlyingMinMaxMethodOptionName;
+ static const std::string extendRelevantValuesOptionName;
 };
 
 } // namespace modules

src/storm/solver/AbstractEquationSolver.cpp

@@ -75,6 +75,11 @@ void AbstractEquationSolver<ValueType>::setRelevantValues(storm::storage::BitVec
  this->relevantValues = std::move(relevantValues);
 }
 
+template<typename ValueType>
+void AbstractEquationSolver<ValueType>::setRelevantValues(storm::storage::BitVector const& relevantValues) {
+ this->relevantValues = relevantValues;
+}
+
 template<typename ValueType>
 void AbstractEquationSolver<ValueType>::clearRelevantValues() {
  relevantValues = boost::none;

src/storm/solver/AbstractEquationSolver.h

@@ -58,6 +58,11 @@ class AbstractEquationSolver {
  */
  void setRelevantValues(storm::storage::BitVector&& valuesOfInterest);
 
+ /*!
+ * Sets the relevant values.
+ */
+ void setRelevantValues(storm::storage::BitVector const& valuesOfInterest);
+
  /*!
  * Removes the values of interest (if there were any).
  */