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

started to make game solver flexible enough to also solve the (explicit) games of game-based abstraction

main
dehnert 7 years ago
parent
d3bbe4df10
commit
d557ef1075
8 changed files with 233 additions and 110 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. 6
      src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp
  2. 29
      src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
  3. 2
      src/storm/solver/GameSolver.cpp
  4. 14
      src/storm/solver/GameSolver.h
  5. 2
      src/storm/solver/MinMaxLinearEquationSolver.h
  6. 266
      src/storm/solver/StandardGameSolver.cpp
  7. 22
      src/storm/solver/StandardGameSolver.h
  8. 2
      src/storm/storage/SparseMatrix.h

6
src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp
View File

@ -275,8 +275,8 @@ namespace storm {
}
// Invoke the solver
if(stepBound) {
assert(*stepBound > 0);
if (stepBound) {
STORM_LOG_ASSERT(*stepBound > 0, "Expected positive step bound.");
solver->repeatedMultiply(env, this->currentCheckTask->getOptimizationDirection(), dirForParameters, x, &parameterLifter->getVector(), *stepBound);
} else {
solver->solveGame(env, this->currentCheckTask->getOptimizationDirection(), dirForParameters, x, parameterLifter->getVector());
@ -293,7 +293,7 @@ namespace storm {
// Get the result for the complete model (including maybestates)
std::vector<ConstantType> result = resultsForNonMaybeStates;
auto maybeStateResIt = x.begin();
for(auto const& maybeState : maybeStates) {
for (auto const& maybeState : maybeStates) {
result[maybeState] = *maybeStateResIt;
++maybeStateResIt;
}

29
src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
View File

@ -391,31 +391,30 @@ namespace storm {
template<typename ValueType>
ExplicitQuantitativeResult<ValueType> computeQuantitativeResult(Environment const& env, storm::OptimizationDirection player1Direction, storm::OptimizationDirection player2Direction, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& player1Groups, ExplicitQualitativeGameResultMinMax const& qualitativeResult, storm::storage::BitVector const& maybeStates, ExplicitGameStrategyPair& minStrategyPair) {
bool player1Min = player1Direction == storm::OptimizationDirection::Minimize;
bool player2Min = player2Direction == storm::OptimizationDirection::Minimize;
auto const& player1Prob0States = player2Min ? qualitativeResult.getProb0Min().asExplicitQualitativeGameResult().getPlayer1States() : qualitativeResult.getProb0Max().asExplicitQualitativeGameResult().getPlayer1States();
auto const& player1Prob1States = player2Min ? qualitativeResult.getProb1Min().asExplicitQualitativeGameResult().getPlayer1States() : qualitativeResult.getProb1Max().asExplicitQualitativeGameResult().getPlayer1States();
auto const& player2Prob0States = player2Min ? qualitativeResult.getProb0Min().asExplicitQualitativeGameResult().getPlayer2States() : qualitativeResult.getProb0Max().asExplicitQualitativeGameResult().getPlayer2States();
auto const& player2Prob1States = player2Min ? qualitativeResult.getProb1Min().asExplicitQualitativeGameResult().getPlayer2States() : qualitativeResult.getProb1Max().asExplicitQualitativeGameResult().getPlayer2States();
// Determine which rows to keep.
storm::storage::BitVector rows(transitionMatrix.getRowCount());
storm::storage::BitVector player2MaybeStates(transitionMatrix.getRowCount());
for (uint64_t player2State = 0; player2State < transitionMatrix.getRowGroupCount(); ++player2State) {
if (!player2Prob0States.get(player2State) && !player2Prob1States.get(player2State)) {
// Mark all rows that have a maybe state as a successor.
for (uint64_t row = transitionMatrix.getRowGroupIndices()[player2State]; row < transitionMatrix.getRowGroupIndices()[player2State + 1]; ++row) {
bool hasMaybeStateSuccessor = false;
for (auto const& entry : transitionMatrix.getRow(row)) {
if (maybeStates.get(entry.getColumn())) {
hasMaybeStateSuccessor = true;
}
}
if (!hasMaybeStateSuccessor) {
rows.set(row);
}
}
player2MaybeStates.set(player2State);
}
}
storm::storage::SparseMatrix<ValueType> submatrix = transitionMatrix.getSubmatrix(true, player2MaybeStates, <#const storm::storage::BitVector &columnConstraint#>)
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.
}
template<storm::dd::DdType Type, typename ModelType>

2
src/storm/solver/GameSolver.cpp
View File

@ -10,7 +10,7 @@ namespace storm {
namespace solver {
template<typename ValueType>
GameSolver<ValueType>::GameSolver() : trackSchedulers(false), cachingEnabled(false) {
GameSolver<ValueType>::GameSolver() : trackSchedulers(false), uniqueSolution(false), cachingEnabled(false) {
// Intentionally left empty
}

14
src/storm/solver/GameSolver.h
View File

@ -111,6 +111,16 @@ namespace storm {
* Clears the currently cached data that has been stored during previous calls of the solver.
*/
virtual void clearCache() const;
/*!
* Sets whether the solution to the min max equation system is known to be unique.
*/
void setHasUniqueSolution(bool value = true);
/*!
* Retrieves whether the solution to the min max equation system is assumed to be unique
*/
bool hasUniqueSolution() const;
protected:
@ -128,9 +138,11 @@ namespace storm {
boost::optional<std::vector<uint_fast64_t>> player2ChoicesHint;
private:
/// Whether the solver can assume that the min-max equation system has a unique solution
bool uniqueSolution;
/// Whether some of the generated data during solver calls should be cached.
bool cachingEnabled;
};
template<typename ValueType>

2
src/storm/solver/MinMaxLinearEquationSolver.h
View File

@ -170,7 +170,7 @@ namespace storm {
boost::optional<std::vector<uint_fast64_t>> initialScheduler;
private:
// Whether the solver can assume that the min-max equation system has a unique solution
/// Whether the solver can assume that the min-max equation system has a unique solution
bool uniqueSolution;
/// Whether some of the generated data during solver calls should be cached.

266
src/storm/solver/StandardGameSolver.cpp
View File

@ -16,12 +16,22 @@ namespace storm {
namespace solver {
template<typename ValueType>
StandardGameSolver<ValueType>::StandardGameSolver(storm::storage::SparseMatrix<storm::storage::sparse::state_type> const& player1Matrix, storm::storage::SparseMatrix<ValueType> const& player2Matrix, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory) : linearEquationSolverFactory(std::move(linearEquationSolverFactory)), localP1Matrix(nullptr), localP2Matrix(nullptr), player1Matrix(player1Matrix), player2Matrix(player2Matrix) {
StandardGameSolver<ValueType>::StandardGameSolver(storm::storage::SparseMatrix<storm::storage::sparse::state_type> const& player1Matrix, storm::storage::SparseMatrix<ValueType> const& player2Matrix, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory) : linearEquationSolverFactory(std::move(linearEquationSolverFactory)), localPlayer1Grouping(nullptr), localPlayer1Matrix(nullptr), localPlayer2Matrix(nullptr), player1Grouping(nullptr), player1Matrix(&player1Matrix), player2Matrix(player2Matrix) {
// Intentionally left empty.
}
template<typename ValueType>
StandardGameSolver<ValueType>::StandardGameSolver(storm::storage::SparseMatrix<storm::storage::sparse::state_type>&& player1Matrix, storm::storage::SparseMatrix<ValueType>&& player2Matrix, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory) : linearEquationSolverFactory(std::move(linearEquationSolverFactory)), localP1Matrix(std::make_unique<storm::storage::SparseMatrix<storm::storage::sparse::state_type>>(std::move(player1Matrix))), localP2Matrix(std::make_unique<storm::storage::SparseMatrix<ValueType>>(std::move(player2Matrix))), player1Matrix(*localP1Matrix), player2Matrix(*localP2Matrix) {
StandardGameSolver<ValueType>::StandardGameSolver(storm::storage::SparseMatrix<storm::storage::sparse::state_type>&& player1Matrix, storm::storage::SparseMatrix<ValueType>&& player2Matrix, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory) : linearEquationSolverFactory(std::move(linearEquationSolverFactory)), localPlayer1Grouping(nullptr), localPlayer1Matrix(std::make_unique<storm::storage::SparseMatrix<storm::storage::sparse::state_type>>(std::move(player1Matrix))), localPlayer2Matrix(std::make_unique<storm::storage::SparseMatrix<ValueType>>(std::move(player2Matrix))), player1Grouping(nullptr), player1Matrix(localPlayer1Matrix.get()), player2Matrix(*localPlayer2Matrix) {
// Intentionally left empty.
}
template<typename ValueType>
StandardGameSolver<ValueType>::StandardGameSolver(std::vector<uint64_t> const& player1Grouping, storm::storage::SparseMatrix<ValueType> const& player2Matrix, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory) : linearEquationSolverFactory(std::move(linearEquationSolverFactory)), localPlayer1Grouping(nullptr), localPlayer1Matrix(nullptr), localPlayer2Matrix(nullptr), player1Grouping(&player1Grouping), player1Matrix(nullptr), player2Matrix(player2Matrix) {
}
template<typename ValueType>
StandardGameSolver<ValueType>::StandardGameSolver(std::vector<uint64_t>&& player1Grouping, storm::storage::SparseMatrix<ValueType>&& player2Matrix, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory) : linearEquationSolverFactory(std::move(linearEquationSolverFactory)), localPlayer1Grouping(std::make_unique<std::vector<uint64_t>>(std::move(player1Grouping))), localPlayer1Matrix(nullptr), localPlayer2Matrix(std::make_unique<storm::storage::SparseMatrix<ValueType>>(std::move(player2Matrix))), player1Grouping(localPlayer1Grouping.get()), player1Matrix(nullptr), player2Matrix(*localPlayer2Matrix) {
// Intentionally left empty.
}
@ -63,20 +73,30 @@ namespace storm {
bool StandardGameSolver<ValueType>::solveGamePolicyIteration(Environment const& env, OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
// Create the initial choice selections.
std::vector<storm::storage::sparse::state_type> player1Choices = this->hasSchedulerHints() ? this->player1ChoicesHint.get() : std::vector<storm::storage::sparse::state_type>(this->player1Matrix.getRowGroupCount(), 0);
std::vector<storm::storage::sparse::state_type> player1Choices;
if (this->hasSchedulerHints()) {
player1Choices = this->player1ChoicesHint.get();
} else if (this->player1RepresentedByMatrix()) {
// Player 1 represented by matrix.
player1Choices = std::vector<storm::storage::sparse::state_type>(this->getPlayer1Matrix().getRowGroupCount(), 0);
} else {
// Player 1 represented by grouping of player 2 states.
player1Choices = this->getPlayer1Grouping();
player1Choices.resize(player1Choices.size() - 1);
}
std::vector<storm::storage::sparse::state_type> player2Choices = this->hasSchedulerHints() ? this->player2ChoicesHint.get() : std::vector<storm::storage::sparse::state_type>(this->player2Matrix.getRowGroupCount(), 0);
if(!auxiliaryP2RowGroupVector) {
if (!auxiliaryP2RowGroupVector) {
auxiliaryP2RowGroupVector = std::make_unique<std::vector<ValueType>>(this->player2Matrix.getRowGroupCount());
}
if(!auxiliaryP1RowGroupVector) {
auxiliaryP1RowGroupVector = std::make_unique<std::vector<ValueType>>(this->player1Matrix.getRowGroupCount());
if (!auxiliaryP1RowGroupVector) {
auxiliaryP1RowGroupVector = std::make_unique<std::vector<ValueType>>(this->player1Matrix->getRowGroupCount());
}
std::vector<ValueType>& subB = *auxiliaryP1RowGroupVector;
uint64_t maxIter = env.solver().game().getMaximalNumberOfIterations();
// The linear equation solver should be at least as precise as this solver
// The linear equation solver should be at least as precise as this solver.
std::unique_ptr<storm::Environment> environmentOfSolverStorage;
auto precOfSolver = env.solver().getPrecisionOfLinearEquationSolver(env.solver().getLinearEquationSolverType());
if (!storm::NumberTraits<ValueType>::IsExact) {
@ -104,8 +124,13 @@ namespace storm {
submatrix.convertToEquationSystem();
}
auto submatrixSolver = linearEquationSolverFactory->create(environmentOfSolver, std::move(submatrix));
if (this->lowerBound) { submatrixSolver->setLowerBound(this->lowerBound.get()); }
if (this->upperBound) { submatrixSolver->setUpperBound(this->upperBound.get()); }
if (this->lowerBound) {
submatrixSolver->setLowerBound(this->lowerBound.get());
}
if (this->upperBound) {
submatrixSolver->setUpperBound(this->upperBound.get());
}
submatrixSolver->setCachingEnabled(true);
Status status = Status::InProgress;
@ -140,7 +165,7 @@ namespace storm {
this->player2SchedulerChoices = std::move(player2Choices);
}
if(!this->isCachingEnabled()) {
if (!this->isCachingEnabled()) {
clearCache();
}
@ -163,25 +188,21 @@ namespace storm {
multiplierPlayer2Matrix = storm::solver::MultiplierFactory<ValueType>().create(env, player2Matrix);
}
if (!auxiliaryP2RowVector) {
auxiliaryP2RowVector = std::make_unique<std::vector<ValueType>>(player2Matrix.getRowCount());
}
if (!auxiliaryP2RowGroupVector) {
auxiliaryP2RowGroupVector = std::make_unique<std::vector<ValueType>>(player2Matrix.getRowGroupCount());
}
if (!auxiliaryP1RowGroupVector) {
auxiliaryP1RowGroupVector = std::make_unique<std::vector<ValueType>>(player1Matrix.getRowGroupCount());
auxiliaryP1RowGroupVector = std::make_unique<std::vector<ValueType>>(this->getNumberOfPlayer1States());
}
ValueType precision = storm::utility::convertNumber<ValueType>(env.solver().game().getPrecision());
bool relative = env.solver().game().getRelativeTerminationCriterion();
uint64_t maxIter = env.solver().game().getMaximalNumberOfIterations();
std::vector<ValueType>& multiplyResult = *auxiliaryP2RowVector;
std::vector<ValueType>& reducedMultiplyResult = *auxiliaryP2RowGroupVector;
std::vector<ValueType>& reducedPlayer2Result = *auxiliaryP2RowGroupVector;
bool trackSchedulersInValueIteration = this->isTrackSchedulersSet() && !this->hasUniqueSolution();
if (this->hasSchedulerHints()) {
// Solve the equation system induced by the two schedulers.
storm::storage::SparseMatrix<ValueType> submatrix;
@ -190,9 +211,25 @@ namespace storm {
submatrix.convertToEquationSystem();
}
auto submatrixSolver = linearEquationSolverFactory->create(env, std::move(submatrix));
if (this->lowerBound) { submatrixSolver->setLowerBound(this->lowerBound.get()); }
if (this->upperBound) { submatrixSolver->setUpperBound(this->upperBound.get()); }
if (this->lowerBound) {
submatrixSolver->setLowerBound(this->lowerBound.get());
}
if (this->upperBound) {
submatrixSolver->setUpperBound(this->upperBound.get());
}
submatrixSolver->solveEquations(env, x, *auxiliaryP1RowGroupVector);
// If requested, we store the scheduler for retrieval. Initialize the schedulers to the hint we have.
if (trackSchedulersInValueIteration) {
this->player1SchedulerChoices = this->player1ChoicesHint.get();
this->player2SchedulerChoices = this->player2ChoicesHint.get();
}
} else if (trackSchedulersInValueIteration) {
// If requested, we store the scheduler for retrieval. Create empty schedulers here so we can fill them
// during VI.
this->player1SchedulerChoices = std::vector<uint_fast64_t>(this->getNumberOfPlayer1States(), 0);
this->player2SchedulerChoices = std::vector<uint_fast64_t>(this->getNumberOfPlayer2States(), 0);
}
std::vector<ValueType>* newX = auxiliaryP1RowGroupVector.get();
@ -203,7 +240,7 @@ namespace storm {
Status status = Status::InProgress;
while (status == Status::InProgress) {
multiplyAndReduce(env, player1Dir, player2Dir, *currentX, &b, *multiplierPlayer2Matrix, multiplyResult, reducedMultiplyResult, *newX);
multiplyAndReduce(env, player1Dir, player2Dir, *currentX, &b, *multiplierPlayer2Matrix, reducedPlayer2Result, *newX, trackSchedulersInValueIteration ? &this->getPlayer1SchedulerChoices() : nullptr, trackSchedulersInValueIteration ? &this->getPlayer2SchedulerChoices() : nullptr);
// Determine whether the method converged.
if (storm::utility::vector::equalModuloPrecision<ValueType>(*currentX, *newX, precision, relative)) {
@ -225,13 +262,13 @@ namespace storm {
}
// If requested, we store the scheduler for retrieval.
if (this->isTrackSchedulersSet()) {
this->player1SchedulerChoices = std::vector<uint_fast64_t>(player1Matrix.getRowGroupCount(), 0);
this->player2SchedulerChoices = std::vector<uint_fast64_t>(player2Matrix.getRowGroupCount(), 0);
if (this->isTrackSchedulersSet() && this->hasUniqueSolution()) {
this->player1SchedulerChoices = std::vector<uint_fast64_t>(this->getNumberOfPlayer1States(), 0);
this->player2SchedulerChoices = std::vector<uint_fast64_t>(this->getNumberOfPlayer2States(), 0);
extractChoices(player1Dir, player2Dir, x, b, *auxiliaryP2RowGroupVector, this->player1SchedulerChoices.get(), this->player2SchedulerChoices.get());
}
if(!this->isCachingEnabled()) {
if (!this->isCachingEnabled()) {
clearCache();
}
@ -245,54 +282,53 @@ namespace storm {
multiplierPlayer2Matrix = storm::solver::MultiplierFactory<ValueType>().create(env, player2Matrix);
}
if (!auxiliaryP2RowVector) {
auxiliaryP2RowVector = std::make_unique<std::vector<ValueType>>(player2Matrix.getRowCount());
}
if (!auxiliaryP2RowGroupVector) {
auxiliaryP2RowGroupVector = std::make_unique<std::vector<ValueType>>(player2Matrix.getRowGroupCount());
}
std::vector<ValueType>& multiplyResult = *auxiliaryP2RowVector;
std::vector<ValueType>& reducedMultiplyResult = *auxiliaryP2RowGroupVector;
std::vector<ValueType>& reducedPlayer2Result = *auxiliaryP2RowGroupVector;
for (uint_fast64_t iteration = 0; iteration < n; ++iteration) {
multiplyAndReduce(env, player1Dir, player2Dir, x, b, *multiplierPlayer2Matrix, multiplyResult, reducedMultiplyResult, x);
multiplyAndReduce(env, player1Dir, player2Dir, x, b, *multiplierPlayer2Matrix, reducedPlayer2Result, x);
}
if(!this->isCachingEnabled()) {
if (!this->isCachingEnabled()) {
clearCache();
}
}
template<typename ValueType>
void StandardGameSolver<ValueType>::multiplyAndReduce(Environment const& env, OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector<ValueType>& x, std::vector<ValueType> const* b, storm::solver::Multiplier<ValueType> const& multiplier, std::vector<ValueType>& multiplyResult, std::vector<ValueType>& p2ReducedMultiplyResult, std::vector<ValueType>& p1ReducedMultiplyResult) const {
void StandardGameSolver<ValueType>::multiplyAndReduce(Environment const& env, OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector<ValueType>& x, std::vector<ValueType> const* b, storm::solver::Multiplier<ValueType> const& multiplier, std::vector<ValueType>& player2ReducedResult, std::vector<ValueType>& player1ReducedResult, std::vector<uint64_t>* player1SchedulerChoices, std::vector<uint64_t>* player2SchedulerChoices) const {
multiplier.multiply(env, x, b, multiplyResult);
multiplier.multiplyAndReduce(env, player2Dir, x, b, player2ReducedResult, player2SchedulerChoices);
storm::utility::vector::reduceVectorMinOrMax(player2Dir, multiplyResult, p2ReducedMultiplyResult, player2Matrix.getRowGroupIndices());
uint_fast64_t pl1State = 0;
for (auto& result : p1ReducedMultiplyResult) {
storm::storage::SparseMatrix<storm::storage::sparse::state_type>::const_rows relevantRows = player1Matrix.getRowGroup(pl1State);
STORM_LOG_ASSERT(relevantRows.getNumberOfEntries() != 0, "There is a choice of player 1 that does not lead to any player 2 choice");
auto it = relevantRows.begin();
auto ite = relevantRows.end();
// Set the first value.
result = p2ReducedMultiplyResult[it->getColumn()];
++it;
// Now iterate through the different values and pick the extremal one.
if (player1Dir == OptimizationDirection::Minimize) {
for (; it != ite; ++it) {
result = std::min(result, p2ReducedMultiplyResult[it->getColumn()]);
}
} else {
for (; it != ite; ++it) {
result = std::max(result, p2ReducedMultiplyResult[it->getColumn()]);
if (this->player1RepresentedByMatrix()) {
// Player 1 represented by matrix.
uint_fast64_t player1State = 0;
for (auto& result : player1ReducedResult) {
storm::storage::SparseMatrix<storm::storage::sparse::state_type>::const_rows relevantRows = this->getPlayer1Matrix().getRowGroup(player1State);
STORM_LOG_ASSERT(relevantRows.getNumberOfEntries() != 0, "There is a choice of player 1 that does not lead to any player 2 choice");
auto it = relevantRows.begin();
auto ite = relevantRows.end();
// Set the first value.
result = player2ReducedResult[it->getColumn()];
++it;
// Now iterate through the different values and pick the extremal one.
if (player1Dir == OptimizationDirection::Minimize) {
for (; it != ite; ++it) {
result = std::min(result, player2ReducedResult[it->getColumn()]);
}
} else {
for (; it != ite; ++it) {
result = std::max(result, player2ReducedResult[it->getColumn()]);
}
}
++player1State;
}
++pl1State;
} else {
// Player 1 represented by grouping of player 2 states (vector).
storm::utility::vector::reduceVectorMinOrMax(player1Dir, player2ReducedResult, player1ReducedResult, this->getPlayer1Grouping(), player1SchedulerChoices);
}
}
@ -333,22 +369,45 @@ namespace storm {
}
}
// Now extract the choices of player 1
for (uint_fast64_t p1Group = 0; p1Group < this->player1Matrix.getRowGroupCount(); ++p1Group) {
uint_fast64_t firstRowInGroup = this->player1Matrix.getRowGroupIndices()[p1Group];
uint_fast64_t rowGroupSize = this->player1Matrix.getRowGroupIndices()[p1Group + 1] - firstRowInGroup;
uint_fast64_t currentChoice = player1Choices[p1Group];
ValueType currentValue = player2ChoiceValues[this->player1Matrix.getRow(firstRowInGroup + currentChoice).begin()->getColumn()];
for (uint_fast64_t p1Choice = 0; p1Choice < rowGroupSize; ++p1Choice) {
// If the choice is the currently selected one, we can skip it.
if (p1Choice == currentChoice) {
continue;
// Now extract the choices of player 1.
if (this->player1RepresentedByMatrix()) {
// Player 1 represented by matrix.
for (uint_fast64_t p1Group = 0; p1Group < this->getPlayer1Matrix().getRowGroupCount(); ++p1Group) {
uint_fast64_t firstRowInGroup = this->getPlayer1Matrix().getRowGroupIndices()[p1Group];
uint_fast64_t rowGroupSize = this->getPlayer1Matrix().getRowGroupIndices()[p1Group + 1] - firstRowInGroup;
uint_fast64_t currentChoice = player1Choices[p1Group];
ValueType currentValue = player2ChoiceValues[this->getPlayer1Matrix().getRow(firstRowInGroup + currentChoice).begin()->getColumn()];
for (uint_fast64_t p1Choice = 0; p1Choice < rowGroupSize; ++p1Choice) {
// If the choice is the currently selected one, we can skip it.
if (p1Choice == currentChoice) {
continue;
}
ValueType const& choiceValue = player2ChoiceValues[this->getPlayer1Matrix().getRow(firstRowInGroup + p1Choice).begin()->getColumn()];
if (valueImproved(player1Dir, currentValue, choiceValue)) {
schedulerImproved = true;
player1Choices[p1Group] = p1Choice;
currentValue = choiceValue;
}
}
ValueType const& choiceValue = player2ChoiceValues[this->player1Matrix.getRow(firstRowInGroup + p1Choice).begin()->getColumn()];
if (valueImproved(player1Dir, currentValue, choiceValue)) {
schedulerImproved = true;
player1Choices[p1Group] = p1Choice;
currentValue = choiceValue;
}
} else {
// Player 1 represented by grouping of player 2 states (vector).
for (uint64_t player1State = 0; player1State < this->getPlayer1Grouping().size() - 1; ++player1State) {
uint64_t currentChoice = player1Choices[player1State];
ValueType currentValue = player2ChoiceValues[currentChoice];
uint64_t numberOfPlayer2Successors = this->getPlayer1Grouping()[player1State + 1] - this->getPlayer1Grouping()[player1State];
for (uint64_t player2State = 0; player2State < numberOfPlayer2Successors; ++player2State) {
// If the choice is the currently selected one, we can skip it.
if (currentChoice == player2State + this->getPlayer1Grouping()[player1State]) {
continue;
}
ValueType const& choiceValue = player2ChoiceValues[this->getPlayer1Grouping()[player1State] + player2State];
if (valueImproved(player1Dir, currentValue, choiceValue)) {
schedulerImproved = true;
player1Choices[player1State] = player2State;
currentValue = choiceValue;
}
}
}
}
@ -358,25 +417,66 @@ namespace storm {
template<typename ValueType>
void StandardGameSolver<ValueType>::getInducedMatrixVector(std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<uint_fast64_t> const& player1Choices, std::vector<uint_fast64_t> const& player2Choices, storm::storage::SparseMatrix<ValueType>& inducedMatrix, std::vector<ValueType>& inducedVector) const {
//Get the rows of the player2matrix that are selected by the schedulers
//Note that rows can be selected more then once and in an arbitrary order.
// Get the rows of the player 2 matrix that are selected by the schedulers.
// Note that rows can be selected more than once and in an arbitrary order.
std::vector<storm::storage::sparse::state_type> selectedRows;
selectedRows.reserve(player1Matrix.getRowGroupCount());
uint_fast64_t pl1State = 0;
for (auto const& pl1Choice : player1Choices){
auto const& pl1Row = player1Matrix.getRow(pl1State, pl1Choice);
STORM_LOG_ASSERT(pl1Row.getNumberOfEntries() == 1, "It is assumed that rows of player one have one entry, but this is not the case.");
uint_fast64_t const& pl2State = pl1Row.begin()->getColumn();
selectedRows.push_back(player2Matrix.getRowGroupIndices()[pl2State] + player2Choices[pl2State]);
++pl1State;
if (this->player1RepresentedByMatrix()) {
// Player 1 is represented by a matrix.
selectedRows.reserve(this->getPlayer1Matrix().getRowGroupCount());
uint_fast64_t player1State = 0;
for (auto const& player1Choice : player1Choices) {
auto const& player1Row = this->getPlayer1Matrix().getRow(player1State, player1Choice);
STORM_LOG_ASSERT(player1Row.getNumberOfEntries() == 1, "It is assumed that rows of player one have one entry, but this is not the case.");
uint_fast64_t player2State = player1Row.begin()->getColumn();
selectedRows.push_back(player2Matrix.getRowGroupIndices()[player2State] + player2Choices[player2State]);
++player1State;
}
} else {
// Player 1 is represented by the grouping of player 2 states (vector).
selectedRows.reserve(this->player2Matrix.getRowGroupCount());
for (uint64_t player1State = 0; player1State < this->getPlayer1Grouping().size() - 1; ++player1State) {
uint64_t player2State = player1Choices[player1State];
selectedRows.emplace_back(player2Matrix.getRowGroupIndices()[player2State] + player2Choices[player2State]);
}
}
//Get the matrix and the vector induced by this selection. Note that we add entries at the diagonal
// Get the matrix and the vector induced by this selection and add entries on the diagonal in the process.
inducedMatrix = player2Matrix.selectRowsFromRowIndexSequence(selectedRows, true);
inducedVector.resize(inducedMatrix.getRowCount());
storm::utility::vector::selectVectorValues<ValueType>(inducedVector, selectedRows, b);
}
template<typename ValueType>
bool StandardGameSolver<ValueType>::player1RepresentedByMatrix() const {
return player1Matrix != nullptr;
}
template<typename ValueType>
storm::storage::SparseMatrix<storm::storage::sparse::state_type> const& StandardGameSolver<ValueType>::getPlayer1Matrix() const {
STORM_LOG_ASSERT(player1RepresentedByMatrix(), "Player 1 is represented by a matrix.");
return *player1Matrix;
}
template<typename ValueType>
std::vector<uint64_t> const& StandardGameSolver<ValueType>::getPlayer1Grouping() const {
STORM_LOG_ASSERT(!player1RepresentedByMatrix(), "Player 1 is represented by a matrix.");
return *player1Grouping;
}
template<typename ValueType>
uint64_t StandardGameSolver<ValueType>::getNumberOfPlayer1States() const {
if (this->player1RepresentedByMatrix()) {
return this->getPlayer1Matrix().getRowGroupCount();
} else {
return this->getPlayer1Grouping().size() - 1;
}
}
template<typename ValueType>
uint64_t StandardGameSolver<ValueType>::getNumberOfPlayer2States() const {
return this->player2Matrix.getRowGroupCount();
}
template<typename ValueType>
typename StandardGameSolver<ValueType>::Status StandardGameSolver<ValueType>::updateStatusIfNotConverged(Status status, std::vector<ValueType> const& x, uint64_t iterations, uint64_t maximalNumberOfIterations) const {
if (status != Status::Converged) {

22
src/storm/solver/StandardGameSolver.h
View File

@ -11,10 +11,14 @@ namespace storm {
template<typename ValueType>
class StandardGameSolver : public GameSolver<ValueType> {
public:
// Constructors for when the first player is represented using a matrix.
StandardGameSolver(storm::storage::SparseMatrix<storm::storage::sparse::state_type> const& player1Matrix, storm::storage::SparseMatrix<ValueType> const& player2Matrix, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory);
StandardGameSolver(storm::storage::SparseMatrix<storm::storage::sparse::state_type>&& player1Matrix, storm::storage::SparseMatrix<ValueType>&& player2Matrix, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory);
// Constructor for when the first player is represented by a grouping of the player 2 states (row groups).
StandardGameSolver(std::vector<uint64_t> const& player1Groups, storm::storage::SparseMatrix<ValueType> const& player2Matrix, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory);
StandardGameSolver(std::vector<uint64_t>&& player1Groups, storm::storage::SparseMatrix<ValueType>&& player2Matrix, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory);
virtual bool solveGame(Environment const& env, OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const override;
virtual void repeatedMultiply(Environment const& env, OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector<ValueType>& x, std::vector<ValueType> const* b, uint_fast64_t n = 1) const override;
@ -27,7 +31,7 @@ namespace storm {
bool solveGameValueIteration(Environment const& env, OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const;
// Computes p2Matrix * x + b, reduces the result w.r.t. player 2 choices, and then reduces the result w.r.t. player 1 choices.
void multiplyAndReduce(Environment const& env, OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector<ValueType>& x, std::vector<ValueType> const* b, storm::solver::Multiplier<ValueType> const& multiplier, std::vector<ValueType>& multiplyResult, std::vector<ValueType>& p2ReducedMultiplyResult, std::vector<ValueType>& p1ReducedMultiplyResult) const;
void multiplyAndReduce(Environment const& env, OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector<ValueType>& x, std::vector<ValueType> const* b, storm::solver::Multiplier<ValueType> const& multiplier, std::vector<ValueType>& player2ReducedResult, std::vector<ValueType>& player1ReducedResult, std::vector<uint64_t>* player1SchedulerChoices = nullptr, std::vector<uint64_t>* player2SchedulerChoices = nullptr) const;
// Solves the equation system given by the two choice selections
void getInducedMatrixVector(std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<uint_fast64_t> const& player1Choices, std::vector<uint_fast64_t> const& player2Choices, storm::storage::SparseMatrix<ValueType>& inducedMatrix, std::vector<ValueType>& inducedVector) const;
@ -38,6 +42,12 @@ namespace storm {
bool valueImproved(OptimizationDirection dir, ValueType const& value1, ValueType const& value2) const;
bool player1RepresentedByMatrix() const;
storm::storage::SparseMatrix<storm::storage::sparse::state_type> const& getPlayer1Matrix() const;
std::vector<uint64_t> const& getPlayer1Grouping() const;
uint64_t getNumberOfPlayer1States() const;
uint64_t getNumberOfPlayer2States() const;
enum class Status {
Converged, TerminatedEarly, MaximalIterationsExceeded, InProgress
};
@ -56,12 +66,14 @@ namespace storm {
// If the solver takes posession of the matrix, we store the moved matrix in this member, so it gets deleted
// when the solver is destructed.
std::unique_ptr<storm::storage::SparseMatrix<storm::storage::sparse::state_type>> localP1Matrix;
std::unique_ptr<storm::storage::SparseMatrix<ValueType>> localP2Matrix;
std::unique_ptr<std::vector<uint64_t>> localPlayer1Grouping;
std::unique_ptr<storm::storage::SparseMatrix<storm::storage::sparse::state_type>> localPlayer1Matrix;
std::unique_ptr<storm::storage::SparseMatrix<ValueType>> localPlayer2Matrix;
// 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<storm::storage::sparse::state_type> const& player1Matrix;
std::vector<uint64_t> const* player1Grouping;
storm::storage::SparseMatrix<storm::storage::sparse::state_type> const* player1Matrix;
storm::storage::SparseMatrix<ValueType> const& player2Matrix;
};

2
src/storm/storage/SparseMatrix.h
View File

@ -756,7 +756,7 @@ namespace storm {
/*!
* Selects the rows that are given by the sequence of row indices, allowing to select rows arbitrarily often and with an arbitrary order
* The resulting matrix will have a trivial row grouping
* The resulting matrix will have a trivial row grouping.
*
* @param rowIndexSequence the sequence of row indices which specifies, which rows are contained in the new matrix
* @param insertDiagonalEntries If set to true, the resulting matrix will have zero entries in column i for

Write Preview
Loading…
Cancel
Save