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

commit to switch workplace, debugging in progress 

Former-commit-id: 9ab5d903e9
main
dehnert 9 years ago
parent
673c329311
commit
059f55eefc
4 changed files with 47 additions and 9 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 2
      src/abstraction/AbstractionInformation.cpp
  2. 38
      src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
  3. 8
      src/solver/SymbolicGameSolver.cpp
  4. 4
      src/utility/graph.cpp

2
src/abstraction/AbstractionInformation.cpp
View File

@ -283,7 +283,7 @@ namespace storm {
std::map<storm::expressions::Expression, storm::dd::Bdd<DdType>> result; std::map<storm::expressions::Expression, storm::dd::Bdd<DdType>> result;
for (uint_fast64_t index = 0; index < predicates.size(); ++index) { for (uint_fast64_t index = 0; index < predicates.size(); ++index) {
result[predicates[index]] = predicateBdds[index].first;
result[predicates[index]] = predicateBdds[index].first && !bottomStateBdds.first;
} }
return result; return result;

38
src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
View File

@ -335,7 +335,7 @@ namespace storm {
// //
// minResult.exportToDot("minresult.dot"); // minResult.exportToDot("minresult.dot");
// maxResult.exportToDot("maxresult.dot"); // maxResult.exportToDot("maxresult.dot");
// pivotState.template toAdd<ValueType>().exportToDot("pivot.dot");
pivotState.template toAdd<ValueType>().exportToDot("pivot.dot");
// pivotStateLower.exportToDot("pivot_lower.dot"); // pivotStateLower.exportToDot("pivot_lower.dot");
// pivotStateUpper.exportToDot("pivot_upper.dot"); // pivotStateUpper.exportToDot("pivot_upper.dot");
// pivotStateIsMinProb0.template toAdd<ValueType>().exportToDot("pivot_is_minprob0.dot"); // pivotStateIsMinProb0.template toAdd<ValueType>().exportToDot("pivot_is_minprob0.dot");
@ -361,9 +361,9 @@ namespace storm {
// lowerChoice2.template toAdd<ValueType>().exportToDot("tmp_lower.dot"); // lowerChoice2.template toAdd<ValueType>().exportToDot("tmp_lower.dot");
// lowerChoice2 = lowerChoice2.existsAbstract(variablesToAbstract); // lowerChoice2 = lowerChoice2.existsAbstract(variablesToAbstract);
// lowerChoice.template toAdd<ValueType>().exportToDot("ref_lower.dot");
// lowerChoice1.template toAdd<ValueType>().exportToDot("ref_lower1.dot");
// lowerChoice2.template toAdd<ValueType>().exportToDot("ref_lower2.dot");
lowerChoice.template toAdd<ValueType>().exportToDot("ref_lower.dot");
lowerChoice1.template toAdd<ValueType>().exportToDot("ref_lower1.dot");
lowerChoice2.template toAdd<ValueType>().exportToDot("ref_lower2.dot");
bool lowerChoicesDifferent = !lowerChoice1.exclusiveOr(lowerChoice2).isZero(); bool lowerChoicesDifferent = !lowerChoice1.exclusiveOr(lowerChoice2).isZero();
if (lowerChoicesDifferent) { if (lowerChoicesDifferent) {
@ -478,6 +478,9 @@ namespace storm {
if (result) { if (result) {
return result; return result;
} }
if (iterations == 18) {
exit(-1);
}
prob01.max = computeProb01States(player1Direction, storm::OptimizationDirection::Maximize, game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates); prob01.max = computeProb01States(player1Direction, storm::OptimizationDirection::Maximize, game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates);
result = checkForResultAfterQualitativeCheck<Type, ValueType>(checkTask, storm::OptimizationDirection::Maximize, game.getInitialStates(), prob01.max.first.getPlayer1States(), prob01.max.second.getPlayer1States()); result = checkForResultAfterQualitativeCheck<Type, ValueType>(checkTask, storm::OptimizationDirection::Maximize, game.getInitialStates(), prob01.max.first.getPlayer1States(), prob01.max.second.getPlayer1States());
if (result) { if (result) {
@ -529,8 +532,6 @@ namespace storm {
minMaybeStateResult = solveMaybeStates(player1Direction, storm::OptimizationDirection::Minimize, game, maybeMin, prob01.min.second.getPlayer1States()); minMaybeStateResult = solveMaybeStates(player1Direction, storm::OptimizationDirection::Minimize, game, maybeMin, prob01.min.second.getPlayer1States());
minResult += minMaybeStateResult.values; minResult += minMaybeStateResult.values;
storm::dd::Add<Type, ValueType> initialStateMin = initialStatesAdd * minResult; storm::dd::Add<Type, ValueType> initialStateMin = initialStatesAdd * minResult;
initialStatesAdd.exportToDot("init.dot");
initialStateMin.exportToDot("initmin.dot");
// Here we can only require a non-zero count of *at most* one, because the result may actually be 0. // Here we can only require a non-zero count of *at most* one, because the result may actually be 0.
STORM_LOG_ASSERT(initialStateMin.getNonZeroCount() <= 1, "Wrong number of results for initial states. Expected <= 1, but got " << initialStateMin.getNonZeroCount() << "."); STORM_LOG_ASSERT(initialStateMin.getNonZeroCount() <= 1, "Wrong number of results for initial states. Expected <= 1, but got " << initialStateMin.getNonZeroCount() << ".");
minValue = initialStateMin.getMax(); minValue = initialStateMin.getMax();
@ -576,10 +577,35 @@ namespace storm {
// Start by extending the quantitative strategies by the qualitative ones. // Start by extending the quantitative strategies by the qualitative ones.
minMaybeStateResult.player1Strategy |= prob01.min.first.getPlayer1Strategy() || prob01.min.second.getPlayer1Strategy(); minMaybeStateResult.player1Strategy |= prob01.min.first.getPlayer1Strategy() || prob01.min.second.getPlayer1Strategy();
storm::dd::Bdd<Type> tmp = (prob01.min.first.getPlayer2Strategy().existsAbstract(game.getPlayer2Variables()) && prob01.min.second.getPlayer2Strategy().existsAbstract(game.getPlayer2Variables()));
STORM_LOG_ASSERT(tmp.isZero(), "wth?");
tmp = prob01.min.first.getPlayer2Strategy().existsAbstract(game.getPlayer2Variables()) && minMaybeStateResult.player2Strategy.existsAbstract(game.getPlayer2Variables());
if (!tmp.isZero()) {
tmp = tmp && prob01.min.first.getPlayer2Strategy().exclusiveOr(minMaybeStateResult.player2Strategy).existsAbstract(game.getPlayer2Variables());
(tmp && prob01.min.first.getPlayer2Strategy()).template toAdd<ValueType>().exportToDot("prob0_strat.dot");
(tmp && minMaybeStateResult.player2Strategy).template toAdd<ValueType>().exportToDot("maybe_strat.dot");
if (!tmp.isZero()) {
storm::dd::Add<Type, ValueType> values = (tmp.template toAdd<ValueType>() * game.getTransitionMatrix() * minResult.swapVariables(game.getRowColumnMetaVariablePairs())).sumAbstract(game.getColumnVariables());
tmp.template toAdd<ValueType>().exportToDot("illegal.dot");
minResult.exportToDot("vals.dot");
}
STORM_LOG_ASSERT(tmp.isZero(), "ddduuuudde?");
}
STORM_LOG_ASSERT(tmp.isZero(), "wth2?");
tmp = prob01.min.second.getPlayer2Strategy().existsAbstract(game.getPlayer2Variables()) && minMaybeStateResult.player2Strategy;
(minMaybeStateResult.player2Strategy && (prob01.min.first.getPlayer2Strategy() || prob01.min.second.getPlayer2Strategy())).template toAdd<ValueType>().exportToDot("strat_overlap.dot");
minMaybeStateResult.player2Strategy |= prob01.min.first.getPlayer2Strategy() || prob01.min.second.getPlayer2Strategy(); minMaybeStateResult.player2Strategy |= prob01.min.first.getPlayer2Strategy() || prob01.min.second.getPlayer2Strategy();
maxMaybeStateResult.player1Strategy |= prob01.max.first.getPlayer1Strategy() || prob01.max.second.getPlayer1Strategy(); maxMaybeStateResult.player1Strategy |= prob01.max.first.getPlayer1Strategy() || prob01.max.second.getPlayer1Strategy();
maxMaybeStateResult.player2Strategy |= prob01.max.first.getPlayer2Strategy() || prob01.max.second.getPlayer2Strategy(); maxMaybeStateResult.player2Strategy |= prob01.max.first.getPlayer2Strategy() || prob01.max.second.getPlayer2Strategy();
// Make sure that all strategies are still valid strategies.
STORM_LOG_ASSERT(minMaybeStateResult.player1Strategy.template toAdd<ValueType>().sumAbstract(game.getPlayer1Variables()).getMax() <= 1, "Player 1 strategy for min is illegal.");
STORM_LOG_ASSERT(maxMaybeStateResult.player1Strategy.template toAdd<ValueType>().sumAbstract(game.getPlayer1Variables()).getMax() <= 1, "Player 1 strategy for max is illegal.");
STORM_LOG_ASSERT(minMaybeStateResult.player2Strategy.template toAdd<ValueType>().sumAbstract(game.getPlayer2Variables()).getMax() <= 1, "Player 2 strategy for min is illegal.");
STORM_LOG_ASSERT(maxMaybeStateResult.player2Strategy.template toAdd<ValueType>().sumAbstract(game.getPlayer2Variables()).getMax() <= 1, "Player 2 strategy for max is illegal.");
refineAfterQuantitativeCheck(abstractor, game, minResult, maxResult, prob01, std::make_pair(minMaybeStateResult.player1Strategy, minMaybeStateResult.player2Strategy), std::make_pair(maxMaybeStateResult.player1Strategy, maxMaybeStateResult.player2Strategy), transitionMatrixBdd); refineAfterQuantitativeCheck(abstractor, game, minResult, maxResult, prob01, std::make_pair(minMaybeStateResult.player1Strategy, minMaybeStateResult.player2Strategy), std::make_pair(maxMaybeStateResult.player1Strategy, maxMaybeStateResult.player2Strategy), transitionMatrixBdd);
} }
} }

8
src/solver/SymbolicGameSolver.cpp
View File

@ -53,11 +53,14 @@ namespace storm {
} }
} }
this->A.exportToDot("matrix.dot");
do { do {
// Compute tmp = A * x + b. // Compute tmp = A * x + b.
storm::dd::Add<Type, ValueType> xCopyAsColumn = xCopy.swapVariables(this->rowColumnMetaVariablePairs); storm::dd::Add<Type, ValueType> xCopyAsColumn = xCopy.swapVariables(this->rowColumnMetaVariablePairs);
storm::dd::Add<Type, ValueType> tmp = this->A.multiplyMatrix(xCopyAsColumn, this->columnMetaVariables); storm::dd::Add<Type, ValueType> tmp = this->A.multiplyMatrix(xCopyAsColumn, this->columnMetaVariables);
tmp += b; tmp += b;
tmp.exportToDot("tmp_pre_" + std::to_string(iterations) + ".dot");
// Now abstract from player 2 and player 1 variables. // Now abstract from player 2 and player 1 variables.
if (player2Goal == storm::OptimizationDirection::Maximize) { if (player2Goal == storm::OptimizationDirection::Maximize) {
@ -74,9 +77,11 @@ namespace storm {
} else { } else {
tmp = (tmp + illegalPlayer2Mask); tmp = (tmp + illegalPlayer2Mask);
storm::dd::Add<Type, ValueType> newValues = tmp.minAbstract(this->player2Variables); storm::dd::Add<Type, ValueType> newValues = tmp.minAbstract(this->player2Variables);
newValues.exportToDot("vals_iter_" + std::to_string(iterations) + ".dot");
if (generatePlayer2Strategy) { if (generatePlayer2Strategy) {
player2Strategy = tmp.minAbstractRepresentative(this->player2Variables); player2Strategy = tmp.minAbstractRepresentative(this->player2Variables);
player2Strategy.get().template toAdd<ValueType>().exportToDot("pl2_strat_iter_" + std::to_string(iterations) + ".dot");
} }
tmp = newValues; tmp = newValues;
@ -103,6 +108,8 @@ namespace storm {
tmp = newValues; tmp = newValues;
} }
tmp.exportToDot("pl1_vals_iter_" + std::to_string(iterations) + ".dot");
// Now check if the process already converged within our precision. // Now check if the process already converged within our precision.
converged = xCopy.equalModuloPrecision(tmp, precision, relative); converged = xCopy.equalModuloPrecision(tmp, precision, relative);
@ -113,6 +120,7 @@ namespace storm {
++iterations; ++iterations;
} while (!converged && iterations < maximalNumberOfIterations); } while (!converged && iterations < maximalNumberOfIterations);
STORM_LOG_TRACE("Numerically solving the game took " << iterations << " iterations.");
return xCopy; return xCopy;
} }

4
src/utility/graph.cpp
View File

@ -960,14 +960,18 @@ namespace storm {
} }
// Since we have determined the complements of the desired sets, we need to complement it now. // Since we have determined the complements of the desired sets, we need to complement it now.
player1States.template toAdd<ValueType>().exportToDot("not_pl1_prob0.dot");
(!player1States).template toAdd<ValueType>().exportToDot("pl1_negated_prob0.dot");
player1States = !player1States && model.getReachableStates(); player1States = !player1States && model.getReachableStates();
player2States = !player2States && model.getReachableStates(); player2States = !player2States && model.getReachableStates();
// Determine all transitions between prob0 states. // Determine all transitions between prob0 states.
storm::dd::Bdd<Type> transitionsBetweenProb0States = player2States && (transitionMatrix && player1States.swapVariables(model.getRowColumnMetaVariablePairs())); storm::dd::Bdd<Type> transitionsBetweenProb0States = player2States && (transitionMatrix && player1States.swapVariables(model.getRowColumnMetaVariablePairs()));
player1States.template toAdd<ValueType>().exportToDot("pl1_prob0.dot");
// Determine the distributions that have only successors that are prob0 states. // Determine the distributions that have only successors that are prob0 states.
storm::dd::Bdd<Type> onlyProb0Successors = (transitionsBetweenProb0States || model.getIllegalSuccessorMask()).universalAbstract(model.getColumnVariables()); storm::dd::Bdd<Type> onlyProb0Successors = (transitionsBetweenProb0States || model.getIllegalSuccessorMask()).universalAbstract(model.getColumnVariables());
onlyProb0Successors.template toAdd<ValueType>().exportToDot("only_prob0.dot");
boost::optional<storm::dd::Bdd<Type>> player2StrategyBdd; boost::optional<storm::dd::Bdd<Type>> player2StrategyBdd;
if (producePlayer2Strategy) { if (producePlayer2Strategy) {

Write Preview
Loading…
Cancel
Save