sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Using multiplier in MDP Model checker helpers

tempestpy_adaptions
TimQu 7 years ago
parent
9e875adea9
commit
56061c0bfa
4 changed files with 34 additions and 24 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 17
      src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp
  2. 25
      src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
  3. 11
      src/storm/solver/Multiplier.cpp
  4. 5
      src/storm/solver/Multiplier.h

17
src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp
View File

@ -21,6 +21,7 @@
#include "storm/modelchecker/results/HybridQuantitativeCheckResult.h"
#include "storm/solver/MinMaxLinearEquationSolver.h"
#include "storm/solver/Multiplier.h"
#include "storm/exceptions/InvalidPropertyException.h"
#include "storm/exceptions/UncheckedRequirementException.h"
@ -309,8 +310,8 @@ namespace storm {
// Translate the symbolic matrix/vector to their explicit representations.
std::pair<storm::storage::SparseMatrix<ValueType>, std::vector<ValueType>> explicitRepresentation = submatrix.toMatrixVector(subvector, model.getNondeterminismVariables(), odd, odd);
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(env, std::move(explicitRepresentation.first));
solver->repeatedMultiply(env, dir, x, &explicitRepresentation.second, stepBound);
auto multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, explicitRepresentation.first);
multiplier->repeatedMultiplyAndReduce(env, dir, x, &explicitRepresentation.second, stepBound);
// Return a hybrid check result that stores the numerical values explicitly.
return std::unique_ptr<CheckResult>(new storm::modelchecker::HybridQuantitativeCheckResult<DdType, ValueType>(model.getReachableStates(), model.getReachableStates() && !maybeStates, psiStates.template toAdd<ValueType>(), maybeStates, odd, x));
@ -334,9 +335,9 @@ namespace storm {
std::vector<ValueType> x = rewardModel.getStateRewardVector().toVector(odd);
// Perform the matrix-vector multiplication.
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(env, std::move(explicitMatrix));
solver->repeatedMultiply(env, dir, x, nullptr, stepBound);
auto multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, explicitMatrix);
multiplier->repeatedMultiplyAndReduce(env, dir, x, nullptr, stepBound);
// Return a hybrid check result that stores the numerical values explicitly.
return std::unique_ptr<CheckResult>(new HybridQuantitativeCheckResult<DdType, ValueType>(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero<ValueType>(), model.getReachableStates(), odd, x));
}
@ -359,9 +360,9 @@ namespace storm {
std::pair<storm::storage::SparseMatrix<ValueType>, std::vector<ValueType>> explicitRepresentation = transitionMatrix.toMatrixVector(totalRewardVector, model.getNondeterminismVariables(), odd, odd);
// Perform the matrix-vector multiplication.
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(env, std::move(explicitRepresentation.first));
solver->repeatedMultiply(env, dir, x, &explicitRepresentation.second, stepBound);
auto multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, explicitRepresentation.first);
multiplier->repeatedMultiplyAndReduce(env, dir, x, &explicitRepresentation.second, stepBound);
// Return a hybrid check result that stores the numerical values explicitly.
return std::unique_ptr<CheckResult>(new HybridQuantitativeCheckResult<DdType, ValueType>(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero<ValueType>(), model.getReachableStates(), odd, x));
}

25
src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
View File

@ -21,6 +21,7 @@
#include "storm/storage/Scheduler.h"
#include "storm/solver/MinMaxLinearEquationSolver.h"
#include "storm/solver/Multiplier.h"
#include "storm/solver/LpSolver.h"
#include "storm/settings/SettingsManager.h"
@ -75,9 +76,8 @@ namespace storm {
// Create the vector with which to multiply.
std::vector<ValueType> subresult(maybeStates.getNumberOfSetBits());
goal.restrictRelevantValues(maybeStates);
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = storm::solver::configureMinMaxLinearEquationSolver(env, std::move(goal), minMaxLinearEquationSolverFactory, std::move(submatrix));
solver->repeatedMultiply(env, subresult, &b, stepBound);
auto multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, submatrix);
multiplier->repeatedMultiplyAndReduce(env, goal.direction(), subresult, &b, stepBound);
// Set the values of the resulting vector accordingly.
storm::utility::vector::setVectorValues(result, maybeStates, subresult);
@ -272,8 +272,8 @@ namespace storm {
std::vector<ValueType> result(transitionMatrix.getRowGroupCount());
storm::utility::vector::setVectorValues(result, nextStates, storm::utility::one<ValueType>());
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = minMaxLinearEquationSolverFactory.create(env, transitionMatrix);
solver->repeatedMultiply(env, dir, result, nullptr, 1);
auto multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, transitionMatrix);
multiplier->multiplyAndReduce(env, dir, result, nullptr, result);
return result;
}
@ -812,9 +812,9 @@ namespace storm {
// Initialize result to state rewards of the this->getModel().
std::vector<ValueType> result(rewardModel.getStateRewardVector());
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = storm::solver::configureMinMaxLinearEquationSolver(env, std::move(goal), minMaxLinearEquationSolverFactory, transitionMatrix);
solver->repeatedMultiply(env, result, nullptr, stepCount);
auto multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, transitionMatrix);
multiplier->repeatedMultiplyAndReduce(env, goal.direction(), result, nullptr, stepCount);
return result;
}
@ -831,8 +831,8 @@ namespace storm {
// Initialize result to the zero vector.
std::vector<ValueType> result(transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = storm::solver::configureMinMaxLinearEquationSolver(env, std::move(goal), minMaxLinearEquationSolverFactory, transitionMatrix);
solver->repeatedMultiply(env, result, &totalRewardVector, stepBound);
auto multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, transitionMatrix);
multiplier->repeatedMultiplyAndReduce(env, goal.direction(), result, &totalRewardVector, stepBound);
return result;
}
@ -1459,12 +1459,11 @@ namespace storm {
std::vector<ValueType> x(mecTransitions.getRowGroupCount(), storm::utility::zero<ValueType>());
std::vector<ValueType> xPrime = x;
auto solver = minMaxLinearEquationSolverFactory.create(env, std::move(mecTransitions));
solver->setCachingEnabled(true);
auto multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, mecTransitions);
ValueType maxDiff, minDiff;
while (true) {
// Compute the obtained rewards for the next step
solver->repeatedMultiply(env, dir, x, &choiceRewards, 1);
multiplier->multiplyAndReduce(env, dir, x, &choiceRewards, x);
// update xPrime and check for convergence
// to avoid large (and numerically unstable) x-values, we substract a reference value.

11
src/storm/solver/Multiplier.cpp
View File

@ -24,6 +24,16 @@ namespace storm {
void Multiplier<ValueType>::clearCache() const {
cachedVector.reset();
}
template<typename ValueType>
void Multiplier<ValueType>::multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint_fast64_t>* choices = nullptr) {
multiplyAndReduce(env, dir, this->matrix.getRowGroupIndices(), x, b, result, choices);
}
template<typename ValueType>
void Multiplier<ValueType>::multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector<ValueType>& x, std::vector<ValueType> const* b, std::vector<uint_fast64_t>* choices = nullptr) {
multiplyAndReduceGaussSeidel(env, dir, this->matrix.getRowGroupIndices(), x, b, choices);
}
template<typename ValueType>
void Multiplier<ValueType>::repeatedMultiply(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const* b, uint64_t n) const {
@ -49,7 +59,6 @@ namespace storm {
return std::make_unique<NativeMultiplier<ValueType>>(matrix);
}
}
template class Multiplier<double>;
template class MultiplierFactory<double>;

5
src/storm/solver/Multiplier.h
View File

@ -61,6 +61,7 @@ namespace storm {
* to the number of rows of A. Can be the same as the x vector.
* @param choices If given, the choices made in the reduction process are written to this vector.
*/
void multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint_fast64_t>* choices = nullptr) const;
virtual void multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint_fast64_t>* choices = nullptr) const = 0;
/*!
@ -77,6 +78,7 @@ namespace storm {
* to the number of rows of A. Can be the same as the x vector.
* @param choices If given, the choices made in the reduction process are written to this vector.
*/
void multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector<ValueType>& x, std::vector<ValueType> const* b, std::vector<uint_fast64_t>* choices = nullptr) const;
virtual void multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType>& x, std::vector<ValueType> const* b, std::vector<uint_fast64_t>* choices = nullptr) const = 0;
/*!
@ -97,7 +99,6 @@ namespace storm {
* so that the resulting vector has the size of number of row groups of A.
*
* @param dir The direction for the reduction step.
* @param rowGroupIndices A vector storing the row groups over which to reduce.
* @param x The input vector with which to multiply the matrix. Its length must be equal
* to the number of columns of A.
* @param b If non-null, this vector is added after the multiplication. If given, its length must be equal
@ -106,7 +107,7 @@ namespace storm {
* to the number of rows of A.
* @param n The number of times to perform the multiplication.
*/
void repeatedMultiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType>& x, std::vector<ValueType> const* b, uint64_t n) const;
void repeatedMultiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector<ValueType>& x, std::vector<ValueType> const* b, uint64_t n) const;
/*!
* Multiplies the row with the given index with x and adds the given offset

Write Preview
Loading…
Cancel
Save