Browse Source

fix some compile issues

main
dehnert 7 years ago
parent
commit
3952b47d1b
  1. 10
      src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
  2. 10
      src/storm/solver/GameSolver.cpp
  3. 1
      src/storm/solver/NativeMultiplier.cpp
  4. 2
      src/storm/solver/StandardGameSolver.cpp
  5. 4
      src/storm/storage/SparseMatrix.h

10
src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp

@ -410,11 +410,11 @@ namespace storm {
storm::storage::SparseMatrix<ValueType> submatrix = transitionMatrix.getSubmatrix(true, player2MaybeStates, maybeStates);
std::vector<ValueType> b = transitionMatrix.getConstrainedRowGroupSumVector(player2MaybeStates, maybeStates);
auto multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, submatrix);
multiplier->repeatedMultiplyAndReduce(env, goal.direction(), subresult, &b, stepBound);
env.
// auto multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, submatrix);
// multiplier->repeatedMultiplyAndReduce(env, goal.direction(), subresult, &b, stepBound);
//
//
// env.
}
template<storm::dd::DdType Type, typename ModelType>

10
src/storm/solver/GameSolver.cpp

@ -99,6 +99,16 @@ namespace storm {
// Intentionally left empty.
}
template<typename ValueType>
void GameSolver<ValueType>::setHasUniqueSolution(bool value) {
this->uniqueSolution = value;
}
template<typename ValueType>
bool GameSolver<ValueType>::hasUniqueSolution() const {
return this->uniqueSolution;
}
template<typename ValueType>
GameSolverFactory<ValueType>::GameSolverFactory() {
// Intentionally left empty.

1
src/storm/solver/NativeMultiplier.cpp

@ -97,7 +97,6 @@ namespace storm {
}
}
template<typename ValueType>
void NativeMultiplier<ValueType>::multAdd(std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result) const {
this->matrix.multiplyWithVector(x, result, b);

2
src/storm/solver/StandardGameSolver.cpp

@ -240,7 +240,7 @@ namespace storm {
Status status = Status::InProgress;
while (status == Status::InProgress) {
multiplyAndReduce(env, player1Dir, player2Dir, *currentX, &b, *multiplierPlayer2Matrix, reducedPlayer2Result, *newX, trackSchedulersInValueIteration ? &this->getPlayer1SchedulerChoices() : nullptr, trackSchedulersInValueIteration ? &this->getPlayer2SchedulerChoices() : nullptr);
multiplyAndReduce(env, player1Dir, player2Dir, *currentX, &b, *multiplierPlayer2Matrix, reducedPlayer2Result, *newX, trackSchedulersInValueIteration ? &this->player1SchedulerChoices.get() : nullptr, trackSchedulersInValueIteration ? &this->player2SchedulerChoices.get() : nullptr);
// Determine whether the method converged.
if (storm::utility::vector::equalModuloPrecision<ValueType>(*currentX, *newX, precision, relative)) {

4
src/storm/storage/SparseMatrix.h

@ -851,7 +851,9 @@ namespace storm {
* @param vector The vector with which to multiply the matrix.
* @param summand If given, this summand will be added to the result of the multiplication.
* @param result The vector that is supposed to hold the result of the multiplication after the operation.
* @param choices If given, the choices made in the reduction process will be written to this vector.
* @param choices If given, the choices made in the reduction process will be written to this vector. Note
* that if the direction is maximize, the choice for a row group is only updated if the value obtained with
* the 'new' choice has a value strictly better (wrt. to the optimization direction) value.
* @return The resulting vector the content of the given result vector.
*/
void multiplyAndReduce(storm::solver::OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& vector, std::vector<ValueType> const* summand, std::vector<ValueType>& result, std::vector<uint_fast64_t>* choices) const;

Loading…
Cancel
Save