Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
TopologicalMinMaxLinearEquationSolver.h
Go to the documentation of this file.
1#pragma once
2
3#include <optional>
4
6
9
10namespace storm {
11
12class Environment;
13
14namespace solver {
15
16template<typename ValueType, typename SolutionType = ValueType>
18 public:
22
24
25 virtual void clearCache() const override;
26
28 boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none,
29 bool const& hasInitialScheduler = false) const override;
30
31 protected:
32 virtual bool internalSolveEquations(storm::Environment const& env, OptimizationDirection d, std::vector<SolutionType>& x,
33 std::vector<ValueType> const& b) const override;
34
35 private:
36 storm::Environment getEnvironmentForUnderlyingSolver(storm::Environment const& env, bool adaptPrecision = false) const;
37
38 // Creates an SCC decomposition and sorts the SCCs according to a topological sort.
39 void createSortedSccDecomposition(bool needLongestChainSize) const;
40
41 // Solves the SCC with the given index
42 // ... for the case that the SCC is trivial
43 bool solveTrivialScc(uint64_t const& sccState, OptimizationDirection d, std::vector<ValueType>& globalX, std::vector<ValueType> const& globalB) const;
44 // ... for the case that there is just one large SCC
45 bool solveFullyConnectedEquationSystem(storm::Environment const& sccSolverEnvironment, OptimizationDirection d, std::vector<SolutionType>& x,
46 std::vector<ValueType> const& b) const;
47 // ... for the remaining cases (1 < scc.size() < x.size())
48 bool solveScc(storm::Environment const& sccSolverEnvironment, OptimizationDirection d, storm::storage::BitVector const& sccRowGroups,
49 storm::storage::BitVector const& sccRows, std::vector<ValueType>& globalX, std::vector<ValueType> const& globalB,
50 std::optional<storm::storage::BitVector> const& globalRelevantValues) const;
51
52 // cached auxiliary data
53 mutable std::unique_ptr<storm::storage::StronglyConnectedComponentDecomposition<ValueType>> sortedSccDecomposition;
54 mutable boost::optional<uint64_t> longestSccChainSize;
55 mutable std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> sccSolver;
56 mutable std::unique_ptr<std::vector<ValueType>> auxiliaryRowGroupVector; // A.rowGroupCount() entries
57};
58} // namespace solver
59} // namespace storm
OptimizationDirectionSetting direction
The optimization direction to use for calls to functions that do not provide it explicitly....
bool hasInitialScheduler() const
Returns true iff an initial scheduler is set.
storm::storage::SparseMatrix< ValueType > const * A
virtual bool internalSolveEquations(storm::Environment const &env, OptimizationDirection d, std::vector< SolutionType > &x, std::vector< ValueType > const &b) const override
virtual void clearCache() const override
Clears the currently cached data that has been stored during previous calls of the solver.
virtual MinMaxLinearEquationSolverRequirements getRequirements(Environment const &env, boost::optional< storm::solver::OptimizationDirection > const &direction=boost::none, bool const &hasInitialScheduler=false) const override
Retrieves the requirements of this solver for solving equations with the current settings.
A bit vector that is internally represented as a vector of 64-bit values.
Definition BitVector.h:18
A class that holds a possibly non-square matrix in the compressed row storage format.
LabParser.cpp.
Definition cli.cpp:18