Storm 1.10.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
NativeLinearEquationSolver.cpp
Go to the documentation of this file.
2
3#include <limits>
4
7
22
23namespace storm {
24namespace solver {
25
26template<typename ValueType>
28 // Intentionally left empty.
29}
30
31template<typename ValueType>
35
36template<typename ValueType>
40
41template<typename ValueType>
43 localA.reset();
44 this->A = &A;
45 clearCache();
46}
47
48template<typename ValueType>
50 localA = std::make_unique<storm::storage::SparseMatrix<ValueType>>(std::move(A));
51 this->A = localA.get();
52 clearCache();
53}
54
55template<typename ValueType>
57 if (!viOperator) {
58 viOperator = std::make_shared<helper::ValueIterationOperator<ValueType, true>>();
59 viOperator->setMatrixBackwards(*this->A);
60 }
61}
62
63template<typename ValueType>
64bool NativeLinearEquationSolver<ValueType>::solveEquationsSOR(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const& b,
65 ValueType const& omega) const {
66 STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with NativeLinearEquationSolver (Gauss-Seidel, SOR omega = " << omega << ")");
67
68 if (!this->cachedRowVector) {
69 this->cachedRowVector = std::make_unique<std::vector<ValueType>>(getMatrixRowCount());
70 }
71
72 ValueType precision = storm::utility::convertNumber<ValueType>(env.solver().native().getPrecision());
73 uint64_t maxIter = env.solver().native().getMaximalNumberOfIterations();
74 bool relative = env.solver().native().getRelativeTerminationCriterion();
75
76 // Set up additional environment variables.
77 uint_fast64_t iterations = 0;
79
80 this->startMeasureProgress();
81 while (status == SolverStatus::InProgress && iterations < maxIter) {
82 A->performSuccessiveOverRelaxationStep(omega, x, b);
83
84 // Now check if the process already converged within our precision.
85 if (storm::utility::vector::equalModuloPrecision<ValueType>(*this->cachedRowVector, x, precision, relative)) {
87 }
88 // If we did not yet converge, we need to backup the contents of x.
89 if (status != SolverStatus::Converged) {
90 *this->cachedRowVector = x;
91 }
92
93 // Potentially show progress.
94 this->showProgressIterative(iterations);
95
96 // Increase iteration count so we can abort if convergence is too slow.
97 ++iterations;
98
99 status = this->updateStatus(status, x, SolverGuarantee::None, iterations, maxIter);
100 }
101
102 if (!this->isCachingEnabled()) {
103 clearCache();
104 }
105
106 this->reportStatus(status, iterations);
107
108 return status == SolverStatus::Converged;
109}
110
111template<typename ValueType>
112NativeLinearEquationSolver<ValueType>::JacobiDecomposition::JacobiDecomposition(Environment const& env, storm::storage::SparseMatrix<ValueType> const& A) {
113 auto decomposition = A.getJacobiDecomposition();
114 this->LUMatrix = std::move(decomposition.first);
115 this->DVector = std::move(decomposition.second);
116 this->multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, this->LUMatrix);
117}
118
119template<typename ValueType>
120bool NativeLinearEquationSolver<ValueType>::solveEquationsJacobi(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
121 STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with NativeLinearEquationSolver (Jacobi)");
122
123 if (!this->cachedRowVector) {
124 this->cachedRowVector = std::make_unique<std::vector<ValueType>>(getMatrixRowCount());
125 }
126
127 // Get a Jacobi decomposition of the matrix A.
128 if (!jacobiDecomposition) {
129 jacobiDecomposition = std::make_unique<JacobiDecomposition>(env, *A);
130 }
131
132 ValueType precision = storm::utility::convertNumber<ValueType>(env.solver().native().getPrecision());
133 uint64_t maxIter = env.solver().native().getMaximalNumberOfIterations();
134 bool relative = env.solver().native().getRelativeTerminationCriterion();
135
136 std::vector<ValueType>* currentX = &x;
137 std::vector<ValueType>* nextX = this->cachedRowVector.get();
138
139 // Set up additional environment variables.
140 uint_fast64_t iterations = 0;
142
143 this->startMeasureProgress();
144 while (status == SolverStatus::InProgress && iterations < maxIter) {
145 // Compute D^-1 * (b - LU * x) and store result in nextX.
146 jacobiDecomposition->multiplier->multiply(env, *currentX, nullptr, *nextX);
148 storm::utility::vector::multiplyVectorsPointwise(jacobiDecomposition->DVector, *nextX, *nextX);
149
150 // Now check if the process already converged within our precision.
151 if (storm::utility::vector::equalModuloPrecision<ValueType>(*currentX, *nextX, precision, relative)) {
153 }
154 // Swap the two pointers as a preparation for the next iteration.
155 std::swap(nextX, currentX);
156
157 // Potentially show progress.
158 this->showProgressIterative(iterations);
159
160 // Increase iteration count so we can abort if convergence is too slow.
161 ++iterations;
162
163 status = this->updateStatus(status, *currentX, SolverGuarantee::None, iterations, maxIter);
164 }
165
166 // If the last iteration did not write to the original x we have to swap the contents, because the
167 // output has to be written to the input parameter x.
168 if (currentX == this->cachedRowVector.get()) {
169 std::swap(x, *currentX);
170 }
171
172 if (!this->isCachingEnabled()) {
173 clearCache();
174 }
175
176 this->reportStatus(status, iterations);
177
178 return status == SolverStatus::Converged;
179}
180
181template<typename ValueType>
182NativeLinearEquationSolver<ValueType>::WalkerChaeData::WalkerChaeData(Environment const& env, storm::storage::SparseMatrix<ValueType> const& originalMatrix,
183 std::vector<ValueType> const& originalB)
184 : t(storm::utility::convertNumber<ValueType>(1000.0)) {
185 computeWalkerChaeMatrix(originalMatrix);
186 computeNewB(originalB);
187 precomputeAuxiliaryData();
188 multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, this->matrix);
189}
190
191template<typename ValueType>
192void NativeLinearEquationSolver<ValueType>::WalkerChaeData::computeWalkerChaeMatrix(storm::storage::SparseMatrix<ValueType> const& originalMatrix) {
193 storm::storage::BitVector columnsWithNegativeEntries(originalMatrix.getColumnCount());
194 ValueType zero = storm::utility::zero<ValueType>();
195 for (auto const& e : originalMatrix) {
196 if (e.getValue() < zero) {
197 columnsWithNegativeEntries.set(e.getColumn());
198 }
199 }
200 std::vector<uint64_t> columnsWithNegativeEntriesBefore = columnsWithNegativeEntries.getNumberOfSetBitsBeforeIndices();
201
202 // We now build an extended equation system matrix that only has non-negative coefficients.
204
205 uint64_t row = 0;
206 for (; row < originalMatrix.getRowCount(); ++row) {
207 for (auto const& entry : originalMatrix.getRow(row)) {
208 if (entry.getValue() < zero) {
209 builder.addNextValue(row, originalMatrix.getRowCount() + columnsWithNegativeEntriesBefore[entry.getColumn()], -entry.getValue());
210 } else {
211 builder.addNextValue(row, entry.getColumn(), entry.getValue());
212 }
213 }
214 }
215 ValueType one = storm::utility::one<ValueType>();
216 for (auto column : columnsWithNegativeEntries) {
217 builder.addNextValue(row, column, one);
218 builder.addNextValue(row, originalMatrix.getRowCount() + columnsWithNegativeEntriesBefore[column], one);
219 ++row;
220 }
221
222 matrix = builder.build();
223}
224
225template<typename ValueType>
226void NativeLinearEquationSolver<ValueType>::WalkerChaeData::computeNewB(std::vector<ValueType> const& originalB) {
227 b = std::vector<ValueType>(originalB);
228 b.resize(matrix.getRowCount());
229}
230
231template<typename ValueType>
232void NativeLinearEquationSolver<ValueType>::WalkerChaeData::precomputeAuxiliaryData() {
233 columnSums = std::vector<ValueType>(matrix.getColumnCount());
234 for (auto const& e : matrix) {
235 columnSums[e.getColumn()] += e.getValue();
236 }
237
238 newX.resize(matrix.getRowCount());
239}
240
241template<typename ValueType>
242bool NativeLinearEquationSolver<ValueType>::solveEquationsWalkerChae(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
243 STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with NativeLinearEquationSolver (WalkerChae)");
244
245 // (1) Compute an equivalent equation system that has only non-negative coefficients.
246 if (!walkerChaeData) {
247 walkerChaeData = std::make_unique<WalkerChaeData>(env, *this->A, b);
248 }
249
250 // (2) Enlarge the vectors x and b to account for additional variables.
251 x.resize(walkerChaeData->matrix.getRowCount());
252
253 // Square the error bound, so we can use it to check for convergence. We take the squared error, because we
254 // do not want to compute the root in the 2-norm computation.
255 ValueType squaredErrorBound = storm::utility::pow(storm::utility::convertNumber<ValueType>(env.solver().native().getPrecision()), 2);
256
257 uint64_t maxIter = env.solver().native().getMaximalNumberOfIterations();
258
259 // Set up references to the x-vectors used in the iteration loop.
260 std::vector<ValueType>* currentX = &x;
261 std::vector<ValueType>* nextX = &walkerChaeData->newX;
262
263 std::vector<ValueType> tmp = walkerChaeData->matrix.getRowSumVector();
264 storm::utility::vector::applyPointwise(tmp, walkerChaeData->b, walkerChaeData->b,
265 [this](ValueType const& first, ValueType const& second) -> ValueType { return walkerChaeData->t * first + second; });
266
267 // Add t to all entries of x.
268 storm::utility::vector::applyPointwise(x, x, [this](ValueType const& value) -> ValueType { return value + walkerChaeData->t; });
269
270 // Create a vector that always holds Ax.
271 std::vector<ValueType> currentAx(x.size());
272 walkerChaeData->multiplier->multiply(env, *currentX, nullptr, currentAx);
273
274 // (3) Perform iterations until convergence.
276 uint64_t iterations = 0;
277 this->startMeasureProgress();
278 while (status == SolverStatus::InProgress && iterations < maxIter) {
279 // Perform one Walker-Chae step.
280 walkerChaeData->matrix.performWalkerChaeStep(*currentX, walkerChaeData->columnSums, walkerChaeData->b, currentAx, *nextX);
281
282 // Compute new Ax.
283 walkerChaeData->multiplier->multiply(env, *nextX, nullptr, currentAx);
284
285 // Check for convergence.
286 if (storm::utility::vector::computeSquaredNorm2Difference(currentAx, walkerChaeData->b) <= squaredErrorBound) {
288 }
289
290 // Swap the x vectors for the next iteration.
291 std::swap(currentX, nextX);
292
293 // Potentially show progress.
294 this->showProgressIterative(iterations);
295
296 // Increase iteration count so we can abort if convergence is too slow.
297 ++iterations;
298
300 status = SolverStatus::Aborted;
301 }
302 }
303
304 // If the last iteration did not write to the original x we have to swap the contents, because the
305 // output has to be written to the input parameter x.
306 if (currentX == &walkerChaeData->newX) {
307 std::swap(x, *currentX);
308 }
309
310 // Resize the solution to the right size.
311 x.resize(this->A->getRowCount());
312
313 // Finalize solution vector.
314 storm::utility::vector::applyPointwise(x, x, [this](ValueType const& value) -> ValueType { return value - walkerChaeData->t; });
315
316 if (!this->isCachingEnabled()) {
317 clearCache();
318 }
319
320 this->reportStatus(status, iterations);
321
322 return status == SolverStatus::Converged;
323}
324
325template<typename ValueType>
326typename NativeLinearEquationSolver<ValueType>::PowerIterationResult NativeLinearEquationSolver<ValueType>::performPowerIteration(
327 Environment const& env, std::vector<ValueType>*& currentX, std::vector<ValueType>*& newX, std::vector<ValueType> const& b, ValueType const& precision,
328 bool relative, SolverGuarantee const& guarantee, uint64_t currentIterations, uint64_t maxIterations,
329 storm::solver::MultiplicationStyle const& multiplicationStyle) const {
330 bool useGaussSeidelMultiplication = multiplicationStyle == storm::solver::MultiplicationStyle::GaussSeidel;
331
332 uint64_t iterations = currentIterations;
333 SolverStatus status = this->terminateNow(*currentX, guarantee) ? SolverStatus::TerminatedEarly : SolverStatus::InProgress;
334 while (status == SolverStatus::InProgress && iterations < maxIterations) {
335 if (useGaussSeidelMultiplication) {
336 *newX = *currentX;
337 this->multiplier->multiplyGaussSeidel(env, *newX, &b);
338 } else {
339 this->multiplier->multiply(env, *currentX, &b, *newX);
340 }
341
342 // Check for convergence.
343 if (storm::utility::vector::equalModuloPrecision<ValueType>(*currentX, *newX, precision, relative)) {
345 }
346
347 // Check for termination.
348 std::swap(currentX, newX);
349 ++iterations;
350
351 status = this->updateStatus(status, *currentX, guarantee, iterations, maxIterations);
352
353 // Potentially show progress.
354 this->showProgressIterative(iterations);
355 }
356
357 return PowerIterationResult(iterations - currentIterations, status);
358}
359
360template<typename ValueType>
361bool NativeLinearEquationSolver<ValueType>::solveEquationsPower(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
362 STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with NativeLinearEquationSolver (Power)");
363 // Prepare the solution vectors.
364 setUpViOperator();
365
367 if (this->hasCustomTerminationCondition()) {
368 if (this->getTerminationCondition().requiresGuarantee(SolverGuarantee::LessOrEqual) && this->hasLowerBound()) {
369 this->createLowerBoundsVector(x);
371 } else if (this->getTerminationCondition().requiresGuarantee(SolverGuarantee::GreaterOrEqual) && this->hasUpperBound()) {
372 this->createUpperBoundsVector(x);
374 }
375 }
376
378 uint64_t numIterations{0};
379 auto viCallback = [&](SolverStatus const& current) {
380 this->showProgressIterative(numIterations);
381 return this->updateStatus(current, x, guarantee, numIterations, env.solver().native().getMaximalNumberOfIterations());
382 };
383 this->startMeasureProgress();
384 auto status = viHelper.VI(x, b, numIterations, env.solver().native().getRelativeTerminationCriterion(),
385 storm::utility::convertNumber<ValueType>(env.solver().native().getPrecision()), {}, viCallback,
386 env.solver().native().getPowerMethodMultiplicationStyle());
387
388 this->reportStatus(status, numIterations);
389
390 if (!this->isCachingEnabled()) {
391 clearCache();
392 }
393
394 return status == SolverStatus::Converged || status == SolverStatus::TerminatedEarly;
395}
396
397template<typename ValueType>
398void preserveOldRelevantValues(std::vector<ValueType> const& allValues, storm::storage::BitVector const& relevantValues, std::vector<ValueType>& oldValues) {
399 storm::utility::vector::selectVectorValues(oldValues, relevantValues, allValues);
400}
401
402template<typename ValueType>
403ValueType computeMaxAbsDiff(std::vector<ValueType> const& allValues, storm::storage::BitVector const& relevantValues, std::vector<ValueType> const& oldValues) {
404 ValueType result = storm::utility::zero<ValueType>();
405 auto oldValueIt = oldValues.begin();
406 for (auto value : relevantValues) {
407 result = storm::utility::max<ValueType>(result, storm::utility::abs<ValueType>(allValues[value] - *oldValueIt));
408 }
409 return result;
410}
411
412template<typename ValueType>
413ValueType computeMaxAbsDiff(std::vector<ValueType> const& allOldValues, std::vector<ValueType> const& allNewValues,
414 storm::storage::BitVector const& relevantValues) {
415 ValueType result = storm::utility::zero<ValueType>();
416 for (auto value : relevantValues) {
417 result = storm::utility::max<ValueType>(result, storm::utility::abs<ValueType>(allNewValues[value] - allOldValues[value]));
418 }
419 return result;
420}
421
422template<typename ValueType>
423bool NativeLinearEquationSolver<ValueType>::solveEquationsIntervalIteration(Environment const& env, std::vector<ValueType>& x,
424 std::vector<ValueType> const& b) const {
425 STORM_LOG_THROW(this->hasLowerBound(), storm::exceptions::UnmetRequirementException, "Solver requires lower bound, but none was given.");
426 STORM_LOG_THROW(this->hasUpperBound(), storm::exceptions::UnmetRequirementException, "Solver requires upper bound, but none was given.");
427 STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with NativeLinearEquationSolver (IntervalIteration)");
428 setUpViOperator();
429 helper::IntervalIterationHelper<ValueType, true> iiHelper(viOperator);
430 auto prec = storm::utility::convertNumber<ValueType>(env.solver().native().getPrecision());
431 auto lowerBoundsCallback = [&](std::vector<ValueType>& vector) { this->createLowerBoundsVector(vector); };
432 auto upperBoundsCallback = [&](std::vector<ValueType>& vector) { this->createUpperBoundsVector(vector); };
433
434 uint64_t numIterations{0};
435 auto iiCallback = [&](helper::IIData<ValueType> const& data) {
436 this->showProgressIterative(numIterations);
437 bool terminateEarly = this->hasCustomTerminationCondition() && this->getTerminationCondition().terminateNow(data.x, SolverGuarantee::LessOrEqual) &&
438 this->getTerminationCondition().terminateNow(data.y, SolverGuarantee::GreaterOrEqual);
439 return this->updateStatus(data.status, terminateEarly, numIterations, env.solver().native().getMaximalNumberOfIterations());
440 };
441 std::optional<storm::storage::BitVector> optionalRelevantValues;
442 if (this->hasRelevantValues()) {
443 optionalRelevantValues = this->getRelevantValues();
444 }
445 this->startMeasureProgress();
446 auto status = iiHelper.II(x, b, numIterations, env.solver().native().getRelativeTerminationCriterion(), prec, lowerBoundsCallback, upperBoundsCallback, {},
447 iiCallback, optionalRelevantValues);
448 this->reportStatus(status, numIterations);
449
450 if (!this->isCachingEnabled()) {
451 clearCache();
452 }
453
454 return status == SolverStatus::Converged || status == SolverStatus::TerminatedEarly;
455}
456
457template<typename ValueType>
458bool NativeLinearEquationSolver<ValueType>::solveEquationsSoundValueIteration(Environment const& env, std::vector<ValueType>& x,
459 std::vector<ValueType> const& b) const {
460 // Prepare the solution vectors and the helper.
461 assert(x.size() == this->A->getRowGroupCount());
462
463 std::optional<ValueType> lowerBound, upperBound;
464 if (this->hasLowerBound()) {
465 lowerBound = this->getLowerBound(true);
466 }
467 if (this->hasUpperBound()) {
468 upperBound = this->getUpperBound(true);
469 }
470
471 setUpViOperator();
472
473 auto precision = storm::utility::convertNumber<ValueType>(env.solver().native().getPrecision());
474 uint64_t numIterations{0};
475 auto sviCallback = [&](typename helper::SoundValueIterationHelper<ValueType, true>::SVIData const& current) {
476 this->showProgressIterative(numIterations);
477 return this->updateStatus(current.status,
478 this->hasCustomTerminationCondition() && current.checkCustomTerminationCondition(this->getTerminationCondition()),
479 numIterations, env.solver().native().getMaximalNumberOfIterations());
480 };
481 std::optional<storm::storage::BitVector> optionalRelevantValues;
482 if (this->hasRelevantValues()) {
483 optionalRelevantValues = this->getRelevantValues();
484 }
485 this->startMeasureProgress();
486 helper::SoundValueIterationHelper<ValueType, true> sviHelper(viOperator);
487 auto status = sviHelper.SVI(x, b, numIterations, env.solver().native().getRelativeTerminationCriterion(), precision, {}, lowerBound, upperBound,
488 sviCallback, optionalRelevantValues);
489
490 this->reportStatus(status, numIterations);
491
492 if (!this->isCachingEnabled()) {
493 clearCache();
494 }
495
496 return status == SolverStatus::Converged || status == SolverStatus::TerminatedEarly;
497}
498
499template<typename ValueType>
500bool NativeLinearEquationSolver<ValueType>::solveEquationsOptimisticValueIteration(Environment const& env, std::vector<ValueType>& x,
501 std::vector<ValueType> const& b) const {
503 // If all entries are zero, OVI might run in an endless loop. However, the result is easy in this case.
504 x.assign(x.size(), storm::utility::zero<ValueType>());
505 return true;
506 }
507
508 setUpViOperator();
509
510 helper::OptimisticValueIterationHelper<ValueType, true> oviHelper(viOperator);
511 auto prec = storm::utility::convertNumber<ValueType>(env.solver().native().getPrecision());
512 std::optional<ValueType> lowerBound, upperBound;
513 if (this->hasLowerBound()) {
514 lowerBound = this->getLowerBound(true);
515 }
516 if (this->hasUpperBound()) {
517 upperBound = this->getUpperBound(true);
518 }
519 uint64_t numIterations{0};
520 auto oviCallback = [&](SolverStatus const& current, std::vector<ValueType> const& v) {
521 this->showProgressIterative(numIterations);
522 return this->updateStatus(current, v, SolverGuarantee::LessOrEqual, numIterations, env.solver().native().getMaximalNumberOfIterations());
523 };
524 this->createLowerBoundsVector(x);
525 std::optional<ValueType> guessingFactor;
526 if (env.solver().ovi().getUpperBoundGuessingFactor()) {
527 guessingFactor = storm::utility::convertNumber<ValueType>(*env.solver().ovi().getUpperBoundGuessingFactor());
528 }
529 this->startMeasureProgress();
530 auto status = oviHelper.OVI(x, b, env.solver().native().getRelativeTerminationCriterion(), prec, {}, guessingFactor, lowerBound, upperBound, oviCallback);
531 this->reportStatus(status, numIterations);
532
533 if (!this->isCachingEnabled()) {
534 clearCache();
535 }
536
537 return status == SolverStatus::Converged || status == SolverStatus::TerminatedEarly;
538}
539
540template<typename ValueType>
541bool NativeLinearEquationSolver<ValueType>::solveEquationsGuessingValueIteration(const Environment& env, std::vector<ValueType>& x,
542 const std::vector<ValueType>& b) const {
543 if (!this->cachedRowVector) {
544 this->cachedRowVector = std::make_unique<std::vector<ValueType>>(this->A->getRowCount());
545 }
546 setUpViOperator();
547
548 std::vector<ValueType>* lowerX = &x;
549 this->createLowerBoundsVector(*lowerX);
550 this->createUpperBoundsVector(this->cachedRowVector, this->getMatrixRowCount());
551 std::vector<ValueType>* upperX = this->cachedRowVector.get();
552
554
555 uint64_t numIterations{0};
556 auto gviCallback = [&](helper::GVIData<ValueType> const& data) {
557 this->showProgressIterative(numIterations);
558 bool terminateEarly = this->hasCustomTerminationCondition() && this->getTerminationCondition().terminateNow(data.x, SolverGuarantee::LessOrEqual) &&
559 this->getTerminationCondition().terminateNow(data.y, SolverGuarantee::GreaterOrEqual);
560 return this->updateStatus(data.status, terminateEarly, numIterations, env.solver().native().getMaximalNumberOfIterations());
561 };
562
563 this->startMeasureProgress();
564 auto status = helper.solveEquations(*lowerX, *upperX, b, numIterations, storm::utility::convertNumber<ValueType>(env.solver().native().getPrecision()),
565 {}, // No optimization dir
566 gviCallback);
567 auto two = storm::utility::convertNumber<ValueType>(2.0);
568 storm::utility::vector::applyPointwise<ValueType, ValueType, ValueType>(
569 *lowerX, *upperX, x, [&two](ValueType const& a, ValueType const& b) -> ValueType { return (a + b) / two; });
570 this->reportStatus(status, numIterations);
571
572 if (!this->isCachingEnabled()) {
573 clearCache();
574 }
575 return status == SolverStatus::Converged || status == SolverStatus::TerminatedEarly;
576}
577
578template<typename ValueType>
579bool NativeLinearEquationSolver<ValueType>::solveEquationsRationalSearch(Environment const& env, std::vector<ValueType>& x,
580 std::vector<ValueType> const& b) const {
581 // Set up two value iteration operators. One for exact and one for imprecise computations
582 setUpViOperator();
583 std::shared_ptr<helper::ValueIterationOperator<storm::RationalNumber, true>> exactOp;
584 std::shared_ptr<helper::ValueIterationOperator<double, true>> impreciseOp;
585
586 if constexpr (std::is_same_v<ValueType, storm::RationalNumber>) {
587 exactOp = viOperator;
588 impreciseOp = std::make_shared<helper::ValueIterationOperator<double, true>>();
589 impreciseOp->setMatrixBackwards(this->A->template toValueType<double>());
590 } else {
591 impreciseOp = viOperator;
592 exactOp = std::make_shared<helper::ValueIterationOperator<storm::RationalNumber, true>>();
593 exactOp->setMatrixBackwards(this->A->template toValueType<storm::RationalNumber>());
594 }
595
597 uint64_t numIterations{0};
598 auto rsCallback = [&](SolverStatus const& current) {
599 this->showProgressIterative(numIterations);
600 return this->updateStatus(current, x, SolverGuarantee::None, numIterations, env.solver().native().getMaximalNumberOfIterations());
601 };
602 this->startMeasureProgress();
603 auto status = rsHelper.RS(x, b, numIterations, storm::utility::convertNumber<ValueType>(env.solver().native().getPrecision()), {}, rsCallback);
604
605 this->reportStatus(status, numIterations);
606
607 if (!this->isCachingEnabled()) {
608 clearCache();
609 }
610
611 return status == SolverStatus::Converged || status == SolverStatus::TerminatedEarly;
612}
613
614template<typename ValueType>
615NativeLinearEquationSolverMethod NativeLinearEquationSolver<ValueType>::getMethod(Environment const& env, bool isExactMode) const {
616 // Adjust the method if none was specified and we want exact or sound computations
617 auto method = env.solver().native().getMethod();
618
619 if (isExactMode && method != NativeLinearEquationSolverMethod::RationalSearch) {
620 if (env.solver().native().isMethodSetFromDefault()) {
621 method = NativeLinearEquationSolverMethod::RationalSearch;
623 "Selecting '" + toString(method) +
624 "' as the solution technique to guarantee exact results. If you want to override this, please explicitly specify a different method.");
625 } else {
626 STORM_LOG_WARN("The selected solution method does not guarantee exact results.");
627 }
628 } else if (env.solver().isForceSoundness() && method != NativeLinearEquationSolverMethod::SoundValueIteration &&
629 method != NativeLinearEquationSolverMethod::OptimisticValueIteration && method != NativeLinearEquationSolverMethod::IntervalIteration &&
630 method != NativeLinearEquationSolverMethod::RationalSearch) {
631 if (env.solver().native().isMethodSetFromDefault()) {
632 method = NativeLinearEquationSolverMethod::OptimisticValueIteration;
634 "Selecting '" + toString(method) +
635 "' as the solution technique to guarantee sound results. If you want to override this, please explicitly specify a different method.");
636 } else {
637 STORM_LOG_WARN("The selected solution method does not guarantee sound results.");
638 }
639 }
640 return method;
641}
642
643template<typename ValueType>
644bool NativeLinearEquationSolver<ValueType>::internalSolveEquations(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
645 switch (getMethod(env, storm::NumberTraits<ValueType>::IsExact || env.solver().isForceExact())) {
646 case NativeLinearEquationSolverMethod::SOR:
647 return this->solveEquationsSOR(env, x, b, storm::utility::convertNumber<ValueType>(env.solver().native().getSorOmega()));
648 case NativeLinearEquationSolverMethod::GaussSeidel:
649 return this->solveEquationsSOR(env, x, b, storm::utility::one<ValueType>());
650 case NativeLinearEquationSolverMethod::Jacobi:
651 return this->solveEquationsJacobi(env, x, b);
652 case NativeLinearEquationSolverMethod::WalkerChae:
653 return this->solveEquationsWalkerChae(env, x, b);
654 case NativeLinearEquationSolverMethod::Power:
655 return this->solveEquationsPower(env, x, b);
656 case NativeLinearEquationSolverMethod::SoundValueIteration:
657 return this->solveEquationsSoundValueIteration(env, x, b);
658 case NativeLinearEquationSolverMethod::OptimisticValueIteration:
659 return this->solveEquationsOptimisticValueIteration(env, x, b);
660 case NativeLinearEquationSolverMethod::GuessingValueIteration:
661 return this->solveEquationsGuessingValueIteration(env, x, b);
662 case NativeLinearEquationSolverMethod::IntervalIteration:
663 return this->solveEquationsIntervalIteration(env, x, b);
664 case NativeLinearEquationSolverMethod::RationalSearch:
665 return this->solveEquationsRationalSearch(env, x, b);
666 }
667 STORM_LOG_THROW(false, storm::exceptions::InvalidEnvironmentException, "Unknown solving technique.");
668 return false;
669}
670
671template<typename ValueType>
673 auto method = getMethod(env, storm::NumberTraits<ValueType>::IsExact || env.solver().isForceExact());
674 if (method == NativeLinearEquationSolverMethod::Power || method == NativeLinearEquationSolverMethod::SoundValueIteration ||
675 method == NativeLinearEquationSolverMethod::OptimisticValueIteration || method == NativeLinearEquationSolverMethod::RationalSearch ||
676 method == NativeLinearEquationSolverMethod::IntervalIteration || method == NativeLinearEquationSolverMethod::GuessingValueIteration) {
678 } else {
680 }
681}
682
683template<typename ValueType>
686 auto method = getMethod(env, storm::NumberTraits<ValueType>::IsExact || env.solver().isForceExact());
687 if (method == NativeLinearEquationSolverMethod::IntervalIteration || method == NativeLinearEquationSolverMethod::GuessingValueIteration) {
688 requirements.requireBounds();
689 } else if (method == NativeLinearEquationSolverMethod::RationalSearch || method == NativeLinearEquationSolverMethod::OptimisticValueIteration) {
690 requirements.requireLowerBounds();
691 } else if (method == NativeLinearEquationSolverMethod::SoundValueIteration) {
692 requirements.requireBounds(false);
693 }
694 return requirements;
695}
696
697template<typename ValueType>
699 jacobiDecomposition.reset();
700 walkerChaeData.reset();
701 multiplier.reset();
702 viOperator.reset();
704}
705
706template<typename ValueType>
708 return this->A->getRowCount();
709}
710
711template<typename ValueType>
712uint64_t NativeLinearEquationSolver<ValueType>::getMatrixColumnCount() const {
713 return this->A->getColumnCount();
714}
715
716template<typename ValueType>
717std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> NativeLinearEquationSolverFactory<ValueType>::create(Environment const&) const {
718 return std::make_unique<storm::solver::NativeLinearEquationSolver<ValueType>>();
719}
720
721template<typename ValueType>
722std::unique_ptr<LinearEquationSolverFactory<ValueType>> NativeLinearEquationSolverFactory<ValueType>::clone() const {
723 return std::make_unique<NativeLinearEquationSolverFactory<ValueType>>(*this);
724}
725
726// Explicitly instantiate the linear equation solver.
729
730#ifdef STORM_HAVE_CARL
733
734#endif
735} // namespace solver
736} // namespace storm
SolverEnvironment & solver()
storm::RationalNumber const & getPrecision() const
uint64_t const & getMaximalNumberOfIterations() const
bool const & getRelativeTerminationCriterion() const
storm::RationalNumber const & getSorOmega() const
NativeSolverEnvironment & native()
LinearEquationSolverRequirements & requireLowerBounds(bool critical=true)
LinearEquationSolverRequirements & requireBounds(bool critical=true)
std::unique_ptr< Multiplier< ValueType > > create(Environment const &env, storm::storage::SparseMatrix< ValueType > const &matrix)
virtual std::unique_ptr< storm::solver::LinearEquationSolver< ValueType > > create(Environment const &env) const override
Creates an equation solver with the current settings, but without a matrix.
virtual std::unique_ptr< LinearEquationSolverFactory< ValueType > > clone() const override
Creates a copy of this factory.
A class that uses storm's native matrix operations to implement the LinearEquationSolver interface.
virtual LinearEquationSolverProblemFormat getEquationProblemFormat(storm::Environment const &env) const override
Retrieves the format in which this solver expects to solve equations.
virtual bool internalSolveEquations(storm::Environment const &env, std::vector< ValueType > &x, std::vector< ValueType > const &b) const override
virtual void setMatrix(storm::storage::SparseMatrix< ValueType > const &A) override
virtual LinearEquationSolverRequirements getRequirements(Environment const &env) const override
Retrieves the requirements of the solver under the current settings.
A bit vector that is internally represented as a vector of 64-bit values.
Definition BitVector.h:18
A class that can be used to build a sparse matrix by adding value by value.
void addNextValue(index_type row, index_type column, value_type const &value)
Sets the matrix entry at the given row and column to the given value.
SparseMatrix< value_type > build(index_type overriddenRowCount=0, index_type overriddenColumnCount=0, index_type overriddenRowGroupCount=0)
A class that holds a possibly non-square matrix in the compressed row storage format.
index_type getColumnCount() const
Returns the number of columns of the matrix.
std::pair< storm::storage::SparseMatrix< value_type >, std::vector< value_type > > getJacobiDecomposition() const
Calculates the Jacobi decomposition of this sparse matrix.
index_type getRowCount() const
Returns the number of rows of the matrix.
#define STORM_LOG_INFO(message)
Definition logging.h:29
#define STORM_LOG_WARN(message)
Definition logging.h:30
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30
SFTBDDChecker::ValueType ValueType
void preserveOldRelevantValues(std::vector< ValueType > const &allValues, storm::storage::BitVector const &relevantValues, std::vector< ValueType > &oldValues)
std::string toString(GurobiSolverMethod const &method)
Yields a string representation of the GurobiSolverMethod.
ValueType computeMaxAbsDiff(std::vector< ValueType > const &allValues, storm::storage::BitVector const &relevantValues, std::vector< ValueType > const &oldValues)
bool isTerminate()
Check whether the program should terminate (due to some abort signal).
void selectVectorValues(std::vector< T > &vector, storm::storage::BitVector const &positions, std::vector< T > const &values)
Selects the elements from a vector at the specified positions and writes them consecutively into anot...
Definition vector.h:188
T computeSquaredNorm2Difference(std::vector< T > const &b1, std::vector< T > const &b2)
Definition vector.h:872
void multiplyVectorsPointwise(std::vector< InValueType1 > const &firstOperand, std::vector< InValueType2 > const &secondOperand, std::vector< OutValueType > &target)
Multiplies the two given vectors (pointwise) and writes the result to the target vector.
Definition vector.h:427
void applyPointwise(std::vector< InValueType1 > const &firstOperand, std::vector< InValueType2 > const &secondOperand, std::vector< OutValueType > &target, Operation f=Operation())
Applies the given operation pointwise on the two given vectors and writes the result to the third vec...
Definition vector.h:378
void subtractVectors(std::vector< InValueType1 > const &firstOperand, std::vector< InValueType2 > const &secondOperand, std::vector< OutValueType > &target)
Subtracts the two given vectors and writes the result to the target vector.
Definition vector.h:415
bool hasNonZeroEntry(std::vector< T > const &v)
Definition vector.h:1103
ValueType zero()
Definition constants.cpp:26
ValueType pow(ValueType const &value, int_fast64_t exponent)
ValueType one()
Definition constants.cpp:21
TargetType convertNumber(SourceType const &number)
Definition constants.cpp:98
LabParser.cpp.
Definition cli.cpp:18