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

minor fix before bedtime 

Former-commit-id: c558c23122
tempestpy_adaptions
dehnert 8 years ago
parent
9e64e998f3
commit
f7f14f13fc
1 changed files with 11 additions and 6 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/modelchecker/abstraction/GameBasedMdpModelChecker.cpp

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

@ -98,13 +98,18 @@ namespace storm {
game.getTransitionMatrix().exportToDot("trans.dot");
bottomStatesBdd.template toAdd<ValueType>().exportToDot("bottom.dot");
// Start by computing the states with probability 0/1 for the case in which player 2 minimizes.
storm::utility::graph::GameProb01Result<Type> prob0Min = storm::utility::graph::performProb0(game, transitionMatrixBdd, game.getStates(constraintExpression), game.getStates(targetStateExpression), player1Direction, storm::OptimizationDirection::Minimize, true);
storm::utility::graph::GameProb01Result<Type> prob1Min = storm::utility::graph::performProb1(game, transitionMatrixBdd, game.getStates(constraintExpression), game.getStates(targetStateExpression), player1Direction, storm::OptimizationDirection::Minimize, true);
storm::dd::Bdd<Type> targetStates = game.getStates(targetStateExpression);
if (player1Direction == storm::OptimizationDirection::Minimize) {
targetStates |= game.getBottomStates();
}
// Start by computing the states with probability 0/1 when player 2 minimizes.
storm::utility::graph::GameProb01Result<Type> prob0Min = storm::utility::graph::performProb0(game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates, player1Direction, storm::OptimizationDirection::Minimize, true);
storm::utility::graph::GameProb01Result<Type> prob1Min = storm::utility::graph::performProb1(game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates, player1Direction, storm::OptimizationDirection::Minimize, true);
// Now compute the states with probability 0/1 for the case in which player 2 maximizes.
storm::utility::graph::GameProb01Result<Type> prob0Max = storm::utility::graph::performProb0(game, transitionMatrixBdd, game.getStates(constraintExpression), game.getStates(targetStateExpression), player1Direction, storm::OptimizationDirection::Maximize, true);
storm::utility::graph::GameProb01Result<Type> prob1Max = storm::utility::graph::performProb1(game, transitionMatrixBdd, game.getStates(constraintExpression), game.getStates(targetStateExpression), player1Direction, storm::OptimizationDirection::Maximize, true);
// Now compute the states with probability 0/1 when player 2 maximizes.
storm::utility::graph::GameProb01Result<Type> prob0Max = storm::utility::graph::performProb0(game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates, player1Direction, storm::OptimizationDirection::Maximize, true);
storm::utility::graph::GameProb01Result<Type> prob1Max = storm::utility::graph::performProb1(game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates, player1Direction, storm::OptimizationDirection::Maximize, true);
STORM_LOG_DEBUG("Min: " << prob0Min.states.getNonZeroCount() << " no states, " << prob1Min.states.getNonZeroCount() << " yes states.");
STORM_LOG_DEBUG("Max: " << prob0Max.states.getNonZeroCount() << " no states, " << prob1Max.states.getNonZeroCount() << " yes states.");

Write Preview
Loading…
Cancel
Save