SymbolicGameSolver.h

Go to the documentation of this file.

#pragma once
 
#include <set>
#include <vector>
 
#include "storm/solver/OptimizationDirection.h"
 
#include "storm/storage/dd/Add.h"
#include "storm/storage/dd/Bdd.h"
#include "storm/storage/expressions/Variable.h"
 
namespace storm {
 
class Environment;
 
namespace solver {

template<storm::dd::DdType Type, typename ValueType = double>
class SymbolicGameSolver {
   public:
    SymbolicGameSolver(storm::dd::Add<Type, ValueType> const& A, storm::dd::Bdd<Type> const& allRows, storm::dd::Bdd<Type> const& illegalPlayer1Mask,
                       storm::dd::Bdd<Type> const& illegalPlayer2Mask, std::set<storm::expressions::Variable> const& rowMetaVariables,
                       std::set<storm::expressions::Variable> const& columnMetaVariables,
                       std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs,
                       std::set<storm::expressions::Variable> const& player1Variables, std::set<storm::expressions::Variable> const& player2Variables);
 
    virtual ~SymbolicGameSolver() = default;

    virtual storm::dd::Add<Type, ValueType> solveGame(Environment const& env, 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);
 
    // Setters that enable the generation of the players' strategies.
    void setGeneratePlayer1Strategy(bool value);
    void setGeneratePlayer2Strategy(bool value);
    void setGeneratePlayersStrategies(bool value);
 
    // Getters to retrieve the players' strategies. Only legal if they were generated.
    storm::dd::Bdd<Type> const& getPlayer1Strategy() const;
    storm::dd::Bdd<Type> const& getPlayer2Strategy() const;
 
   protected:
    // The matrix defining the coefficients of the linear equation system.
    storm::dd::Add<Type, ValueType> A;
 
    // A BDD characterizing all rows of the equation system.
    storm::dd::Bdd<Type> allRows;
 
    // An ADD that can be used to compensate for the illegal choices of player 1.
    storm::dd::Add<Type, ValueType> illegalPlayer1Mask;
 
    // An ADD that can be used to compensate for the illegal choices of player 2.
    storm::dd::Add<Type, ValueType> illegalPlayer2Mask;
 
    // The row variables.
    std::set<storm::expressions::Variable> rowMetaVariables;
 
    // The column variables.
    std::set<storm::expressions::Variable> columnMetaVariables;
 
    // The pairs of meta variables used for renaming.
    std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> rowColumnMetaVariablePairs;
 
    // The player 1 variables.
    std::set<storm::expressions::Variable> player1Variables;
 
    // The player 2 variables.
    std::set<storm::expressions::Variable> player2Variables;
 
    // A flag indicating whether a player 1 is to be generated.
    bool generatePlayer1Strategy;
 
    // A player 1 strategy if one was generated.
    boost::optional<storm::dd::Bdd<Type>> player1Strategy;
 
    // A flag indicating whether a player 2 is to be generated.
    bool generatePlayer2Strategy;
 
    // A player 1 strategy if one was generated.
    boost::optional<storm::dd::Bdd<Type>> player2Strategy;
};
 
template<storm::dd::DdType Type, typename ValueType>
class SymbolicGameSolverFactory {
   public:
    virtual ~SymbolicGameSolverFactory() = default;
 
    virtual std::unique_ptr<storm::solver::SymbolicGameSolver<Type, ValueType>> create(
        storm::dd::Add<Type, ValueType> const& A, storm::dd::Bdd<Type> const& allRows, storm::dd::Bdd<Type> const& illegalPlayer1Mask,
        storm::dd::Bdd<Type> const& illegalPlayer2Mask, std::set<storm::expressions::Variable> const& rowMetaVariables,
        std::set<storm::expressions::Variable> const& columnMetaVariables,
        std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs,
        std::set<storm::expressions::Variable> const& player1Variables, std::set<storm::expressions::Variable> const& player2Variables) const;
};
 
}  // namespace solver
}  // namespace storm