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

fixed some issues in qualitative sparse solution of game-based abstraction

main
dehnert 7 years ago
parent
9665f4fa30
commit
3f6a8fed92
3 changed files with 31 additions and 28 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 17
      src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
  2. 34
      src/storm/utility/graph.cpp
  3. 8
      src/storm/utility/graph.h

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

@ -534,15 +534,18 @@ namespace storm {
std::vector<uint64_t> player1RowGrouping = transitionMatrix.swapRowGroupIndices(std::move(tmpPlayer2RowGrouping));
auto const& player2RowGrouping = transitionMatrix.getRowGroupIndices();
// Create the backward transitions for both players.
// Create the player 1 groups and backward transitions (for both players).
std::vector<uint64_t> player1Groups(player1RowGrouping.size());
storm::storage::SparseMatrix<ValueType> player1BackwardTransitions = transitionMatrix.transpose(true);
std::vector<uint64_t> player2BackwardTransitions(transitionMatrix.getRowGroupCount());
uint64_t player2State = 0;
for (uint64_t player1State = 0; player1State < player2RowGrouping.size() - 1; ++player1State) {
while (player1RowGrouping[player1State + 1] > player2RowGrouping[player2State]) {
player2BackwardTransitions[player2State] = player1State;
++player2State;
}
player1Groups[player1State + 1] = player2State;
}
storm::storage::BitVector initialStates = initialStatesBdd.toVector(odd);
@ -551,7 +554,7 @@ namespace storm {
// (1) compute all states with probability 0/1 wrt. to the two different player 2 goals (min/max).
auto qualitativeStart = std::chrono::high_resolution_clock::now();
ExplicitQualitativeGameResultMinMax qualitativeResult = computeProb01States(previousQualitativeResult, player1Direction, transitionMatrix, player1RowGrouping, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates);
ExplicitQualitativeGameResultMinMax qualitativeResult = computeProb01States(previousQualitativeResult, player1Direction, transitionMatrix, player1Groups, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates);
// std::unique_ptr<CheckResult> result = checkForResultAfterQualitativeCheck<Type, ValueType>(checkTask, initialStates, qualitativeResult);
// if (result) {
// return result;
@ -627,7 +630,7 @@ namespace storm {
}
template<storm::dd::DdType Type, typename ModelType>
ExplicitQualitativeGameResultMinMax GameBasedMdpModelChecker<Type, ModelType>::computeProb01States(boost::optional<ExplicitQualitativeGameResultMinMax> const& previousQualitativeResult, storm::OptimizationDirection player1Direction, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& player1RowGrouping, storm::storage::SparseMatrix<ValueType> const& player1BackwardTransitions, std::vector<uint64_t> const& player2BackwardTransitions, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates) {
ExplicitQualitativeGameResultMinMax GameBasedMdpModelChecker<Type, ModelType>::computeProb01States(boost::optional<ExplicitQualitativeGameResultMinMax> const& previousQualitativeResult, storm::OptimizationDirection player1Direction, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& player1Groups, storm::storage::SparseMatrix<ValueType> const& player1BackwardTransitions, std::vector<uint64_t> const& player2BackwardTransitions, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates) {
ExplicitQualitativeGameResultMinMax result;
@ -676,10 +679,10 @@ namespace storm {
// result.prob1Min = storm::utility::graph::performProb1(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, true, true, boost::make_optional(prob1MaxMaxMdp));
// }
// } else {
result.prob0Min = storm::utility::graph::performProb0(transitionMatrix, player1RowGrouping, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, true, true);
result.prob1Min = storm::utility::graph::performProb1(transitionMatrix, player1RowGrouping, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, true, true);
result.prob0Max = storm::utility::graph::performProb0(transitionMatrix, player1RowGrouping, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Maximize, true, true);
result.prob1Max = storm::utility::graph::performProb1(transitionMatrix, player1RowGrouping, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Maximize, true, true);
result.prob0Min = storm::utility::graph::performProb0(transitionMatrix, player1Groups, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, true, true);
result.prob1Min = storm::utility::graph::performProb1(transitionMatrix, player1Groups, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, true, true);
result.prob0Max = storm::utility::graph::performProb0(transitionMatrix, player1Groups, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Maximize, true, true);
result.prob1Max = storm::utility::graph::performProb1(transitionMatrix, player1Groups, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Maximize, true, true);
// }
STORM_LOG_TRACE("Qualitative precomputation completed.");

34
src/storm/utility/graph.cpp
View File

@ -1084,7 +1084,7 @@ namespace storm {
}
template <typename ValueType>
ExplicitGameProb01Result performProb0(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& player1RowGrouping, storm::storage::SparseMatrix<ValueType> const& player1BackwardTransitions, std::vector<uint64_t> const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy) {
ExplicitGameProb01Result performProb0(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& player1Groups, storm::storage::SparseMatrix<ValueType> const& player1BackwardTransitions, std::vector<uint64_t> const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy) {
ExplicitGameProb01Result result(psiStates, storm::storage::BitVector(transitionMatrix.getRowGroupCount()));
@ -1134,7 +1134,7 @@ namespace storm {
bool addPlayer1State = false;
if (player1Strategy == OptimizationDirection::Minimize) {
bool allPlayer2Successors = true;
for (uint64_t player2State = player1RowGrouping[player1Predecessor]; player2State < player1RowGrouping[player1Predecessor + 1]; ++player2State) {
for (uint64_t player2State = player1Groups[player1Predecessor]; player2State < player1Groups[player1Predecessor + 1]; ++player2State) {
if (!result.player2States.get(player2State)) {
allPlayer2Successors = false;
break;
@ -1170,18 +1170,18 @@ namespace storm {
// At least one player 2 successor is a state with probability 0, find it.
bool foundProb0Successor = false;
uint64_t player2State;
for (player2State = player1RowGrouping[player1State]; player2State < player1RowGrouping[player1State + 1]; ++player2State) {
for (player2State = player1Groups[player1State]; player2State < player1Groups[player1State + 1]; ++player2State) {
if (result.player2States.get(player2State)) {
result.player1Strategy.get()[player1State] = player2State - player1RowGrouping[player1State];
result.player1Strategy.get()[player1State] = player2State;
foundProb0Successor = true;
break;
}
}
STORM_LOG_ASSERT(foundProb0Successor, "Expected at least one state 2 successor with probability 0.");
result.player1Strategy.get()[player1State] = player2State - player1RowGrouping[player1State];
result.player1Strategy.get()[player1State] = player2State;
} else {
// Since all player 2 successors are states with probability 0, just pick any.
result.player1Strategy.get()[player1State] = 0;
result.player1Strategy.get()[player1State] = player1Groups[player1State];
}
}
}
@ -1211,10 +1211,10 @@ namespace storm {
}
STORM_LOG_ASSERT(foundProb0SuccessorDistribution, "Expected at least one distribution with only successors with probability 0.");
result.player2Strategy.get()[player2State] = row - transitionMatrix.getRowGroupIndices()[player2State];
result.player2Strategy.get()[player2State] = row;
} else {
// Since all player 1 successors are states with probability 0, just pick any.
result.player2Strategy.get()[player2State] = 0;
result.player2Strategy.get()[player2State] = transitionMatrix.getRowGroupIndices()[player2State];
}
}
}
@ -1290,8 +1290,8 @@ namespace storm {
}
template <typename ValueType>
ExplicitGameProb01Result performProb1(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& player1RowGrouping, storm::storage::SparseMatrix<ValueType> const& player1BackwardTransitions, std::vector<uint64_t> const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy, boost::optional<storm::storage::BitVector> const& player1Candidates) {
ExplicitGameProb01Result performProb1(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& player1Groups, storm::storage::SparseMatrix<ValueType> const& player1BackwardTransitions, std::vector<uint64_t> const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy, boost::optional<storm::storage::BitVector> const& player1Candidates) {
// During the execution, the two state sets in the result hold the potential player 1/2 states.
ExplicitGameProb01Result result;
if (player1Candidates) {
@ -1335,8 +1335,8 @@ namespace storm {
if (!player2Solution.get(player2PredecessorEntry.getColumn())) {
bool addPlayer2State = player2Strategy == storm::OptimizationDirection::Minimize ? true : false;
uint64_t validChoice = 0;
for (uint64_t row = transitionMatrix.getRowGroupIndices()[player2Predecessor]; row < transitionMatrix.getRowGroupIndices()[player2Predecessor + 1]; ++row) {
uint64_t validChoice = transitionMatrix.getRowGroupIndices()[player2Predecessor];
for (uint64_t row = validChoice; row < transitionMatrix.getRowGroupIndices()[player2Predecessor + 1]; ++row) {
bool choiceHasSolutionSuccessor = false;
bool choiceStaysInMaybeStates = true;
for (auto const& entry : transitionMatrix.getRow(row)) {
@ -1351,7 +1351,7 @@ namespace storm {
if (choiceHasSolutionSuccessor && choiceStaysInMaybeStates) {
if (player2Strategy == storm::OptimizationDirection::Maximize) {
validChoice = row - transitionMatrix.getRowGroupIndices()[player2Predecessor];
validChoice = row;
addPlayer2State = true;
break;
}
@ -1374,11 +1374,11 @@ namespace storm {
if (!player1Solution.get(player1Predecessor)) {
bool addPlayer1State = player1Strategy == storm::OptimizationDirection::Minimize ? true : false;
validChoice = 0;
for (uint64_t player2Successor = player1RowGrouping[player1Predecessor]; player2Successor < player1RowGrouping[player1Predecessor + 1]; ++player2Successor) {
validChoice = player1Groups[player1Predecessor];
for (uint64_t player2Successor = validChoice; player2Successor < player1Groups[player1Predecessor + 1]; ++player2Successor) {
if (player2Solution.get(player2Successor)) {
if (player1Strategy == storm::OptimizationDirection::Maximize) {
validChoice = player2Successor - player1RowGrouping[player1Predecessor];
validChoice = player2Successor;
addPlayer1State = true;
break;
}
@ -1395,7 +1395,7 @@ namespace storm {
result.player1Strategy.get()[player1Predecessor] = validChoice;
}
stack.emplace_back();
stack.emplace_back(player1Predecessor);
}
}
}

8
src/storm/utility/graph.h
View File

@ -667,7 +667,7 @@ namespace storm {
* Computes the set of states that have probability 0 given the strategies of the two players.
*
* @param transitionMatrix The transition matrix of the model as a BDD.
* @param player1RowGrouping The row grouping of player 1 states.
* @param player1Groups The grouping of player 1 states (in terms of player 2 states).
* @param player1BackwardTransitions The backward transitions (player 1 to player 2).
* @param player2BackwardTransitions The backward transitions (player 2 to player 1).
* @param phiStates The phi states of the model.
@ -676,13 +676,13 @@ namespace storm {
* @param producePlayer2Strategy A flag indicating whether the strategy of player 2 shall be produced.
*/
template <typename ValueType>
ExplicitGameProb01Result performProb0(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& player1RowGrouping, storm::storage::SparseMatrix<ValueType> const& player1BackwardTransitions, std::vector<uint64_t> const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy = false, bool producePlayer2Strategy = false);
ExplicitGameProb01Result performProb0(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& player1Groups, storm::storage::SparseMatrix<ValueType> const& player1BackwardTransitions, std::vector<uint64_t> const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy = false, bool producePlayer2Strategy = false);
/*!
* Computes the set of states that have probability 1 given the strategies of the two players.
*
* @param transitionMatrix The transition matrix of the model as a BDD.
* @param player1RowGrouping The row grouping of player 1 states.
* @param player1Groups The grouping of player 1 states (in terms of player 2 states).
* @param player1BackwardTransitions The backward transitions (player 1 to player 2).
* @param player2BackwardTransitions The backward transitions (player 2 to player 1).
* @param phiStates The phi states of the model.
@ -692,7 +692,7 @@ namespace storm {
* @param player1Candidates If given, this set constrains the candidates of player 1 states that are considered.
*/
template <typename ValueType>
ExplicitGameProb01Result performProb1(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& player1RowGrouping, storm::storage::SparseMatrix<ValueType> const& player1BackwardTransitions, std::vector<uint64_t> const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy = false, bool producePlayer2Strategy = false, boost::optional<storm::storage::BitVector> const& player1Candidates = boost::none);
ExplicitGameProb01Result performProb1(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& player1Groups, storm::storage::SparseMatrix<ValueType> const& player1BackwardTransitions, std::vector<uint64_t> const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy = false, bool producePlayer2Strategy = false, boost::optional<storm::storage::BitVector> const& player1Candidates = boost::none);
/*!
* Performs a topological sort of the states of the system according to the given transitions.

Write Preview
Loading…
Cancel
Save