An interface that represents an abstract symbolic game solver. More...

#include <SymbolicGameSolver.h>

Collaboration diagram for storm::solver::SymbolicGameSolver< Type, ValueType >:

[legend]

Public Member Functions
	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)
	Constructs a symbolic game solver with the given meta variable sets and pairs.

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)
	Solves the equation system defined by the game matrix.

void	setGeneratePlayer1Strategy (bool value)

void	setGeneratePlayer2Strategy (bool value)

void	setGeneratePlayersStrategies (bool value)

storm::dd::Bdd< Type > const &	getPlayer1Strategy () const

storm::dd::Bdd< Type > const &	getPlayer2Strategy () const

Protected Attributes
storm::dd::Add< Type, ValueType >	A

storm::dd::Bdd< Type >	allRows

storm::dd::Add< Type, ValueType >	illegalPlayer1Mask

storm::dd::Add< Type, ValueType >	illegalPlayer2Mask

std::set< storm::expressions::Variable >	rowMetaVariables

std::set< storm::expressions::Variable >	columnMetaVariables

std::vector< std::pair< storm::expressions::Variable, storm::expressions::Variable > >	rowColumnMetaVariablePairs

std::set< storm::expressions::Variable >	player1Variables

std::set< storm::expressions::Variable >	player2Variables

bool	generatePlayer1Strategy

boost::optional< storm::dd::Bdd< Type > >	player1Strategy

bool	generatePlayer2Strategy

boost::optional< storm::dd::Bdd< Type > >	player2Strategy

Detailed Description

template<storm::dd::DdType Type, typename ValueType = double>
class storm::solver::SymbolicGameSolver< Type, ValueType >

An interface that represents an abstract symbolic game solver.

Definition at line 23 of file SymbolicGameSolver.h.

Constructor & Destructor Documentation

◆ SymbolicGameSolver()

template<storm::dd::DdType Type, typename ValueType >

storm::solver::SymbolicGameSolver< Type, ValueType >::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
	)

Constructs a symbolic game solver with the given meta variable sets and pairs.

Parameters

A	The matrix defining the coefficients of the game.
allRows	A BDD characterizing all rows of the equation system.
illegalPlayer1Mask	A BDD characterizing the illegal choices of player 1.
illegalPlayer2Mask	A BDD characterizing the illegal choices of player 2.
rowMetaVariables	The meta variables used to encode the rows of the matrix.
columnMetaVariables	The meta variables used to encode the columns of the matrix.
rowColumnMetaVariablePairs	The pairs of row meta variables and the corresponding column meta variables.
player1Variables	The meta variables used to encode the player 1 choices.
player2Variables	The meta variables used to encode the player 2 choices.

Definition at line 17 of file SymbolicGameSolver.cpp.

◆ ~SymbolicGameSolver()

template<storm::dd::DdType Type, typename ValueType = double>

virtual storm::solver::SymbolicGameSolver< Type, ValueType >::~SymbolicGameSolver ( )

virtualdefault

Member Function Documentation

◆ getPlayer1Strategy()

template<storm::dd::DdType Type, typename ValueType >

storm::dd::Bdd< Type > const & storm::solver::SymbolicGameSolver< Type, ValueType >::getPlayer1Strategy ( ) const

Definition at line 162 of file SymbolicGameSolver.cpp.

◆ getPlayer2Strategy()

template<storm::dd::DdType Type, typename ValueType >

storm::dd::Bdd< Type > const & storm::solver::SymbolicGameSolver< Type, ValueType >::getPlayer2Strategy ( ) const

Definition at line 168 of file SymbolicGameSolver.cpp.

◆ setGeneratePlayer1Strategy()

template<storm::dd::DdType Type, typename ValueType >

void storm::solver::SymbolicGameSolver< Type, ValueType >::setGeneratePlayer1Strategy ( bool value )

Definition at line 146 of file SymbolicGameSolver.cpp.

◆ setGeneratePlayer2Strategy()

template<storm::dd::DdType Type, typename ValueType >

void storm::solver::SymbolicGameSolver< Type, ValueType >::setGeneratePlayer2Strategy ( bool value )

Definition at line 151 of file SymbolicGameSolver.cpp.

◆ setGeneratePlayersStrategies()

template<storm::dd::DdType Type, typename ValueType >

void storm::solver::SymbolicGameSolver< Type, ValueType >::setGeneratePlayersStrategies ( bool value )

Definition at line 156 of file SymbolicGameSolver.cpp.

◆ solveGame()

template<storm::dd::DdType Type, typename ValueType >

storm::dd::Add< Type, ValueType > storm::solver::SymbolicGameSolver< 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`
	)

virtual

Solves the equation system defined by the game matrix.

Note that the game matrix has to be given upon construction time of the solver object.

Parameters

player1Goal	Sets whether player 1 wants to minimize or maximize.
player2Goal	Sets whether player 2 wants to minimize or maximize.
x	The initial guess of the solution.
b	The vector to add after matrix-vector multiplication.
basePlayer1Strategy	If the vector x is not the zero vector and a strategy for player 1 is generated, then this strategy can be used to generate a strategy that only differs from the given one if it has to.
basePlayer2Strategy	If the vector x is not the zero vector and a strategy for player 1 is generated, then this strategy can be used to generate a strategy that only differs from the given one if it has to.

Returns: The solution vector.

Definition at line 40 of file SymbolicGameSolver.cpp.

Member Data Documentation

◆ A

template<storm::dd::DdType Type, typename ValueType = double>

storm::dd::Add<Type, ValueType> storm::solver::SymbolicGameSolver< Type, ValueType >::A

protected

Definition at line 77 of file SymbolicGameSolver.h.

◆ allRows

template<storm::dd::DdType Type, typename ValueType = double>

storm::dd::Bdd<Type> storm::solver::SymbolicGameSolver< Type, ValueType >::allRows

protected

Definition at line 80 of file SymbolicGameSolver.h.

◆ columnMetaVariables

template<storm::dd::DdType Type, typename ValueType = double>

std::set<storm::expressions::Variable> storm::solver::SymbolicGameSolver< Type, ValueType >::columnMetaVariables

protected

Definition at line 92 of file SymbolicGameSolver.h.

◆ generatePlayer1Strategy

template<storm::dd::DdType Type, typename ValueType = double>

bool storm::solver::SymbolicGameSolver< Type, ValueType >::generatePlayer1Strategy

protected

Definition at line 104 of file SymbolicGameSolver.h.

◆ generatePlayer2Strategy

template<storm::dd::DdType Type, typename ValueType = double>

bool storm::solver::SymbolicGameSolver< Type, ValueType >::generatePlayer2Strategy

protected

Definition at line 110 of file SymbolicGameSolver.h.

◆ illegalPlayer1Mask

template<storm::dd::DdType Type, typename ValueType = double>

storm::dd::Add<Type, ValueType> storm::solver::SymbolicGameSolver< Type, ValueType >::illegalPlayer1Mask

protected

Definition at line 83 of file SymbolicGameSolver.h.

◆ illegalPlayer2Mask

template<storm::dd::DdType Type, typename ValueType = double>

storm::dd::Add<Type, ValueType> storm::solver::SymbolicGameSolver< Type, ValueType >::illegalPlayer2Mask

protected

Definition at line 86 of file SymbolicGameSolver.h.

◆ player1Strategy

template<storm::dd::DdType Type, typename ValueType = double>

boost::optional<storm::dd::Bdd<Type> > storm::solver::SymbolicGameSolver< Type, ValueType >::player1Strategy

protected

Definition at line 107 of file SymbolicGameSolver.h.

◆ player1Variables

template<storm::dd::DdType Type, typename ValueType = double>

std::set<storm::expressions::Variable> storm::solver::SymbolicGameSolver< Type, ValueType >::player1Variables

protected

Definition at line 98 of file SymbolicGameSolver.h.

◆ player2Strategy

template<storm::dd::DdType Type, typename ValueType = double>

boost::optional<storm::dd::Bdd<Type> > storm::solver::SymbolicGameSolver< Type, ValueType >::player2Strategy

protected

Definition at line 113 of file SymbolicGameSolver.h.

◆ player2Variables

template<storm::dd::DdType Type, typename ValueType = double>

std::set<storm::expressions::Variable> storm::solver::SymbolicGameSolver< Type, ValueType >::player2Variables

protected

Definition at line 101 of file SymbolicGameSolver.h.

◆ rowColumnMetaVariablePairs

template<storm::dd::DdType Type, typename ValueType = double>

std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable> > storm::solver::SymbolicGameSolver< Type, ValueType >::rowColumnMetaVariablePairs

protected

Definition at line 95 of file SymbolicGameSolver.h.

◆ rowMetaVariables

template<storm::dd::DdType Type, typename ValueType = double>

std::set<storm::expressions::Variable> storm::solver::SymbolicGameSolver< Type, ValueType >::rowMetaVariables

protected

Definition at line 89 of file SymbolicGameSolver.h.

The documentation for this class was generated from the following files:

src/storm/solver/SymbolicGameSolver.h
src/storm/solver/SymbolicGameSolver.cpp

Public Member Functions

Protected Attributes

Detailed Description

Constructor & Destructor Documentation

◆ SymbolicGameSolver()

◆ ~SymbolicGameSolver()

Member Function Documentation

◆ getPlayer1Strategy()

◆ getPlayer2Strategy()

◆ setGeneratePlayer1Strategy()

◆ setGeneratePlayer2Strategy()

◆ setGeneratePlayersStrategies()

◆ solveGame()

Member Data Documentation

◆ A

◆ allRows

◆ columnMetaVariables

◆ generatePlayer1Strategy

◆ generatePlayer2Strategy

◆ illegalPlayer1Mask

◆ illegalPlayer2Mask

◆ player1Strategy

◆ player1Variables

◆ player2Strategy

◆ player2Variables

◆ rowColumnMetaVariablePairs

◆ rowMetaVariables