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

Finally, some progress. 

Former-commit-id: 2eb5173abc
main
PBerger 9 years ago
parent
2d51ef2c0c
commit
bd36c7a2e6
4 changed files with 35 additions and 27 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. 32
      src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
  2. 12
      src/solver/SymbolicGameSolver.cpp
  3. 2
      src/solver/SymbolicGameSolver.h
  4. 16
      test/functional/solver/FullySymbolicGameSolverTest.cpp

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

@ -400,35 +400,35 @@ namespace storm {
}; };
template<storm::dd::DdType Type, typename ValueType> template<storm::dd::DdType Type, typename ValueType>
MaybeStateResult<Type, ValueType> solveMaybeStates(storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Bdd<Type> const& maybeStates, storm::dd::Bdd<Type> const& prob1States, boost::optional<MaybeStateResult<Type, ValueType>> startInfo = boost::none) {
MaybeStateResult<Type, ValueType> solveMaybeStates(storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Bdd<Type> const& prob0States, storm::dd::Bdd<Type> const& prob1States, boost::optional<MaybeStateResult<Type, ValueType>> startInfo = boost::none) {
STORM_LOG_TRACE("Performing quantative solution step. Player 1: " << player1Direction << ", player 2: " << player2Direction << "."); STORM_LOG_TRACE("Performing quantative solution step. Player 1: " << player1Direction << ", player 2: " << player2Direction << ".");
// Compute the ingredients of the equation system.
storm::dd::Add<Type, ValueType> maybeStatesAdd = maybeStates.template toAdd<ValueType>();
storm::dd::Bdd<Type> allStates = game.getReachableStates();
storm::dd::Add<Type, ValueType> allStatesAdd = allStates.template toAdd<ValueType>();
storm::dd::Add<Type, ValueType> submatrix = allStatesAdd * game.getTransitionMatrix();
storm::dd::Add<Type, ValueType> prob1StatesAsColumn = prob1States.template toAdd<ValueType>().swapVariables(game.getRowColumnMetaVariablePairs());
storm::dd::Add<Type, ValueType> subvector = submatrix * prob1StatesAsColumn;
subvector = subvector.sumAbstract(game.getColumnVariables());
// Compute the ingredients of the equation system.
storm::dd::Add<Type, ValueType> maybeStatesAdd = game.getReachableStates().template toAdd<ValueType>();
storm::dd::Add<Type, ValueType> submatrix = maybeStatesAdd * game.getTransitionMatrix();
storm::dd::Add<Type, ValueType> subvector = game.getManager().template getAddZero<ValueType>();
// Cut away all columns targeting non-maybe states. // 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. // Cut the starting vector to the maybe states of this query.
storm::dd::Add<Type, ValueType> startVector; storm::dd::Add<Type, ValueType> startVector;
if (startInfo) { if (startInfo) {
startVector = startInfo.get().values * allStatesAdd;
startVector = startInfo.get().values * maybeStatesAdd;
} else { } else {
startVector = game.getManager().template getAddZero<ValueType>(); startVector = game.getManager().template getAddZero<ValueType>();
} }
// Set all target- and Prob1-states to 1 and all Prob0-states to 0
startVector = prob0States.ite(game.getManager().template getAddZero<ValueType>(), startVector);
startVector = prob1States.ite(game.getManager().template getAddOne<ValueType>(), startVector);
// Create the solver and solve the equation system. // Create the solver and solve the equation system.
storm::utility::solver::SymbolicGameSolverFactory<Type, ValueType> solverFactory; storm::utility::solver::SymbolicGameSolverFactory<Type, ValueType> solverFactory;
std::unique_ptr<storm::solver::SymbolicGameSolver<Type, ValueType>> solver = solverFactory.create(submatrix, allStates, game.getIllegalPlayer1Mask(), game.getIllegalPlayer2Mask(), game.getRowVariables(), game.getColumnVariables(), game.getRowColumnMetaVariablePairs(), game.getPlayer1Variables(), game.getPlayer2Variables());
std::unique_ptr<storm::solver::SymbolicGameSolver<Type, ValueType>> solver = solverFactory.create(submatrix, game.getReachableStates(), game.getIllegalPlayer1Mask(), game.getIllegalPlayer2Mask(), game.getRowVariables(), game.getColumnVariables(), game.getRowColumnMetaVariablePairs(), game.getPlayer1Variables(), game.getPlayer2Variables());
solver->setGeneratePlayersStrategies(true); 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<Type, ValueType>(values, solver->getPlayer1Strategy(), solver->getPlayer2Strategy()); return MaybeStateResult<Type, ValueType>(values, solver->getPlayer1Strategy(), solver->getPlayer2Strategy());
} }
@ -527,13 +527,13 @@ namespace storm {
storm::dd::Add<Type, ValueType> minResult = prob01.min.second.getPlayer1States().template toAdd<ValueType>(); storm::dd::Add<Type, ValueType> minResult = prob01.min.second.getPlayer1States().template toAdd<ValueType>();
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>();
// 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, prob01.min.first.getPlayer1States(), 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;
// 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.
@ -553,7 +553,7 @@ namespace storm {
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, prob01.max.first.getPlayer1States(), prob01.max.second.getPlayer1States(), boost::make_optional(minMaybeStateResult));
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

12
src/solver/SymbolicGameSolver.cpp
View File

@ -25,12 +25,16 @@ namespace storm {
} }
template<storm::dd::DdType Type, typename ValueType> template<storm::dd::DdType Type, typename ValueType>
storm::dd::Add<Type, ValueType> SymbolicGameSolver<Type, ValueType>::solveGame(OptimizationDirection player1Goal, OptimizationDirection player2Goal, storm::dd::Add<Type, ValueType> const& x, storm::dd::Add<Type, ValueType> const& b, boost::optional<storm::dd::Bdd<Type>> const& basePlayer1Strategy, boost::optional<storm::dd::Bdd<Type>> const& basePlayer2Strategy) {
storm::dd::Add<Type, ValueType> SymbolicGameSolver<Type, ValueType>::solveGame(OptimizationDirection player1Goal, OptimizationDirection player2Goal, storm::dd::Add<Type, ValueType> const& x, storm::dd::Add<Type, ValueType> const& b, storm::dd::Bdd<Type> const& prob0States, storm::dd::Bdd<Type> const& prob1States, boost::optional<storm::dd::Bdd<Type>> const& basePlayer1Strategy, boost::optional<storm::dd::Bdd<Type>> const& basePlayer2Strategy) {
// Set up the environment. // Set up the environment.
storm::dd::Add<Type, ValueType> xCopy = x; storm::dd::Add<Type, ValueType> xCopy = x;
uint_fast64_t iterations = 0; uint_fast64_t iterations = 0;
bool converged = false; bool converged = false;
// Constants
storm::dd::Add<Type, ValueType> const addOne = A.getDdManager().template getAddOne<ValueType>();
storm::dd::Add<Type, ValueType> const addZero = A.getDdManager().template getAddZero<ValueType>();
// Prepare some data storage in case we need to generate strategies. // Prepare some data storage in case we need to generate strategies.
if (generatePlayer1Strategy) { if (generatePlayer1Strategy) {
if (basePlayer1Strategy) { if (basePlayer1Strategy) {
@ -49,7 +53,7 @@ namespace storm {
previousPlayer2Values = (player2Strategy.get().template toAdd<ValueType>() * (this->A.multiplyMatrix(x.swapVariables(this->rowColumnMetaVariablePairs), this->columnMetaVariables) + b)).sumAbstract(this->player2Variables); previousPlayer2Values = (player2Strategy.get().template toAdd<ValueType>() * (this->A.multiplyMatrix(x.swapVariables(this->rowColumnMetaVariablePairs), this->columnMetaVariables) + b)).sumAbstract(this->player2Variables);
} else { } else {
player2Strategy = A.getDdManager().getBddZero(); player2Strategy = A.getDdManager().getBddZero();
previousPlayer2Values = A.getDdManager().template getAddZero<ValueType>();
previousPlayer2Values = addZero;
} }
} }
@ -103,6 +107,10 @@ namespace storm {
tmp = newValues; 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. // Now check if the process already converged within our precision.
converged = xCopy.equalModuloPrecision(tmp, this->precision, this->relative); converged = xCopy.equalModuloPrecision(tmp, this->precision, this->relative);

2
src/solver/SymbolicGameSolver.h
View File

@ -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. * 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. * @return The solution vector.
*/ */
virtual storm::dd::Add<Type, ValueType> solveGame(OptimizationDirection player1Goal, OptimizationDirection player2Goal, storm::dd::Add<Type, ValueType> const& x, storm::dd::Add<Type, ValueType> const& b, boost::optional<storm::dd::Bdd<Type>> const& basePlayer1Strategy = boost::none, boost::optional<storm::dd::Bdd<Type>> const& basePlayer2Strategy = boost::none);
virtual storm::dd::Add<Type, ValueType> solveGame(OptimizationDirection player1Goal, OptimizationDirection player2Goal, storm::dd::Add<Type, ValueType> const& x, storm::dd::Add<Type, ValueType> const& b, storm::dd::Bdd<Type> const& prob0States, storm::dd::Bdd<Type> const& prob1States, boost::optional<storm::dd::Bdd<Type>> const& basePlayer1Strategy = boost::none, boost::optional<storm::dd::Bdd<Type>> const& basePlayer2Strategy = boost::none);
// Setters that enable the generation of the players' strategies. // Setters that enable the generation of the players' strategies.
void setGeneratePlayer1Strategy(bool value); void setGeneratePlayer1Strategy(bool value);

16
test/functional/solver/FullySymbolicGameSolverTest.cpp
View File

@ -49,25 +49,25 @@ TEST(FullySymbolicGameSolverTest, Solve_Cudd) {
storm::dd::Add<storm::dd::DdType::CUDD, double> b = manager->getEncoding(state.first, 2).template toAdd<double>() + manager->getEncoding(state.first, 4).template toAdd<double>(); storm::dd::Add<storm::dd::DdType::CUDD, double> b = manager->getEncoding(state.first, 2).template toAdd<double>() + manager->getEncoding(state.first, 4).template toAdd<double>();
// Now solve the game with different strategies for the players. // Now solve the game with different strategies for the players.
storm::dd::Add<storm::dd::DdType::CUDD> result = solver->solveGame(storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, x, b);
storm::dd::Add<storm::dd::DdType::CUDD> result = solver->solveGame(storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, x, b, manager->getBddZero(), manager->getBddZero());
result *= manager->getEncoding(state.first, 1).template toAdd<double>(); result *= manager->getEncoding(state.first, 1).template toAdd<double>();
result = result.sumAbstract({state.first}); result = result.sumAbstract({state.first});
EXPECT_NEAR(0, result.getValue(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); EXPECT_NEAR(0, result.getValue(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
x = manager->getAddZero<double>(); x = manager->getAddZero<double>();
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<double>(); result *= manager->getEncoding(state.first, 1).template toAdd<double>();
result = result.sumAbstract({state.first}); result = result.sumAbstract({state.first});
EXPECT_NEAR(0.5, result.getValue(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); EXPECT_NEAR(0.5, result.getValue(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
x = manager->getAddZero<double>(); x = manager->getAddZero<double>();
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<double>(); result *= manager->getEncoding(state.first, 1).template toAdd<double>();
result = result.sumAbstract({state.first}); result = result.sumAbstract({state.first});
EXPECT_NEAR(0.2, result.getValue(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); EXPECT_NEAR(0.2, result.getValue(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
x = manager->getAddZero<double>(); x = manager->getAddZero<double>();
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<double>(); result *= manager->getEncoding(state.first, 1).template toAdd<double>();
result = result.sumAbstract({state.first}); result = result.sumAbstract({state.first});
EXPECT_NEAR(0.99999892625817599, result.getValue(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); EXPECT_NEAR(0.99999892625817599, result.getValue(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
@ -114,25 +114,25 @@ TEST(FullySymbolicGameSolverTest, Solve_Sylvan) {
storm::dd::Add<storm::dd::DdType::Sylvan, double> b = manager->getEncoding(state.first, 2).template toAdd<double>() + manager->getEncoding(state.first, 4).template toAdd<double>(); storm::dd::Add<storm::dd::DdType::Sylvan, double> b = manager->getEncoding(state.first, 2).template toAdd<double>() + manager->getEncoding(state.first, 4).template toAdd<double>();
// Now solve the game with different strategies for the players. // Now solve the game with different strategies for the players.
storm::dd::Add<storm::dd::DdType::Sylvan> result = solver->solveGame(storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, x, b);
storm::dd::Add<storm::dd::DdType::Sylvan> result = solver->solveGame(storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, x, b, manager->getBddZero(), manager->getBddZero());
result *= manager->getEncoding(state.first, 1).template toAdd<double>(); result *= manager->getEncoding(state.first, 1).template toAdd<double>();
result = result.sumAbstract({state.first}); result = result.sumAbstract({state.first});
EXPECT_NEAR(0, result.getValue(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); EXPECT_NEAR(0, result.getValue(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
x = manager->getAddZero<double>(); x = manager->getAddZero<double>();
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<double>(); result *= manager->getEncoding(state.first, 1).template toAdd<double>();
result = result.sumAbstract({state.first}); result = result.sumAbstract({state.first});
EXPECT_NEAR(0.5, result.getValue(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); EXPECT_NEAR(0.5, result.getValue(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
x = manager->getAddZero<double>(); x = manager->getAddZero<double>();
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<double>(); result *= manager->getEncoding(state.first, 1).template toAdd<double>();
result = result.sumAbstract({state.first}); result = result.sumAbstract({state.first});
EXPECT_NEAR(0.2, result.getValue(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); EXPECT_NEAR(0.2, result.getValue(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
x = manager->getAddZero<double>(); x = manager->getAddZero<double>();
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<double>(); result *= manager->getEncoding(state.first, 1).template toAdd<double>();
result = result.sumAbstract({state.first}); result = result.sumAbstract({state.first});
EXPECT_NEAR(0.99999892625817599, result.getValue(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); EXPECT_NEAR(0.99999892625817599, result.getValue(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
Write Preview
Loading…
Cancel
Save