Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
MultiplierTest.cpp
Go to the documentation of this file.
1#include "storm-config.h"
2#include "test/storm_gtest.h"
3
7
9namespace {
10
11class NativeEnvironment {
12 public:
13 typedef double ValueType;
14 static const bool isExact = false;
15 static storm::Environment createEnvironment() {
17 env.solver().multiplier().setType(storm::solver::MultiplierType::Native);
18 return env;
19 }
20};
21
22class GmmxxEnvironment {
23 public:
24 typedef double ValueType;
25 static const bool isExact = false;
26 static storm::Environment createEnvironment() {
28 env.solver().multiplier().setType(storm::solver::MultiplierType::Gmmxx);
29 return env;
30 }
31};
32
33template<typename TestType>
34class MultiplierTest : public ::testing::Test {
35 public:
36 typedef typename TestType::ValueType ValueType;
37 MultiplierTest() : _environment(TestType::createEnvironment()) {}
38 storm::Environment const& env() const {
39 return _environment;
40 }
41 ValueType precision() const {
42 return TestType::isExact ? parseNumber("0") : parseNumber("1e-15");
43 }
44 ValueType parseNumber(std::string const& input) const {
45 return storm::utility::convertNumber<ValueType>(input);
46 }
47
48 private:
49 storm::Environment _environment;
50};
51
52typedef ::testing::Types<NativeEnvironment, GmmxxEnvironment> TestingTypes;
53
54TYPED_TEST_SUITE(MultiplierTest, TestingTypes, );
55
56TYPED_TEST(MultiplierTest, repeatedMultiplyTest) {
57 typedef typename TestFixture::ValueType ValueType;
60 ASSERT_NO_THROW(builder.addNextValue(0, 1, this->parseNumber("0.5")));
61 ASSERT_NO_THROW(builder.addNextValue(0, 4, this->parseNumber("0.5")));
62 ASSERT_NO_THROW(builder.addNextValue(1, 2, this->parseNumber("0.5")));
63 ASSERT_NO_THROW(builder.addNextValue(1, 4, this->parseNumber("0.5")));
64 ASSERT_NO_THROW(builder.addNextValue(2, 3, this->parseNumber("0.5")));
65 ASSERT_NO_THROW(builder.addNextValue(2, 4, this->parseNumber("0.5")));
66 ASSERT_NO_THROW(builder.addNextValue(3, 4, this->parseNumber("1")));
67 ASSERT_NO_THROW(builder.addNextValue(4, 4, this->parseNumber("1")));
68
70 ASSERT_NO_THROW(A = builder.build());
71
72 std::vector<ValueType> x(5);
73 x[4] = this->parseNumber("1");
74
76 auto multiplier = factory.create(this->env(), A);
77 ASSERT_NO_THROW(multiplier->repeatedMultiply(this->env(), x, nullptr, 4));
78 EXPECT_NEAR(x[0], this->parseNumber("1"), this->precision());
79}
80
81TYPED_TEST(MultiplierTest, repeatedMultiplyAndReduceTest) {
82 typedef typename TestFixture::ValueType ValueType;
83
84 storm::storage::SparseMatrixBuilder<ValueType> builder(0, 0, 0, false, true);
85 ASSERT_NO_THROW(builder.newRowGroup(0));
86 ASSERT_NO_THROW(builder.addNextValue(0, 0, this->parseNumber("0.9")));
87 ASSERT_NO_THROW(builder.addNextValue(0, 1, this->parseNumber("0.099")));
88 ASSERT_NO_THROW(builder.addNextValue(0, 2, this->parseNumber("0.001")));
89 ASSERT_NO_THROW(builder.addNextValue(1, 1, this->parseNumber("0.5")));
90 ASSERT_NO_THROW(builder.addNextValue(1, 2, this->parseNumber("0.5")));
91 ASSERT_NO_THROW(builder.newRowGroup(2));
92 ASSERT_NO_THROW(builder.addNextValue(2, 1, this->parseNumber("1")));
93 ASSERT_NO_THROW(builder.newRowGroup(3));
94 ASSERT_NO_THROW(builder.addNextValue(3, 2, this->parseNumber("1")));
95
97 ASSERT_NO_THROW(A = builder.build());
98
99 std::vector<ValueType> initialX = {this->parseNumber("0"), this->parseNumber("1"), this->parseNumber("0")};
100 std::vector<ValueType> x;
101
103 auto multiplier = factory.create(this->env(), A);
104
105 x = initialX;
106 ASSERT_NO_THROW(multiplier->repeatedMultiplyAndReduce(this->env(), storm::OptimizationDirection::Minimize, x, nullptr, 1));
107 EXPECT_NEAR(x[0], this->parseNumber("0.099"), this->precision());
108
109 x = initialX;
110 ASSERT_NO_THROW(multiplier->repeatedMultiplyAndReduce(this->env(), storm::OptimizationDirection::Minimize, x, nullptr, 2));
111 EXPECT_NEAR(x[0], this->parseNumber("0.1881"), this->precision());
112
113 x = initialX;
114 ASSERT_NO_THROW(multiplier->repeatedMultiplyAndReduce(this->env(), storm::OptimizationDirection::Minimize, x, nullptr, 20));
115 EXPECT_NEAR(x[0], this->parseNumber("0.5"), this->precision());
116
117 x = initialX;
118 ASSERT_NO_THROW(multiplier->repeatedMultiplyAndReduce(this->env(), storm::OptimizationDirection::Maximize, x, nullptr, 1));
119 EXPECT_NEAR(x[0], this->parseNumber("0.5"), this->precision());
120
121 x = initialX;
122 ASSERT_NO_THROW(multiplier->repeatedMultiplyAndReduce(this->env(), storm::OptimizationDirection::Maximize, x, nullptr, 20));
123 EXPECT_NEAR(x[0], this->parseNumber("0.923808265834023387639"), this->precision());
124}
125
126} // namespace
SolverEnvironment & solver()
void setType(storm::solver::MultiplierType value, bool isSetFromDefault=false)
MultiplierEnvironment & multiplier()
A class that can be used to build a sparse matrix by adding value by value.
void addNextValue(index_type row, index_type column, value_type const &value)
Sets the matrix entry at the given row and column to the given value.
void newRowGroup(index_type startingRow)
Starts a new row group in the matrix.
SparseMatrix< value_type > build(index_type overriddenRowCount=0, index_type overriddenColumnCount=0, index_type overriddenRowGroupCount=0)
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:49
TYPED_TEST_SUITE(GraphTestAR, TestingTypes,)
::testing::Types< Cudd, Sylvan > TestingTypes
Definition GraphTest.cpp:46