19template<
typename ValueType,
typename SolutionType>
24template<
typename ValueType,
typename SolutionType>
30template<
typename ValueType,
typename SolutionType>
36template<
typename ValueType,
typename SolutionType>
38 bool adaptPrecision)
const {
43 STORM_LOG_ASSERT(this->longestSccChainSize,
"Did not compute the longest SCC chain size although it is needed.");
44 storm::RationalNumber subEnvPrec =
45 subEnv.solver().minMax().getPrecision() / storm::utility::convertNumber<storm::RationalNumber>(this->longestSccChainSize.get());
46 subEnv.solver().minMax().setPrecision(subEnvPrec);
51template<
typename ValueType,
typename SolutionType>
53 std::vector<SolutionType>& x,
54 std::vector<ValueType>
const& b)
const {
55 STORM_LOG_ASSERT(x.size() == this->A->getRowGroupCount(),
"Provided x-vector has invalid size.");
56 STORM_LOG_ASSERT(b.size() == this->A->getRowCount(),
"Provided b-vector has invalid size.");
61 if (!this->sortedSccDecomposition || (needAdaptPrecision && !this->longestSccChainSize)) {
64 createSortedSccDecomposition(needAdaptPrecision);
67 << sccSw <<
". Found " << this->sortedSccDecomposition->size() <<
" SCC(s) containing a total of " << x.size()
68 <<
" states. Average SCC size is "
69 <<
static_cast<double>(this->A->getRowGroupCount()) /
static_cast<double>(this->sortedSccDecomposition->size()) <<
".");
73 needAdaptPrecision = needAdaptPrecision && (this->sortedSccDecomposition->size() != this->A->getRowGroupCount());
75 storm::Environment sccSolverEnvironment = getEnvironmentForUnderlyingSolver(env, needAdaptPrecision);
77 if (this->longestSccChainSize) {
78 STORM_LOG_INFO(
"Longest SCC chain size is " << this->longestSccChainSize.get());
81 bool returnValue =
true;
82 if (this->sortedSccDecomposition->size() == 1 && (!this->choiceFixedForRowGroup || this->choiceFixedForRowGroup.get().empty())) {
84 if (
auto const& scc = *this->sortedSccDecomposition->begin(); scc.size() == 1) {
86 if (this->isTrackSchedulerSet()) {
87 this->schedulerChoices = std::vector<uint64_t>(1);
89 returnValue = solveTrivialScc(*scc.begin(), dir, x, b);
91 returnValue = solveFullyConnectedEquationSystem(sccSolverEnvironment, dir, x, b);
95 if (this->isTrackSchedulerSet()) {
96 if (this->schedulerChoices) {
97 this->schedulerChoices.get().resize(x.size());
99 this->schedulerChoices = std::vector<uint64_t>(x.size());
102 std::optional<storm::storage::BitVector> newRelevantValues;
104 this->sortedSccDecomposition->size() < this->A->getRowGroupCount()) {
105 newRelevantValues = this->getRelevantValues();
107 std::vector<uint64_t> rowGroupToScc = this->sortedSccDecomposition->computeStateToSccIndexMap(this->A->getRowGroupCount());
108 for (uint64_t rowGroup = 0; rowGroup < this->A->getRowGroupCount(); ++rowGroup) {
109 auto currScc = rowGroupToScc[rowGroup];
110 for (
auto const& successor : this->A->getRowGroup(rowGroup)) {
111 if (rowGroupToScc[successor.getColumn()] != currScc) {
112 newRelevantValues->set(successor.getColumn(),
true);
119 uint64_t sccIndex = 0;
123 for (
auto const& scc : *this->sortedSccDecomposition) {
124 if (scc.size() == 1) {
125 returnValue = solveTrivialScc(*scc.begin(), dir, x, b) && returnValue;
128 sccRowGroupsAsBitVector.
clear();
129 sccRowsAsBitVector.
clear();
130 for (
auto const& group : scc) {
131 sccRowGroupsAsBitVector.
set(group,
true);
133 if (!this->choiceFixedForRowGroup || !this->choiceFixedForRowGroup.get()[group]) {
134 for (uint64_t row = this->A->getRowGroupIndices()[group]; row < this->A->getRowGroupIndices()[group + 1]; ++row) {
135 sccRowsAsBitVector.
set(row,
true);
138 auto row = this->A->getRowGroupIndices()[group] + this->getInitialScheduler()[group];
139 sccRowsAsBitVector.
set(row,
true);
140 STORM_LOG_TRACE(
"Fixing state " << group <<
" to choice " << this->getInitialScheduler()[group] <<
".");
143 returnValue = solveScc(sccSolverEnvironment, dir, sccRowGroupsAsBitVector, sccRowsAsBitVector, x, b, newRelevantValues) && returnValue;
148 STORM_LOG_WARN(
"Topological solver aborted after analyzing " << sccIndex <<
"/" << this->sortedSccDecomposition->size() <<
" SCCs.");
154 if (this->isTrackSchedulerSet()) {
155 if (!auxiliaryRowGroupVector) {
156 auxiliaryRowGroupVector = std::make_unique<std::vector<ValueType>>(this->A->getRowGroupCount());
158 this->schedulerChoices = std::vector<uint_fast64_t>(this->A->getRowGroupCount());
159 this->A->multiplyAndReduce(dir, this->A->getRowGroupIndices(), x, &b, *auxiliaryRowGroupVector.get(), &this->schedulerChoices.get());
163 if (!this->isCachingEnabled()) {
170template<
typename ValueType,
typename SolutionType>
173 this->sortedSccDecomposition = std::make_unique<storm::storage::StronglyConnectedComponentDecomposition<ValueType>>(
175 if (needLongestChainSize) {
176 this->longestSccChainSize = this->sortedSccDecomposition->getMaxSccDepth() + 1;
180template<
typename ValueType,
typename SolutionType>
181bool TopologicalMinMaxLinearEquationSolver<ValueType, SolutionType>::solveTrivialScc(uint64_t
const& sccState,
OptimizationDirection dir,
182 std::vector<ValueType>& globalX,
183 std::vector<ValueType>
const& globalB)
const {
184 ValueType& xi = globalX[sccState];
185 if (this->choiceFixedForRowGroup && this->choiceFixedForRowGroup.get()[sccState]) {
187 uint_fast64_t row = this->A->getRowGroupIndices()[sccState] + this->getInitialScheduler()[sccState];
188 ValueType rowValue = globalB[row];
189 bool hasDiagonalEntry =
false;
190 ValueType denominator;
191 for (
auto const& entry : this->A->getRow(row)) {
192 if (entry.getColumn() == sccState) {
193 hasDiagonalEntry =
true;
194 denominator = storm::utility::one<ValueType>() - entry.getValue();
196 rowValue += entry.getValue() * globalX[entry.getColumn()];
199 if (hasDiagonalEntry) {
202 "State " << sccState <<
" has a selfloop with probability '1-(" << denominator <<
")'. This could be an indication for numerical issues.");
211 xi = std::move(rowValue);
213 bool firstRow =
true;
215 for (uint64_t row = this->A->getRowGroupIndices()[sccState]; row < this->A->getRowGroupIndices()[sccState + 1]; ++row) {
217 bool hasDiagonalEntry =
false;
219 for (
auto const& entry : this->A->getRow(row)) {
220 if (entry.getColumn() == sccState) {
221 hasDiagonalEntry =
true;
222 denominator = storm::utility::one<ValueType>() - entry.getValue();
224 rowValue += entry.getValue() * globalX[entry.getColumn()];
227 if (hasDiagonalEntry) {
230 "State " << sccState <<
" has a selfloop with probability '1-(" << denominator <<
")'. This could be an indication for numerical issues.");
241 xi = std::move(rowValue);
247 xi = std::move(rowValue);
252 xi = std::move(rowValue);
258 if (this->isTrackSchedulerSet()) {
259 this->schedulerChoices.get()[sccState] = bestRow - this->A->getRowGroupIndices()[sccState];
261 STORM_LOG_THROW(!firstRow, storm::exceptions::UnexpectedException,
"Empty row group in MinMax equation system.");
266template<
typename ValueType,
typename SolutionType>
267bool TopologicalMinMaxLinearEquationSolver<ValueType, SolutionType>::solveFullyConnectedEquationSystem(
storm::Environment const& sccSolverEnvironment,
269 std::vector<ValueType>
const& b)
const {
270 STORM_LOG_ASSERT(!this->choiceFixedForRowGroup || this->choiceFixedForRowGroup.get().empty(),
271 "Expecting no fixed choices for states when solving the fully connected equation system");
272 if (!this->sccSolver) {
273 this->sccSolver = GeneralMinMaxLinearEquationSolverFactory<ValueType>().create(sccSolverEnvironment);
274 this->sccSolver->setCachingEnabled(
true);
276 this->sccSolver->setMatrix(*this->A);
277 this->sccSolver->setHasUniqueSolution(this->hasUniqueSolution());
278 this->sccSolver->setHasNoEndComponents(this->hasNoEndComponents());
279 this->sccSolver->setTrackScheduler(this->isTrackSchedulerSet());
280 if (this->hasInitialScheduler()) {
281 auto choices = this->getInitialScheduler();
282 this->sccSolver->setInitialScheduler(std::move(choices));
284 if (this->hasRelevantValues()) {
285 this->sccSolver->setRelevantValues(this->getRelevantValues());
287 auto req = this->sccSolver->getRequirements(sccSolverEnvironment, dir);
288 this->sccSolver->setBoundsFromOtherSolver(*
this);
289 if (req.upperBounds() && this->hasUpperBound()) {
290 req.clearUpperBounds();
292 if (req.lowerBounds() && this->hasLowerBound()) {
293 req.clearLowerBounds();
295 if (req.validInitialScheduler() && this->hasInitialScheduler()) {
296 req.clearValidInitialScheduler();
298 if (req.uniqueSolution() && this->hasUniqueSolution()) {
299 req.clearUniqueSolution();
301 STORM_LOG_THROW(!req.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException,
302 "Solver requirements " + req.getEnabledRequirementsAsString() +
" not checked.");
303 this->sccSolver->setRequirementsChecked(
true);
305 bool res = this->sccSolver->solveEquations(sccSolverEnvironment, dir, x, b);
306 if (this->isTrackSchedulerSet()) {
307 this->schedulerChoices = this->sccSolver->getSchedulerChoices();
312template<
typename ValueType,
typename SolutionType>
316 std::vector<ValueType>
const& globalB,
317 std::optional<storm::storage::BitVector>
const& globalRelevantValues)
const {
319 if (!this->sccSolver) {
320 this->sccSolver = GeneralMinMaxLinearEquationSolverFactory<ValueType>().create(sccSolverEnvironment);
321 this->sccSolver->setCachingEnabled(
true);
323 this->sccSolver->setHasUniqueSolution(this->hasUniqueSolution());
324 this->sccSolver->setHasNoEndComponents(this->hasNoEndComponents());
325 this->sccSolver->setTrackScheduler(this->isTrackSchedulerSet());
326 if (globalRelevantValues) {
327 this->sccSolver->setRelevantValues((*globalRelevantValues) % sccRowGroups);
331 if (this->choiceFixedForRowGroup) {
334 sccA = this->A->
getSubmatrix(
false, sccRows, sccRowGroups);
337 if (this->hasInitialScheduler()) {
341 storm::utility::vector::setVectorValues<uint_fast64_t>(sccInitChoices, choiceFixedForStateSCC, 0);
342 this->sccSolver->setInitialScheduler(std::move(sccInitChoices));
346 sccA = this->A->
getSubmatrix(
true, sccRowGroups, sccRowGroups);
349 if (this->hasInitialScheduler()) {
351 this->sccSolver->setInitialScheduler(std::move(sccInitChoices));
355 this->sccSolver->setMatrix(std::move(sccA));
361 std::vector<ValueType> sccB;
363 for (
auto row : sccRows) {
365 for (
auto const& entry : this->A->getRow(row)) {
366 if (!sccRowGroups.
get(entry.getColumn())) {
367 bi += entry.getValue() * globalX[entry.getColumn()];
370 sccB.push_back(std::move(bi));
373 auto req = this->sccSolver->getRequirements(sccSolverEnvironment, dir);
374 this->sccSolver->clearBounds();
377 this->sccSolver->setLowerBound(this->getLowerBound());
378 req.clearLowerBounds();
381 req.clearLowerBounds();
384 this->sccSolver->setUpperBound(this->getUpperBound());
385 req.clearUpperBounds();
388 req.clearUpperBounds();
392 if (req.validInitialScheduler() && (this->hasInitialScheduler() || this->hasNoEndComponents())) {
393 req.clearValidInitialScheduler();
395 if (req.uniqueSolution() && this->hasUniqueSolution()) {
396 req.clearUniqueSolution();
398 STORM_LOG_THROW(!req.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException,
399 "Solver requirements " + req.getEnabledRequirementsAsString() +
" not checked.");
400 this->sccSolver->setRequirementsChecked(
true);
403 bool res = this->sccSolver->solveEquations(sccSolverEnvironment, dir, sccX, sccB);
406 if (this->isTrackSchedulerSet()) {
416template<
typename ValueType,
typename SolutionType>
418 Environment const& env, boost::optional<storm::solver::OptimizationDirection>
const& direction,
bool const& hasInitialScheduler)
const {
421 this->hasNoEndComponents(), direction, hasInitialScheduler,
422 this->isTrackSchedulerSet());
425template<
typename ValueType,
typename SolutionType>
427 sortedSccDecomposition.reset();
428 longestSccChainSize = boost::none;
430 auxiliaryRowGroupVector.reset();
SolverEnvironment & solver()
TopologicalSolverEnvironment & topological()
bool isForceSoundness() const
storm::solver::MinMaxMethod const & getUnderlyingMinMaxMethod() const
bool const & isUnderlyingMinMaxMethodSetFromDefault() const
bool isExtendRelevantValues() const
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.
virtual void clearCache() const
Clears the currently cached data that has been stored during previous calls of the solver.
TopologicalMinMaxLinearEquationSolver()
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.
void clear()
Removes all set bits from the bit vector.
void set(uint_fast64_t index, bool value=true)
Sets the given truth value at the given index.
uint_fast64_t getNumberOfSetBits() const
Returns the number of bits that are set to true in this bit vector.
bool get(uint_fast64_t index) const
Retrieves the truth value of the bit at the given index and performs a bound check.
A class that holds a possibly non-square matrix in the compressed row storage format.
SparseMatrix getSubmatrix(bool useGroups, storm::storage::BitVector const &rowConstraint, storm::storage::BitVector const &columnConstraint, bool insertDiagonalEntries=false, storm::storage::BitVector const &makeZeroColumns=storm::storage::BitVector()) const
Creates a submatrix of the current matrix by dropping all rows and columns whose bits are not set to ...
A class that provides convenience operations to display run times.
bool updateProgress(uint64_t count)
Updates the progress to the current count and prints it if the delay passed.
void setMaxCount(uint64_t maxCount)
Sets the maximal possible count.
void startNewMeasurement(uint64_t startCount)
Starts a new measurement, dropping all progress information collected so far.
A class that provides convenience operations to display run times.
void stop()
Stop stopwatch and add measured time to total time.
#define STORM_LOG_INFO(message)
#define STORM_LOG_WARN(message)
#define STORM_LOG_TRACE(message)
#define STORM_LOG_ASSERT(cond, message)
#define STORM_LOG_THROW(cond, exception, message)
#define STORM_LOG_WARN_COND_DEBUG(cond, message)
SFTBDDChecker::ValueType ValueType
bool constexpr minimize(OptimizationDirection d)
bool isTerminate()
Check whether the program should terminate (due to some abort signal).
void setVectorValues(std::vector< T > &vector, storm::storage::BitVector const &positions, std::vector< T > const &values)
Sets the provided values at the provided positions in the given vector.
std::vector< Type > filterVector(std::vector< Type > const &in, storm::storage::BitVector const &filter)
NumberTraits< RationalType >::IntegerType denominator(RationalType const &number)
bool isAlmostZero(ValueType const &a)
bool isZero(ValueType const &a)
StronglyConnectedComponentDecompositionOptions & computeSccDepths(bool value=true)
Sets if scc depths can be retrieved.
StronglyConnectedComponentDecompositionOptions & forceTopologicalSort(bool value=true)
Enforces that the returned SCCs are sorted in a topological order.