Storm 1.11.1.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
GameSolverTest.cpp
Go to the documentation of this file.
1#include "storm-config.h"
2#include "test/storm_gtest.h"
3
9
10namespace {
11
12class DoubleViEnvironment {
13 public:
14 typedef double ValueType;
15 static const bool isExact = false;
16 static storm::Environment createEnvironment() {
18 env.solver().game().setMethod(storm::solver::GameMethod::ValueIteration);
19 env.solver().game().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
20 return env;
21 }
22};
23
24class DoublePiEnvironment {
25 public:
26 typedef double ValueType;
27 static const bool isExact = false;
28 static storm::Environment createEnvironment() {
30 env.solver().game().setMethod(storm::solver::GameMethod::PolicyIteration);
31 env.solver().game().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
32 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
33 env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::Jacobi);
35 return env;
36 }
37};
38
39class RationalPiEnvironment {
40 public:
41 typedef storm::RationalNumber ValueType;
42 static const bool isExact = true;
43 static storm::Environment createEnvironment() {
45 env.solver().game().setMethod(storm::solver::GameMethod::PolicyIteration);
46 return env;
47 }
48};
49
50template<typename TestType>
51class GameSolverTest : public ::testing::Test {
52 public:
53 typedef typename TestType::ValueType ValueType;
54 GameSolverTest() : _environment(TestType::createEnvironment()) {}
55 storm::Environment const& env() const {
56 return _environment;
57 }
58 ValueType precision() const {
59 return TestType::isExact ? parseNumber("0") : parseNumber("1e-6");
60 }
61 ValueType parseNumber(std::string const& input) const {
62 return storm::utility::convertNumber<ValueType>(input);
63 }
64
65 private:
66 storm::Environment _environment;
67};
68
69typedef ::testing::Types<DoubleViEnvironment, DoublePiEnvironment, RationalPiEnvironment> TestingTypes;
70
71TYPED_TEST_SUITE(GameSolverTest, TestingTypes, );
72
73TYPED_TEST(GameSolverTest, SolveEquations) {
74 typedef typename TestFixture::ValueType ValueType;
75 // Construct simple game. Start with player 2 matrix.
76 storm::storage::SparseMatrixBuilder<ValueType> player2MatrixBuilder(0, 0, 0, false, true);
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);
88 storm::storage::SparseMatrix<ValueType> player2Matrix = player2MatrixBuilder.build();
89
90 // Now build player 1 matrix.
91 storm::storage::SparseMatrixBuilder<storm::storage::sparse::state_type> player1MatrixBuilder(0, 0, 0, false, true);
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);
101 storm::storage::SparseMatrix<storm::storage::sparse::state_type> player1Matrix = player1MatrixBuilder.build();
102
104 auto solver = factory.create(this->env(), player1Matrix, player2Matrix);
105
106 // Create solution and target state vector.
107 std::vector<ValueType> result(4);
108 std::vector<ValueType> b(7);
109 b[4] = this->parseNumber("1");
110 b[6] = this->parseNumber("1");
111
112 // Now solve the game with different strategies for the players.
113 solver->solveGame(this->env(), storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, result, b);
114 EXPECT_NEAR(this->parseNumber("0"), result[0], this->precision());
115
116 result = std::vector<ValueType>(4);
117 solver->setBounds(this->parseNumber("0"), this->parseNumber("1"));
118
119 solver->solveGame(this->env(), storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize, result, b);
120 EXPECT_NEAR(this->parseNumber("0.5"), result[0], this->precision());
121
122 result = std::vector<ValueType>(4);
123
124 solver->solveGame(this->env(), storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize, result, b);
125 EXPECT_NEAR(this->parseNumber("0.2"), result[0], this->precision());
126
127 result = std::vector<ValueType>(4);
128
129 solver->solveGame(this->env(), storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, result, b);
130 EXPECT_NEAR(this->parseNumber("1"), result[0], this->precision());
131}
132
133} // namespace
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)
Definition GraphTest.cpp:62
TYPED_TEST_SUITE(GraphTestAR, TestingTypes,)
::testing::Types< Cudd, Sylvan > TestingTypes
Definition GraphTest.cpp:59