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

moving from internal reference to pointer in StandardMinMax solver 

equipped MinMax solvers with default constructors
tempestpy_adaptions
dehnert 7 years ago
parent
0c5aa1645d
commit
e278c3ef69
6 changed files with 55 additions and 46 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. 56
      src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
  2. 1
      src/storm/solver/IterativeMinMaxLinearEquationSolver.h
  3. 22
      src/storm/solver/LpMinMaxLinearEquationSolver.cpp
  4. 3
      src/storm/solver/LpMinMaxLinearEquationSolver.h
  5. 15
      src/storm/solver/StandardMinMaxLinearEquationSolver.cpp
  6. 4
      src/storm/solver/StandardMinMaxLinearEquationSolver.h

56
src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
View File

@ -74,7 +74,7 @@ namespace storm {
bool IterativeMinMaxLinearEquationSolverSettings<ValueType>::getRelativeTerminationCriterion() const {
return relative;
}
template<typename ValueType>
IterativeMinMaxLinearEquationSolver<ValueType>::IterativeMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory, IterativeMinMaxLinearEquationSolverSettings<ValueType> const& settings) : StandardMinMaxLinearEquationSolver<ValueType>(A, std::move(linearEquationSolverFactory)), settings(settings) {
// Intentionally left empty.
@ -103,18 +103,18 @@ namespace storm {
template<typename ValueType>
bool IterativeMinMaxLinearEquationSolver<ValueType>::solveEquationsPolicyIteration(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
// Create the initial scheduler.
std::vector<storm::storage::sparse::state_type> scheduler = this->hasSchedulerHint() ? this->choicesHint.get() : std::vector<storm::storage::sparse::state_type>(this->A.getRowGroupCount());
std::vector<storm::storage::sparse::state_type> scheduler = this->hasSchedulerHint() ? this->choicesHint.get() : std::vector<storm::storage::sparse::state_type>(this->A->getRowGroupCount());
// Get a vector for storing the right-hand side of the inner equation system.
if(!auxiliaryRowGroupVector) {
auxiliaryRowGroupVector = std::make_unique<std::vector<ValueType>>(this->A.getRowGroupCount());
auxiliaryRowGroupVector = std::make_unique<std::vector<ValueType>>(this->A->getRowGroupCount());
}
std::vector<ValueType>& subB = *auxiliaryRowGroupVector;
// Resolve the nondeterminism according to the current scheduler.
storm::storage::SparseMatrix<ValueType> submatrix = this->A.selectRowsFromRowGroups(scheduler, true);
storm::storage::SparseMatrix<ValueType> submatrix = this->A->selectRowsFromRowGroups(scheduler, true);
submatrix.convertToEquationSystem();
storm::utility::vector::selectVectorValues<ValueType>(subB, scheduler, this->A.getRowGroupIndices(), b);
storm::utility::vector::selectVectorValues<ValueType>(subB, scheduler, this->A->getRowGroupIndices(), b);
// Create a solver that we will use throughout the procedure. We will modify the matrix in each iteration.
auto solver = this->linearEquationSolverFactory->create(std::move(submatrix));
@ -137,17 +137,17 @@ namespace storm {
// Go through the multiplication result and see whether we can improve any of the choices.
bool schedulerImproved = false;
for (uint_fast64_t group = 0; group < this->A.getRowGroupCount(); ++group) {
for (uint_fast64_t group = 0; group < this->A->getRowGroupCount(); ++group) {
uint_fast64_t currentChoice = scheduler[group];
for (uint_fast64_t choice = this->A.getRowGroupIndices()[group]; choice < this->A.getRowGroupIndices()[group + 1]; ++choice) {
for (uint_fast64_t choice = this->A->getRowGroupIndices()[group]; choice < this->A->getRowGroupIndices()[group + 1]; ++choice) {
// If the choice is the currently selected one, we can skip it.
if (choice - this->A.getRowGroupIndices()[group] == currentChoice) {
if (choice - this->A->getRowGroupIndices()[group] == currentChoice) {
continue;
}
// Create the value of the choice.
ValueType choiceValue = storm::utility::zero<ValueType>();
for (auto const& entry : this->A.getRow(choice)) {
for (auto const& entry : this->A->getRow(choice)) {
choiceValue += entry.getValue() * x[entry.getColumn()];
}
choiceValue += b[choice];
@ -157,7 +157,7 @@ namespace storm {
// only changing the scheduler if the values are not equal (modulo precision) would make this unsound.
if (valueImproved(dir, x[group], choiceValue)) {
schedulerImproved = true;
scheduler[group] = choice - this->A.getRowGroupIndices()[group];
scheduler[group] = choice - this->A->getRowGroupIndices()[group];
x[group] = std::move(choiceValue);
}
}
@ -168,9 +168,9 @@ namespace storm {
status = Status::Converged;
} else {
// Update the scheduler and the solver.
submatrix = this->A.selectRowsFromRowGroups(scheduler, true);
submatrix = this->A->selectRowsFromRowGroups(scheduler, true);
submatrix.convertToEquationSystem();
storm::utility::vector::selectVectorValues<ValueType>(subB, scheduler, this->A.getRowGroupIndices(), b);
storm::utility::vector::selectVectorValues<ValueType>(subB, scheduler, this->A->getRowGroupIndices(), b);
solver->setMatrix(std::move(submatrix));
}
@ -215,24 +215,24 @@ namespace storm {
template<typename ValueType>
bool IterativeMinMaxLinearEquationSolver<ValueType>::solveEquationsValueIteration(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
if(!this->linEqSolverA) {
this->linEqSolverA = this->linearEquationSolverFactory->create(this->A);
this->linEqSolverA = this->linearEquationSolverFactory->create(*this->A);
this->linEqSolverA->setCachingEnabled(true);
}
if (!this->auxiliaryRowVector) {
this->auxiliaryRowVector = std::make_unique<std::vector<ValueType>>(this->A.getRowCount());
this->auxiliaryRowVector = std::make_unique<std::vector<ValueType>>(this->A->getRowCount());
}
std::vector<ValueType>& multiplyResult = *this->auxiliaryRowVector;
if (!auxiliaryRowGroupVector) {
auxiliaryRowGroupVector = std::make_unique<std::vector<ValueType>>(this->A.getRowGroupCount());
auxiliaryRowGroupVector = std::make_unique<std::vector<ValueType>>(this->A->getRowGroupCount());
}
if (this->hasSchedulerHint()) {
// Resolve the nondeterminism according to the scheduler hint
storm::storage::SparseMatrix<ValueType> submatrix = this->A.selectRowsFromRowGroups(this->choicesHint.get(), true);
storm::storage::SparseMatrix<ValueType> submatrix = this->A->selectRowsFromRowGroups(this->choicesHint.get(), true);
submatrix.convertToEquationSystem();
storm::utility::vector::selectVectorValues<ValueType>(*auxiliaryRowGroupVector, this->choicesHint.get(), this->A.getRowGroupIndices(), b);
storm::utility::vector::selectVectorValues<ValueType>(*auxiliaryRowGroupVector, this->choicesHint.get(), this->A->getRowGroupIndices(), b);
// Solve the resulting equation system.
// Note that the linEqSolver might consider a slightly different interpretation of "equalModuloPrecision". Hence, we iteratively increase its precision.
@ -256,7 +256,7 @@ namespace storm {
this->linEqSolverA->multiply(*currentX, &b, multiplyResult);
// Reduce the vector x' by applying min/max for all non-deterministic choices.
storm::utility::vector::reduceVectorMinOrMax(dir, multiplyResult, *newX, this->A.getRowGroupIndices());
storm::utility::vector::reduceVectorMinOrMax(dir, multiplyResult, *newX, this->A->getRowGroupIndices());
// Determine whether the method converged.
if (storm::utility::vector::equalModuloPrecision<ValueType>(*currentX, *newX, this->getSettings().getPrecision(), this->getSettings().getRelativeTerminationCriterion())) {
@ -284,9 +284,9 @@ namespace storm {
if (iterations==0) {
this->linEqSolverA->multiply(x, &b, multiplyResult);
}
this->schedulerChoices = std::vector<uint_fast64_t>(this->A.getRowGroupCount());
this->schedulerChoices = std::vector<uint_fast64_t>(this->A->getRowGroupCount());
// Reduce the multiplyResult and keep track of the choices made
storm::utility::vector::reduceVectorMinOrMax(dir, multiplyResult, x, this->A.getRowGroupIndices(), &this->schedulerChoices.get());
storm::utility::vector::reduceVectorMinOrMax(dir, multiplyResult, x, this->A->getRowGroupIndices(), &this->schedulerChoices.get());
}
if (!this->isCachingEnabled()) {
@ -298,7 +298,7 @@ namespace storm {
template<typename ValueType>
bool IterativeMinMaxLinearEquationSolver<ValueType>::solveEquationsAcyclic(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
uint64_t numGroups = this->A.getRowGroupCount();
uint64_t numGroups = this->A->getRowGroupCount();
// Allocate memory for the scheduler (if required)
if (this->isTrackSchedulerSet()) {
@ -323,7 +323,7 @@ namespace storm {
}
}
auto transposedMatrix = this->A.transpose(true);
auto transposedMatrix = this->A->transpose(true);
// We store the groups that have already been processed, i.e., the groups for which x[group] was already set to the correct value.
storm::storage::BitVector processedGroups(numGroups, false);
@ -338,7 +338,7 @@ namespace storm {
// Check if the candidate row group has an unprocessed successor
bool hasUnprocessedSuccessor = false;
for (auto const& entry : this->A.getRowGroup(candidate)) {
for (auto const& entry : this->A->getRowGroup(candidate)) {
if (!processedGroups.get(entry.getColumn())) {
hasUnprocessedSuccessor = true;
break;
@ -375,17 +375,17 @@ namespace storm {
template<typename ValueType>
void IterativeMinMaxLinearEquationSolver<ValueType>::computeOptimalValueForRowGroup(uint_fast64_t group, OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b, uint_fast64_t* choice) const {
uint64_t row = this->A.getRowGroupIndices()[group];
uint64_t groupEnd = this->A.getRowGroupIndices()[group + 1];
uint64_t row = this->A->getRowGroupIndices()[group];
uint64_t groupEnd = this->A->getRowGroupIndices()[group + 1];
assert(row != groupEnd);
auto bIt = b.begin() + row;
ValueType& xi = x[group];
xi = this->A.multiplyRowWithVector(row, x) + *bIt;
xi = this->A->multiplyRowWithVector(row, x) + *bIt;
uint64_t optimalRow = row;
for (++row, ++bIt; row < groupEnd; ++row, ++bIt) {
ValueType choiceVal = this->A.multiplyRowWithVector(row, x) + *bIt;
ValueType choiceVal = this->A->multiplyRowWithVector(row, x) + *bIt;
if (minimize(dir)) {
if (choiceVal < xi) {
xi = choiceVal;
@ -399,7 +399,7 @@ namespace storm {
}
}
if (choice != nullptr) {
*choice = optimalRow - this->A.getRowGroupIndices()[group];
*choice = optimalRow - this->A->getRowGroupIndices()[group];
}
}

1
src/storm/solver/IterativeMinMaxLinearEquationSolver.h
View File

@ -36,6 +36,7 @@ namespace storm {
template<typename ValueType>
class IterativeMinMaxLinearEquationSolver : public StandardMinMaxLinearEquationSolver<ValueType> {
public:
IterativeMinMaxLinearEquationSolver() = default;
IterativeMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory, IterativeMinMaxLinearEquationSolverSettings<ValueType> const& settings = IterativeMinMaxLinearEquationSolverSettings<ValueType>());
IterativeMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType>&& A, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory, IterativeMinMaxLinearEquationSolverSettings<ValueType> const& settings = IterativeMinMaxLinearEquationSolverSettings<ValueType>());

22
src/storm/solver/LpMinMaxLinearEquationSolver.cpp
View File

@ -28,8 +28,8 @@ namespace storm {
// Create a variable for each row group
std::vector<storm::expressions::Variable> variables;
variables.reserve(this->A.getRowGroupCount());
for (uint64_t rowGroup = 0; rowGroup < this->A.getRowGroupCount(); ++rowGroup) {
variables.reserve(this->A->getRowGroupCount());
for (uint64_t rowGroup = 0; rowGroup < this->A->getRowGroupCount(); ++rowGroup) {
if (this->lowerBound) {
if (this->upperBound) {
variables.push_back(solver->addBoundedContinuousVariable("x" + std::to_string(rowGroup), this->lowerBound.get(), this->upperBound.get(), storm::utility::one<ValueType>()));
@ -47,10 +47,10 @@ namespace storm {
solver->update();
// Add a constraint for each row
for (uint64_t rowGroup = 0; rowGroup < this->A.getRowGroupCount(); ++rowGroup) {
for (uint64_t row = this->A.getRowGroupIndices()[rowGroup]; row < this->A.getRowGroupIndices()[rowGroup + 1]; ++row) {
for (uint64_t rowGroup = 0; rowGroup < this->A->getRowGroupCount(); ++rowGroup) {
for (uint64_t row = this->A->getRowGroupIndices()[rowGroup]; row < this->A->getRowGroupIndices()[rowGroup + 1]; ++row) {
storm::expressions::Expression rowConstraint = solver->getConstant(b[row]);
for (auto const& entry : this->A.getRow(row)) {
for (auto const& entry : this->A->getRow(row)) {
rowConstraint = rowConstraint + (solver->getConstant(entry.getValue()) * variables[entry.getColumn()].getExpression());
}
if (minimize(dir)) {
@ -78,14 +78,14 @@ namespace storm {
// If requested, we store the scheduler for retrieval.
if (this->isTrackSchedulerSet()) {
this->schedulerChoices = std::vector<uint_fast64_t>(this->A.getRowGroupCount());
for (uint64_t rowGroup = 0; rowGroup < this->A.getRowGroupCount(); ++rowGroup) {
uint64_t row = this->A.getRowGroupIndices()[rowGroup];
this->schedulerChoices = std::vector<uint_fast64_t>(this->A->getRowGroupCount());
for (uint64_t rowGroup = 0; rowGroup < this->A->getRowGroupCount(); ++rowGroup) {
uint64_t row = this->A->getRowGroupIndices()[rowGroup];
uint64_t optimalChoiceIndex = 0;
uint64_t currChoice = 0;
ValueType optimalGroupValue = this->A.multiplyRowWithVector(row, x) + b[row];
for (++row, ++currChoice; row < this->A.getRowGroupIndices()[rowGroup + 1]; ++row, ++currChoice) {
ValueType rowValue = this->A.multiplyRowWithVector(row, x) + b[row];
ValueType optimalGroupValue = this->A->multiplyRowWithVector(row, x) + b[row];
for (++row, ++currChoice; row < this->A->getRowGroupIndices()[rowGroup + 1]; ++row, ++currChoice) {
ValueType rowValue = this->A->multiplyRowWithVector(row, x) + b[row];
if ((minimize(dir) && rowValue < optimalGroupValue) || (maximize(dir) && rowValue > optimalGroupValue)) {
optimalGroupValue = rowValue;
optimalChoiceIndex = currChoice;

3
src/storm/solver/LpMinMaxLinearEquationSolver.h
View File

@ -10,6 +10,7 @@ namespace storm {
template<typename ValueType>
class LpMinMaxLinearEquationSolver : public StandardMinMaxLinearEquationSolver<ValueType> {
public:
LpMinMaxLinearEquationSolver() = default;
LpMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory, std::unique_ptr<storm::utility::solver::LpSolverFactory<ValueType>>&& lpSolverFactory);
LpMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType>&& A, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory, std::unique_ptr<storm::utility::solver::LpSolverFactory<ValueType>>&& lpSolverFactory);
@ -21,7 +22,7 @@ namespace storm {
std::unique_ptr<storm::utility::solver::LpSolverFactory<ValueType>> lpSolverFactory;
};
template<typename ValueType>
template<typename ValueType>
class LpMinMaxLinearEquationSolverFactory : public StandardMinMaxLinearEquationSolverFactory<ValueType> {
public:
LpMinMaxLinearEquationSolverFactory(bool trackScheduler = false);

15
src/storm/solver/StandardMinMaxLinearEquationSolver.cpp
View File

@ -15,24 +15,29 @@ namespace storm {
namespace solver {
template<typename ValueType>
StandardMinMaxLinearEquationSolver<ValueType>::StandardMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory) : linearEquationSolverFactory(std::move(linearEquationSolverFactory)), localA(nullptr), A(A) {
StandardMinMaxLinearEquationSolver<ValueType>::StandardMinMaxLinearEquationSolver() : A(nullptr) {
// Intentionally left empty.
}
template<typename ValueType>
StandardMinMaxLinearEquationSolver<ValueType>::StandardMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType>&& A, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory) : linearEquationSolverFactory(std::move(linearEquationSolverFactory)), localA(std::make_unique<storm::storage::SparseMatrix<ValueType>>(std::move(A))), A(*localA) {
StandardMinMaxLinearEquationSolver<ValueType>::StandardMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory) : linearEquationSolverFactory(std::move(linearEquationSolverFactory)), localA(nullptr), A(&A) {
// Intentionally left empty.
}
template<typename ValueType>
StandardMinMaxLinearEquationSolver<ValueType>::StandardMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType>&& A, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory) : linearEquationSolverFactory(std::move(linearEquationSolverFactory)), localA(std::make_unique<storm::storage::SparseMatrix<ValueType>>(std::move(A))), A(localA.get()) {
// Intentionally left empty.
}
template<typename ValueType>
void StandardMinMaxLinearEquationSolver<ValueType>::repeatedMultiply(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const* b, uint_fast64_t n) const {
if (!linEqSolverA) {
linEqSolverA = linearEquationSolverFactory->create(A);
linEqSolverA = linearEquationSolverFactory->create(*A);
linEqSolverA->setCachingEnabled(true);
}
if (!auxiliaryRowVector) {
auxiliaryRowVector = std::make_unique<std::vector<ValueType>>(A.getRowCount());
auxiliaryRowVector = std::make_unique<std::vector<ValueType>>(A->getRowCount());
}
std::vector<ValueType>& multiplyResult = *auxiliaryRowVector;
@ -41,7 +46,7 @@ namespace storm {
// Reduce the vector x' by applying min/max for all non-deterministic choices as given by the topmost
// element of the min/max operator stack.
storm::utility::vector::reduceVectorMinOrMax(dir, multiplyResult, x, this->A.getRowGroupIndices());
storm::utility::vector::reduceVectorMinOrMax(dir, multiplyResult, x, this->A->getRowGroupIndices());
}
if (!this->isCachingEnabled()) {

4
src/storm/solver/StandardMinMaxLinearEquationSolver.h
View File

@ -9,6 +9,8 @@ namespace storm {
template<typename ValueType>
class StandardMinMaxLinearEquationSolver : public MinMaxLinearEquationSolver<ValueType> {
public:
StandardMinMaxLinearEquationSolver();
StandardMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory);
StandardMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType>&& A, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory);
@ -33,7 +35,7 @@ namespace storm {
// A reference to the original sparse matrix given to this solver. If the solver takes posession of the matrix
// the reference refers to localA.
storm::storage::SparseMatrix<ValueType> const& A;
storm::storage::SparseMatrix<ValueType> const* A;
};

Write Preview
Loading…
Cancel
Save