From bd36c7a2e649191f9c4abbbcc3e5a1f4d345f095 Mon Sep 17 00:00:00 2001 From: PBerger Date: Mon, 12 Sep 2016 16:59:03 +0200 Subject: [PATCH] Finally, some progress. Former-commit-id: 2eb5173abc8fac60b0c0a270d415bbb51e971566 --- .../abstraction/GameBasedMdpModelChecker.cpp | 32 +++++++++---------- src/solver/SymbolicGameSolver.cpp | 12 +++++-- src/solver/SymbolicGameSolver.h | 2 +- .../solver/FullySymbolicGameSolverTest.cpp | 16 +++++----- 4 files changed, 35 insertions(+), 27 deletions(-) diff --git a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index de5f8de9f..9bdc468c9 100644 --- a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -400,35 +400,35 @@ namespace storm { }; template - MaybeStateResult solveMaybeStates(storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::MenuGame const& game, storm::dd::Bdd const& maybeStates, storm::dd::Bdd const& prob1States, boost::optional> startInfo = boost::none) { + MaybeStateResult solveMaybeStates(storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::MenuGame const& game, storm::dd::Bdd const& prob0States, storm::dd::Bdd const& prob1States, boost::optional> startInfo = boost::none) { STORM_LOG_TRACE("Performing quantative solution step. Player 1: " << player1Direction << ", player 2: " << player2Direction << "."); - // Compute the ingredients of the equation system. - storm::dd::Add maybeStatesAdd = maybeStates.template toAdd(); - storm::dd::Bdd allStates = game.getReachableStates(); - storm::dd::Add allStatesAdd = allStates.template toAdd(); - storm::dd::Add submatrix = allStatesAdd * game.getTransitionMatrix(); - storm::dd::Add prob1StatesAsColumn = prob1States.template toAdd().swapVariables(game.getRowColumnMetaVariablePairs()); - storm::dd::Add subvector = submatrix * prob1StatesAsColumn; - subvector = subvector.sumAbstract(game.getColumnVariables()); + // Compute the ingredients of the equation system. + storm::dd::Add maybeStatesAdd = game.getReachableStates().template toAdd(); + storm::dd::Add submatrix = maybeStatesAdd * game.getTransitionMatrix(); + storm::dd::Add subvector = game.getManager().template getAddZero(); // Cut away all columns targeting non-maybe states. - submatrix *= allStatesAdd.swapVariables(game.getRowColumnMetaVariablePairs()); + submatrix *= maybeStatesAdd.swapVariables(game.getRowColumnMetaVariablePairs()); // Cut the starting vector to the maybe states of this query. storm::dd::Add startVector; if (startInfo) { - startVector = startInfo.get().values * allStatesAdd; + startVector = startInfo.get().values * maybeStatesAdd; } else { startVector = game.getManager().template getAddZero(); } + + // Set all target- and Prob1-states to 1 and all Prob0-states to 0 + startVector = prob0States.ite(game.getManager().template getAddZero(), startVector); + startVector = prob1States.ite(game.getManager().template getAddOne(), startVector); // Create the solver and solve the equation system. storm::utility::solver::SymbolicGameSolverFactory solverFactory; - std::unique_ptr> solver = solverFactory.create(submatrix, allStates, game.getIllegalPlayer1Mask(), game.getIllegalPlayer2Mask(), game.getRowVariables(), game.getColumnVariables(), game.getRowColumnMetaVariablePairs(), game.getPlayer1Variables(), game.getPlayer2Variables()); + std::unique_ptr> solver = solverFactory.create(submatrix, game.getReachableStates(), game.getIllegalPlayer1Mask(), game.getIllegalPlayer2Mask(), game.getRowVariables(), game.getColumnVariables(), game.getRowColumnMetaVariablePairs(), game.getPlayer1Variables(), game.getPlayer2Variables()); solver->setGeneratePlayersStrategies(true); - auto values = solver->solveGame(player1Direction, player2Direction, startVector, subvector, startInfo ? boost::make_optional(startInfo.get().player1Strategy) : boost::none, startInfo ? boost::make_optional(startInfo.get().player2Strategy) : boost::none); + auto values = solver->solveGame(player1Direction, player2Direction, startVector, subvector, prob0States, prob1States, startInfo ? boost::make_optional(startInfo.get().player1Strategy) : boost::none, startInfo ? boost::make_optional(startInfo.get().player2Strategy) : boost::none); return MaybeStateResult(values, solver->getPlayer1Strategy(), solver->getPlayer2Strategy()); } @@ -527,13 +527,13 @@ namespace storm { storm::dd::Add minResult = prob01.min.second.getPlayer1States().template toAdd(); storm::dd::Add maxResult = prob01.max.second.getPlayer1States().template toAdd(); storm::dd::Add initialStatesAdd = game.getInitialStates().template toAdd(); - + // The minimal value after qualitative checking can only be zero. It it was 1, we could have given // the result right away. ValueType minValue = storm::utility::zero(); MaybeStateResult minMaybeStateResult(game.getManager().template getAddZero(), game.getManager().getBddZero(), game.getManager().getBddZero()); if (!maybeMin.isZero()) { - minMaybeStateResult = solveMaybeStates(player1Direction, storm::OptimizationDirection::Minimize, game, maybeMin, prob01.min.second.getPlayer1States()); + minMaybeStateResult = solveMaybeStates(player1Direction, storm::OptimizationDirection::Minimize, game, prob01.min.first.getPlayer1States(), prob01.min.second.getPlayer1States()); minResult = minMaybeStateResult.values; storm::dd::Add initialStateMin = initialStatesAdd * minResult; // Here we can only require a non-zero count of *at most* one, because the result may actually be 0. @@ -553,7 +553,7 @@ namespace storm { ValueType maxValue = storm::utility::one(); MaybeStateResult maxMaybeStateResult(game.getManager().template getAddZero(), game.getManager().getBddZero(), game.getManager().getBddZero()); 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, prob01.max.first.getPlayer1States(), prob01.max.second.getPlayer1States(), boost::make_optional(minMaybeStateResult)); maxResult = maxMaybeStateResult.values; storm::dd::Add initialStateMax = (initialStatesAdd * maxResult); // Unlike in the min-case, we can require a non-zero count of 1 here, because if the max was in diff --git a/src/solver/SymbolicGameSolver.cpp b/src/solver/SymbolicGameSolver.cpp index db297cafb..428374ee3 100644 --- a/src/solver/SymbolicGameSolver.cpp +++ b/src/solver/SymbolicGameSolver.cpp @@ -25,12 +25,16 @@ namespace storm { } template - storm::dd::Add SymbolicGameSolver::solveGame(OptimizationDirection player1Goal, OptimizationDirection player2Goal, storm::dd::Add const& x, storm::dd::Add const& b, boost::optional> const& basePlayer1Strategy, boost::optional> const& basePlayer2Strategy) { + storm::dd::Add SymbolicGameSolver::solveGame(OptimizationDirection player1Goal, OptimizationDirection player2Goal, storm::dd::Add const& x, storm::dd::Add const& b, storm::dd::Bdd const& prob0States, storm::dd::Bdd const& prob1States, boost::optional> const& basePlayer1Strategy, boost::optional> const& basePlayer2Strategy) { // Set up the environment. storm::dd::Add xCopy = x; uint_fast64_t iterations = 0; bool converged = false; + // Constants + storm::dd::Add const addOne = A.getDdManager().template getAddOne(); + storm::dd::Add const addZero = A.getDdManager().template getAddZero(); + // Prepare some data storage in case we need to generate strategies. if (generatePlayer1Strategy) { if (basePlayer1Strategy) { @@ -49,7 +53,7 @@ namespace storm { previousPlayer2Values = (player2Strategy.get().template toAdd() * (this->A.multiplyMatrix(x.swapVariables(this->rowColumnMetaVariablePairs), this->columnMetaVariables) + b)).sumAbstract(this->player2Variables); } else { player2Strategy = A.getDdManager().getBddZero(); - previousPlayer2Values = A.getDdManager().template getAddZero(); + previousPlayer2Values = addZero; } } @@ -103,6 +107,10 @@ namespace storm { tmp = newValues; } + // Fix Prob0 and Prob1 States + tmp = prob0States.ite(addZero, tmp); + tmp = prob1States.ite(addOne, tmp); + // Now check if the process already converged within our precision. converged = xCopy.equalModuloPrecision(tmp, this->precision, this->relative); diff --git a/src/solver/SymbolicGameSolver.h b/src/solver/SymbolicGameSolver.h index 211dc8f33..a9d430fc0 100644 --- a/src/solver/SymbolicGameSolver.h +++ b/src/solver/SymbolicGameSolver.h @@ -70,7 +70,7 @@ namespace storm { * then this strategy can be used to generate a strategy that only differs from the given one if it has to. * @return The solution vector. */ - virtual storm::dd::Add solveGame(OptimizationDirection player1Goal, OptimizationDirection player2Goal, storm::dd::Add const& x, storm::dd::Add const& b, boost::optional> const& basePlayer1Strategy = boost::none, boost::optional> const& basePlayer2Strategy = boost::none); + virtual storm::dd::Add solveGame(OptimizationDirection player1Goal, OptimizationDirection player2Goal, storm::dd::Add const& x, storm::dd::Add const& b, storm::dd::Bdd const& prob0States, storm::dd::Bdd const& prob1States, boost::optional> const& basePlayer1Strategy = boost::none, boost::optional> const& basePlayer2Strategy = boost::none); // Setters that enable the generation of the players' strategies. void setGeneratePlayer1Strategy(bool value); diff --git a/test/functional/solver/FullySymbolicGameSolverTest.cpp b/test/functional/solver/FullySymbolicGameSolverTest.cpp index 8da44ca92..2f64c36e1 100644 --- a/test/functional/solver/FullySymbolicGameSolverTest.cpp +++ b/test/functional/solver/FullySymbolicGameSolverTest.cpp @@ -49,25 +49,25 @@ TEST(FullySymbolicGameSolverTest, Solve_Cudd) { storm::dd::Add b = manager->getEncoding(state.first, 2).template toAdd() + manager->getEncoding(state.first, 4).template toAdd(); // Now solve the game with different strategies for the players. - storm::dd::Add result = solver->solveGame(storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, x, b); + storm::dd::Add result = solver->solveGame(storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, x, b, manager->getBddZero(), manager->getBddZero()); result *= manager->getEncoding(state.first, 1).template toAdd(); result = result.sumAbstract({state.first}); EXPECT_NEAR(0, result.getValue(), storm::settings::getModule().getPrecision()); x = manager->getAddZero(); - result = solver->solveGame(storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize, x, b); + result = solver->solveGame(storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize, x, b, manager->getBddZero(), manager->getBddZero()); result *= manager->getEncoding(state.first, 1).template toAdd(); result = result.sumAbstract({state.first}); EXPECT_NEAR(0.5, result.getValue(), storm::settings::getModule().getPrecision()); x = manager->getAddZero(); - result = solver->solveGame(storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize, x, b); + result = solver->solveGame(storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize, x, b, manager->getBddZero(), manager->getBddZero()); result *= manager->getEncoding(state.first, 1).template toAdd(); result = result.sumAbstract({state.first}); EXPECT_NEAR(0.2, result.getValue(), storm::settings::getModule().getPrecision()); x = manager->getAddZero(); - result = solver->solveGame(storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, x, b); + result = solver->solveGame(storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, x, b, manager->getBddZero(), manager->getBddZero()); result *= manager->getEncoding(state.first, 1).template toAdd(); result = result.sumAbstract({state.first}); EXPECT_NEAR(0.99999892625817599, result.getValue(), storm::settings::getModule().getPrecision()); @@ -114,25 +114,25 @@ TEST(FullySymbolicGameSolverTest, Solve_Sylvan) { storm::dd::Add b = manager->getEncoding(state.first, 2).template toAdd() + manager->getEncoding(state.first, 4).template toAdd(); // Now solve the game with different strategies for the players. - storm::dd::Add result = solver->solveGame(storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, x, b); + storm::dd::Add result = solver->solveGame(storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, x, b, manager->getBddZero(), manager->getBddZero()); result *= manager->getEncoding(state.first, 1).template toAdd(); result = result.sumAbstract({state.first}); EXPECT_NEAR(0, result.getValue(), storm::settings::getModule().getPrecision()); x = manager->getAddZero(); - result = solver->solveGame(storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize, x, b); + result = solver->solveGame(storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize, x, b, manager->getBddZero(), manager->getBddZero()); result *= manager->getEncoding(state.first, 1).template toAdd(); result = result.sumAbstract({state.first}); EXPECT_NEAR(0.5, result.getValue(), storm::settings::getModule().getPrecision()); x = manager->getAddZero(); - result = solver->solveGame(storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize, x, b); + result = solver->solveGame(storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize, x, b, manager->getBddZero(), manager->getBddZero()); result *= manager->getEncoding(state.first, 1).template toAdd(); result = result.sumAbstract({state.first}); EXPECT_NEAR(0.2, result.getValue(), storm::settings::getModule().getPrecision()); x = manager->getAddZero(); - result = solver->solveGame(storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, x, b); + result = solver->solveGame(storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, x, b, manager->getBddZero(), manager->getBddZero()); result *= manager->getEncoding(state.first, 1).template toAdd(); result = result.sumAbstract({state.first}); EXPECT_NEAR(0.99999892625817599, result.getValue(), storm::settings::getModule().getPrecision());