1#include "storm-config.h"
12class DoubleViEnvironment {
15 static const bool isExact =
false;
24class DoublePiEnvironment {
27 static const bool isExact =
false;
39class RationalPiEnvironment {
42 static const bool isExact =
true;
50template<
typename TestType>
51class GameSolverTest :
public ::testing::Test {
53 typedef typename TestType::ValueType
ValueType;
54 GameSolverTest() : _environment(TestType::createEnvironment()) {}
62 return storm::utility::convertNumber<ValueType>(input);
69typedef ::testing::Types<DoubleViEnvironment, DoublePiEnvironment, RationalPiEnvironment>
TestingTypes;
74 typedef typename TestFixture::ValueType
ValueType;
77 player2MatrixBuilder.newRowGroup(0);
78 player2MatrixBuilder.addNextValue(0, 0, this->
parseNumber(
"0.4"));
79 player2MatrixBuilder.addNextValue(0, 1, this->
parseNumber(
"0.6"));
80 player2MatrixBuilder.addNextValue(1, 1, this->
parseNumber(
"0.2"));
81 player2MatrixBuilder.addNextValue(1, 2, this->
parseNumber(
"0.8"));
82 player2MatrixBuilder.newRowGroup(2);
83 player2MatrixBuilder.addNextValue(2, 2, this->
parseNumber(
"0.5"));
84 player2MatrixBuilder.addNextValue(2, 3, this->
parseNumber(
"0.5"));
85 player2MatrixBuilder.newRowGroup(4);
86 player2MatrixBuilder.newRowGroup(5);
87 player2MatrixBuilder.newRowGroup(6);
92 player1MatrixBuilder.newRowGroup(0);
93 player1MatrixBuilder.addNextValue(0, 0, 1);
94 player1MatrixBuilder.addNextValue(1, 1, 1);
95 player1MatrixBuilder.newRowGroup(2);
96 player1MatrixBuilder.addNextValue(2, 2, 1);
97 player1MatrixBuilder.newRowGroup(3);
98 player1MatrixBuilder.addNextValue(3, 3, 1);
99 player1MatrixBuilder.newRowGroup(4);
100 player1MatrixBuilder.addNextValue(4, 4, 1);
104 auto solver = factory.
create(this->env(), player1Matrix, player2Matrix);
107 std::vector<ValueType> result(4);
108 std::vector<ValueType> b(7);
113 solver->solveGame(this->env(), storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, result, b);
114 EXPECT_NEAR(this->
parseNumber(
"0"), result[0], this->precision());
116 result = std::vector<ValueType>(4);
119 solver->solveGame(this->env(), storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize, result, b);
120 EXPECT_NEAR(this->
parseNumber(
"0.5"), result[0], this->precision());
122 result = std::vector<ValueType>(4);
124 solver->solveGame(this->env(), storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize, result, b);
125 EXPECT_NEAR(this->
parseNumber(
"0.2"), result[0], this->precision());
127 result = std::vector<ValueType>(4);
129 solver->solveGame(this->env(), storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, result, b);
130 EXPECT_NEAR(this->
parseNumber(
"1"), result[0], this->precision());
SolverEnvironment & solver()
storm::RationalNumber const & getPrecision() const
void setMethod(storm::solver::GameMethod value)
void setPrecision(storm::RationalNumber value)
void setMethod(storm::solver::NativeLinearEquationSolverMethod value)
void setLinearEquationSolverType(storm::solver::EquationSolverType const &value, bool isSetFromDefault=false)
void setLinearEquationSolverPrecision(boost::optional< storm::RationalNumber > const &newPrecision, boost::optional< bool > const &relativePrecision=boost::none)
GameSolverEnvironment & game()
NativeSolverEnvironment & native()
virtual std::unique_ptr< GameSolver< ValueType > > create(Environment const &env, storm::storage::SparseMatrix< storm::storage::sparse::state_type > const &player1Matrix, storm::storage::SparseMatrix< ValueType > const &player2Matrix) const
A class that can be used to build a sparse matrix by adding value by value.
A class that holds a possibly non-square matrix in the compressed row storage format.
SFTBDDChecker::ValueType ValueType
NumberType parseNumber(std::string const &value)
Parse number from string.
TYPED_TEST(GraphTestAR, SymbolicProb01StochasticGameDieSmall)
TYPED_TEST_SUITE(GraphTestAR, TestingTypes,)
::testing::Types< Cudd, Sylvan > TestingTypes