Storm 1.10.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
MinMaxLinearEquationSolver.h
Go to the documentation of this file.
1#pragma once
2
3#include <cstdint>
4#include <memory>
5#include <vector>
6
7#include <boost/optional.hpp>
8
14
17
18namespace storm {
19
20class Environment;
21
22namespace storage {
23template<typename T>
24class SparseMatrix;
25template<typename ValueType>
26class Scheduler;
27} // namespace storage
28
29namespace solver {
30
34template<typename ValueType, typename SolutionType = ValueType>
36 protected:
38
39 public:
41
42 virtual void setMatrix(storm::storage::SparseMatrix<ValueType> const& matrix) = 0;
44
55 bool solveEquations(Environment const& env, OptimizationDirection d, std::vector<SolutionType>& x, std::vector<ValueType> const& b) const;
56
62 void solveEquations(Environment const& env, std::vector<SolutionType>& x, std::vector<ValueType> const& b) const;
63
68
73
77 void setUncertaintyIsRobust(bool robust);
78
82 bool isUncertaintyRobust() const;
83
88 virtual void setSchedulerFixedForRowGroup(storm::storage::BitVector&& schedulerFixedForRowGroup);
89
93 void setHasUniqueSolution(bool value = true);
94
102 bool hasUniqueSolution() const;
103
107 void setHasNoEndComponents(bool value = true);
108
112 bool hasNoEndComponents() const;
113
118 void setTrackScheduler(bool trackScheduler = true);
119
123 bool isTrackSchedulerSet() const;
124
128 bool hasScheduler() const;
129
134
138 std::vector<uint_fast64_t> const& getSchedulerChoices() const;
139
143 std::vector<uint_fast64_t> const& getRobustSchedulerIndex() const;
144
149 void setCachingEnabled(bool value);
150
154 bool isCachingEnabled() const;
155
159 virtual void clearCache() const;
160
164 void setInitialScheduler(std::vector<uint_fast64_t>&& choices);
165
169 bool hasInitialScheduler() const;
170
174 std::vector<uint_fast64_t> const& getInitialScheduler() const;
175
181 boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none,
182 bool const& hasInitialScheduler = false) const;
183
188 void setRequirementsChecked(bool value = true);
189
193 bool isRequirementsCheckedSet() const;
194
195 protected:
196 virtual bool internalSolveEquations(Environment const& env, OptimizationDirection d, std::vector<SolutionType>& x,
197 std::vector<ValueType> const& b) const = 0;
198
201
204
206 mutable boost::optional<std::vector<uint_fast64_t>> schedulerChoices;
207
217 mutable boost::optional<std::vector<uint_fast64_t>> robustSchedulerIndex;
218
220 boost::optional<std::vector<uint_fast64_t>> initialScheduler;
221
223 boost::optional<storm::storage::BitVector> choiceFixedForRowGroup;
224
225 private:
227 bool uniqueSolution;
228
230 bool noEndComponents;
231
233 bool cachingEnabled;
234
236 bool requirementsChecked;
237
239 bool robustUncertainty;
240};
241
242template<typename ValueType, typename SolutionType = ValueType>
244 public:
247
248 std::unique_ptr<MinMaxLinearEquationSolver<ValueType, SolutionType>> create(Environment const& env,
249 storm::storage::SparseMatrix<ValueType> const& matrix) const;
250 std::unique_ptr<MinMaxLinearEquationSolver<ValueType, SolutionType>> create(Environment const& env, storm::storage::SparseMatrix<ValueType>&& matrix) const;
251 virtual std::unique_ptr<MinMaxLinearEquationSolver<ValueType, SolutionType>> create(Environment const& env) const = 0;
252
257 MinMaxLinearEquationSolverRequirements getRequirements(Environment const& env, bool hasUniqueSolution = false, bool hasNoEndComponents = false,
258 boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none,
259 bool hasInitialScheduler = false, bool trackScheduler = false) const;
260 void setRequirementsChecked(bool value = true);
261 bool isRequirementsCheckedSet() const;
262
263 private:
264 bool requirementsChecked;
265};
266
267template<typename ValueType, typename SolutionType = ValueType>
269 public:
271
272 // Make the other create methods visible.
273 using MinMaxLinearEquationSolverFactory<ValueType, SolutionType>::create;
274
275 virtual std::unique_ptr<MinMaxLinearEquationSolver<ValueType, SolutionType>> create(Environment const& env) const override;
276};
277
278} // namespace solver
279} // namespace storm
virtual std::unique_ptr< MinMaxLinearEquationSolver< ValueType, SolutionType > > create(Environment const &env) const override
MinMaxLinearEquationSolverRequirements getRequirements(Environment const &env, bool hasUniqueSolution=false, bool hasNoEndComponents=false, boost::optional< storm::solver::OptimizationDirection > const &direction=boost::none, bool hasInitialScheduler=false, bool trackScheduler=false) const
Retrieves the requirements of the solver that would be created when calling create() right now.
std::unique_ptr< MinMaxLinearEquationSolver< ValueType, SolutionType > > create(Environment const &env, storm::storage::SparseMatrix< ValueType > const &matrix) const
virtual std::unique_ptr< MinMaxLinearEquationSolver< ValueType, SolutionType > > create(Environment const &env) const =0
A class representing the interface that all min-max linear equation solvers shall implement.
virtual void setSchedulerFixedForRowGroup(storm::storage::BitVector &&schedulerFixedForRowGroup)
Sets the states for which the choices are fixed.
void unsetOptimizationDirection()
Unsets the optimization direction to use for calls to methods that do not explicitly provide one.
storm::storage::Scheduler< ValueType > computeScheduler() const
Retrieves the generated scheduler.
void setHasUniqueSolution(bool value=true)
Sets whether the solution to the min max equation system is known to be unique.
void setUncertaintyIsRobust(bool robust)
Set whether uncertainty should be interpreted adverserially (robust) or not.
bool solveEquations(Environment const &env, OptimizationDirection d, std::vector< SolutionType > &x, std::vector< ValueType > const &b) const
Solves the equation system x = min/max(A*x + b) given by the parameters.
boost::optional< std::vector< uint_fast64_t > > robustSchedulerIndex
For interval models, this index points into the schedulerChoices and is a state -> index map.
virtual void clearCache() const
Clears the currently cached data that has been stored during previous calls of the solver.
void setOptimizationDirection(OptimizationDirection direction)
Sets an optimization direction to use for calls to methods that do not explicitly provide one.
OptimizationDirectionSetting direction
The optimization direction to use for calls to functions that do not provide it explicitly....
boost::optional< std::vector< uint_fast64_t > > initialScheduler
A scheduler that can be used by solvers that require a valid initial scheduler.
void setInitialScheduler(std::vector< uint_fast64_t > &&choices)
Sets a valid initial scheduler that is required by some solvers (see requirements of solvers).
bool hasScheduler() const
Retrieves whether the solver generated a scheduler.
std::vector< uint_fast64_t > const & getSchedulerChoices() const
Retrieves the generated (deterministic) choices of the optimal scheduler.
std::vector< uint_fast64_t > const & getInitialScheduler() const
Retrieves the initial scheduler if one was set.
bool trackScheduler
Whether we generate a scheduler during solving.
void setRequirementsChecked(bool value=true)
Notifies the solver that the requirements for solving equations have been checked.
bool hasUniqueSolution() const
Retrieves whether the solution to the min max equation system is assumed to be unique.
virtual MinMaxLinearEquationSolverRequirements getRequirements(Environment const &env, boost::optional< storm::solver::OptimizationDirection > const &direction=boost::none, bool const &hasInitialScheduler=false) const
Retrieves the requirements of this solver for solving equations with the current settings.
boost::optional< storm::storage::BitVector > choiceFixedForRowGroup
void setHasNoEndComponents(bool value=true)
Sets whether the min max equation system is known to not have any end components.
bool isUncertaintyRobust() const
Is the uncertainty to be interpreted robustly (adverserially) or not?
std::vector< uint_fast64_t > const & getRobustSchedulerIndex() const
Retrieves the generated robust index into the scheduler.
bool isTrackSchedulerSet() const
Retrieves whether this solver is set to generate schedulers.
bool hasNoEndComponents() const
Retrieves whether the min max equation system is known to not have any end components.
virtual bool internalSolveEquations(Environment const &env, OptimizationDirection d, std::vector< SolutionType > &x, std::vector< ValueType > const &b) const =0
void setCachingEnabled(bool value)
Sets whether some of the generated data during solver calls should be cached.
bool isRequirementsCheckedSet() const
Retrieves whether the solver is aware that the requirements were checked.
bool isCachingEnabled() const
Retrieves whether some of the generated data during solver calls should be cached.
boost::optional< std::vector< uint_fast64_t > > schedulerChoices
The scheduler choices that induce the optimal values (if they could be successfully generated).
virtual void setMatrix(storm::storage::SparseMatrix< ValueType > const &matrix)=0
bool hasInitialScheduler() const
Returns true iff an initial scheduler is set.
void setTrackScheduler(bool trackScheduler=true)
Sets whether schedulers are generated when solving equation systems.
virtual void setMatrix(storm::storage::SparseMatrix< ValueType > &&matrix)=0
A bit vector that is internally represented as a vector of 64-bit values.
Definition BitVector.h:18
This class defines which action is chosen in a particular state of a non-deterministic model.
Definition Scheduler.h:18
A class that holds a possibly non-square matrix in the compressed row storage format.
LabParser.cpp.
Definition cli.cpp:18