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

Re-applied all necessary fixes. Things that work: Some DTMCs, emptyset MDPs. 

Former-commit-id: 0f782fdf61
tempestpy_adaptions
PBerger 8 years ago
parent
dc1aea83ed
commit
4b95f72a0a
1 changed files with 37 additions and 3 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. 38
      src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp

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

@ -218,7 +218,7 @@ namespace storm {
minPlayer1Strategy = (maxPlayer1Strategy && prob01.min.first.getPlayer2States()).existsAbstract(game.getPlayer1Variables()).ite(maxPlayer1Strategy, minPlayer1Strategy); minPlayer1Strategy = (maxPlayer1Strategy && prob01.min.first.getPlayer2States()).existsAbstract(game.getPlayer1Variables()).ite(maxPlayer1Strategy, minPlayer1Strategy);
// Build the fragment of transitions that is reachable by both the min and the max strategies. // Build the fragment of transitions that is reachable by both the min and the max strategies.
storm::dd::Bdd<Type> reachableTransitions = transitionMatrixBdd && minPlayer1Strategy && minPlayer2Strategy && maxPlayer1Strategy && maxPlayer2Strategy;
storm::dd::Bdd<Type> reachableTransitions = transitionMatrixBdd && (minPlayer1Strategy || minPlayer2Strategy) && maxPlayer1Strategy && maxPlayer2Strategy;
reachableTransitions = reachableTransitions.existsAbstract(game.getNondeterminismVariables()); reachableTransitions = reachableTransitions.existsAbstract(game.getNondeterminismVariables());
storm::dd::Bdd<Type> pivotStates = storm::utility::dd::computeReachableStates(game.getInitialStates(), reachableTransitions, game.getRowVariables(), game.getColumnVariables()); storm::dd::Bdd<Type> pivotStates = storm::utility::dd::computeReachableStates(game.getInitialStates(), reachableTransitions, game.getRowVariables(), game.getColumnVariables());
@ -526,12 +526,17 @@ namespace storm {
storm::dd::Add<Type, ValueType> maxResult = prob01.max.second.getPlayer1States().template toAdd<ValueType>(); storm::dd::Add<Type, ValueType> maxResult = prob01.max.second.getPlayer1States().template toAdd<ValueType>();
storm::dd::Add<Type, ValueType> initialStatesAdd = game.getInitialStates().template toAdd<ValueType>(); storm::dd::Add<Type, ValueType> initialStatesAdd = game.getInitialStates().template toAdd<ValueType>();
storm::dd::Bdd<Type> combinedMinPlayer1QualitativeStrategies = (prob01.min.first.getPlayer1Strategy() || prob01.min.second.getPlayer1Strategy());
storm::dd::Bdd<Type> combinedMinPlayer2QualitativeStrategies = (prob01.min.first.getPlayer2Strategy() || prob01.min.second.getPlayer2Strategy());
// The minimal value after qualitative checking can only be zero. It it was 1, we could have given // The minimal value after qualitative checking can only be zero. It it was 1, we could have given
// the result right away. // the result right away.
ValueType minValue = storm::utility::zero<ValueType>(); ValueType minValue = storm::utility::zero<ValueType>();
MaybeStateResult<Type, ValueType> minMaybeStateResult(game.getManager().template getAddZero<ValueType>(), game.getManager().getBddZero(), game.getManager().getBddZero()); MaybeStateResult<Type, ValueType> minMaybeStateResult(game.getManager().template getAddZero<ValueType>(), game.getManager().getBddZero(), game.getManager().getBddZero());
if (!maybeMin.isZero()) { if (!maybeMin.isZero()) {
minMaybeStateResult = solveMaybeStates(player1Direction, storm::OptimizationDirection::Minimize, game, maybeMin, prob01.min.second.getPlayer1States()); minMaybeStateResult = solveMaybeStates(player1Direction, storm::OptimizationDirection::Minimize, game, maybeMin, prob01.min.second.getPlayer1States());
minMaybeStateResult.player1Strategy &= game.getReachableStates();
minMaybeStateResult.player2Strategy &= game.getReachableStates();
minResult += minMaybeStateResult.values; minResult += minMaybeStateResult.values;
storm::dd::Add<Type, ValueType> initialStateMin = initialStatesAdd * minResult; storm::dd::Add<Type, ValueType> initialStateMin = initialStatesAdd * minResult;
// 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.
@ -540,18 +545,27 @@ namespace storm {
} }
STORM_LOG_TRACE("Obtained quantitative lower bound " << minValue << "."); STORM_LOG_TRACE("Obtained quantitative lower bound " << minValue << ".");
minMaybeStateResult.player1Strategy = combinedMinPlayer1QualitativeStrategies.existsAbstract(game.getPlayer1Variables()).ite(combinedMinPlayer1QualitativeStrategies, minMaybeStateResult.player1Strategy);
minMaybeStateResult.player2Strategy = combinedMinPlayer2QualitativeStrategies.existsAbstract(game.getPlayer2Variables()).ite(combinedMinPlayer2QualitativeStrategies, minMaybeStateResult.player2Strategy);
// Check whether we can abort the computation because of the lower value. // Check whether we can abort the computation because of the lower value.
result = checkForResultAfterQuantitativeCheck<ValueType>(checkTask, storm::OptimizationDirection::Minimize, minValue); result = checkForResultAfterQuantitativeCheck<ValueType>(checkTask, storm::OptimizationDirection::Minimize, minValue);
if (result) { if (result) {
return result; return result;
} }
storm::dd::Bdd<Type> combinedMaxPlayer1QualitativeStrategies = (prob01.max.first.getPlayer1Strategy() || prob01.max.second.getPlayer1Strategy());
storm::dd::Bdd<Type> combinedMaxPlayer2QualitativeStrategies = (prob01.max.first.getPlayer2Strategy() || prob01.max.second.getPlayer2Strategy());
// Likewise, the maximal value after qualitative checking can only be 1. If it was 0, we could have // Likewise, the maximal value after qualitative checking can only be 1. If it was 0, we could have
// given the result right awy. // given the result right awy.
ValueType maxValue = storm::utility::one<ValueType>(); ValueType maxValue = storm::utility::one<ValueType>();
MaybeStateResult<Type, ValueType> maxMaybeStateResult(game.getManager().template getAddZero<ValueType>(), game.getManager().getBddZero(), game.getManager().getBddZero()); MaybeStateResult<Type, ValueType> maxMaybeStateResult(game.getManager().template getAddZero<ValueType>(), game.getManager().getBddZero(), game.getManager().getBddZero());
if (!maybeMax.isZero()) { if (!maybeMax.isZero()) {
maxMaybeStateResult = solveMaybeStates(player1Direction, storm::OptimizationDirection::Maximize, game, maybeMax, prob01.max.second.getPlayer1States(), boost::make_optional(minMaybeStateResult)); maxMaybeStateResult = solveMaybeStates(player1Direction, storm::OptimizationDirection::Maximize, game, maybeMax, prob01.max.second.getPlayer1States(), boost::make_optional(minMaybeStateResult));
maxMaybeStateResult.player1Strategy &= game.getReachableStates();
maxMaybeStateResult.player2Strategy &= game.getReachableStates();
maxResult += maxMaybeStateResult.values; maxResult += maxMaybeStateResult.values;
storm::dd::Add<Type, ValueType> initialStateMax = (initialStatesAdd * maxResult); storm::dd::Add<Type, ValueType> initialStateMax = (initialStatesAdd * maxResult);
// Unlike in the min-case, we can require a non-zero count of 1 here, because if the max was in // Unlike in the min-case, we can require a non-zero count of 1 here, because if the max was in
@ -561,6 +575,9 @@ namespace storm {
} }
STORM_LOG_TRACE("Obtained quantitative upper bound " << maxValue << "."); STORM_LOG_TRACE("Obtained quantitative upper bound " << maxValue << ".");
maxMaybeStateResult.player1Strategy = combinedMaxPlayer1QualitativeStrategies.existsAbstract(game.getPlayer1Variables()).ite(combinedMaxPlayer1QualitativeStrategies, maxMaybeStateResult.player1Strategy);
maxMaybeStateResult.player2Strategy = combinedMaxPlayer2QualitativeStrategies.existsAbstract(game.getPlayer2Variables()).ite(combinedMaxPlayer2QualitativeStrategies, maxMaybeStateResult.player2Strategy);
// Check whether we can abort the computation because of the upper value. // Check whether we can abort the computation because of the upper value.
result = checkForResultAfterQuantitativeCheck<ValueType>(checkTask, storm::OptimizationDirection::Maximize, maxValue); result = checkForResultAfterQuantitativeCheck<ValueType>(checkTask, storm::OptimizationDirection::Maximize, maxValue);
if (result) { if (result) {
@ -577,8 +594,25 @@ namespace storm {
// If we arrived at this point, it means that we have all qualitative and quantitative information // If we arrived at this point, it means that we have all qualitative and quantitative information
// about the game, but we could not yet answer the query. In this case, we need to refine. // about the game, but we could not yet answer the query. In this case, we need to refine.
// Redirect all player 1 choices of the min strategy to that of the max strategy if this leads to a player 2 state that has the same prob.
// Get all relevant strategies.
storm::dd::Add<Type, ValueType> matrix = game.getTransitionMatrix();
storm::dd::Add<Type, ValueType> minResultTmp = minResult.swapVariables(game.getRowColumnMetaVariablePairs());
storm::dd::Add<Type, ValueType> minValuesForPlayer1UnderMinP1Strategy = (matrix * minMaybeStateResult.player1Strategy.template toAdd<ValueType>() * minMaybeStateResult.player2Strategy.template toAdd<ValueType>() * minResultTmp).sumAbstract(game.getColumnVariables()).sumAbstract(game.getPlayer2Variables()).sumAbstract(game.getPlayer1Variables());
storm::dd::Add<Type, ValueType> minValuesForPlayer1UnderMaxP1P2Strategy = (matrix * maxMaybeStateResult.player1Strategy.template toAdd<ValueType>() * maxMaybeStateResult.player2Strategy.template toAdd<ValueType>() * minResultTmp).sumAbstract(game.getColumnVariables()).sumAbstract(game.getPlayer2Variables()).sumAbstract(game.getPlayer1Variables());
storm::dd::Add<Type, ValueType> minValuesForPlayer1UnderMaxP1Strategy = (matrix * maxMaybeStateResult.player1Strategy.template toAdd<ValueType>() * minMaybeStateResult.player2Strategy.template toAdd<ValueType>() * minResultTmp).sumAbstract(game.getColumnVariables()).sumAbstract(game.getPlayer2Variables()).sumAbstract(game.getPlayer1Variables());
minValuesForPlayer1UnderMinP1Strategy = prob01.min.first.getPlayer1States().ite(game.getManager().template getAddZero<ValueType>(), prob01.min.second.getPlayer1States().ite(game.getManager().template getAddOne<ValueType>(), minValuesForPlayer1UnderMinP1Strategy));
minValuesForPlayer1UnderMaxP1Strategy = prob01.min.first.getPlayer1States().ite(game.getManager().template getAddZero<ValueType>(), prob01.min.second.getPlayer1States().ite(game.getManager().template getAddOne<ValueType>(), minValuesForPlayer1UnderMaxP1Strategy));
// This BDD has a 1 for every state (s) that can switch the strategy.
storm::dd::Bdd<Type> minIsGreaterOrEqual = minValuesForPlayer1UnderMinP1Strategy.greaterOrEqual(minValuesForPlayer1UnderMaxP1Strategy);
minMaybeStateResult.player1Strategy = minIsGreaterOrEqual.ite(maxMaybeStateResult.player1Strategy, minMaybeStateResult.player1Strategy);
// 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::dd::Bdd<Type> tmp = (prob01.min.first.getPlayer2Strategy().existsAbstract(game.getPlayer2Variables()) && prob01.min.second.getPlayer2Strategy().existsAbstract(game.getPlayer2Variables()));
STORM_LOG_ASSERT(tmp.isZero(), "wth?"); STORM_LOG_ASSERT(tmp.isZero(), "wth?");
Write Preview
Loading…
Cancel
Save