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

making policy iteration available for game-based abstraction (prototypical for now)

main
dehnert 7 years ago
parent
9b80c65d72
commit
48f5608157
7 changed files with 147 additions and 235 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. 256
      src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
  2. 86
      src/storm/solver/StandardGameSolver.cpp
  3. 4
      src/storm/solver/StandardGameSolver.h
  4. 12
      src/storm/storage/SparseMatrix.cpp
  5. 12
      src/storm/utility/constants.cpp
  6. 7
      src/storm/utility/constants.h
  7. 5
      src/storm/utility/vector.h

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

@ -476,37 +476,21 @@ namespace storm {
uint64_t maybeStatePosition = 0;
previousPlayer2States = 0;
for (auto state : maybeStates) {
if (state == 2324 || state == 50377 || state == 50209) {
std::cout << "dealing with problematic state " << state << " whose local offset is " << maybeStatePosition << std::endl;
}
uint64_t chosenPlayer2State = startingStrategyPair->getPlayer1Strategy().getChoice(state);
uint64_t previousPlayer2MaybeStatesForState = 0;
for (uint64_t player2State = player1Groups[state]; player2State < player1Groups[state + 1]; ++player2State) {
if (player2MaybeStates.get(player2State)) {
if (state == 2324 || state == 50377 || state == 50209) {
std::cout << "player 2 state " << player2State << " is a player 2 maybe state with local index " << previousPlayer2States << " ranging from row " << submatrix.getRowGroupIndices()[previousPlayer2States] << " to " << submatrix.getRowGroupIndices()[previousPlayer2States + 1] << std::endl;
}
if (player2State == chosenPlayer2State) {
player1Scheduler[maybeStatePosition] = previousPlayer2MaybeStatesForState;
if (state == 2324 || state == 50377 || state == 50209) {
std::cout << "player 1 scheduler chooses " << previousPlayer2MaybeStatesForState << " which globally is " << player2State << std::endl;
}
}
// Copy over the player 2 action (modulo making it local) as all rows for the player 2 state are taken.
if (startingStrategyPair->getPlayer2Strategy().hasDefinedChoice(player2State)) {
player2Scheduler[previousPlayer2States] = startingStrategyPair->getPlayer2Strategy().getChoice(player2State) - transitionMatrix.getRowGroupIndices()
[player2State];
if (state == 2324 || state == 50377 || state == 50209) {
std::cout << "copied over choice " << player2Scheduler[previousPlayer2States] << " for player 2 (global index " << startingStrategyPair->getPlayer2Strategy().getChoice(player2State) << ")" << std::endl;
}
} else {
player2Scheduler[previousPlayer2States] = 0;
if (state == 2324 || state == 50377 || state == 50209) {
std::cout << "did not copy (undefined) choice for player 2 (global index " << startingStrategyPair->getPlayer2Strategy().getChoice(player2State) << ")" << std::endl;
}
}
++previousPlayer2MaybeStatesForState;
@ -517,37 +501,6 @@ namespace storm {
++maybeStatePosition;
}
STORM_LOG_ASSERT(previousPlayer2States == submatrix.getRowGroupCount(), "Expected correct number of player 2 states.");
} else {
// If the starting strategy pair was provided, we need to extract the choices of the maybe states here.
uint64_t maybeStatePosition = 0;
previousPlayer2States = 0;
for (auto state : maybeStates) {
if (state == 2324 || state == 50377 || state == 50209) {
std::cout << "dealing with problematic state " << state << " whose local offset is " << maybeStatePosition << std::endl;
}
if (state == 2324 || state == 50377 || state == 50209) {
std::cout << "player 1 scheduler chooses " << player1Scheduler[maybeStatePosition] << " which globally is " << (player1Groups[state] + player1Scheduler[maybeStatePosition]) << std::endl;
}
uint64_t previousPlayer2MaybeStatesForState = 0;
for (uint64_t player2State = player1Groups[state]; player2State < player1Groups[state + 1]; ++player2State) {
if (player2MaybeStates.get(player2State)) {
if (state == 2324 || state == 50377 || state == 50209) {
std::cout << "player 2 state " << player2State << " is a player 2 maybe state with local index " << previousPlayer2States << " ranging from row " << submatrix.getRowGroupIndices()[previousPlayer2States] << " to " << submatrix.getRowGroupIndices()[previousPlayer2States + 1] << std::endl;
}
if (state == 2324 || state == 50377 || state == 50209) {
std::cout << "player 2 scheduler chooses " << player2Scheduler[previousPlayer2States] << " for player 2 (global index " << (transitionMatrix.getRowGroupIndices()[player2State] + player2Scheduler[previousPlayer2States]) << ")" << std::endl;
}
++previousPlayer2MaybeStatesForState;
++previousPlayer2States;
}
}
++maybeStatePosition;
}
STORM_LOG_ASSERT(previousPlayer2States == submatrix.getRowGroupCount(), "Expected correct number of player 2 states.");
}
// Solve actual game and track schedulers.
@ -564,24 +517,18 @@ namespace storm {
bool madePlayer1Choice = false;
for (uint64_t player2State = player1Groups[state]; player2State < player1Groups[state + 1]; ++player2State) {
if (player1Scheduler[previousPlayer1MaybeStates] == previousPlayer2MaybeStatesForState) {
if (state == 2324 || state == 50377 || state == 50209) {
std::cout << "player 1 choosing " << player2State << " in " << state << std::endl;
}
strategyPair.getPlayer1Strategy().setChoice(state, player2State);
madePlayer1Choice = true;
}
if (player2MaybeStates.get(player2State)) {
if (state == 2324 || state == 50377 || state == 50209) {
std::cout << "player 2 choosing " << (transitionMatrix.getRowGroupIndices()[player2State] + player2Scheduler[previousPlayer2MaybeStates]) << " in " << player2State << " for player 1 state " << state << std::endl;
}
strategyPair.getPlayer2Strategy().setChoice(player2State, transitionMatrix.getRowGroupIndices()[player2State] + player2Scheduler[previousPlayer2MaybeStates]);
++previousPlayer2MaybeStatesForState;
++previousPlayer2MaybeStates;
}
}
STORM_LOG_ASSERT(madePlayer1Choice, "Player 1 state " << state << " did not make a choice, scheduler: " << player1Scheduler[previousPlayer1MaybeStates] << ".");
STORM_LOG_ASSERT(madePlayer1Choice, "[" << player1Direction << "]: player 1 state " << state << " did not make a choice, scheduler: " << player1Scheduler[previousPlayer1MaybeStates] << ".");
++previousPlayer1MaybeStates;
}
@ -1088,82 +1035,76 @@ namespace storm {
template <typename ValueType>
void postProcessStrategies(uint64_t iteration, storm::OptimizationDirection const& player1Direction, abstraction::ExplicitGameStrategyPair& minStrategyPair, abstraction::ExplicitGameStrategyPair& maxStrategyPair, std::vector<uint64_t> const& player1Groups, std::vector<uint64_t> const& player2Groups, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, ExplicitQuantitativeResultMinMax<ValueType> const& quantitativeResult, bool redirectPlayer1, bool redirectPlayer2, bool sanityCheck) {
if (!redirectPlayer1 && !redirectPlayer2) {
return;
}
for (uint64_t state = 0; state < player1Groups.size() - 1; ++state) {
STORM_LOG_ASSERT(targetStates.get(state) || minStrategyPair.getPlayer1Strategy().hasDefinedChoice(state), "Expected lower player 1 choice in state " << state << ".");
STORM_LOG_ASSERT(targetStates.get(state) || maxStrategyPair.getPlayer1Strategy().hasDefinedChoice(state), "Expected upper player 1 choice in state " << state << ".");
bool hasMinPlayer1Choice = false;
uint64_t lowerPlayer1Choice = 0;
ValueType lowerValueUnderMinChoicePlayer1 = storm::utility::zero<ValueType>();
bool hasMaxPlayer1Choice = false;
uint64_t upperPlayer1Choice = 0;
ValueType lowerValueUnderMaxChoicePlayer1 = storm::utility::zero<ValueType>();
if (minStrategyPair.getPlayer1Strategy().hasDefinedChoice(state)) {
hasMinPlayer1Choice = true;
lowerPlayer1Choice = minStrategyPair.getPlayer1Strategy().getChoice(state);
STORM_LOG_ASSERT(minStrategyPair.getPlayer2Strategy().hasDefinedChoice(lowerPlayer1Choice), "Expected lower player 2 choice for state " << state << " (lower player 1 choice " << lowerPlayer1Choice << ").");
uint64_t lowerPlayer2Choice = minStrategyPair.getPlayer2Strategy().getChoice(lowerPlayer1Choice);
if (redirectPlayer1 || redirectPlayer2) {
for (uint64_t state = 0; state < player1Groups.size() - 1; ++state) {
STORM_LOG_ASSERT(targetStates.get(state) || minStrategyPair.getPlayer1Strategy().hasDefinedChoice(state), "Expected lower player 1 choice in state " << state << ".");
STORM_LOG_ASSERT(targetStates.get(state) || maxStrategyPair.getPlayer1Strategy().hasDefinedChoice(state), "Expected upper player 1 choice in state " << state << ".");
ValueType lowerValueUnderLowerChoicePlayer2 = transitionMatrix.multiplyRowWithVector(lowerPlayer2Choice, quantitativeResult.getMin().getValues());
lowerValueUnderMinChoicePlayer1 = lowerValueUnderLowerChoicePlayer2;
bool hasMinPlayer1Choice = false;
uint64_t lowerPlayer1Choice = 0;
ValueType lowerValueUnderMinChoicePlayer1 = storm::utility::zero<ValueType>();
bool hasMaxPlayer1Choice = false;
uint64_t upperPlayer1Choice = 0;
ValueType lowerValueUnderMaxChoicePlayer1 = storm::utility::zero<ValueType>();
if (maxStrategyPair.getPlayer2Strategy().hasDefinedChoice(lowerPlayer1Choice)) {
uint64_t upperPlayer2Choice = maxStrategyPair.getPlayer2Strategy().getChoice(lowerPlayer1Choice);
if (minStrategyPair.getPlayer1Strategy().hasDefinedChoice(state)) {
hasMinPlayer1Choice = true;
lowerPlayer1Choice = minStrategyPair.getPlayer1Strategy().getChoice(state);
if (lowerPlayer2Choice != upperPlayer2Choice) {
ValueType lowerValueUnderUpperChoicePlayer2 = transitionMatrix.multiplyRowWithVector(upperPlayer2Choice, quantitativeResult.getMin().getValues());
STORM_LOG_ASSERT(minStrategyPair.getPlayer2Strategy().hasDefinedChoice(lowerPlayer1Choice), "Expected lower player 2 choice for state " << state << " (lower player 1 choice " << lowerPlayer1Choice << ").");
uint64_t lowerPlayer2Choice = minStrategyPair.getPlayer2Strategy().getChoice(lowerPlayer1Choice);
ValueType lowerValueUnderLowerChoicePlayer2 = transitionMatrix.multiplyRowWithVector(lowerPlayer2Choice, quantitativeResult.getMin().getValues());
lowerValueUnderMinChoicePlayer1 = lowerValueUnderLowerChoicePlayer2;
if (maxStrategyPair.getPlayer2Strategy().hasDefinedChoice(lowerPlayer1Choice)) {
uint64_t upperPlayer2Choice = maxStrategyPair.getPlayer2Strategy().getChoice(lowerPlayer1Choice);
if (redirectPlayer2 && lowerValueUnderUpperChoicePlayer2 <= lowerValueUnderLowerChoicePlayer2) {
lowerValueUnderMinChoicePlayer1 = lowerValueUnderUpperChoicePlayer2;
minStrategyPair.getPlayer2Strategy().setChoice(lowerPlayer1Choice, upperPlayer2Choice);
if (lowerPlayer2Choice != upperPlayer2Choice) {
ValueType lowerValueUnderUpperChoicePlayer2 = transitionMatrix.multiplyRowWithVector(upperPlayer2Choice, quantitativeResult.getMin().getValues());
if (redirectPlayer2 && lowerValueUnderUpperChoicePlayer2 <= lowerValueUnderLowerChoicePlayer2) {
lowerValueUnderMinChoicePlayer1 = lowerValueUnderUpperChoicePlayer2;
minStrategyPair.getPlayer2Strategy().setChoice(lowerPlayer1Choice, upperPlayer2Choice);
}
}
}
}
}
if (maxStrategyPair.getPlayer1Strategy().hasDefinedChoice(state)) {
upperPlayer1Choice = maxStrategyPair.getPlayer1Strategy().getChoice(state);
if (upperPlayer1Choice != lowerPlayer1Choice && minStrategyPair.getPlayer2Strategy().hasDefinedChoice(upperPlayer1Choice)) {
hasMaxPlayer1Choice = true;
uint64_t lowerPlayer2Choice = minStrategyPair.getPlayer2Strategy().getChoice(upperPlayer1Choice);
if (maxStrategyPair.getPlayer1Strategy().hasDefinedChoice(state)) {
upperPlayer1Choice = maxStrategyPair.getPlayer1Strategy().getChoice(state);
ValueType lowerValueUnderLowerChoicePlayer2 = transitionMatrix.multiplyRowWithVector(lowerPlayer2Choice, quantitativeResult.getMin().getValues());
lowerValueUnderMaxChoicePlayer1 = lowerValueUnderLowerChoicePlayer2;
STORM_LOG_ASSERT(maxStrategyPair.getPlayer2Strategy().hasDefinedChoice(upperPlayer1Choice), "Expected upper player 2 choice for state " << state << " (upper player 1 choice " << upperPlayer1Choice << ").");
uint64_t upperPlayer2Choice = maxStrategyPair.getPlayer2Strategy().getChoice(upperPlayer1Choice);
if (lowerPlayer2Choice != upperPlayer2Choice) {
ValueType lowerValueUnderUpperChoicePlayer2 = transitionMatrix.multiplyRowWithVector(upperPlayer2Choice, quantitativeResult.getMin().getValues());
if (upperPlayer1Choice != lowerPlayer1Choice && minStrategyPair.getPlayer2Strategy().hasDefinedChoice(upperPlayer1Choice)) {
hasMaxPlayer1Choice = true;
uint64_t lowerPlayer2Choice = minStrategyPair.getPlayer2Strategy().getChoice(upperPlayer1Choice);
ValueType lowerValueUnderLowerChoicePlayer2 = transitionMatrix.multiplyRowWithVector(lowerPlayer2Choice, quantitativeResult.getMin().getValues());
lowerValueUnderMaxChoicePlayer1 = lowerValueUnderLowerChoicePlayer2;
STORM_LOG_ASSERT(maxStrategyPair.getPlayer2Strategy().hasDefinedChoice(upperPlayer1Choice), "Expected upper player 2 choice for state " << state << " (upper player 1 choice " << upperPlayer1Choice << ").");
uint64_t upperPlayer2Choice = maxStrategyPair.getPlayer2Strategy().getChoice(upperPlayer1Choice);
if (redirectPlayer2 && lowerValueUnderUpperChoicePlayer2 <= lowerValueUnderLowerChoicePlayer2) {
minStrategyPair.getPlayer2Strategy().setChoice(upperPlayer1Choice, upperPlayer2Choice);
if (lowerPlayer2Choice != upperPlayer2Choice) {
ValueType lowerValueUnderUpperChoicePlayer2 = transitionMatrix.multiplyRowWithVector(upperPlayer2Choice, quantitativeResult.getMin().getValues());
if (redirectPlayer2 && lowerValueUnderUpperChoicePlayer2 <= lowerValueUnderLowerChoicePlayer2) {
minStrategyPair.getPlayer2Strategy().setChoice(upperPlayer1Choice, upperPlayer2Choice);
}
}
}
}
}
if (redirectPlayer1 && player1Direction == storm::OptimizationDirection::Minimize) {
if (hasMinPlayer1Choice && hasMaxPlayer1Choice && lowerPlayer1Choice != upperPlayer1Choice) {
if (lowerValueUnderMaxChoicePlayer1 <= lowerValueUnderMinChoicePlayer1) {
minStrategyPair.getPlayer1Strategy().setChoice(state, upperPlayer1Choice);
if (redirectPlayer1 && player1Direction == storm::OptimizationDirection::Minimize) {
if (hasMinPlayer1Choice && hasMaxPlayer1Choice && lowerPlayer1Choice != upperPlayer1Choice) {
if (lowerValueUnderMaxChoicePlayer1 <= lowerValueUnderMinChoicePlayer1) {
minStrategyPair.getPlayer1Strategy().setChoice(state, upperPlayer1Choice);
}
}
}
}
}
// ExplicitGameExporter<ValueType> exporter;
// exporter.exportToJson("game" + std::to_string(iteration) + ".json", player1Groups, player2Groups, transitionMatrix, initialStates, constraintStates, targetStates, quantitativeResult, &minStrategyPair, &maxStrategyPair);
// exit(-1);
if (sanityCheck) {
storm::utility::ConstantsComparator<ValueType> sanityComparator( 1e-6, true);
@ -1196,44 +1137,6 @@ namespace storm {
}
STORM_LOG_TRACE("Got maximal deviation of " << maxDiff << ".");
STORM_LOG_WARN_COND(sanityComparator.isZero(maxDiff), "Deviation " << maxDiff << " between computed value (" << quantitativeResult.getMin().getValues()[maxState] << ") and sanity check value (" << sanityValues[maxState] << ") in state " << maxState << " appears to be too high. (Obtained bounds were [" << quantitativeResult.getMin().getValues()[maxState] << ", " << quantitativeResult.getMax().getValues()[maxState] << "].)");
if (!sanityComparator.isZero(maxDiff)) {
ExplicitGameExporter<ValueType> exporter;
storm::storage::BitVector newInitialStates(player1Groups.size() - 1);
newInitialStates.set(maxState);
exporter.exportToJson("game" + std::to_string(iteration) + "_min.json", player1Groups, player2Groups, transitionMatrix, newInitialStates, constraintStates, targetStates, quantitativeResult, &minStrategyPair, static_cast<ExplicitGameStrategyPair const*>(nullptr));
exporter.exportToJson("game" + std::to_string(iteration) + "_max.json", player1Groups, player2Groups, transitionMatrix, newInitialStates, constraintStates, targetStates, quantitativeResult, static_cast<ExplicitGameStrategyPair const*>(nullptr), &maxStrategyPair);
// Perform DFS from max diff state in upper system.
std::vector<uint64_t> stack;
stack.push_back(maxState);
storm::storage::BitVector reachable(dtmcMatrix.getRowCount());
while (!stack.empty()) {
uint64_t currentState = stack.back();
stack.pop_back();
std::cout << "exploring player 1 state " << currentState << " with " << (player1Groups[currentState + 1] - player1Groups[currentState]) << " player 2 successors from" << player1Groups[currentState] << " to " << player1Groups[currentState + 1] << std::endl;
uint64_t player2State = minStrategyPair.getPlayer1Strategy().getChoice(currentState);
std::cout << "going to player 2 state " << player2State << " with " << (player2Groups[player2State + 1] - player2Groups[player2State]) << " player 2 choices from " << player2Groups[player2State] << " to " << player2Groups[player2State + 1] << std::endl;
uint64_t player2Choice = minStrategyPair.getPlayer2Strategy().getChoice(player2State);
std::cout << "which takes choice " << player2Choice << " which locally is " << (player2Choice - transitionMatrix.getRowGroupIndices()[player2State]) << std::endl;
for (auto const& entry : transitionMatrix.getRow(player2Choice)) {
std::cout << entry.getColumn() << " -> " << entry.getValue() << std::endl;
auto successor = entry.getColumn();
if (!reachable.get(successor)) {
if (!targetStates.get(successor)) {
reachable.set(successor);
stack.push_back(successor);
} else {
std::cout << "found target state " << std::endl;
}
}
}
}
exit(-1);
}
///////// SANITY CHECK: apply upper strategy, obtain DTMC matrix and model check it. the values should
///////// still be the upper ones.
@ -1248,10 +1151,6 @@ namespace storm {
for (auto const& entry : transitionMatrix.getRow(player2Choice)) {
dtmcMatrixBuilder.addNextValue(state, entry.getColumn(), entry.getValue());
if (state == 25305) {
std::cout << "entry " << entry.getColumn() << " -> " << entry.getValue() << std::endl;
std::cout << "values [" << quantitativeResult.getMin().getValues()[entry.getColumn()] << ", " << quantitativeResult.getMax().getValues()[entry.getColumn()] << "]" << std::endl;
}
}
}
}
@ -1266,58 +1165,9 @@ namespace storm {
maxState = state;
maxDiff = diff;
}
if (dtmcMatrix.getRowCount() > 25305 && !targetStates.get(state)) {
uint64_t player2Choice = maxStrategyPair.getPlayer2Strategy().getChoice(maxStrategyPair.getPlayer1Strategy().getChoice(state));
for (auto const& entry : transitionMatrix.getRow(player2Choice)) {
if (state == 25305) {
std::cout << "entry " << entry.getColumn() << " -> " << entry.getValue() << std::endl;
std::cout << "sanity value " << sanityValues[entry.getColumn()] << std::endl;
}
}
}
}
STORM_LOG_TRACE("Got maximal deviation of " << maxDiff << ".");
STORM_LOG_WARN_COND(sanityComparator.isZero(maxDiff), "Deviation " << maxDiff << " between computed value (" << quantitativeResult.getMax().getValues()[maxState] << ") and sanity check value (" << sanityValues[maxState] << ") in state " << maxState << " appears to be too high. (Obtained bounds were [" << quantitativeResult.getMin().getValues()[maxState] << ", " << quantitativeResult.getMax().getValues()[maxState] << "].)");
if (!sanityComparator.isZero(maxDiff)) {
ExplicitGameExporter<ValueType> exporter;
storm::storage::BitVector newInitialStates(player1Groups.size() - 1);
newInitialStates.set(maxState);
exporter.exportToJson("game" + std::to_string(iteration) + "_min.json", player1Groups, player2Groups, transitionMatrix, newInitialStates, constraintStates, targetStates, quantitativeResult, &minStrategyPair, static_cast<ExplicitGameStrategyPair const*>(nullptr));
exporter.exportToJson("game" + std::to_string(iteration) + "_max.json", player1Groups, player2Groups, transitionMatrix, newInitialStates, constraintStates, targetStates, quantitativeResult, static_cast<ExplicitGameStrategyPair const*>(nullptr), &maxStrategyPair);
// Perform DFS from max diff state in upper system.
std::vector<uint64_t> stack;
stack.push_back(maxState);
storm::storage::BitVector reachable(dtmcMatrix.getRowCount());
while (!stack.empty()) {
uint64_t currentState = stack.back();
stack.pop_back();
std::cout << "exploring player 1 state " << currentState << " with " << (player1Groups[currentState + 1] - player1Groups[currentState]) << " player 2 successors from" << player1Groups[currentState] << " to " << player1Groups[currentState + 1] << std::endl;
uint64_t player2State = maxStrategyPair.getPlayer1Strategy().getChoice(currentState);
std::cout << "going to player 2 state " << player2State << " with " << (player2Groups[player2State + 1] - player2Groups[player2State]) << " player 2 choices from " << player2Groups[player2State] << " to " << player2Groups[player2State + 1] << std::endl;
uint64_t player2Choice = maxStrategyPair.getPlayer2Strategy().getChoice(player2State);
std::cout << "which takes choice " << player2Choice << " which locally is " << (player2Choice - transitionMatrix.getRowGroupIndices()[player2State]) << std::endl;
for (auto const& entry : transitionMatrix.getRow(player2Choice)) {
std::cout << entry.getColumn() << " -> " << entry.getValue() << std::endl;
auto successor = entry.getColumn();
if (!reachable.get(successor)) {
if (!targetStates.get(successor)) {
reachable.set(successor);
stack.push_back(successor);
} else {
std::cout << "found target state " << std::endl;
}
}
}
}
exit(-1);
}
}
}

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

@ -7,11 +7,13 @@
#include "storm/environment/solver/GameSolverEnvironment.h"
#include "storm/utility/graph.h"
#include "storm/utility/vector.h"
#include "storm/utility/macros.h"
#include "storm/exceptions/InvalidEnvironmentException.h"
#include "storm/exceptions/InvalidStateException.h"
#include "storm/exceptions/NotImplementedException.h"
namespace storm {
namespace solver {
@ -87,7 +89,7 @@ namespace storm {
localPlayer2Choices = std::make_unique<std::vector<uint64_t>>();
player2Choices = localPlayer2Choices.get();
}
if (this->hasSchedulerHints()) {
*player1Choices = this->player1ChoicesHint.get();
} else if (this->player1RepresentedByMatrix()) {
@ -95,7 +97,6 @@ namespace storm {
*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);
}
if (this->hasSchedulerHints()) {
@ -103,12 +104,12 @@ namespace storm {
} else if (!(providedPlayer1Choices && providedPlayer2Choices)) {
player2Choices->resize(this->player2Matrix.getRowGroupCount());
}
if (!auxiliaryP2RowGroupVector) {
auxiliaryP2RowGroupVector = std::make_unique<std::vector<ValueType>>(this->player2Matrix.getRowGroupCount());
}
if (!auxiliaryP1RowGroupVector) {
auxiliaryP1RowGroupVector = std::make_unique<std::vector<ValueType>>(this->player1Matrix->getRowGroupCount());
auxiliaryP1RowGroupVector = std::make_unique<std::vector<ValueType>>(this->player1RepresentedByMatrix() ? this->player1Matrix->getRowGroupCount() : this->player1Grouping->size() - 1);
}
std::vector<ValueType>& subB = *auxiliaryP1RowGroupVector;
@ -138,9 +139,29 @@ namespace storm {
// Solve the equation system induced by the two schedulers.
storm::storage::SparseMatrix<ValueType> submatrix;
getInducedMatrixVector(x, b, *player1Choices, *player2Choices, submatrix, subB);
storm::storage::BitVector targetStates;
storm::storage::BitVector zeroStates;
if (!this->hasUniqueSolution()) {
// If there is no unique solution, we need to compute the states with probability 0 and set their values explicitly.
targetStates = storm::utility::vector::filterGreaterZero(subB);
zeroStates = ~storm::utility::graph::performProbGreater0(submatrix.transpose(), storm::storage::BitVector(targetStates.size(), true), targetStates);
}
if (this->linearEquationSolverFactory->getEquationProblemFormat(environmentOfSolver) == LinearEquationSolverProblemFormat::EquationSystem) {
submatrix.convertToEquationSystem();
}
if (!this->hasUniqueSolution()) {
for (auto state : zeroStates) {
for (auto& element : submatrix.getRow(state)) {
if (element.getColumn() == state) {
element.setValue(storm::utility::one<ValueType>());
} else {
element.setValue(storm::utility::zero<ValueType>());
}
}
subB[state] = storm::utility::zero<ValueType>();
}
}
auto submatrixSolver = linearEquationSolverFactory->create(environmentOfSolver, std::move(submatrix));
if (this->lowerBound) {
submatrixSolver->setLowerBound(this->lowerBound.get());
@ -154,10 +175,8 @@ namespace storm {
Status status = Status::InProgress;
uint64_t iterations = 0;
do {
// Solve the equation system for the 'DTMC'.
// FIXME: we need to remove the 0- and 1- states to make the solution unique.
submatrixSolver->solveEquations(environmentOfSolver, x, subB);
bool schedulerImproved = extractChoices(player1Dir, player2Dir, x, b, *auxiliaryP2RowGroupVector, *player1Choices, *player2Choices);
// If the scheduler did not improve, we are done.
@ -166,7 +185,27 @@ namespace storm {
} else {
// Update the solver.
getInducedMatrixVector(x, b, *player1Choices, *player2Choices, submatrix, subB);
submatrix.convertToEquationSystem();
if (!this->hasUniqueSolution()) {
// If there is no unique solution, we need to compute the states with probability 0 and set their values explicitly.
targetStates = storm::utility::vector::filterGreaterZero(subB);
zeroStates = ~storm::utility::graph::performProbGreater0(submatrix.transpose(), storm::storage::BitVector(targetStates.size(), true), targetStates);
}
if (this->linearEquationSolverFactory->getEquationProblemFormat(environmentOfSolver) == LinearEquationSolverProblemFormat::EquationSystem) {
submatrix.convertToEquationSystem();
}
if (!this->hasUniqueSolution()) {
for (auto state : zeroStates) {
for (auto& element : submatrix.getRow(state)) {
if (element.getColumn() == state) {
element.setValue(storm::utility::one<ValueType>());
} else {
element.setValue(storm::utility::zero<ValueType>());
}
}
subB[state] = storm::utility::zero<ValueType>();
}
}
submatrixSolver->setMatrix(std::move(submatrix));
}
@ -360,6 +399,29 @@ namespace storm {
template<typename ValueType>
bool StandardGameSolver<ValueType>::extractChoices(OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector<ValueType> const& x, std::vector<ValueType> const& b, std::vector<ValueType>& player2ChoiceValues, std::vector<uint_fast64_t>& player1Choices, std::vector<uint_fast64_t>& player2Choices) const {
if (player1Dir == storm::OptimizationDirection::Minimize) {
if (player2Dir == storm::OptimizationDirection::Minimize) {
return extractChoices<storm::utility::ElementLess<ValueType>, storm::utility::ElementLess<ValueType>>(x, b, player2ChoiceValues, player1Choices, player2Choices);
} else {
return extractChoices<storm::utility::ElementLess<ValueType>, storm::utility::ElementGreater<ValueType>>(x, b, player2ChoiceValues, player1Choices, player2Choices);
}
} else {
if (player2Dir == storm::OptimizationDirection::Minimize) {
return extractChoices<storm::utility::ElementGreater<ValueType>, storm::utility::ElementLess<ValueType>>(x, b, player2ChoiceValues, player1Choices, player2Choices);
} else {
return extractChoices<storm::utility::ElementGreater<ValueType>, storm::utility::ElementGreater<ValueType>>(x, b, player2ChoiceValues, player1Choices, player2Choices);
}
}
return false;
}
template<typename ValueType>
template<typename ComparePlayer1, typename ComparePlayer2>
bool StandardGameSolver<ValueType>::extractChoices(std::vector<ValueType> const& x, std::vector<ValueType> const& b, std::vector<ValueType>& player2ChoiceValues, std::vector<uint_fast64_t>& player1Choices, std::vector<uint_fast64_t>& player2Choices) const {
ComparePlayer1 comparePlayer1;
ComparePlayer2 comparePlayer2;
// get the choices of player 2 and the corresponding values.
bool schedulerImproved = false;
@ -387,7 +449,7 @@ namespace storm {
}
choiceValue += b[firstRowInGroup + p2Choice];
if (valueImproved(player2Dir, *currentValueIt, choiceValue)) {
if (comparePlayer2(choiceValue, *currentValueIt)) {
schedulerImproved = true;
player2Choices[p2Group] = p2Choice;
*currentValueIt = std::move(choiceValue);
@ -409,7 +471,7 @@ namespace storm {
continue;
}
ValueType const& choiceValue = player2ChoiceValues[this->getPlayer1Matrix().getRow(firstRowInGroup + p1Choice).begin()->getColumn()];
if (valueImproved(player1Dir, currentValue, choiceValue)) {
if (comparePlayer1(choiceValue, currentValue)) {
schedulerImproved = true;
player1Choices[p1Group] = p1Choice;
currentValue = choiceValue;
@ -429,7 +491,7 @@ namespace storm {
}
ValueType const& choiceValue = player2ChoiceValues[this->getPlayer1Grouping()[player1State] + player2State];
if (valueImproved(player1Dir, currentValue, choiceValue)) {
if (comparePlayer1(choiceValue, currentValue)) {
schedulerImproved = true;
player1Choices[player1State] = player2State;
currentValue = choiceValue;
@ -461,7 +523,7 @@ namespace storm {
// 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];
uint64_t player2State = this->getPlayer1Grouping()[player1State] + player1Choices[player1State];
selectedRows.emplace_back(player2Matrix.getRowGroupIndices()[player2State] + player2Choices[player2State]);
}
}

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

@ -39,7 +39,9 @@ namespace storm {
// Extracts the choices of the different players for the given solution x.
// Returns true iff the newly extracted choices yield "better" values then the given choices for one of the players.
bool extractChoices(OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector<ValueType> const& x, std::vector<ValueType> const& b, std::vector<ValueType>& player2ChoiceValues, std::vector<uint_fast64_t>& player1Choices, std::vector<uint_fast64_t>& player2Choices) const;
template<typename ComparePlayer1, typename ComparePlayer2>
bool extractChoices(std::vector<ValueType> const& x, std::vector<ValueType> const& b, std::vector<ValueType>& player2ChoiceValues, std::vector<uint_fast64_t>& player1Choices, std::vector<uint_fast64_t>& player2Choices) const;
bool valueImproved(OptimizationDirection dir, ValueType const& value1, ValueType const& value2) const;
bool player1RepresentedByMatrix() const;

12
src/storm/storage/SparseMatrix.cpp
View File

@ -1630,11 +1630,6 @@ namespace storm {
currentValue += elementIt->getValue() * vector[elementIt->getColumn()];
}
if (std::distance(result.begin(), resultIt) == 2240 || std::distance(result.begin(), resultIt) == 2241 || std::distance(result.begin(), resultIt) == 8262 || std::distance(result.begin(), resultIt) == 8263 || std::distance(result.begin(), resultIt) == 8266 || std::distance(result.begin(), resultIt) == 8267) {
std::cout << "got initial value " << currentValue << " for state " << std::distance(result.begin(), resultIt) << " in row " << currentRow << std::endl;
}
if (choices) {
selectedChoice = 0;
if (*choiceIt == 0) {
@ -1651,10 +1646,6 @@ namespace storm {
newValue += elementIt->getValue() * vector[elementIt->getColumn()];
}
if (std::distance(result.begin(), resultIt) == 2240 || std::distance(result.begin(), resultIt) == 2241 || std::distance(result.begin(), resultIt) == 8262 || std::distance(result.begin(), resultIt) == 8263 || std::distance(result.begin(), resultIt) == 8266 || std::distance(result.begin(), resultIt) == 8267) {
std::cout << "got value " << currentValue << " for state " << std::distance(result.begin(), resultIt) << " in row " << currentRow << std::endl;
}
if (choices && currentRow == *choiceIt + *rowGroupIt) {
oldSelectedChoiceValue = newValue;
}
@ -1673,9 +1664,6 @@ namespace storm {
// Finally write value to target vector.
*resultIt = currentValue;
if (choices && compare(currentValue, oldSelectedChoiceValue)) {
if (std::distance(result.begin(), resultIt) == 2240 || std::distance(result.begin(), resultIt) == 2241 || std::distance(result.begin(), resultIt) == 8262 || std::distance(result.begin(), resultIt) == 8263 || std::distance(result.begin(), resultIt) == 8266 || std::distance(result.begin(), resultIt) == 8267) {
std::cout << "changing choice in " << std::distance(result.begin(), resultIt) << " from " << *choiceIt << " to " << selectedChoice << " because " << currentValue << " is better than " << oldSelectedChoiceValue << std::endl;
}
*choiceIt = selectedChoice;
}
}

12
src/storm/utility/constants.cpp
View File

@ -45,6 +45,16 @@ namespace storm {
return a == zero<ValueType>();
}
template<typename ValueType>
bool isNan(ValueType const& value) {
return false;
}
template<>
bool isNan(double const& value) {
return isnan(value);
}
bool isAlmostZero(double const& a) {
return a < 1e-12 && a > -1e-12;
}
@ -950,6 +960,7 @@ namespace storm {
template bool isZero(NumberTraits<storm::ClnRationalNumber>::IntegerType const& value);
template bool isConstant(storm::ClnRationalNumber const& value);
template bool isInfinity(storm::ClnRationalNumber const& value);
template bool isNan(storm::ClnRationalNumber const& value);
template storm::NumberTraits<ClnRationalNumber>::IntegerType convertNumber(storm::NumberTraits<ClnRationalNumber>::IntegerType const& number);
template storm::ClnRationalNumber convertNumber(storm::ClnRationalNumber const& number);
template storm::ClnRationalNumber simplify(storm::ClnRationalNumber value);
@ -974,6 +985,7 @@ namespace storm {
template bool isZero(NumberTraits<storm::GmpRationalNumber>::IntegerType const& value);
template bool isConstant(storm::GmpRationalNumber const& value);
template bool isInfinity(storm::GmpRationalNumber const& value);
template bool isNan(storm::GmpRationalNumber const& value);
template storm::NumberTraits<GmpRationalNumber>::IntegerType convertNumber(storm::NumberTraits<GmpRationalNumber>::IntegerType const& number);
template storm::GmpRationalNumber convertNumber(storm::GmpRationalNumber const& number);
template storm::GmpRationalNumber simplify(storm::GmpRationalNumber value);

7
src/storm/utility/constants.h
View File

@ -38,7 +38,7 @@ namespace storm {
struct DoubleLess {
bool operator()(double a, double b) const {
return b - a > 1e-17;
return (a == 0.0 && b > 0.0) || (b - a > 1e-17);
}
};
@ -54,7 +54,7 @@ namespace storm {
struct DoubleGreater {
bool operator()(double a, double b) const {
return a - b > 1e-17;
return (b == 0.0 && a > 0.0) || (a - b > 1e-17);
}
};
@ -84,6 +84,9 @@ namespace storm {
template<typename ValueType>
bool isZero(ValueType const& a);
template<typename ValueType>
bool isNan(ValueType const& a);
bool isAlmostZero(double const& a);

5
src/storm/utility/vector.h
View File

@ -725,10 +725,6 @@ namespace storm {
}
if (choices && f(*targetIt, oldSelectedChoiceValue)) {
uint64_t distance = std::distance(target.begin(), targetIt);
if (distance == 1693 || distance == 4715 || distance == 4713) {
std::cout << std::setprecision(50) << "improving value at " << distance << ": moving from " << *choiceIt << " to " << selectedChoice << " because " << *targetIt << " is better than " << oldSelectedChoiceValue << std::endl;
}
*choiceIt = selectedChoice;
}
} else {
@ -796,7 +792,6 @@ namespace storm {
*/
template<class T>
void reduceVectorMinOrMax(storm::solver::OptimizationDirection dir, std::vector<T> const& source, std::vector<T>& target, std::vector<uint_fast64_t> const& rowGrouping, std::vector<uint_fast64_t>* choices = nullptr) {
std::cout << "[" << dir << "]: reducing vector " << std::endl;
if (dir == storm::solver::OptimizationDirection::Minimize) {
reduceVectorMin(source, target, rowGrouping, choices);
} else {

Write Preview
Loading…
Cancel
Save